1. Arlen Cox
  2. z3

Commits

Leonardo de Moura  committed a5ceff9

cleaned exampled

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

  • Participants
  • Parent commits 1cf8d61
  • Branches master

Comments (0)

Files changed (1)

File examples/c++/example.cpp

View file
     std::cout << "unsat core example 2\n";
     context c;
     // 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");
     solver s(c);
         std::cout << core[i] << "\n";
     }
     // 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
-    // into individual clauses. First, we flat the conjunctions by
+    // into individual subformulas. 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.