diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-03-05 14:05:26 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-05 14:05:26 -0800 |
commit | d51c8347a3c6bf7857c474bd3493377f9fed58e5 (patch) | |
tree | 56da229cd8fcbe6988937514820c13c3894f2558 /examples/api | |
parent | d1aa4ae101987093a06208650e2ea4878f7437ca (diff) |
Add support for check-sat-assuming. (#1637)
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/bitvectors.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 90b69b10a..a245d4890 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -2,9 +2,9 @@ /*! \file bitvectors.cpp ** \verbatim ** Top contributors (to current version): - ** Liana Hadarean, Morgan Deters, Paul Meng + ** Liana Hadarean, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2018 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 @@ -107,5 +107,10 @@ int main() { cout << " Expect valid. " << endl; cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; + Expr x_neq_x = em.mkExpr(kind::EQUAL, x, x).notExpr(); + std::vector<Expr> v{new_x_eq_new_x_, x_neq_x}; + cout << " Querying: " << v << endl; + cout << " Expect invalid. " << endl; + cout << " CVC4: " << smt.query(v) << endl; return 0; } |