mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

cleaned exampled

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-08 07:11:22 -08:00
parent 1cf8d61def
commit a5ceff98ea
1 changed files with 4 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
examples/c++/example.cpp
View file

@ -378,11 +378,9 @@ void unsat_core_example2() {
std::cout << "unsat core example 2\n"; std::cout << "unsat core example 2\n";
context c; context c;
// The answer literal mechanism, described in the previous example, // The answer literal mechanism, described in the previous example,
// tracks assertions instead of clauses. An assertion can be a complicated // tracks assertions. An assertion can be a complicated
// formula containing many clauses. // formula containing containing the conjunction of many subformulas.
expr p1 = c.bool_const("p1"); expr p1 = c.bool_const("p1");
expr p2 = c.bool_const("p2");
expr p3 = c.bool_const("p3");
expr x = c.int_const("x"); expr x = c.int_const("x");
expr y = c.int_const("y"); expr y = c.int_const("y");
solver s(c); solver s(c);
@ -397,9 +395,9 @@ void unsat_core_example2() {
std::cout << core[i] << "\n"; std::cout << core[i] << "\n";
} }
// The core is not very informative, since p1 is tracking the formula F // The core is not very informative, since p1 is tracking the formula F
// that is a conjunction of clauses. // that is a conjunction of subformulas.
// Now, we use the following piece of code to break this conjunction // Now, we use the following piece of code to break this conjunction
// into individual clauses. First, we flat the conjunctions by // into individual subformulas. First, we flat the conjunctions by
// using the method simplify. // using the method simplify.
std::vector<expr> qs; // auxiliary vector used to store new answer literals. std::vector<expr> qs; // auxiliary vector used to store new answer literals.
assert(F.is_app()); // I'm assuming F is an application. assert(F.is_app()); // I'm assuming F is an application.