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