diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-29 15:35:44 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-29 17:35:44 -0500 |
commit | 19054b3b1d427e662d30d4322df2b2f2361353da (patch) | |
tree | 1ee878fd6c2c36b78ea33607a5668e6a6d8f7144 /examples/simple_vc_quant_cxx.cpp | |
parent | 5cd6f0e5e910ad61ebc5045170842078818a3b80 (diff) |
Make ExprManager constructor private (#4669)
This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.
Diffstat (limited to 'examples/simple_vc_quant_cxx.cpp')
-rw-r--r-- | examples/simple_vc_quant_cxx.cpp | 79 |
1 files changed, 39 insertions, 40 deletions
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 83d011993..4d5767ebb 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -14,64 +14,63 @@ ** A simple demonstration of the C++ interface for quantifiers. **/ -#include <iostream> +#include <cvc4/api/cvc4cpp.h> -#include <cvc4/cvc4.h> +#include <iostream> -using namespace std; -using namespace CVC4; +using namespace CVC4::api; int main() { - ExprManager em; - SmtEngine smt(&em); + Solver slv; // Prove that the following is unsatisfiable: // forall x. P( x ) ^ ~P( 5 ) - Type integer = em.integerType(); - Type boolean = em.booleanType(); - Type integerPredicate = em.mkFunctionType(integer, boolean); - - Expr p = em.mkVar("P", integerPredicate); - Expr x = em.mkBoundVar("x", integer); - + Sort integer = slv.getIntegerSort(); + Sort boolean = slv.getBooleanSort(); + Sort integerPredicate = slv.mkFunctionSort(integer, boolean); + + Term p = slv.mkConst(integerPredicate, "P"); + Term x = slv.mkVar(integer, "x"); + // make forall x. P( x ) - Expr var_list = em.mkExpr(kind::BOUND_VAR_LIST, x); - Expr px = em.mkExpr(kind::APPLY_UF, p, x); - Expr quantpospx = em.mkExpr(kind::FORALL, var_list, px); - cout << "Made expression : " << quantpospx << endl; - + Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x); + Term px = slv.mkTerm(Kind::APPLY_UF, p, x); + Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px); + std::cout << "Made expression : " << quantpospx << std::endl; + //make ~P( 5 ) - Expr five = em.mkConst(Rational(5)); - Expr pfive = em.mkExpr(kind::APPLY_UF, p, five); - Expr negpfive = em.mkExpr(kind::NOT, pfive); - cout << "Made expression : " << negpfive << endl; - - Expr formula = em.mkExpr(kind::AND, quantpospx, negpfive); + Term five = slv.mkReal(5); + Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five); + Term negpfive = slv.mkTerm(Kind::NOT, pfive); + std::cout << "Made expression : " << negpfive << std::endl; - smt.assertFormula(formula); + Term formula = slv.mkTerm(Kind::AND, quantpospx, negpfive); - cout << "Checking SAT after asserting " << formula << " to CVC4." << endl; - cout << "CVC4 should report unsat." << endl; - cout << "Result from CVC4 is: " << smt.checkSat() << endl; + slv.assertFormula(formula); + std::cout << "Checking SAT after asserting " << formula << " to CVC4." + << std::endl; + std::cout << "CVC4 should report unsat." << std::endl; + std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl; - SmtEngine smtp(&em); - - // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x)))) - Expr pattern = em.mkExpr(kind::INST_PATTERN, px); - Expr pattern_list = em.mkExpr(kind::INST_PATTERN_LIST, pattern); - Expr quantpospx_pattern = em.mkExpr(kind::FORALL, var_list, px, pattern_list); - cout << "Made expression : " << quantpospx_pattern << endl; + slv.resetAssertions(); - Expr formula_pattern = em.mkExpr(kind::AND, quantpospx_pattern, negpfive); + // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x)))) + Term pattern = slv.mkTerm(Kind::INST_PATTERN, px); + Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, pattern); + Term quantpospx_pattern = + slv.mkTerm(Kind::FORALL, var_list, px, pattern_list); + std::cout << "Made expression : " << quantpospx_pattern << std::endl; - smtp.assertFormula(formula_pattern); + Term formula_pattern = slv.mkTerm(Kind::AND, quantpospx_pattern, negpfive); - cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." << endl; - cout << "CVC4 should report unsat." << endl; - cout << "Result from CVC4 is: " << smtp.checkSat() << endl; + slv.assertFormula(formula_pattern); + std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." + << std::endl; + std::cout << "CVC4 should report unsat." << std::endl; + std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl; return 0; } |