mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
66 lines
2.1 KiB
C
66 lines
2.1 KiB
C
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Aina Niemetz
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
|
|
* in the top-level source directory and their institutional affiliations.
|
|
* All rights reserved. See the file COPYING in the top-level source
|
|
* directory for licensing information.
|
|
* ****************************************************************************
|
|
*
|
|
* A simple demonstration of using the parser via the C API.
|
|
*/
|
|
|
|
#include <assert.h>
|
|
#include <cvc5/c/cvc5.h>
|
|
#include <cvc5/c/cvc5_parser.h>
|
|
#include <stdio.h>
|
|
|
|
int main()
|
|
{
|
|
Cvc5TermManager* tm = cvc5_term_manager_new();
|
|
Cvc5* slv = cvc5_new(tm);
|
|
|
|
// set that we should print success after each successful command
|
|
cvc5_set_option(slv, "print-success", "true");
|
|
|
|
// construct an input parser associated the solver above
|
|
Cvc5InputParser* parser = cvc5_parser_new(slv, NULL);
|
|
cvc5_parser_set_str_input(
|
|
parser,
|
|
CVC5_INPUT_LANGUAGE_SMT_LIB_2_6,
|
|
"(set-logic QF_LIA)\n(declare-fun a () Int)\n(declare-fun b () "
|
|
"Int)\n(declare-fun c () Int)\n(assert (> a (+ b c)))\n(assert (< a "
|
|
"b))\n(assert (> c 0))\n",
|
|
"foo");
|
|
|
|
// get the symbol manager of the parser, used when invoking commands below
|
|
Cvc5SymbolManager* sm = cvc5_parser_get_sm(parser);
|
|
|
|
// parse commands until finished
|
|
Cvc5Command cmd;
|
|
do
|
|
{
|
|
const char* error_msg;
|
|
cmd = cvc5_parser_next_command(parser, &error_msg);
|
|
assert(error_msg == NULL);
|
|
if (cmd)
|
|
{
|
|
printf("Executing command %s:\n", cvc5_cmd_to_string(cmd));
|
|
// invoke the command on the solver and the symbol manager, print the
|
|
// result to stdout
|
|
printf("%s", cvc5_cmd_invoke(cmd, slv, sm));
|
|
}
|
|
} while (cmd);
|
|
printf("Finished parsing commands\n");
|
|
|
|
// now, check sat with the solver
|
|
Cvc5Result r = cvc5_check_sat(slv);
|
|
printf("expected: unsat\n");
|
|
printf("result: %s\n", cvc5_result_to_string(r));
|
|
cvc5_delete(slv);
|
|
cvc5_term_manager_delete(tm);
|
|
}
|