From 98d113e88556f05d4486b784e3bc96b37cd35d56 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 30 Nov 2012 22:33:28 +0000 Subject: [PATCH] Updating the combination.cpp example. --- examples/api/combination.cpp | 57 +++++++++++++++++++++++------------- src/expr/options | 2 +- 2 files changed, 38 insertions(+), 21 deletions(-) diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index f91e78ce6..e0e5a6e13 100644 --- 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 24810962e..cd59e4875 100644 --- 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 -- 2.30.2