diff options
31 files changed, 513 insertions, 59 deletions
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 004f0c9a9..70f1047f5 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -71,7 +71,7 @@ void NodeValue::toStream(std::ostream& out, int toDepth, bool types, VarNameAttr(), s)) { out << s; } else { - out << "var_" << d_id << "[" << this << "]"; + out << "var_" << d_id; } if(types) { // print the whole type, but not *its* type diff --git a/src/expr/type.h b/src/expr/type.h index 435d640d0..453eaf5c4 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -216,7 +216,7 @@ public: /** * Is this a predicate type, i.e. if it's a function type mapping to Boolean. - * Aall predicate types are also function types. + * All predicate types are also function types. * @return true if the type is a predicate type */ bool isPredicate() const; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 2c460c831..4c447f9c1 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -257,6 +257,35 @@ command returns [CVC4::Command* cmd] | /* get-assertions */ GET_ASSERTIONS_TOK { cmd = new GetAssertionsCommand; } + | /* push */ + PUSH_TOK k=INTEGER_LITERAL + { unsigned n = AntlrInput::tokenToUnsigned(k); + if(n == 0) { + cmd = new EmptyCommand; + } else if(n == 1) { + cmd = new PushCommand; + } else { + CommandSequence* seq = new CommandSequence; + do { + seq->addCommand(new PushCommand); + } while(--n > 0); + cmd = seq; + } + } + | POP_TOK k=INTEGER_LITERAL + { unsigned n = AntlrInput::tokenToUnsigned(k); + if(n == 0) { + cmd = new EmptyCommand; + } else if(n == 1) { + cmd = new PopCommand; + } else { + CommandSequence* seq = new CommandSequence; + do { + seq->addCommand(new PopCommand); + } while(--n > 0); + cmd = seq; + } + } | EXIT_TOK { cmd = NULL; } ; @@ -536,6 +565,8 @@ SET_INFO_TOK : 'set-info'; GET_INFO_TOK : 'get-info'; SET_OPTION_TOK : 'set-option'; GET_OPTION_TOK : 'get-option'; +PUSH_TOK : 'push'; +POP_TOK : 'pop'; // operators (NOTE: theory symbols go here) AMPERSAND_TOK : '&'; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 2ff107068..919214f9b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -184,7 +184,7 @@ public: const NodeCache& getNodeCache() const { return d_nodeCache; } -}; /* class CnfStream */ +};/* class CnfStream */ /** * TseitinCnfStream is based on the following recursive algorithm diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index c49d5f38a..961a18bdb 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -130,6 +130,20 @@ Result PropEngine::checkSat() { return Result(result ? Result::SAT : Result::UNSAT); } +Node PropEngine::getValue(TNode node) { + Assert(node.getKind() == kind::VARIABLE && + node.getType().isBoolean()); + SatLiteralValue v = d_satSolver->value(d_cnfStream->getLiteral(node)); + if(v == l_True) { + return NodeManager::currentNM()->mkConst(true); + } else if(v == l_False) { + return NodeManager::currentNM()->mkConst(false); + } else { + Assert(v == l_Undef); + return Node::null(); + } +} + void PropEngine::push() { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "push()" << endl; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index c33982ddc..7eb903180 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -114,6 +114,14 @@ public: Result checkSat(); /** + * Get the value of a boolean variable. + * + * @return mkConst<true>, mkConst<false>, or Node::null() if + * unassigned. + */ + Node getValue(TNode node); + + /** * Push the context level. */ void push(); diff --git a/src/prop/sat.h b/src/prop/sat.h index d780230a8..776895b4c 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -89,9 +89,9 @@ inline std::string stringOfLiteralValue(SatLiteralValue val) { } #endif /* __CVC4_USE_MINISAT */ -/** Interface encapsulating the "input" to the solver, e.g., from the - * CNF converter. - * +/** Interface encapsulating the "input" to the solver, e.g., from the + * CNF converter. + * * TODO: Is it possible to push the typedefs of SatClause and SatVariable * into here, somehow? */ @@ -226,7 +226,7 @@ public: void setCnfStream(CnfStream* cnfStream); SatLiteralValue value(SatLiteral l); -}; +};/* class SatSolver */ /* Functions that delegate to the concrete SAT solver. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index de2fa4ebc..3a4fd90e9 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -119,7 +119,9 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), - d_assertionList(NULL) { + d_assertionList(NULL), + d_haveAdditions(false), + d_lastResult() { NodeManagerScope nms(d_nodeManager); @@ -162,7 +164,9 @@ SmtEngine::~SmtEngine() { void SmtEngine::setInfo(const string& key, const SExpr& value) throw(BadOptionException) { - if(key == ":status" || + Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; + if(key == ":name" || + key == ":status" || key == ":source" || key == ":category" || key == ":difficulty" || @@ -176,18 +180,21 @@ void SmtEngine::setInfo(const string& key, const SExpr& value) const SExpr& SmtEngine::getInfo(const string& key) const throw(BadOptionException) { + Debug("smt") << "SMT getInfo(" << key << ")" << endl; // FIXME implement me throw BadOptionException(); } void SmtEngine::setOption(const string& key, const SExpr& value) throw(BadOptionException) { + Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; // FIXME implement me throw BadOptionException(); } const SExpr& SmtEngine::getOption(const string& key) const throw(BadOptionException) { + Debug("smt") << "SMT getOption(" << key << ")" << endl; // FIXME implement me throw BadOptionException(); } @@ -195,6 +202,7 @@ const SExpr& SmtEngine::getOption(const string& key) const void SmtEngine::defineFunction(Expr func, const vector<Expr>& formals, Expr formula) { + Debug("smt") << "SMT defineFunction(" << func << ")" << endl; NodeManagerScope nms(d_nodeManager); Type formulaType = formula.getType(true);// type check body if(formulaType != FunctionType(func.getType()).getRangeType()) { @@ -217,6 +225,7 @@ void SmtEngine::defineFunction(Expr func, } TNode formulaNode = formula.getTNode(); DefinedFunction def(funcNode, formalsNodes, formulaNode); + d_haveAdditions = true; d_definedFunctions->insert(funcNode, def); } @@ -303,6 +312,7 @@ Result SmtEngine::quickCheck() { void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) throw(NoSuchFunctionException, AssertionException) { Debug("smt") << "push_back assertion " << n << endl; + smt.d_haveAdditions = true; smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n)); } @@ -319,42 +329,56 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) { } Result SmtEngine::checkSat(const BoolExpr& e) { + Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT checkSat(" << e << ")" << endl; ensureBoolean(e);// ensure expr is type-checked at this point SmtEnginePrivate::addFormula(*this, e.getNode()); Result r = check().asSatisfiabilityResult(); + d_lastResult = r; + d_haveAdditions = false; Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::query(const BoolExpr& e) { + Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT query(" << e << ")" << endl; ensureBoolean(e);// ensure expr is type-checked at this point SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); + d_lastResult = r; + d_haveAdditions = false; Debug("smt") << "SMT query(" << e << ") ==> " << r << endl; return r; } Result SmtEngine::assertFormula(const BoolExpr& e) { + Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT assertFormula(" << e << ")" << endl; ensureBoolean(e);// type check node + if(d_assertionList != NULL) { + d_assertionList->push_back(e); + } SmtEnginePrivate::addFormula(*this, e.getNode()); return quickCheck().asValidityResult(); } Expr SmtEngine::simplify(const Expr& e) { + Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); e.getType(true);// ensure expr is type-checked at this point Debug("smt") << "SMT simplify(" << e << ")" << endl; Unimplemented(); } -Expr SmtEngine::getValue(Expr term) +Expr SmtEngine::getValue(Expr e) throw(ModalException, AssertionException) { + Assert(e.getExprManager() == d_exprManager); + Type type = e.getType(true);// ensure expr is type-checked at this point + Debug("smt") << "SMT getValue(" << e << ")" << endl; if(!d_options->interactive) { const char* msg = "Cannot get value when not in interactive mode."; @@ -365,17 +389,33 @@ Expr SmtEngine::getValue(Expr term) "Cannot get value when produce-models options is off."; throw ModalException(msg); } - // TODO also check that the last query was sat/unknown, without intervening - // assertions + if(d_lastResult.asSatisfiabilityResult() != Result::SAT || + d_haveAdditions) { + const char* msg = + "Cannot get value unless immediately proceded by SAT/INVALID response."; + throw ModalException(msg); + } + if(type.isFunction() || type.isPredicate() || + type.isKind() || type.isSortConstructor()) { + const char* msg = + "Cannot get value of a function, predicate, or sort."; + throw ModalException(msg); + } NodeManagerScope nms(d_nodeManager); - Type type = term.getType(true);// ensure expr is type-checked at this point - SmtEnginePrivate::preprocess(*this, term.getNode()); + Node eNode = e.getNode(); + Node n = SmtEnginePrivate::preprocess(*this, eNode); - Unimplemented(); + Debug("smt") << "--- getting value of " << n << endl; + Node resultNode = d_theoryEngine->getValue(n); + + // type-check the result we got + Assert(resultNode.getType(true) == eNode.getType()); + return Expr(d_exprManager, new Node(resultNode)); } SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { + Debug("smt") << "SMT getAssignment()" << endl; if(!d_options->produceAssignments) { const char* msg = "Cannot get the current assignment when produce-assignments option is off."; @@ -389,7 +429,9 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Unimplemented(); } -vector<Expr> SmtEngine::getAssertions() throw(ModalException, AssertionException) { +vector<Expr> SmtEngine::getAssertions() + throw(ModalException, AssertionException) { + Debug("smt") << "SMT getAssertions()" << endl; if(!d_options->interactive) { const char* msg = "Cannot query the current assertion list when not in interactive mode."; @@ -402,13 +444,22 @@ vector<Expr> SmtEngine::getAssertions() throw(ModalException, AssertionException void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT push()" << endl; - Unimplemented(); + d_context->push(); + d_propEngine->push(); + Debug("userpushpop") << "SmtEngine: pushed to level " + << d_context->getLevel() << endl; } void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT pop()" << endl; - Unimplemented(); + d_propEngine->pop(); + d_context->pop(); + Debug("userpushpop") << "SmtEngine: popped to level " + << d_context->getLevel() << endl; + // clear out last result: get-value/get-assignment no longer + // available here + d_lastResult = Result(); } }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1fd68d2a5..efa48e517 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -112,6 +112,18 @@ class CVC4_PUBLIC SmtEngine { AssertionList* d_assertionList; /** + * Whether or not we have added any + * assertions/declarations/definitions since the last checkSat/query + * (and therefore we're not responsible for an assignment). + */ + bool d_haveAdditions; + + /** + * Result of last checkSat/query. + */ + Result d_lastResult; + + /** * This is called by the destructor, just before destroying the * PropEngine, TheoryEngine, and DecisionEngine (in that order). It * is important because there are destruction ordering issues @@ -213,14 +225,14 @@ public: Expr simplify(const Expr& e); /** - * Get the assigned value of a term (only if preceded by a SAT or - * INVALID query). Only permitted if the SmtEngine is set to - * operate interactively and produce-models is on. + * Get the assigned value of an expr (only if immediately preceded + * by a SAT or INVALID query). Only permitted if the SmtEngine is + * set to operate interactively and produce-models is on. */ - Expr getValue(Expr term) throw(ModalException, AssertionException); + Expr getValue(Expr e) throw(ModalException, AssertionException); /** - * Get the assigned value of a term (only if preceded by a SAT or + * Get the assignment (only if immediately preceded by a SAT or * INVALID query). Only permitted if the SmtEngine is set to * operate interactively and produce-assignments is on. */ diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index f6a460fee..d0e4ed1f4 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -24,12 +24,12 @@ using namespace std; using namespace CVC4; std::ostream& CVC4::operator<<(std::ostream& os, const DeltaRational& dq){ - return os << "(" << dq.getNoninfintestimalPart() - << "," << dq.getInfintestimalPart() << ")"; + return os << "(" << dq.getNoninfinitesimalPart() + << "," << dq.getInfinitesimalPart() << ")"; } std::string DeltaRational::toString() const { - return "(" + getNoninfintestimalPart().toString() + "," + - getInfintestimalPart().toString() + ")"; + return "(" + getNoninfinitesimalPart().toString() + "," + + getInfinitesimalPart().toString() + ")"; } diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 26212ec66..b75f5334c 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -46,11 +46,11 @@ public: DeltaRational(const CVC4::Rational& base, const CVC4::Rational& coeff) : c(base), k(coeff) {} - const CVC4::Rational& getInfintestimalPart() const { + const CVC4::Rational& getInfinitesimalPart() const { return k; } - const CVC4::Rational& getNoninfintestimalPart() const { + const CVC4::Rational& getNoninfinitesimalPart() const { return c; } diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index aaeadb629..d6a30ac91 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -48,7 +48,7 @@ Row::Row(ArithVar basic, Assert(d_coeffs[var_i] != Rational(0,1)); } } -void Row::subsitute(Row& row_s){ +void Row::substitute(Row& row_s){ ArithVar x_s = row_s.basicVar(); Assert(has(x_s)); @@ -133,7 +133,7 @@ void Tableau::addRow(ArithVar basicVar, Assert(isActiveBasicVariable(var)); Row* row_var = lookup(var); - row_current->subsitute(*row_var); + row_current->substitute(*row_var); } } } @@ -163,7 +163,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){ Row* row_k = lookup(basic); if(row_k->has(x_s)){ d_activityMonitor.increaseActivity(basic, 30); - row_k->subsitute(*row_s); + row_k->substitute(*row_s); } } } @@ -189,7 +189,7 @@ void Tableau::updateRow(Row* row){ Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var); Assert(row_var != row); - row->subsitute(*row_var); + row->substitute(*row_var); i = row->begin(); endIter = row->end(); diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index a69493ee0..88a5c2317 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -83,7 +83,7 @@ public: void pivot(ArithVar x_j); - void subsitute(Row& row_s); + void substitute(Row& row_s); void printRow(); }; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 26bb58e90..ac3dc3d40 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -22,6 +22,8 @@ #include "expr/metakind.h" #include "expr/node_builder.h" +#include "theory/theory_engine.h" + #include "util/rational.h" #include "util/integer.h" @@ -927,3 +929,77 @@ void TheoryArith::propagate(Effort e) { } } } + +Node TheoryArith::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + case kind::VARIABLE: { + DeltaRational drat = d_partialModel.getAssignment(asArithVar(n)); + // FIXME our infinitesimal is fixed here at 1e-06 + return nodeManager-> + mkConst( drat.getNoninfinitesimalPart() + + drat.getInfinitesimalPart() * Rational(1, 1000000) ); + } + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + case kind::PLUS: { // 2+ args + Rational value = d_constants.d_ZERO; + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + value += engine->getValue(*i).getConst<Rational>(); + } + return nodeManager->mkConst(value); + } + + case kind::MULT: { // 2+ args + Rational value = d_constants.d_ONE; + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + value *= engine->getValue(*i).getConst<Rational>(); + } + return nodeManager->mkConst(value); + } + + case kind::MINUS: // 2 args + // should have been rewritten + Unreachable(); + + case kind::UMINUS: // 1 arg + // should have been rewritten + Unreachable(); + + case kind::DIVISION: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() / + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::IDENTITY: // 1 arg + return engine->getValue(n[0]); + + case kind::LT: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() < + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::LEQ: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <= + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::GT: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() > + engine->getValue(n[1]).getConst<Rational>() ); + + case kind::GEQ: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() >= + engine->getValue(n[1]).getConst<Rational>() ); + + default: + Unhandled(n.getKind()); + } +} diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index cbfdf27f3..26dcc9825 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -128,6 +128,8 @@ public: void propagate(Effort e); void explain(TNode n, Effort e); + Node getValue(TNode n, TheoryEngine* engine); + void shutdown(){ } std::string identify() const { return std::string("TheoryArith"); } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 8997138cb..55a539f44 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -18,6 +18,7 @@ #include "theory/arrays/theory_arrays.h" +#include "theory/theory_engine.h" #include "expr/kind.h" @@ -58,3 +59,20 @@ void TheoryArrays::check(Effort e) { } Debug("arrays") << "TheoryArrays::check(): done" << endl; } + +Node TheoryArrays::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + + case kind::VARIABLE: + Unhandled(kind::VARIABLE); + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + default: + Unhandled(n.getKind()); + } +} diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index cb738d085..89631d59f 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -53,6 +53,7 @@ public: void check(Effort e); void propagate(Effort e) { } void explain(TNode n, Effort e) { } + Node getValue(TNode n, TheoryEngine* engine); void shutdown() { } std::string identify() const { return std::string("TheoryArrays"); } };/* class TheoryArrays */ diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index a7e343fdc..b1ff472ac 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -18,12 +18,12 @@ #include "theory/theory.h" #include "theory/booleans/theory_bool.h" +#include "theory/theory_engine.h" namespace CVC4 { namespace theory { namespace booleans { - RewriteResponse TheoryBool::preRewrite(TNode n, bool topLevel) { if(n.getKind() == kind::IFF) { NodeManager* nodeManager = NodeManager::currentNM(); @@ -140,6 +140,70 @@ RewriteResponse TheoryBool::postRewrite(TNode n, bool topLevel) { return RewriteComplete(n); } +Node TheoryBool::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + case kind::VARIABLE: + // case for Boolean vars is implemented in TheoryEngine (since it + // appeals to the PropEngine to get the value) + Unreachable(); + + case kind::EQUAL: // 2 args + // should be handled by IFF + Unreachable(); + + case kind::NOT: // 1 arg + return nodeManager->mkConst(! engine->getValue(n[0]).getConst<bool>()); + + case kind::AND: { // 2+ args + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + if(! engine->getValue(*i).getConst<bool>()) { + return nodeManager->mkConst(false); + } + } + return nodeManager->mkConst(true); + } + + case kind::IFF: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() == + engine->getValue(n[1]).getConst<bool>() ); + + case kind::IMPLIES: // 2 args + return nodeManager->mkConst( (! engine->getValue(n[0]).getConst<bool>()) || + engine->getValue(n[1]).getConst<bool>() ); + + case kind::OR: { // 2+ args + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + if(engine->getValue(*i).getConst<bool>()) { + return nodeManager->mkConst(true); + } + } + return nodeManager->mkConst(false); + } + + case kind::XOR: // 2 args + return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() != + engine->getValue(n[1]).getConst<bool>() ); + + case kind::ITE: // 3 args + // all ITEs should be gone except (bool,bool,bool) ones + Assert( n[1].getType() == nodeManager->booleanType() && + n[2].getType() == nodeManager->booleanType() ); + return nodeManager->mkConst( engine->getValue(n[0]).getConst<bool>() ? + engine->getValue(n[1]).getConst<bool>() : + engine->getValue(n[2]).getConst<bool>() ); + + default: + Unhandled(n.getKind()); + } +} }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index d87aa95b5..2c77c09b3 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -46,6 +46,8 @@ public: void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } + Node getValue(TNode n, TheoryEngine* engine); + RewriteResponse preRewrite(TNode n, bool topLevel); RewriteResponse postRewrite(TNode n, bool topLevel); diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index ba258aafd..810cd1d39 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -17,6 +17,7 @@ **/ #include "theory/builtin/theory_builtin.h" +#include "theory/theory_engine.h" #include "expr/kind.h" using namespace std; @@ -26,7 +27,8 @@ namespace theory { namespace builtin { Node TheoryBuiltin::blastDistinct(TNode in) { - Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: " << in << std::endl; + Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: " + << in << std::endl; Assert(in.getKind() == kind::DISTINCT); if(in.getNumChildren() == 2) { // if this is the case exactly 1 != pair will be generated so the @@ -67,6 +69,40 @@ RewriteResponse TheoryBuiltin::preRewrite(TNode in, bool topLevel) { } } +Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) { + switch(n.getKind()) { + + case kind::VARIABLE: + // no variables that the builtin theory is responsible for + Unreachable(); + + case kind::EQUAL: { // 2 args + // has to be an EQUAL over tuples, since all others should be + // handled elsewhere + Assert(n[0].getKind() == kind::TUPLE && + n[1].getKind() == kind::TUPLE); + return NodeManager::currentNM()-> + mkConst( getValue(n[0], engine) == getValue(n[1], engine) ); + } + + case kind::TUPLE: { // 2+ args + NodeBuilder<> nb(kind::TUPLE); + for(TNode::iterator i = n.begin(), + iend = n.end(); + i != iend; + ++i) { + nb << engine->getValue(*i); + } + return Node(nb); + } + + default: + // all other "builtins" should have been rewritten away or handled + // by theory engine, or handled elsewhere. + Unhandled(n.getKind()); + } +} + }/* CVC4::theory::builtin namespace */ }/* CVC4::theory */ }/* CVC4 namespace */ diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index a08ed9b78..57c5d1558 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -39,6 +39,7 @@ public: void check(Effort e) { Unreachable(); } void propagate(Effort e) { Unreachable(); } void explain(TNode n, Effort e) { Unreachable(); } + Node getValue(TNode n, TheoryEngine* engine); void shutdown() { } RewriteResponse preRewrite(TNode n, bool topLevel); std::string identify() const { return std::string("TheoryBuiltin"); } diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index bd0d73865..69ff48721 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -17,9 +17,11 @@ ** \todo document this file **/ -#include "theory_bv.h" -#include "theory_bv_utils.h" -#include "theory_bv_rewrite_rules.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/bv/theory_bv_rewrite_rules.h" + +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::theory; @@ -160,3 +162,19 @@ bool TheoryBV::triggerEquality(size_t triggerId) { return true; } +Node TheoryBV::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + + case kind::VARIABLE: + Unhandled(kind::VARIABLE); + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + default: + Unhandled(n.getKind()); + } +} diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ff5d4c2a2..c673a56b4 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -75,6 +75,8 @@ public: void explain(TNode n, Effort e) { } + Node getValue(TNode n, TheoryEngine* engine); + RewriteResponse postRewrite(TNode n, bool topLevel); std::string identify() const { return std::string("TheoryBV"); } diff --git a/src/theory/theory.h b/src/theory/theory.h index 2711a0b95..df9dcafef 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -262,9 +262,11 @@ public: // TODO add compiler annotation "constant function" here static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; } static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; } - static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && e < STANDARD; } + static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && + e < STANDARD; } static bool standardEffortOrMore(Effort e) { return e >= STANDARD; } - static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; } + static bool standardEffortOnly(Effort e) { return e >= STANDARD && + e < FULL_EFFORT; } static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** @@ -328,7 +330,8 @@ public: * (ITE true x y). */ virtual RewriteResponse preRewrite(TNode n, bool topLevel) { - Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl; + Debug("theory-rewrite") << "no pre-rewriting to perform for " + << n << std::endl; return RewriteComplete(n); } @@ -340,7 +343,8 @@ public: * memory leakage). */ virtual RewriteResponse postRewrite(TNode n, bool topLevel) { - Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl; + Debug("theory-rewrite") << "no post-rewriting to perform for " + << n << std::endl; return RewriteComplete(n); } @@ -366,18 +370,21 @@ public: } /** - * This method is called to notify a theory that the node n should be considered a "shared term" by this theory + * This method is called to notify a theory that the node n should + * be considered a "shared term" by this theory */ virtual void addSharedTerm(TNode n) { } /** - * This method is called by the shared term manager when a shared term lhs - * which this theory cares about (either because it received a previous - * addSharedTerm call with lhs or because it received a previous notifyEq call - * with lhs as the second argument) becomes equal to another shared term rhs. - * This call also serves as notice to the theory that the shared term manager - * now considers rhs the representative for this equivalence class of shared - * terms, so future notifications for this class will be based on rhs not lhs. + * This method is called by the shared term manager when a shared + * term lhs which this theory cares about (either because it + * received a previous addSharedTerm call with lhs or because it + * received a previous notifyEq call with lhs as the second + * argument) becomes equal to another shared term rhs. This call + * also serves as notice to the theory that the shared term manager + * now considers rhs the representative for this equivalence class + * of shared terms, so future notifications for this class will be + * based on rhs not lhs. */ virtual void notifyEq(TNode lhs, TNode rhs) { } @@ -405,6 +412,38 @@ public: virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0; /** + * Return the value of a node (typically used after a ). If the + * theory supports model generation but has no value for this node, + * it should return Node::null(). If the theory doesn't support + * model generation at all, or usually would but doesn't in its + * current state, it should throw an exception saying so. + * + * The TheoryEngine is passed in so that you can recursively request + * values for the Node's children. This is important because the + * TheoryEngine takes care of simple cases (metakind CONSTANT, + * Boolean-valued VARIABLES, ...) and can dispatch to other theories + * if that's necessary. Only call your own getValue() recursively + * if you *know* that you are responsible handle the Node you're + * asking for; other theories can use your types, so be careful + * here! To be safe, it's best to delegate back to the + * TheoryEngine. + * + * Usually, you need to handle at least the two cases of EQUAL and + * VARIABLE---EQUAL in case a value of yours is on the LHS of an + * EQUAL, and VARIABLE for variables of your types. You also need + * to support any operators that can survive your rewriter. You + * don't need to handle constants, as they are handled by the + * TheoryEngine. + * + * There are some gotchas here. The user may be requesting the + * value of an expression that wasn't part of the satisfiable + * assertion, or has been declared since. If you don't have a value + * and suspect this situation is the case, return Node::null() + * rather than throwing an exception. + */ + virtual Node getValue(TNode n, TheoryEngine* engine) = 0; + + /** * Identify this theory (for debugging, dynamic configuration, * etc..) */ @@ -550,7 +589,8 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level); }/* CVC4::theory namespace */ -inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) { +inline std::ostream& operator<<(std::ostream& out, + const CVC4::theory::Theory& theory) { return out << theory.identify(); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 041b6852b..388167e00 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -537,4 +537,20 @@ Node TheoryEngine::rewrite(TNode in, bool topLevel) { return out; }/* TheoryEngine::rewrite(TNode in) */ + +Node TheoryEngine::getValue(TNode node) { + kind::MetaKind metakind = node.getMetaKind(); + // special case: prop engine handles boolean vars + if(metakind == kind::metakind::VARIABLE && node.getType().isBoolean()) { + return d_propEngine->getValue(node); + } + // special case: value of a constant == itself + if(metakind == kind::metakind::CONSTANT) { + return node; + } + + // otherwise ask the theory-in-charge + return theoryOf(node)->getValue(node, this); +}/* TheoryEngine::getValue(TNode node) */ + }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 5227d32f0..0eaf61055 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -380,7 +380,7 @@ public: return d_theoryOut.d_explanationNode; } - inline Node getExplanation(TNode node){ + inline Node getExplanation(TNode node) { d_theoryOut.d_explanationNode = Node::null(); theory::Theory* theory = node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node); @@ -388,6 +388,8 @@ public: return d_theoryOut.d_explanationNode; } + Node getValue(TNode node); + private: class Statistics { public: diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index eb6c430ba..a1eec9d4c 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -17,6 +17,7 @@ **/ #include "theory/uf/morgan/theory_uf_morgan.h" +#include "theory/theory_engine.h" #include "expr/kind.h" #include "util/congruence_closure.h" @@ -451,6 +452,32 @@ void TheoryUFMorgan::propagate(Effort level) { Debug("uf") << "uf: end propagate(" << level << ")" << std::endl; } +Node TheoryUFMorgan::getValue(TNode n, TheoryEngine* engine) { + NodeManager* nodeManager = NodeManager::currentNM(); + + switch(n.getKind()) { + + case kind::VARIABLE: + case kind::APPLY_UF: + if(n.getType().isBoolean()) { + if(d_cc.areCongruent(d_trueNode, n)) { + return nodeManager->mkConst(true); + } else if(d_cc.areCongruent(d_trueNode, n)) { + return nodeManager->mkConst(false); + } + return Node::null(); + } + return d_cc.normalize(n); + + case kind::EQUAL: // 2 args + return nodeManager-> + mkConst( engine->getValue(n[0]) == engine->getValue(n[1]) ); + + default: + Unhandled(n.getKind()); + } +} + void TheoryUFMorgan::dump() { if(!Debug.isOn("uf")) { return; diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index d17eb87f5..7a12f216b 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -151,13 +151,21 @@ public: void propagate(Effort level); /** - * Explains a previously reported conflict. Currently does nothing. + * Explains a previously theory-propagated literal. * * Overloads void explain(TNode n, Effort level); from theory.h. * See theory/theory.h for more information about this method. */ void explain(TNode n, Effort level) {} + /** + * Gets a theory value. + * + * Overloads Node getValue(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + Node getValue(TNode n, TheoryEngine* engine); + std::string identify() const { return std::string("TheoryUFMorgan"); } private: diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index 9a2d252c0..4c8a1a71a 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -156,6 +156,16 @@ public: */ void explain(TNode n, Effort level) {} + /** + * Get a theory value. + * + * Overloads Node getValue(TNode n); from theory.h. + * See theory/theory.h for more information about this method. + */ + Node getValue(TNode n, TheoryEngine* engine) { + Unimplemented("TheoryUFTim doesn't support model generation"); + } + std::string identify() const { return std::string("TheoryUFTim"); } private: diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 88c17a193..cc18a3305 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -286,6 +286,11 @@ public: return explain(eq[0], eq[1]); } + /** + * Normalization. + */ + Node normalize(TNode t) const throw(AssertionException); + private: friend std::ostream& operator<< <>(std::ostream& out, @@ -360,11 +365,6 @@ private: void merge(TNode ec1, TNode ec2); void mergeProof(TNode a, TNode b, TNode e); - /** - * Internal normalization. - */ - Node normalize(TNode t) const throw(AssertionException); - };/* class CongruenceClosure */ diff --git a/src/util/result.h b/src/util/result.h index ccc36973d..f1f6ae1c2 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -86,6 +86,21 @@ public: } enum UnknownExplanation whyUnknown(); + inline bool operator==(Result r) { + if(d_which != r.d_which) { + return false; + } + if(d_which == TYPE_SAT) { + return d_sat == r.d_sat; + } + if(d_which == TYPE_VALIDITY) { + return d_validity == r.d_validity; + } + return false; + } + inline bool operator!=(Result r) { + return !(*this == r); + } inline Result asSatisfiabilityResult() const; inline Result asValidityResult() const; |