diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-27 06:50:47 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-09-27 06:50:47 -0500 |
commit | 4a4c0806ef75254f0344978bdfba0f077a1e663a (patch) | |
tree | fa4d8ae7ab380568e5ac852ce9aa9cac1667eb47 /examples | |
parent | 2567868bdf5664e95f998e76512c84d2c63f09a2 (diff) |
Add quantifiers API example, fixes #879 (#1146)
Diffstat (limited to 'examples')
-rw-r--r-- | examples/simple_vc_quant_cxx.cpp | 78 |
1 files changed, 78 insertions, 0 deletions
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp new file mode 100644 index 000000000..299918eea --- /dev/null +++ b/examples/simple_vc_quant_cxx.cpp @@ -0,0 +1,78 @@ +/********************* */ +/*! \file simple_vc_quant_cxx.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 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.\endverbatim + ** + ** \brief A simple demonstration of the C++ interface for quantifiers + ** + ** A simple demonstration of the C++ interface for quantifiers. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + + // 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); + + // 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; + + //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); + + smt.assertFormula(formula); + + cout << "Checking SAT after asserting " << formula << " to CVC4." << endl; + cout << "CVC4 should report unsat." << endl; + cout << "Result from CVC4 is: " << smt.checkSat() << 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; + + Expr formula_pattern = em.mkExpr(kind::AND, quantpospx_pattern, negpfive); + + smtp.assertFormula(formula_pattern); + + cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." << endl; + cout << "CVC4 should report unsat." << endl; + cout << "Result from CVC4 is: " << smtp.checkSat() << endl; + + + return 0; +} |