From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 21 Mar 2018 22:09:46 +0000 (-0700)
Subject: Add bit-vector extract example. (#1681)
X-Git-Tag: cvc5-1.0.0~5223
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=966960b424aa5901a03abbfaa1bcdac6e3ed90dc;p=cvc5.git

Add bit-vector extract example. (#1681)
---

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;
 }