diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-12-01 01:43:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-12-01 01:43:08 +0000 |
commit | 8953b603bd6960eb59ccb41a63d4742096da1c4a (patch) | |
tree | 197300f8a004a5ae01cdefb152690c30248d83c7 /examples/api/bitvectors.cpp | |
parent | e39b94aa9425123420635c298fa6bb8a2ee4f048 (diff) |
updated examples
Diffstat (limited to 'examples/api/bitvectors.cpp')
-rw-r--r-- | examples/api/bitvectors.cpp | 60 |
1 files changed, 30 insertions, 30 deletions
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 4701bf8e3..a0c43142d 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -10,7 +10,7 @@ ** information.\endverbatim ** ** \brief A simple demonstration of the solving capabilities of the CVC4 - ** bit-vector solver. + ** bit-vector solver. ** **/ @@ -27,7 +27,7 @@ int main() { SmtEngine smt(&em); smt.setOption("incremental", true); // Enable incremental solving smt.setLogic("QF_BV"); // Set the logic - + // The following example has been adapted from the book A Hacker's Delight by // Henry S. Warren. // @@ -39,14 +39,14 @@ int main() { // else x = a; // // Two more efficient yet equivalent methods are: - // - //(1) x = a ⊕ b ⊕ x; + // + //(1) x = a ⊕ b ⊕ x; // //(2) x = a + b - x; // // We will use CVC4 to prove that the three pieces of code above are all - // equivalent by encoding the problem in the bit-vector theory. - + // equivalent by encoding the problem in the bit-vector theory. + // Creating a bit-vector type of width 32 Type bitvector32 = em.mkBitVectorType(32); @@ -56,57 +56,57 @@ int main() { Expr b = em.mkVar("b", bitvector32); // First encode the assumption that x must be equal to a or b - Expr x_eq_a = em.mkExpr(kind::EQUAL, x, a); + Expr x_eq_a = em.mkExpr(kind::EQUAL, x, a); Expr x_eq_b = em.mkExpr(kind::EQUAL, x, b); - Expr assumption = em.mkExpr(kind::OR, x_eq_a, x_eq_b); + Expr assumption = em.mkExpr(kind::OR, x_eq_a, x_eq_b); // Assert the assumption - smt.assertFormula(assumption); - - // Introduce a new variable for the new value of x after assignment. - Expr new_x = em.mkVar("new_x", bitvector32); // x after executing code (0) + smt.assertFormula(assumption); + + // Introduce a new variable for the new value of x after assignment. + Expr new_x = em.mkVar("new_x", bitvector32); // x after executing code (0) Expr new_x_ = em.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) // Encoding code (0) - // new_x = x == a ? b : a; - Expr ite = em.mkExpr(kind::ITE, x_eq_a, b, a); - Expr assignment0 = em.mkExpr(kind::EQUAL, new_x, ite); + // new_x = x == a ? b : a; + Expr ite = em.mkExpr(kind::ITE, x_eq_a, b, a); + Expr assignment0 = em.mkExpr(kind::EQUAL, new_x, ite); // Assert the encoding of code (0) - cout << "Asserting " << assignment0 << " to CVC4 " << endl; + cout << "Asserting " << assignment0 << " to CVC4 " << endl; smt.assertFormula(assignment0); cout << "Pushing a new context." << endl; smt.push(); - + // Encoding code (1) // new_x_ = a xor b xor x - Expr a_xor_b_xor_x = em.mkExpr(kind::BITVECTOR_XOR, a, b, x); + Expr a_xor_b_xor_x = em.mkExpr(kind::BITVECTOR_XOR, a, b, x); Expr assignment1 = em.mkExpr(kind::EQUAL, new_x_, a_xor_b_xor_x); - // Assert encoding to CVC4 in current context; - cout << "Asserting " << assignment1 << " to CVC4 " << endl; + // Assert encoding to CVC4 in current context; + cout << "Asserting " << assignment1 << " to CVC4 " << endl; smt.assertFormula(assignment1); Expr new_x_eq_new_x_ = em.mkExpr(kind::EQUAL, new_x, new_x_); cout << " Querying: " << new_x_eq_new_x_ << endl; - cout << " Expect valid. " << endl; - cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; + cout << " Expect valid. " << endl; + cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; cout << " Popping context. " << endl; smt.pop(); // Encoding code (2) // new_x_ = a + b - x - Expr a_plus_b = em.mkExpr(kind::BITVECTOR_PLUS, a, b); - Expr a_plus_b_minus_x = em.mkExpr(kind::BITVECTOR_SUB, a_plus_b, x); + Expr a_plus_b = em.mkExpr(kind::BITVECTOR_PLUS, a, b); + Expr a_plus_b_minus_x = em.mkExpr(kind::BITVECTOR_SUB, a_plus_b, x); Expr assignment2 = em.mkExpr(kind::EQUAL, new_x_, a_plus_b_minus_x); - - // Assert encoding to CVC4 in current context; - cout << "Asserting " << assignment2 << " to CVC4 " << endl; + + // Assert encoding to CVC4 in current context; + cout << "Asserting " << assignment2 << " to CVC4 " << endl; smt.assertFormula(assignment1); cout << " Querying: " << new_x_eq_new_x_ << endl; - cout << " Expect valid. " << endl; - cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; - + cout << " Expect valid. " << endl; + cout << " CVC4: " << smt.query(new_x_eq_new_x_) << endl; + return 0; } |