Updating the combination.cpp example.

diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index f91e78ce6d2189509129df829eafd4de124c7dec..e0e5a6e13cfe03f0ba4369b0519c69c797ce93b6 100644 (file)
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -25,13 +25,30 @@
 using namespace std;
 using namespace CVC4;
 
+void preFixPrintGetValue(SmtEngine& smt, Expr e, int level = 0){
+  for(int i = 0; i < level; ++i){ cout << '-'; }
+  cout << "smt.getValue(" << e << ") -> " << smt.getValue(e) << endl;
+
+  if(e.hasOperator()){
+    preFixPrintGetValue(smt, e.getOperator(), level + 1);
+  }
+
+  for(Expr::const_iterator term_i = e.begin(), term_end = e.end();
+      term_i != term_end; ++term_i)
+  {
+    Expr curr = *term_i;
+    preFixPrintGetValue(smt, curr, level + 1);
+  }
+}
+
+
 int main() {
   ExprManager em;
   SmtEngine smt(&em);
-  smt.setOption("tlimit", 100);
   smt.setOption("produce-models", true); // Produce Models
-  smt.setOption("incremental", true); // Produce Models
+  smt.setOption("incremental", true); // Enable Multiple Queries
   smt.setOption("output-language", "smtlib"); // output-language
+  smt.setOption("default-dag-thresh", 0); //Disable dagifying the output
 
   // Sorts
   SortType u = em.mkSort("u");
@@ -44,7 +61,7 @@ int main() {
   Expr x = em.mkVar("x", u);
   Expr y = em.mkVar("y", u);
 
-  //Functions
+  // Functions
   Expr f = em.mkVar("f", uToInt);
   Expr p = em.mkVar("p", intPred);
 
@@ -52,34 +69,34 @@ int main() {
   Expr zero = em.mkConst(Rational(0));
   Expr one = em.mkConst(Rational(1));
 
-  // terms
+  // Terms
   Expr f_x = em.mkExpr(kind::APPLY_UF, f, x);
   Expr f_y = em.mkExpr(kind::APPLY_UF, f, y);
   Expr sum = em.mkExpr(kind::PLUS, f_x, f_y);
   Expr p_0 = em.mkExpr(kind::APPLY_UF, p, zero);
   Expr p_f_y = em.mkExpr(kind::APPLY_UF, p, f_y);
 
-  smt.assertFormula(em.mkExpr(kind::LEQ, zero, f_x)); // 0 <= f(x)
-  smt.assertFormula(em.mkExpr(kind::LEQ, zero, f_y)); // 0 <= f(y)
-  smt.assertFormula(em.mkExpr(kind::LEQ, sum, one));  // f(x) + f(y) <= 1
-  smt.assertFormula(p_0.notExpr());                   // not p(0)
-  smt.assertFormula(p_f_y);                           // p(f(y))
 
-  cout << "Under the assumptions, prove x cannot equal y is valid: "
-       << " CVC4 says " << smt.query(em.mkExpr(kind::DISTINCT, x, y)) << endl;
+  Expr assumptions =
+    em.mkExpr(kind::AND,
+              em.mkExpr(kind::LEQ, zero, f_x), // 0 <= f(x)
+              em.mkExpr(kind::LEQ, zero, f_y), // 0 <= f(y)
+              em.mkExpr(kind::LEQ, sum, one),  // f(x) + f(y) <= 1
+              p_0.notExpr(),                   // not p(0)
+              p_f_y);                          // p(f(y))
+  smt.assertFormula(assumptions);
+
+  cout << "Given the following assumptions:" << endl
+       << assumptions << endl
+       << "Prove x /= y is valid. "
+       << "CVC4 says: " << smt.query(em.mkExpr(kind::DISTINCT, x, y)) << "." << endl;
 
   cout << "Now we call checksat on a trivial query to show that" << endl
        << "the assumptions are satisfiable: "
        << smt.checkSat(em.mkConst(true)) << "."<< endl;
-  cout << smt.getValue(x) << endl;
-  cout << smt.getValue(y) << endl;
-  cout << smt.getValue(f_x) << endl;
-  cout << smt.getValue(f_y) << endl;
-  cout << smt.getValue(p_f_y) << endl;
-  cout << smt.getValue(p_0) << endl;
-
-  cout << smt.getValue(f) << endl;
-  cout << smt.getValue(p) << endl;
+
+  cout << "Finally, after a SAT call, we use smt.getValue(...) to generate a model." << endl;
+  preFixPrintGetValue(smt, assumptions);
 
   return 0;
 }

diff --git a/src/expr/options b/src/expr/options
index 24810962ea9196aaa1d2ca61b4672a20ba04bd0f..cd59e487578c8f4eb2b57699453875eaf9778aaa 100644 (file)
--- a/src/expr/options
+++ b/src/expr/options
@@ -7,7 +7,7 @@ module EXPR "expr/options.h" Expression package
 
 option defaultExprDepth --default-expr-depth=N int :predicate CVC4::expr::setDefaultExprDepth :predicate-include "expr/options_handlers.h"
  print exprs to depth N (0 == default, -1 == no limit)
-option - --default-dag-thresh=N argument :handler CVC4::expr::setDefaultDagThresh :handler-include "expr/options_handlers.h"
+option - default-dag-thresh --default-dag-thresh=N argument :handler CVC4::expr::setDefaultDagThresh :handler-include "expr/options_handlers.h"
  dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)
 option - --print-expr-types void :handler CVC4::expr::setPrintExprTypes :handler-include "expr/options_handlers.h"
  print types with variables when printing exprs