From 966960b424aa5901a03abbfaa1bcdac6e3ed90dc Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 21 Mar 2018 15:09:46 -0700 Subject: [PATCH] Add bit-vector extract example. (#1681) --- examples/api/bitvectors.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index a245d4890..ec03faef3 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -112,5 +112,16 @@ int main() { cout << " Querying: " << v << endl; cout << " Expect invalid. " << endl; cout << " CVC4: " << smt.query(v) << endl; + + // Assert that a is odd + Expr extract_op = em.mkConst(BitVectorExtract(0, 0)); + Expr lsb_of_a = em.mkExpr(extract_op, a); + cout << "Type of " << lsb_of_a << " is " << lsb_of_a.getType() << endl; + Expr a_odd = em.mkExpr(kind::EQUAL, lsb_of_a, em.mkConst(BitVector(1u, 1u))); + cout << "Assert " << a_odd << endl; + cout << "Check satisfiability." << endl; + smt.assertFormula(a_odd); + cout << " Expect sat. " << endl; + cout << " CVC4: " << smt.checkSat() << endl; return 0; } -- 2.30.2