diff options
49 files changed, 1707 insertions, 1031 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index f416f84bb..8d6748e54 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -286,7 +286,7 @@ SimplifyCommand::SimplifyCommand(Expr term) : } void SimplifyCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->simplify(d_term); +#warning TODO: what is this } Expr SimplifyCommand::getResult() const { diff --git a/src/expr/node.h b/src/expr/node.h index 999719592..f501dba21 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -827,6 +827,11 @@ public: */ inline void printAst(std::ostream& out, int indent = 0) const; + /** + * Check if the node has a subterm t. + */ + inline bool hasSubterm(NodeTemplate<false> t, bool strict = false) const; + NodeTemplate<true> eqNode(const NodeTemplate& right) const; NodeTemplate<true> notNode() const; @@ -1231,7 +1236,7 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement, if(*i == node) { nb << replacement; } else { - (*i).substitute(node, replacement, cache); + nb << (*i).substitute(node, replacement, cache); } } @@ -1359,6 +1364,38 @@ inline Node NodeTemplate<true>::fromExpr(const Expr& e) { return NodeManager::fromExpr(e); } +template<bool ref_count> +bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const { + typedef std::hash_set<TNode, TNodeHashFunction> node_set; + + if (!strict && *this == t) { + return true; + } + + node_set visited; + std::vector<TNode> toProcess; + + toProcess.push_back(*this); + + for (unsigned i = 0; i < toProcess.size(); ++ i) { + TNode current = toProcess[i]; + for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) { + TNode child = current[j]; + if (child == t) { + return true; + } + if (visited.find(child) != visited.end()) { + continue; + } else { + visited.insert(child); + toProcess.push_back(child); + } + } + } + + return false; +} + #ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 95124d297..ce3db4a40 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -247,6 +247,12 @@ TypeNode NodeManager::computeType(TNode n, bool check) // Infer the type switch(n.getKind()) { + case kind::VARIABLE: + typeNode = getAttribute(n, TypeAttr()); + break; + case kind::SKOLEM: + typeNode = getAttribute(n, TypeAttr()); + break; case kind::BUILTIN: typeNode = builtinOperatorType(); break; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 6732b09bc..0967f54ff 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -121,15 +121,16 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { d_nodeCache[~lit] = node.notNode(); } + // If a theory literal, we pre-register it + if (theoryLiteral) { + bool backup = d_assertingLemma; + d_registrar.preRegister(node); + d_assertingLemma = backup; + } + // Here, you can have it Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl; - // have to keep track of this, because with the call to preRegister(), - // the cnf stream is re-entrant! - bool wasAssertingLemma = d_assertingLemma; - d_registrar.preRegister(node); - d_assertingLemma = wasAssertingLemma; - return lit; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 63228a803..7e335a21b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -81,7 +81,7 @@ void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(node, false, false); + d_cnfStream->convertAndAssert(d_theoryEngine->preprocess(node), false, false); } void PropEngine::assertLemma(TNode node) { @@ -93,7 +93,6 @@ void PropEngine::assertLemma(TNode node) { d_cnfStream->convertAndAssert(node, true, false); } - void PropEngine::printSatisfyingAssignment(){ const CnfStream::TranslationCache& transCache = d_cnfStream->getTranslationCache(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c381ba5bd..4185765a8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -43,6 +43,7 @@ #include "theory/substitutions.h" #include "theory/builtin/theory_builtin.h" #include "theory/booleans/theory_bool.h" +#include "theory/booleans/circuit_propagator.h" #include "theory/uf/theory_uf.h" #include "theory/uf/morgan/theory_uf_morgan.h" #include "theory/uf/tim/theory_uf_tim.h" @@ -50,12 +51,14 @@ #include "theory/arrays/theory_arrays.h" #include "theory/bv/theory_bv.h" #include "theory/datatypes/theory_datatypes.h" +#include "util/ite_removal.h" using namespace std; using namespace CVC4; using namespace CVC4::smt; using namespace CVC4::prop; using namespace CVC4::context; +using namespace CVC4::theory; namespace CVC4 { @@ -100,49 +103,53 @@ public: class SmtEnginePrivate { SmtEngine& d_smt; - vector<Node> d_assertionsToSimplify; - vector<Node> d_assertionsToPushToSat; + /** The assertions yet to be preprecessed */ + vector<Node> d_assertionsToPreprocess; - theory::Substitutions d_topLevelSubstitutions; + /** Learned literals */ + vector<Node> d_nonClausalLearnedLiterals; - /** - * Adjust the currently "withheld" assertions for the current - * Options scope's SimplificationMode if purge is false, or push - * them all out to the prop layer if purge is true. - */ - void adjustAssertions(bool purge = false); + /** Assertions to push to sat */ + vector<Node> d_assertionsToCheck; -public: - - SmtEnginePrivate(SmtEngine& smt) : d_smt(smt) { } + /** The top level substitutions */ + theory::SubstitutionMap d_topLevelSubstitutions; /** - * Push withheld assertions out to the propositional layer, if any. + * Runs the nonslausal solver and tries to solve all the assigned + * theory literals. */ - void pushAssertions() { - Trace("smt") << "SMT pushing all withheld assertions" << endl; + void nonClausalSimplify(); - adjustAssertions(true); - Assert(d_assertionsToSimplify.empty()); - Assert(d_assertionsToPushToSat.empty()); + /** + * Performs static learning on the assertions. + */ + void staticLearning(); - Trace("smt") << "SMT done pushing all withheld assertions" << endl; - } + /** + * Remove ITEs from the assertions. + */ + void removeITEs(); /** * Perform non-clausal simplification of a Node. This involves * Theory implementations, but does NOT involve the SAT solver in * any way. */ - Node simplify(TNode n, bool noPersist = false) - throw(NoSuchFunctionException, AssertionException); + void simplifyAssertions() throw(NoSuchFunctionException, AssertionException); + +public: + + SmtEnginePrivate(SmtEngine& smt) : d_smt(smt) { } + + Node applySubstitutions(TNode node) const { + return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); + } /** - * Perform preprocessing of a Node. This involves ITE removal and - * Theory-specific rewriting, but NO action by the SAT solver. + * Process the assertions that have been asserted. */ - Node preprocess(TNode n) - throw(AssertionException); + void processAssertions(); /** * Adds a formula to the current context. Action here depends on @@ -214,7 +221,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : } d_assignments = NULL; - d_haveAdditions = false; + d_problemExtended = false; d_queryMade = false; } @@ -258,7 +265,7 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { - Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; + Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; if(key == ":name" || key == ":source" || key == ":category" || @@ -284,7 +291,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) SExpr SmtEngine::getInfo(const std::string& key) const throw(BadOptionException) { - Trace("smt") << "SMT getInfo(" << key << ")" << endl; + Debug("smt") << "SMT getInfo(" << key << ")" << endl; if(key == ":all-statistics") { vector<SExpr> stats; for(StatisticsRegistry::const_iterator i = StatisticsRegistry::begin(); @@ -322,7 +329,7 @@ SExpr SmtEngine::getInfo(const std::string& key) const void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { - Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; + Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(key == ":print-success") { throw BadOptionException(); @@ -361,7 +368,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) SExpr SmtEngine::getOption(const std::string& key) const throw(BadOptionException) { - Trace("smt") << "SMT getOption(" << key << ")" << endl; + Debug("smt") << "SMT getOption(" << key << ")" << endl; if(key == ":print-success") { return SExpr("true"); } else if(key == ":expand-definitions") { @@ -392,7 +399,7 @@ SExpr SmtEngine::getOption(const std::string& key) const void SmtEngine::defineFunction(Expr func, const std::vector<Expr>& formals, Expr formula) { - Trace("smt") << "SMT defineFunction(" << func << ")" << endl; + Debug("smt") << "SMT defineFunction(" << func << ")" << endl; NodeManagerScope nms(d_nodeManager); Type formulaType = formula.getType(Options::current()->typeChecking);// type check body Type funcType = func.getType(); @@ -424,8 +431,7 @@ void SmtEngine::defineFunction(Expr func, d_definedFunctions->insert(funcNode, def); } -Node SmtEnginePrivate::expandDefinitions(TNode n, - hash_map<TNode, Node, TNodeHashFunction>& cache) +Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache) throw(NoSuchFunctionException, AssertionException) { if(n.getKind() != kind::APPLY && n.getNumChildren() == 0) { @@ -475,7 +481,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, n.begin(), n.end()); Debug("expand") << "made : " << instance << endl; - Node expanded = this->expandDefinitions(instance, cache); + Node expanded = expandDefinitions(instance, cache); cache[n] = (n == expanded ? Node::null() : expanded); return expanded; } else { @@ -489,7 +495,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, iend = n.end(); i != iend; ++i) { - Node expanded = this->expandDefinitions(*i, cache); + Node expanded = expandDefinitions(*i, cache); Debug("expand") << "exchld: " << expanded << endl; nb << expanded; } @@ -499,116 +505,144 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, } } -Node SmtEnginePrivate::simplify(TNode in, bool noPersist) - throw(NoSuchFunctionException, AssertionException) { - try { - Node n; - if(!Options::current()->lazyDefinitionExpansion) { - TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); - Chat() << "Expanding definitions: " << in << endl; - Debug("expand") << "have: " << n << endl; - hash_map<TNode, Node, TNodeHashFunction> cache; - n = this->expandDefinitions(in, cache); - Debug("expand") << "made: " << n << endl; - } else { - n = in; - } +void SmtEnginePrivate::removeITEs() { + Debug("simplify") << "SmtEnginePrivate::removeITEs()" << std::endl; - if(Options::current()->simplificationStyle == Options::NO_SIMPLIFICATION_STYLE) { - Chat() << "Not doing nonclausal simplification (by user request)" << endl; - } else { - if(Options::current()->simplificationStyle == Options::AGGRESSIVE_SIMPLIFICATION_STYLE) { - Unimplemented("can't do aggressive nonclausal simplification yet"); - } - Chat() << "Simplifying (non-clausally): " << n << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_nonclausalSimplificationTime); - Trace("smt-simplify") << "simplifying: " << n << endl; - n = n.substitute(d_topLevelSubstitutions.begin(), d_topLevelSubstitutions.end()); - size_t oldSize = d_topLevelSubstitutions.size(); - n = d_smt.d_theoryEngine->simplify(n, d_topLevelSubstitutions); - if(n.getKind() != kind::AND && d_topLevelSubstitutions.size() > oldSize) { - Debug("smt-simplify") << "new top level substitutions not incorporated " - << "into assertion (" - << (d_topLevelSubstitutions.size() - oldSize) - << "):" << endl; - NodeBuilder<> b(kind::AND); - b << n; - for(size_t i = oldSize; i < d_topLevelSubstitutions.size(); ++i) { - Debug("smt-simplify") << " " << d_topLevelSubstitutions[i] << endl; - TNode x = d_topLevelSubstitutions[i].first; - TNode y = d_topLevelSubstitutions[i].second; - if(x.getType().isBoolean()) { - if(x.getMetaKind() == kind::metakind::CONSTANT) { - if(y.getMetaKind() == kind::metakind::CONSTANT) { - if(x == y) { - b << d_smt.d_nodeManager->mkConst(true); - } else { - b << d_smt.d_nodeManager->mkConst(false); - } - } else { - if(x.getConst<bool>()) { - b << y; - } else { - b << BooleanSimplification::negate(y); - } - } - } else if(y.getMetaKind() == kind::metakind::CONSTANT) { - if(y.getConst<bool>()) { - b << x; - } else { - b << BooleanSimplification::negate(x); - } - } else { - b << x.iffNode(y); - } - } else { - b << x.eqNode(y); - } - } - n = b; - n = BooleanSimplification::simplifyConflict(n); - } - Trace("smt-simplify") << "+++++++ got: " << n << endl; - if(noPersist) { - d_topLevelSubstitutions.resize(oldSize); - } - } + // Remove all of the ITE occurances and normalize + RemoveITE::run(d_assertionsToCheck); + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_assertionsToCheck[i] = theory::Rewriter::rewrite(d_assertionsToCheck[i]); + } +} + +void SmtEnginePrivate::staticLearning() { + + TimerStat::CodeTimer staticLearningTimer(d_smt.d_staticLearningTime); + + Debug("simplify") << "SmtEnginePrivate::staticLearning()" << std::endl; + + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { - // For now, don't re-statically-learn from learned facts; this could - // be useful though (e.g., theory T1 could learn something further - // from something learned previously by T2). - Chat() << "Performing static learning: " << n << endl; - TimerStat::CodeTimer codeTimer(d_smt.d_staticLearningTime); NodeBuilder<> learned(kind::AND); - learned << n; - d_smt.d_theoryEngine->staticLearning(n, learned); + learned << d_assertionsToCheck[i]; + d_smt.d_theoryEngine->staticLearning(d_assertionsToCheck[i], learned); if(learned.getNumChildren() == 1) { learned.clear(); } else { - n = learned; + d_assertionsToCheck[i] = learned; } + } +} - return n; +void SmtEnginePrivate::nonClausalSimplify() { - } catch(TypeCheckingExceptionPrivate& tcep) { - // Calls to this function should have already weeded out any - // typechecking exceptions via (e.g.) ensureBoolean(). But a - // theory could still create a new expression that isn't - // well-typed, and we don't want the C++ runtime to abort our - // process without any error notice. - stringstream ss; - ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage)) - << "A bad expression was produced. Original exception follows:\n" - << tcep; - InternalError(ss.str().c_str()); + TimerStat::CodeTimer nonclauselTimer(d_smt.d_nonclausalSimplificationTime); + + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << std::endl; + + // Apply the substitutions we already have, and normalize + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): applying substitutions" << std::endl; + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + d_assertionsToPreprocess[i] = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); } + + d_nonClausalLearnedLiterals.clear(); + bool goNuts = Options::current()->simplificationStyle == Options::AGGRESSIVE_SIMPLIFICATION_STYLE; + booleans::CircuitPropagator propagator(d_nonClausalLearnedLiterals, true, true, goNuts); + + // Assert all the assertions to the propagator + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting to propagator" << std::endl; + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + propagator.assert(d_assertionsToPreprocess[i]); + } + + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): propagating" << std::endl; + if (propagator.propagate()) { + // If in conflict, just return false + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): conflict in non-clausal propagation" << std::endl; + d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); + return; + } else { + // No, conflict, go through the literals and solve them + unsigned j = 0; + for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals.size(); i < i_end; ++ i) { + // Simplify the literal we learned wrt previous substitutions + Node learnedLiteral = theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i])); + // It might just simplify to a constant + if (learnedLiteral.isConst()) { + if (learnedLiteral.getConst<bool>()) { + // If the learned literal simplifies to true, it's redundant + continue; + } else { + // If the learned literal simplifies to false, we're in conflict + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): conflict with " << d_nonClausalLearnedLiterals[i] << std::endl; + d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); + return; + } + } + // Solve it with the corresponding theory + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): solving " << learnedLiteral << std::endl; + Theory::SolveStatus solveStatus = d_smt.d_theoryEngine->solve(learnedLiteral, d_topLevelSubstitutions); + switch (solveStatus) { + case Theory::SOLVE_STATUS_CONFLICT: + // If in conflict, we return false + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): conflict while solving " << learnedLiteral << std::endl; + d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); + return; + case Theory::SOLVE_STATUS_SOLVED: + // The literal should rewrite to true + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): solved " << learnedLiteral << std::endl; + Assert(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(learnedLiteral)).isConst()); + break; + default: + // Keep the literal + d_nonClausalLearnedLiterals[j++] = d_nonClausalLearnedLiterals[i]; + break; + } + } + // Resize the learnt + d_nonClausalLearnedLiterals.resize(j); + } + + for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) { + d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_nonClausalLearnedLiterals[i]))); + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): non-clausal learned : " << d_assertionsToCheck.back() << std::endl; + } + d_nonClausalLearnedLiterals.clear(); + + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + d_assertionsToCheck.push_back(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]))); + Debug("simplify") << "SmtEnginePrivate::nonClausalSimplify(): non-clausal preprocessed: " << d_assertionsToCheck.back() << std::endl; + } + d_assertionsToPreprocess.clear(); } -Node SmtEnginePrivate::preprocess(TNode in) throw(AssertionException) { +void SmtEnginePrivate::simplifyAssertions() throw(NoSuchFunctionException, AssertionException) { try { - Chat() << "Preprocessing / rewriting: " << in << endl; - return d_smt.d_theoryEngine->preprocess(in); + + Debug("simplify") << "SmtEnginePrivate::simplify()" << std::endl; + + if(!Options::current()->lazyDefinitionExpansion) { + Debug("simplify") << "SmtEnginePrivate::simplify(): exanding definitions" << std::endl; + TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime); + hash_map<TNode, Node, TNodeHashFunction> cache; + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + d_assertionsToPreprocess[i] = expandDefinitions(d_assertionsToPreprocess[i], cache); + } + } + + // Perform the non-clausal simplification + Debug("simplify") << "SmtEnginePrivate::simplify(): performing non-clausal simplification" << std::endl; + nonClausalSimplify(); + + // Perform static learning + Debug("simplify") << "SmtEnginePrivate::simplify(): performing static learning" << std::endl; + staticLearning(); + + // Remove ITEs + removeITEs(); + } catch(TypeCheckingExceptionPrivate& tcep) { // Calls to this function should have already weeded out any // typechecking exceptions via (e.g.) ensureBoolean(). But a @@ -624,75 +658,46 @@ Node SmtEnginePrivate::preprocess(TNode in) throw(AssertionException) { } Result SmtEngine::check() { - Trace("smt") << "SMT check()" << endl; + Debug("smt") << "SmtEngine::check()" << endl; // make sure the prop layer has all assertions - d_private->pushAssertions(); + Debug("smt") << "SmtEngine::check(): processing assertion" << endl; + d_private->processAssertions(); + Debug("smt") << "SmtEngine::check(): running check" << endl; return d_propEngine->checkSat(); } Result SmtEngine::quickCheck() { - Trace("smt") << "SMT quickCheck()" << endl; + Debug("smt") << "SMT quickCheck()" << endl; return Result(Result::VALIDITY_UNKNOWN, Result::REQUIRES_FULL_CHECK); } -void SmtEnginePrivate::adjustAssertions(bool purge) { - - // If the "purge" argument is true, we ignore the mode and push all - // assertions out to the propositional layer (by pretending we're in - // INCREMENTAL mode). - - Options::SimplificationMode mode = - purge ? Options::INCREMENTAL_MODE : Options::current()->simplificationMode; - - Trace("smt") << "SMT processing assertion lists in " << mode << " mode" << endl; +void SmtEnginePrivate::processAssertions() { - if(mode == Options::BATCH_MODE) { - // nothing to do in batch mode until pushAssertions() is called - } else if(mode == Options::INCREMENTAL_LAZY_SAT_MODE || - mode == Options::INCREMENTAL_MODE) { - // make sure d_assertionsToSimplify is cleared out, and everything - // is on d_assertionsToPushToSat - - for(vector<Node>::iterator i = d_assertionsToSimplify.begin(), - i_end = d_assertionsToSimplify.end(); - i != i_end; - ++i) { - Trace("smt") << "SMT simplifying " << *i << endl; - d_assertionsToPushToSat.push_back(this->simplify(*i)); - } - d_assertionsToSimplify.clear(); + Debug("smt") << "SmtEnginePrivate::processAssertions()" << endl; - if(mode == Options::INCREMENTAL_MODE) { - // make sure the d_assertionsToPushToSat queue is also cleared out + // Simplify the assertions + simplifyAssertions(); - for(vector<Node>::iterator i = d_assertionsToPushToSat.begin(), - i_end = d_assertionsToPushToSat.end(); - i != i_end; - ++i) { - Trace("smt") << "SMT preprocessing " << *i << endl; - Node n = this->preprocess(*i); - Trace("smt") << "SMT pushing to MiniSat " << n << endl; - - Chat() << "Pushing to MiniSat: " << n << endl; - d_smt.d_propEngine->assertFormula(n); - } - d_assertionsToPushToSat.clear(); - } - } else { - Unhandled(mode); + // Push the formula to SAT + for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) { + d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]); } + d_assertionsToCheck.clear(); } -void SmtEnginePrivate::addFormula(TNode n) - throw(NoSuchFunctionException, AssertionException) { +void SmtEnginePrivate::addFormula(TNode n) throw(NoSuchFunctionException, AssertionException) { + + Debug("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl; - Trace("smt") << "push_back assertion " << n << endl; - d_smt.d_haveAdditions = true; + // Add the normalized formula to the queue + d_assertionsToPreprocess.push_back(theory::Rewriter::rewrite(n)); - d_assertionsToSimplify.push_back(n); - adjustAssertions(); + // If the mode of processing is incremental prepreocess and assert immediately + if (Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL) { + processAssertions(); + } } void SmtEngine::ensureBoolean(const BoolExpr& e) { @@ -709,30 +714,50 @@ void SmtEngine::ensureBoolean(const BoolExpr& e) { } Result SmtEngine::checkSat(const BoolExpr& e) { + Assert(e.getExprManager() == d_exprManager); + NodeManagerScope nms(d_nodeManager); - Trace("smt") << "SMT checkSat(" << e << ")" << endl; + + Debug("smt") << "SmtEngine::checkSat(" << e << ")" << endl; + if(d_queryMade && !Options::current()->incrementalSolving) { - throw ModalException("Cannot make multiple queries unless " - "incremental solving is enabled " - "(try --incremental)"); + throw ModalException("Cannot make multiple queries unless incremental solving is enabled (try --incremental)"); } - d_queryMade = true; - ensureBoolean(e);// ensure expr is type-checked at this point + + // Enuser that the expression is Boolean + ensureBoolean(e); + + // Push the context internalPush(); + + // Add the + d_queryMade = true; + + // Add the formula + d_problemExtended = true; d_private->addFormula(e.getNode()); + + // Run the check Result r = check().asSatisfiabilityResult(); + + // Pop the context internalPop(); + + // Remember the status d_status = r; - d_haveAdditions = false; - Trace("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; + + d_problemExtended = false; + + Debug("smt") << "SmtEngine::checkSat(" << e << ") => " << r << endl; + return r; } Result SmtEngine::query(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); - Trace("smt") << "SMT query(" << e << ")" << endl; + Debug("smt") << "SMT query(" << e << ")" << endl; if(d_queryMade && !Options::current()->incrementalSolving) { throw ModalException("Cannot make multiple queries unless " "incremental solving is enabled " @@ -745,16 +770,16 @@ Result SmtEngine::query(const BoolExpr& e) { Result r = check().asValidityResult(); internalPop(); d_status = r; - d_haveAdditions = false; - Trace("smt") << "SMT query(" << e << ") ==> " << r << endl; + d_problemExtended = 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); - Trace("smt") << "SMT assertFormula(" << e << ")" << endl; - ensureBoolean(e);// type check node + Debug("smt") << "SmtEngine::assertFormula(" << e << ")" << endl; + ensureBoolean(e); if(d_assertionList != NULL) { d_assertionList->push_back(e); } @@ -768,8 +793,8 @@ Expr SmtEngine::simplify(const Expr& e) { if( Options::current()->typeChecking ) { e.getType(true);// ensure expr is type-checked at this point } - Trace("smt") << "SMT simplify(" << e << ")" << endl; - return BooleanSimplification::simplify(d_private->simplify(e, true)).toExpr(); + Debug("smt") << "SMT simplify(" << e << ")" << endl; + return d_private->applySubstitutions(e).toExpr(); } Expr SmtEngine::getValue(const Expr& e) @@ -777,7 +802,7 @@ Expr SmtEngine::getValue(const Expr& e) Assert(e.getExprManager() == d_exprManager); NodeManagerScope nms(d_nodeManager); Type type = e.getType(Options::current()->typeChecking);// ensure expr is type-checked at this point - Trace("smt") << "SMT getValue(" << e << ")" << endl; + Debug("smt") << "SMT getValue(" << e << ")" << endl; if(!Options::current()->produceModels) { const char* msg = "Cannot get value when produce-models options is off."; @@ -785,7 +810,7 @@ Expr SmtEngine::getValue(const Expr& e) } if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::SAT || - d_haveAdditions) { + d_problemExtended) { const char* msg = "Cannot get value unless immediately proceded by SAT/INVALID response."; throw ModalException(msg); @@ -797,14 +822,14 @@ Expr SmtEngine::getValue(const Expr& e) throw ModalException(msg); } - Node eNode = e.getNode(); - Node n = d_private->preprocess(eNode);// theory rewriting + // Normalize for the theories + Node n = theory::Rewriter::rewrite(e.getNode()); - Trace("smt") << "--- getting value of " << n << endl; + Debug("smt") << "--- getting value of " << n << endl; Node resultNode = d_theoryEngine->getValue(n); // type-check the result we got - Assert(resultNode.isNull() || resultNode.getType() == eNode.getType()); + Assert(resultNode.isNull() || resultNode.getType() == n.getType()); return Expr(d_exprManager, new Node(resultNode)); } @@ -836,7 +861,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { } SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { - Trace("smt") << "SMT getAssignment()" << endl; + Debug("smt") << "SMT getAssignment()" << endl; if(!Options::current()->produceAssignments) { const char* msg = "Cannot get the current assignment when " @@ -845,7 +870,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { } if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::SAT || - d_haveAdditions) { + d_problemExtended) { const char* msg = "Cannot get value unless immediately proceded by SAT/INVALID response."; throw ModalException(msg); @@ -864,9 +889,10 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { ++i) { Assert((*i).getType() == boolType); - Node n = d_private->preprocess(*i);// theory rewriting + // Normalize + Node n = theory::Rewriter::rewrite(*i); - Trace("smt") << "--- getting value of " << n << endl; + Debug("smt") << "--- getting value of " << n << endl; Node resultNode = d_theoryEngine->getValue(n); // type-check the result we got @@ -889,7 +915,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { vector<Expr> SmtEngine::getAssertions() throw(ModalException, AssertionException) { NodeManagerScope nms(d_nodeManager); - Trace("smt") << "SMT getAssertions()" << endl; + Debug("smt") << "SMT getAssertions()" << endl; if(!Options::current()->interactive) { const char* msg = "Cannot query the current assertion list when not in interactive mode."; @@ -901,7 +927,7 @@ vector<Expr> SmtEngine::getAssertions() void SmtEngine::push() { NodeManagerScope nms(d_nodeManager); - Trace("smt") << "SMT push()" << endl; + Debug("smt") << "SMT push()" << endl; if(!Options::current()->incrementalSolving) { throw ModalException("Cannot push when not solving incrementally (use --incremental)"); } @@ -913,7 +939,7 @@ void SmtEngine::push() { void SmtEngine::pop() { NodeManagerScope nms(d_nodeManager); - Trace("smt") << "SMT pop()" << endl; + Debug("smt") << "SMT pop()" << endl; if(!Options::current()->incrementalSolving) { throw ModalException("Cannot pop when not solving incrementally (use --incremental)"); } @@ -930,13 +956,15 @@ void SmtEngine::pop() { } void SmtEngine::internalPop() { - Trace("smt") << "internalPop()" << endl; + Debug("smt") << "internalPop()" << endl; d_propEngine->pop(); d_userContext->pop(); } void SmtEngine::internalPush() { - Trace("smt") << "internalPush()" << endl; + Debug("smt") << "internalPush()" << endl; + // TODO: this is the right thing to do, but needs serious thinking to keep completeness + // d_private->processAssertions(); d_userContext->push(); d_propEngine->push(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 38c064492..81bd5cb47 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -132,7 +132,7 @@ class CVC4_PUBLIC SmtEngine { * since the last checkSat/query (and therefore we're not responsible * for an assignment). */ - bool d_haveAdditions; + bool d_problemExtended; /** * Whether or not a query() or checkSat() has already been made through diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index d720d5136..9e31bd7a3 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -24,6 +24,7 @@ libtheory_la_SOURCES = \ rewriter_attributes.h \ rewriter.cpp \ substitutions.h \ + substitutions.cpp \ valuation.h \ valuation.cpp diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index bc8604e85..d2ecaffe4 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -234,6 +234,7 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ Assert(isAtom(atom)); + NodeManager* currNM = NodeManager::currentNM(); if(atom.getKind() == kind::EQUAL) { @@ -244,7 +245,7 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){ Node reduction = atom; - if(atom[1].getMetaKind() != kind::metakind::CONSTANT){ + if(atom[1].getMetaKind() != kind::metakind::CONSTANT) { // left |><| right TNode left = atom[0]; TNode right = atom[1]; diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index 315c6ce94..77a89b54b 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -112,7 +112,7 @@ void ArithStaticLearner::clear(){ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet& defTrue){ - Debug("arith::static") << "===================== looking at" << n << endl; + Debug("arith::static") << "===================== looking at " << n << endl; switch(n.getKind()){ case ITE: @@ -121,8 +121,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet iteMinMax(n, learned); } - if((n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER) && - (n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER)) { + if((d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) || + (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end())) { iteConstant(n, learned); } break; @@ -145,6 +145,12 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet } } break; + case CONST_RATIONAL: + case CONST_INTEGER: + // Mark constants as minmax + d_minMap[n] = coerceToRational(n); + d_maxMap[n] = coerceToRational(n); + break; default: // Do nothing break; } @@ -198,19 +204,42 @@ void ArithStaticLearner::iteMinMax(TNode n, NodeBuilder<>& learned){ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){ Assert(n.getKind() == ITE); - Assert(n[1].getKind() == CONST_RATIONAL || n[1].getKind() == CONST_INTEGER ); - Assert(n[2].getKind() == CONST_RATIONAL || n[2].getKind() == CONST_INTEGER ); - Rational t = coerceToRational(n[1]); - Rational e = coerceToRational(n[2]); - TNode min = (t <= e) ? n[1] : n[2]; - TNode max = (t >= e) ? n[1] : n[2]; + Debug("arith::static") << "iteConstant(" << n << ")" << endl; - Node nGeqMin = NodeBuilder<2>(GEQ) << n << min; - Node nLeqMax = NodeBuilder<2>(LEQ) << n << max; - Debug("arith::static") << n << " iteConstant" << nGeqMin << nLeqMax << endl; - learned << nGeqMin << nLeqMax; - ++(d_statistics.d_iteConstantApplications); + if (d_minMap.find(n[1]) != d_minMap.end() && d_minMap.find(n[2]) != d_minMap.end()) { + DeltaRational min = std::min(d_minMap[n[1]], d_minMap[n[2]]); + NodeToMinMaxMap::iterator minFind = d_minMap.find(n); + if (minFind == d_minMap.end() || minFind->second < min) { + d_minMap[n] = min; + Node nGeqMin; + if (min.getInfinitesimalPart() == 0) { + nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart()); + } else { + nGeqMin = NodeBuilder<2>(kind::GT) << n << mkRationalNode(min.getNoninfinitesimalPart()); + } + learned << nGeqMin; + Debug("arith::static") << n << " iteConstant" << nGeqMin << endl; + ++(d_statistics.d_iteConstantApplications); + } + } + + if (d_maxMap.find(n[1]) != d_maxMap.end() && d_maxMap.find(n[2]) != d_maxMap.end()) { + DeltaRational max = std::max(d_maxMap[n[1]], d_maxMap[n[2]]); + NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n); + if (maxFind == d_maxMap.end() || maxFind->second > max) { + d_maxMap[n] = max; + Node nLeqMax; + if (max.getInfinitesimalPart() == 0) { + nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart()); + } else { + nLeqMax = NodeBuilder<2>(kind::LT) << n << mkRationalNode(max.getNoninfinitesimalPart()); + } + learned << nLeqMax; + Debug("arith::static") << n << " iteConstant" << nLeqMax << endl; + ++(d_statistics.d_iteConstantApplications); + } + } } @@ -311,3 +340,34 @@ void ArithStaticLearner::miplibTrick(TNode var, set<Rational>& values, NodeBuild learned << excludedMiddle; } } + +void ArithStaticLearner::addBound(TNode n) { + + NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]); + NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n[0]); + + Rational constant = coerceToRational(n[1]); + DeltaRational bound = constant; + + switch(n.getKind()) { + case kind::LT: + bound = DeltaRational(constant, -1); + case kind::LEQ: + if (maxFind == d_maxMap.end() || maxFind->second > bound) { + d_maxMap[n[0]] = bound; + Debug("arith::static") << "adding bound " << n << endl; + } + break; + case kind::GT: + bound = DeltaRational(constant, 1); + case kind::GEQ: + if (minFind == d_minMap.end() || minFind->second < bound) { + d_minMap[n[0]] = bound; + Debug("arith::static") << "adding bound " << n << endl; + } + break; + default: + // nothing else + break; + } +} diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index f2405cd5c..0ed9cbe85 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -44,10 +44,19 @@ private: VarToNodeSetMap d_miplibTrick; std::list<TNode> d_miplibTrickKeys; + /** + * Map from a node to it's minimum and maximum. + */ + typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap; + NodeToMinMaxMap d_minMap; + NodeToMinMaxMap d_maxMap; + public: ArithStaticLearner(); void staticLearning(TNode n, NodeBuilder<>& learned); + void addBound(TNode n); + void clear(); private: diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index a4c9f3ce0..34cb4d666 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -130,10 +130,82 @@ TheoryArith::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_restartTimer); } -Node TheoryArith::simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions) { +Node TheoryArith::preprocess(TNode atom) { + if (atom.getKind() == kind::EQUAL) { + Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; + Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; + return Rewriter::rewrite(leq.andNode(geq)); + } else { + return atom; + } +} + +Theory::SolveStatus TheoryArith::solve(TNode in, SubstitutionMap& outSubstitutions) { TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer); - Trace("simplify:arith") << "arith-simplifying: " << in << endl; - return d_valuation.rewrite(in); + Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl; + + // Solve equalities + Rational minConstant = 0; + Node minMonomial; + Node minVar; + unsigned nVars = 0; + if (in.getKind() == kind::EQUAL) { + Assert(in[1].getKind() == kind::CONST_RATIONAL); + // Find the variable with the smallest coefficient + Polynomial p = Polynomial::parsePolynomial(in[0]); + Polynomial::iterator it = p.begin(), it_end = p.end(); + for (; it != it_end; ++ it) { + Monomial m = *it; + // Skip the constant + if (m.isConstant()) continue; + // This is a ''variable'' + nVars ++; + // Skip the non-linear stuff + if (!m.getVarList().singleton()) continue; + // Get the minimal one + Rational constant = m.getConstant().getValue(); + Rational absSconstant = constant > 0 ? constant : -constant; + if (minVar.isNull() || absSconstant < minConstant) { + Node var = m.getVarList().getNode(); + if (var.getKind() == kind::VARIABLE) { + minVar = var; + minMonomial = m.getNode(); + minConstant = constant; + } + } + } + + // Solve for variable + if (!minVar.isNull()) { + // ax + p = c -> (ax + p) -ax - c = -ax + Node eliminateVar = NodeManager::currentNM()->mkNode(kind::MINUS, in[0], minMonomial); + if (in[1].getConst<Rational>() != 0) { + eliminateVar = NodeManager::currentNM()->mkNode(kind::MINUS, eliminateVar, in[1]); + } + // x = (p - ax - c) * -1/a + eliminateVar = NodeManager::currentNM()->mkNode(kind::MULT, eliminateVar, mkRationalNode(- minConstant.inverse())); + // Add the substitution + outSubstitutions.addSubstitution(minVar, Rewriter::rewrite(eliminateVar)); + return SOLVE_STATUS_SOLVED; + } + } + + // If a relation, remember the bound + switch(in.getKind()) { + case kind::LEQ: + case kind::LT: + case kind::GEQ: + case kind::GT: + if (in[0].getKind() == kind::VARIABLE) { + learner.addBound(in); + } + break; + default: + // Do nothing + break; + } + + return SOLVE_STATUS_UNSOLVED; } void TheoryArith::staticLearning(TNode n, NodeBuilder<>& learned) { diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 241ef8075..255e2a304 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -152,7 +152,8 @@ public: void presolve(); void notifyRestart(); - Node simplify(TNode in, std::vector< std::pair<Node, Node> >& outSubstitutions); + SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions); + Node preprocess(TNode atom); void staticLearning(TNode in, NodeBuilder<>& learned); std::string identify() const { return std::string("TheoryArith"); } diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index e5055c164..fd44ec13b 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -19,6 +19,7 @@ #include "theory/booleans/circuit_propagator.h" #include "util/utility.h" +#include <stack> #include <vector> #include <algorithm> @@ -28,353 +29,363 @@ namespace CVC4 { namespace theory { namespace booleans { -void CircuitPropagator::propagateBackward(TNode in, bool polarity, vector<TNode>& changed) { - if(!isPropagatedBackward(in)) { - Debug("circuit-prop") << push << "propagateBackward(" << polarity << "): " << in << endl; - setPropagatedBackward(in); - // backward rules - switch(Kind k = in.getKind()) { +void CircuitPropagator::assert(TNode assertion) +{ + if (assertion.getKind() == kind::AND) { + for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) { + assert(assertion[i]); + } + } else { + // Analyze the assertion for back-edges and all that + computeBackEdges(assertion); + // Assign the given assertion to true + assignAndEnqueue(assertion, true); + } +} + +void CircuitPropagator::computeBackEdges(TNode node) { + + Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" << endl; + + // Vector of nodes to visit + vector<TNode> toVisit; + + // Start with the top node + if (d_seen.find(node) == d_seen.end()) { + toVisit.push_back(node); + d_seen.insert(node); + } + + // Initialize the back-edges for the root, so we don't have a special case + d_backEdges[node]; + + // Go through the visit list + for (unsigned i = 0; i < toVisit.size(); ++ i) { + // Node we need to visit + TNode current = toVisit[i]; + Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(): processing " << current << endl; + Assert(d_seen.find(current) != d_seen.end()); + + // If this not an atom visit all the children and compute the back edges + if (Theory::theoryOf(current) == THEORY_BOOL) { + for (unsigned child = 0, child_end = current.getNumChildren(); child < child_end; ++ child) { + TNode childNode = current[child]; + // Add the back edge + d_backEdges[childNode].push_back(current); + // Add to the queue if not seen yet + if (d_seen.find(childNode) == d_seen.end()) { + toVisit.push_back(childNode); + d_seen.insert(childNode); + } + } + } + } +} + +void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) { + + Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl; + + // backward rules + switch(parent.getKind()) { + case kind::AND: + if (parentAssignment) { + // AND = TRUE: forall children c, assign(c = TRUE) + for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) { + assignAndEnqueue(*i, true); + } + } else { + // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) + TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + if (holdout != parent.end()) { + assignAndEnqueue(*holdout, false); + } + } + break; + case kind::OR: + if (parentAssignment) { + // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) + TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + if (holdout != parent.end()) { + assignAndEnqueue(*holdout, true); + } + } else { + // OR = FALSE: forall children c, assign(c = FALSE) + for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) { + assignAndEnqueue(*i, false); + } + } + break; + case kind::NOT: + // NOT = b: assign(c = !b) + assignAndEnqueue(parent[0], !parentAssignment); + break; + case kind::ITE: + if (isAssignedTo(parent[0], true)) { + // ITE c x y = v: if c is assigned and TRUE, assign(x = v) + assignAndEnqueue(parent[1], parentAssignment); + } else if (isAssignedTo(parent[0], false)) { + // ITE c x y = v: if c is assigned and FALSE, assign(y = v) + assignAndEnqueue(parent[2], parentAssignment); + } else if (isAssigned(parent[1]) && isAssigned(parent[2])) { + if (getAssignment(parent[1]) == parentAssignment && getAssignment(parent[2]) != parentAssignment) { + // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE) + assignAndEnqueue(parent[0], true); + } else if (getAssignment(parent[1]) != parentAssignment && getAssignment(parent[2]) == parentAssignment) { + // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE) + assignAndEnqueue(parent[0], false); + } + } + break; + case kind::IFF: + if (parentAssignment) { + // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment]) + if (isAssigned(parent[0])) { + assignAndEnqueue(parent[1], getAssignment(parent[0])); + } else if (isAssigned(parent[1])) { + assignAndEnqueue(parent[0], getAssignment(parent[1])); + } + } else { + // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment]) + if (isAssigned(parent[0])) { + assignAndEnqueue(parent[1], !getAssignment(parent[0])); + } else if (isAssigned(parent[1])) { + assignAndEnqueue(parent[0], !getAssignment(parent[1])); + } + } + break; + case kind::IMPLIES: + if (parentAssignment) { + if (isAssignedTo(parent[0], true)) { + // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE) + assignAndEnqueue(parent[1], true); + } + if (isAssignedTo(parent[1], false)) { + // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) + assignAndEnqueue(parent[0], false); + } + } else { + // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE) + assignAndEnqueue(parent[0], true); + assignAndEnqueue(parent[1], false); + } + break; + case kind::XOR: + if (parentAssignment) { + if (isAssigned(parent[0])) { + // XOR x y = TRUE, and x assigned, assign(y = !assignment(x)) + assignAndEnqueue(parent[1], !getAssignment(parent[0])); + } else if (isAssigned(parent[1])) { + // XOR x y = TRUE, and y assigned, assign(x = !assignment(y)) + assignAndEnqueue(parent[0], !getAssignment(parent[1])); + } + } else { + if (isAssigned(parent[0])) { + // XOR x y = FALSE, and x assigned, assign(y = assignment(x)) + assignAndEnqueue(parent[1], getAssignment(parent[0])); + } else if (isAssigned(parent[1])) { + // XOR x y = FALSE, and y assigned, assign(x = assignment(y)) + assignAndEnqueue(parent[0], getAssignment(parent[1])); + } + } + break; + default: + Unhandled(); + } +} + + +void CircuitPropagator::propagateForward(TNode child, bool childAssignment) { + + // The assignment we have + Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child << ", " << childAssignment << ")" << endl; + + // Get the back any nodes where this is child + const vector<TNode>& parents = d_backEdges.find(child)->second; + + // Go through the parents and see if there is anything to propagate + vector<TNode>::const_iterator parent_it = parents.begin(); + vector<TNode>::const_iterator parent_it_end = parents.end(); + for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) { + // The current parent of the child + TNode parent = *parent_it; + Assert(parent.hasSubterm(child)); + + // Forward rules + switch(parent.getKind()) { case kind::AND: - if(polarity) { - // AND = TRUE: forall children c, assign(c = TRUE) - for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) { - Debug("circuit-prop") << "bAND1" << endl; - assign(*i, true, changed); + if (childAssignment) { + TNode::iterator holdout; + holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, true))); + if (holdout == parent.end()) { // all children are assigned TRUE + // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE) + assignAndEnqueue(parent, true); + } else if (isAssignedTo(parent, false)) {// the AND is FALSE + // is the holdout unique ? + TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, true))); + if (other == parent.end()) { // the holdout is unique + // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE) + assignAndEnqueue(*holdout, false); + } } } else { - // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) - TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, true))); - if(holdout != in.end()) { - Debug("circuit-prop") << "bAND2" << endl; - assign(*holdout, false, changed); - } + // AND ...(x=FALSE)...: assign(AND = FALSE) + assignAndEnqueue(parent, false); } break; case kind::OR: - if(polarity) { - // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) - TNode::iterator holdout = find_if_unique(in.begin(), in.end(), not1(IsAssignedTo(*this, false))); - if(holdout != in.end()) { - Debug("circuit-prop") << "bOR1" << endl; - assign(*holdout, true, changed); - } + if (childAssignment) { + // OR ...(x=TRUE)...: assign(OR = TRUE) + assignAndEnqueue(parent, true); } else { - // OR = FALSE: forall children c, assign(c = FALSE) - for(TNode::iterator i = in.begin(), i_end = in.end(); i != i_end; ++i) { - Debug("circuit-prop") << "bOR2" << endl; - assign(*i, false, changed); + TNode::iterator holdout; + holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, false))); + if (holdout == parent.end()) { // all children are assigned FALSE + // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE) + assignAndEnqueue(parent, false); + } else if (isAssignedTo(parent, true)) {// the OR is TRUE + // is the holdout unique ? + TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, false))); + if (other == parent.end()) { // the holdout is unique + // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE) + assignAndEnqueue(*holdout, true); + } } } break; + case kind::NOT: - // NOT = b: assign(c = !b) - Debug("circuit-prop") << "bNOT" << endl; - assign(in[0], !polarity, changed); + // NOT (x=b): assign(NOT = !b) + assignAndEnqueue(parent, !childAssignment); break; + case kind::ITE: - if(isAssignedTo(in[0], true)) { - // ITE c x y = v: if c is assigned and TRUE, assign(x = v) - Debug("circuit-prop") << "bITE1" << endl; - assign(in[1], polarity, changed); - } else if(isAssignedTo(in[0], false)) { - // ITE c x y = v: if c is assigned and FALSE, assign(y = v) - Debug("circuit-prop") << "bITE2" << endl; - assign(in[2], polarity, changed); - } else if(isAssigned(in[1]) && isAssigned(in[2])) { - if(assignment(in[1]) == polarity && assignment(in[2]) != polarity) { - // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE) - Debug("circuit-prop") << "bITE3" << endl; - assign(in[0], true, changed); - } else if(assignment(in[1]) == !polarity && assignment(in[2]) == polarity) { - // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE) - Debug("circuit-prop") << "bITE4" << endl; - assign(in[0], true, changed); + if (child == parent[0]) { + if (childAssignment) { + if (isAssigned(parent[1])) { + // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment) + assignAndEnqueue(parent, getAssignment(parent[1])); + } + } else { + if (isAssigned(parent[2])) { + // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment) + assignAndEnqueue(parent, getAssignment(parent[2])); + } + } + } + if (child == parent[1]) { + if (isAssignedTo(parent[0], true)) { + // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v) + assignAndEnqueue(parent, childAssignment); + } + } + if (child == parent[2]) { + Assert(child == parent[2]); + if (isAssignedTo(parent[0], false)) { + // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v) + assignAndEnqueue(parent, childAssignment); } } break; case kind::IFF: - if(polarity) { - // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment]) - if(isAssigned(in[0])) { - assign(in[1], assignment(in[0]), changed); - Debug("circuit-prop") << "bIFF1" << endl; - } else if(isAssigned(in[1])) { - Debug("circuit-prop") << "bIFF2" << endl; - assign(in[0], assignment(in[1]), changed); - } + if (isAssigned(parent[0]) && isAssigned(parent[1])) { + // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment)) + assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1])); } else { - // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment]) - if(isAssigned(in[0])) { - Debug("circuit-prop") << "bIFF3" << endl; - assign(in[1], !assignment(in[0]), changed); - } else if(isAssigned(in[1])) { - Debug("circuit-prop") << "bIFF4" << endl; - assign(in[0], !assignment(in[1]), changed); + if (isAssigned(parent)) { + if (child == parent[0]) { + if (getAssignment(parent)) { + // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b) + assignAndEnqueue(parent[1], childAssignment); + } else { + // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b) + assignAndEnqueue(parent[1], !childAssignment); + } + } else { + Assert(child == parent[1]); + if (getAssignment(parent)) { + // IFF x y = b: if IFF is assigned to TRUE, assign(x = b) + assignAndEnqueue(parent[0], childAssignment); + } else { + // IFF x y = b y: if IFF is assigned to TRUE, assign(x = !b) + assignAndEnqueue(parent[0], !childAssignment); + } + } } } break; case kind::IMPLIES: - if(polarity) { - if(isAssignedTo(in[0], true)) { - // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE) - Debug("circuit-prop") << "bIMPLIES1" << endl; - assign(in[1], true, changed); + if (isAssigned(parent[0]) && isAssigned(parent[1])) { + // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2)) + assignAndEnqueue(parent, !getAssignment(parent[0]) || getAssignment(parent[1])); + } else { + if (child == parent[0] && childAssignment && isAssignedTo(parent, true)) { + // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE) + assignAndEnqueue(parent[1], true); } - if(isAssignedTo(in[1], false)) { - // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) - Debug("circuit-prop") << "bIMPLIES2" << endl; - assign(in[0], false, changed); + if (child == parent[1] && !childAssignment && isAssignedTo(parent, true)) { + // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE) + assignAndEnqueue(parent[0], false); } - } else { - // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE) - Debug("circuit-prop") << "bIMPLIES3" << endl; - assign(in[0], true, changed); - assign(in[1], false, changed); + // Note that IMPLIES == FALSE doesn't need any cases here + // because if that assignment has been done, we've already + // propagated all the children (in back-propagation). } break; case kind::XOR: - if(polarity) { - if(isAssigned(in[0])) { - // XOR x y = TRUE, and x assigned, assign(y = !assignment(x)) - Debug("circuit-prop") << "bXOR1" << endl; - assign(in[1], !assignment(in[0]), changed); - } else if(isAssigned(in[1])) { - // XOR x y = TRUE, and y assigned, assign(x = !assignment(y)) - Debug("circuit-prop") << "bXOR2" << endl; - assign(in[0], !assignment(in[1]), changed); - } - } else { - if(isAssigned(in[0])) { - // XOR x y = FALSE, and x assigned, assign(y = assignment(x)) - Debug("circuit-prop") << "bXOR3" << endl; - assign(in[1], assignment(in[0]), changed); - } else if(isAssigned(in[1])) { - // XOR x y = FALSE, and y assigned, assign(x = assignment(y)) - Debug("circuit-prop") << "bXOR4" << endl; - assign(in[0], assignment(in[1]), changed); + if (isAssigned(parent)) { + if (child == parent[0]) { + // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR) + assignAndEnqueue(parent[1], childAssignment != getAssignment(parent)); + } else { + Assert(child == parent[1]); + // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR)) + assignAndEnqueue(parent[0], childAssignment != getAssignment(parent)); } } - break; - case kind::CONST_BOOLEAN: - // nothing to do + if (isAssigned(parent[0]) && isAssigned(parent[1])) { + assignAndEnqueue(parent, getAssignment(parent[0]) != getAssignment(parent[1])); + } break; default: - Unhandled(k); + Unhandled(); } - Debug("circuit-prop") << pop; } } +bool CircuitPropagator::propagate() { -void CircuitPropagator::propagateForward(TNode child, bool polarity, vector<TNode>& changed) { - if(!isPropagatedForward(child)) { - IndentedScope(Debug("circuit-prop")); - Debug("circuit-prop") << "propagateForward (" << polarity << "): " << child << endl; - std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>::const_iterator iter = d_backEdges.find(child); - if(d_backEdges.find(child) == d_backEdges.end()) { - Debug("circuit-prop") << "no backedges, must be ROOT?: " << child << endl; - return; - } - const vector<TNode>& uses = (*iter).second; - setPropagatedForward(child); - for(vector<TNode>::const_iterator useIter = uses.begin(), useIter_end = uses.end(); useIter != useIter_end; ++useIter) { - TNode in = *useIter; // this is the outer node - Debug("circuit-prop") << "considering use: " << in << endl; - IndentedScope(Debug("circuit-prop")); - // forward rules - switch(Kind k = in.getKind()) { - case kind::AND: - if(polarity) { - TNode::iterator holdout; - holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, true))); - if(holdout == in.end()) { // all children are assigned TRUE - // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE) - Debug("circuit-prop") << "fAND1" << endl; - assign(in, true, changed); - } else if(isAssignedTo(in, false)) {// the AND is FALSE - // is the holdout unique ? - TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, true))); - if(other == in.end()) { // the holdout is unique - // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE) - Debug("circuit-prop") << "fAND2" << endl; - assign(*holdout, false, changed); - } - } - } else { - // AND ...(x=FALSE)...: assign(AND = FALSE) - Debug("circuit-prop") << "fAND3" << endl; - assign(in, false, changed); - } - break; - case kind::OR: - if(polarity) { - // OR ...(x=TRUE)...: assign(OR = TRUE) - Debug("circuit-prop") << "fOR1" << endl; - assign(in, true, changed); - } else { - TNode::iterator holdout; - holdout = find_if(in.begin(), in.end(), not1(IsAssignedTo(*this, false))); - if(holdout == in.end()) { // all children are assigned FALSE - // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE) - Debug("circuit-prop") << "fOR2" << endl; - assign(in, false, changed); - } else if(isAssignedTo(in, true)) {// the OR is TRUE - // is the holdout unique ? - TNode::iterator other = find_if(holdout, in.end(), not1(IsAssignedTo(*this, false))); - if(other == in.end()) { // the holdout is unique - // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE) - Debug("circuit-prop") << "fOR3" << endl; - assign(*holdout, true, changed); - } - } - } - break; - - case kind::NOT: - // NOT (x=b): assign(NOT = !b) - Debug("circuit-prop") << "fNOT" << endl; - assign(in, !polarity, changed); - break; - case kind::ITE: - if(child == in[0]) { - if(polarity) { - if(isAssigned(in[1])) { - // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment) - Debug("circuit-prop") << "fITE1" << endl; - assign(in, assignment(in[1]), changed); - } - } else { - if(isAssigned(in[2])) { - // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment) - Debug("circuit-prop") << "fITE2" << endl; - assign(in, assignment(in[2]), changed); - } - } - } else if(child == in[1]) { - if(isAssignedTo(in[0], true)) { - // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v) - Debug("circuit-prop") << "fITE3" << endl; - assign(in, assignment(in[1]), changed); - } - } else { - Assert(child == in[2]); - if(isAssignedTo(in[0], false)) { - // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v) - Debug("circuit-prop") << "fITE4" << endl; - assign(in, assignment(in[2]), changed); - } - } - break; - case kind::IFF: - if(child == in[0]) { - if(isAssigned(in[1])) { - // IFF (x=b) y: if y is assigned, assign(IFF = (x.assignment <=> y.assignment)) - Debug("circuit-prop") << "fIFF1" << endl; - assign(in, assignment(in[0]) == assignment(in[1]), changed); - } else if(isAssigned(in)) { - // IFF (x=b) y: if IFF is assigned, assign(y = (b <=> IFF.assignment)) - Debug("circuit-prop") << "fIFF2" << endl; - assign(in[1], polarity == assignment(in), changed); - } - } else { - Assert(child == in[1]); - if(isAssigned(in[0])) { - // IFF x (y=b): if x is assigned, assign(IFF = (x.assignment <=> y.assignment)) - Debug("circuit-prop") << "fIFF3" << endl; - assign(in, assignment(in[0]) == assignment(in[1]), changed); - } else if(isAssigned(in)) { - // IFF x (y=b): if IFF is assigned, assign(x = (b <=> IFF.assignment)) - Debug("circuit-prop") << "fIFF4" << endl; - assign(in[0], polarity == assignment(in), changed); - } - } - break; - case kind::IMPLIES: - if(isAssigned(in[0]) && isAssigned(in[1])) { - // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2)) - assign(in, !assignment(in[0]) || assignment(in[1]), changed); - Debug("circuit-prop") << "fIMPLIES1" << endl; - } else { - if(child == in[0] && assignment(in[0]) && isAssignedTo(in, true)) { - // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE) - Debug("circuit-prop") << "fIMPLIES2" << endl; - assign(in[1], true, changed); - } - if(child == in[1] && !assignment(in[1]) && isAssignedTo(in, true)) { - // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE) - Debug("circuit-prop") << "fIMPLIES3" << endl; - assign(in[0], false, changed); - } - // Note that IMPLIES == FALSE doesn't need any cases here - // because if that assignment has been done, we've already - // propagated all the children (in back-propagation). - } - break; - case kind::XOR: - if(isAssigned(in)) { - if(child == in[0]) { - // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR) - Debug("circuit-prop") << "fXOR1" << endl; - assign(in[1], polarity ^ assignment(in), changed); - } else { - Assert(child == in[1]); - // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR)) - Debug("circuit-prop") << "fXOR2" << endl; - assign(in[0], polarity ^ assignment(in), changed); - } - } - if( (child == in[0] && isAssigned(in[1])) || - (child == in[1] && isAssigned(in[0])) ) { - // XOR (x=v) y [with y assigned], assign(XOR = (v ^ assignment(y)) - // XOR x (y=v) [with x assigned], assign(XOR = (assignment(x) ^ v) - Debug("circuit-prop") << "fXOR3" << endl; - assign(in, assignment(in[0]) ^ assignment(in[1]), changed); - } - break; - case kind::CONST_BOOLEAN: - InternalError("Forward-propagating a constant Boolean value makes no sense"); - default: - Unhandled(k); - } - } - } -} + Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl; + for(unsigned i = 0; i < d_propagationQueue.size() && !d_conflict; ++ i) { -bool CircuitPropagator::propagate(TNode in, bool polarity, vector<Node>& newFacts) { - try { - vector<TNode> changed; + // The current node we are propagating + TNode current = d_propagationQueue[i]; + Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " << current << std::endl; + bool assignment = getAssignment(current); + Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl; - Assert(kindToTheoryId(in.getKind()) == THEORY_BOOL); + // Is this an atom + bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.getMetaKind() == kind::metakind::VARIABLE; - Debug("circuit-prop") << "B: " << (polarity ? "" : "~") << in << endl; - propagateBackward(in, polarity, changed); - Debug("circuit-prop") << "F: " << (polarity ? "" : "~") << in << endl; - propagateForward(in, polarity, changed); - - while(!changed.empty()) { - vector<TNode> worklist; - worklist.swap(changed); + // If an atom, add to the list for simplification + if (atom) { + Debug("circuit-prop") << "CircuitPropagator::propagate(): adding to learned: " << (assignment ? (Node)current : current.notNode()) << std::endl; + d_learnedLiterals.push_back(assignment ? (Node)current : current.notNode()); + } - for(vector<TNode>::iterator i = worklist.begin(), i_end = worklist.end(); i != i_end; ++i) { - if(kindToTheoryId((*i).getKind()) != THEORY_BOOL) { - if(assignment(*i)) { - newFacts.push_back(*i); - } else { - newFacts.push_back((*i).notNode()); - } - } else { - Debug("circuit-prop") << "B: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl; - propagateBackward(*i, assignment(*i), changed); - Debug("circuit-prop") << "F: " << (isAssignedTo(*i, true) ? "" : "~") << *i << endl; - propagateForward(*i, assignment(*i), changed); - } - } + // Propagate this value to the children (if not an atom or a constant) + if (d_backwardPropagation && !atom && !current.isConst()) { + propagateBackward(current, assignment); + } + // Propagate this value to the parents + if (d_forwardPropagation) { + propagateForward(current, assignment); } - } catch(ConflictException& ce) { - return true; } - return false; + + // No conflict + return d_conflict; } }/* CVC4::theory::booleans namespace */ diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index f9efc20af..73a5be0f8 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -33,6 +33,7 @@ namespace CVC4 { namespace theory { namespace booleans { + /** * The main purpose of the CircuitPropagator class is to maintain the * state of the circuit for subsequent calls to propagate(), so that @@ -40,104 +41,103 @@ namespace booleans { * circuit isn't propagated twice, etc. */ class CircuitPropagator { - const std::vector<TNode>& d_atoms; - const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& d_backEdges; - class ConflictException : Exception { - public: - ConflictException() : Exception("A conflict was found in the CircuitPropagator") { - } - };/* class ConflictException */ +public: + + /** + * Value of a particular node + */ + enum AssignmentStatus { + /** Node is currently unassigned */ + UNASSIGNED = 0, + /** Node is assigned to true */ + ASSIGNED_TO_TRUE, + /** Node is assigned to false */ + ASSIGNED_TO_FALSE, + }; + + /** Invert a set value */ + static inline AssignmentStatus neg(AssignmentStatus value) { + Assert(value != UNASSIGNED); + if (value == ASSIGNED_TO_TRUE) return ASSIGNED_TO_FALSE; + else return ASSIGNED_TO_TRUE; + } + +private: + + /** Back edges from nodes to where they are used */ + typedef std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction> BackEdgesMap; + BackEdgesMap d_backEdges; - enum { - ASSIGNMENT_MASK = 1, - IS_ASSIGNED_MASK = 2, - IS_PROPAGATED_FORWARD_MASK = 4, - IS_PROPAGATED_BACKWARD_MASK = 8 - };/* enum */ + /** The propagation queue */ + std::vector<TNode> d_propagationQueue; + + /** Are we in conflict */ + bool d_conflict; + + /** Map of substitutions */ + std::vector<Node>& d_learnedLiterals; + + /** Nodes that have been attached already (computed forward edges for) */ + // All the nodes we've visited so far + std::hash_set<TNode, TNodeHashFunction> d_seen; /** - * For each Node we care about, we have a 4-bit state: - * Bit 0 (ASSIGNMENT_MASK) is set to indicate the current assignment - * Bit 1 (IS_ASSIGNED_MASK) is set if a value is assigned - * Bit 2 (IS_PROPAGATED_FORWARD) is set to indicate it's been propagated forward - * Bit 2 (IS_PROPAGATED_BACKWARD) is set to indicate it's been propagated backward + * Assignment status of each node. */ - std::hash_map<TNode, unsigned, TNodeHashFunction> d_state; - - /** Assign Node in circuit with the value and add it to the changed vector; note conflicts. */ - void assign(TNode n, bool b, std::vector<TNode>& changed) { - if(n.getMetaKind() == kind::metakind::CONSTANT) { - bool c = n.getConst<bool>(); - if(c != b) { - Debug("circuit-prop") << "while assigning(" << b << "): " << n - << ", constant conflict" << std::endl; - throw ConflictException(); - } else { - Debug("circuit-prop") << "assigning(" << b << "): " << n - << ", nothing to do" << std::endl; + typedef std::hash_map<TNode, AssignmentStatus, TNodeHashFunction> AssignmentMap; + AssignmentMap d_state; + + /** + * Assign Node in circuit with the value and add it to the queue; note conflicts. + */ + void assignAndEnqueue(TNode n, bool value) { + + Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl; + + if (n.getKind() == kind::CONST_BOOLEAN) { + // Assigning a constant to the opposite value is dumb + if (value != n.getConst<bool>()) { + d_conflict = true; + return; } - return; } - unsigned& state = d_state[n]; - if((state & IS_ASSIGNED_MASK) != 0) {// if assigned already - if(((state & ASSIGNMENT_MASK) != 0) != b) {// conflict - Debug("circuit-prop") << "while assigning(" << b << "): " << n - << ", got conflicting assignment(" << assignment(n) << "): " - << n << std::endl; - throw ConflictException(); - } else { - Debug("circuit-prop") << "already assigned(" << b << "): " << n << std::endl; + + // Get the current assignement + AssignmentStatus state = d_state[n]; + + if(state != UNASSIGNED) { + // If the node is already assigned we might have a conflict + if(value != (state == ASSIGNED_TO_TRUE)) { + d_conflict = true; } - } else {// if unassigned - Debug("circuit-prop") << "assigning(" << b << "): " << n << std::endl; - state |= IS_ASSIGNED_MASK | (b ? ASSIGNMENT_MASK : 0); - changed.push_back(n); + } else { + // If unassigned, mark it as assigned + d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE; + // Add for further propagation + d_propagationQueue.push_back(n); } } - /** True iff Node is assigned in circuit (either true or false). */ - bool isAssigned(TNode n) { - return (d_state[n] & IS_ASSIGNED_MASK) != 0; - } + /** True iff Node is assigned in circuit (either true or false). */ bool isAssigned(TNode n) const { - std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n); - return i != d_state.end() && ((*i).second & IS_ASSIGNED_MASK) != 0; - } - /** True iff Node is assigned in circuit with the value given. */ - bool isAssignedTo(TNode n, bool b) { - unsigned state = d_state[n]; - return (state & IS_ASSIGNED_MASK) && - (state & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0); + AssignmentMap::const_iterator i = d_state.find(n); + return i != d_state.end() && ((*i).second != UNASSIGNED); } - /** True iff Node is assigned in circuit (either true or false). */ - bool isAssignedTo(TNode n, bool b) const { - std::hash_map<TNode, unsigned, TNodeHashFunction>::const_iterator i = d_state.find(n); - return i != d_state.end() && - ((*i).second & IS_ASSIGNED_MASK) && - ((*i).second & ASSIGNMENT_MASK) == (b ? ASSIGNMENT_MASK : 0); + + /** True iff Node is assigned to the value. */ + bool isAssignedTo(TNode n, bool value) const { + AssignmentMap::const_iterator i = d_state.find(n); + if (i == d_state.end()) return false; + if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true; + if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true; + return false; } + /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */ - bool assignment(TNode n) { - unsigned state = d_state[n]; - Assert((state & IS_ASSIGNED_MASK) != 0); - return (state & ASSIGNMENT_MASK) != 0; - } - /** Has this node already been propagated forward? */ - bool isPropagatedForward(TNode n) { - return (d_state[n] & IS_PROPAGATED_FORWARD_MASK) != 0; - } - /** Has this node already been propagated backward? */ - bool isPropagatedBackward(TNode n) { - return (d_state[n] & IS_PROPAGATED_BACKWARD_MASK) != 0; - } - /** Mark this node as already having been propagated forward. */ - void setPropagatedForward(TNode n) { - d_state[n] |= IS_PROPAGATED_FORWARD_MASK; - } - /** Mark this node as already having been propagated backward. */ - void setPropagatedBackward(TNode n) { - d_state[n] |= IS_PROPAGATED_BACKWARD_MASK; + bool getAssignment(TNode n) const { + Assert(d_state.find(n) != d_state.end() && d_state.find(n)->second != UNASSIGNED); + return d_state.find(n)->second == ASSIGNED_TO_TRUE; } /** Predicate for use in STL functions. */ @@ -169,33 +169,52 @@ class CircuitPropagator { };/* class IsAssignedTo */ /** - * Propagate new information (in = polarity) forward in circuit to + * Compute the map from nodes to the nodes that use it. + */ + void computeBackEdges(TNode node); + + /** + * Propagate new information forward in circuit to * the parents of "in". */ - void propagateForward(TNode in, bool polarity, std::vector<TNode>& newFacts); + void propagateForward(TNode child, bool assignment); + /** - * Propagate new information (in = polarity) backward in circuit to + * Propagate new information backward in circuit to * the children of "in". */ - void propagateBackward(TNode in, bool polarity, std::vector<TNode>& newFacts); + void propagateBackward(TNode parent, bool assignment); + + /** Whether to perform forward propagation */ + bool d_forwardPropagation; + /** Whether to perform backward propagation */ + bool d_backwardPropagation; + /** Whether to perform expensive propagations */ + bool d_expensivePropagation; public: /** * Construct a new CircuitPropagator with the given atoms and backEdges. */ - CircuitPropagator(const std::vector<TNode>& atoms, const std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction>& backEdges) - : d_atoms(atoms), - d_backEdges(backEdges) { + CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true, bool enableExpensive = true) : + d_conflict(false), + d_learnedLiterals(outLearnedLiterals), + d_forwardPropagation(enableForward), + d_backwardPropagation(enableBackward), + d_expensivePropagation(enableExpensive) + { } + /** Assert for propagation */ + void assert(TNode assertion); + /** - * Propagate new information (in == polarity) through the circuit - * propagator. New information discovered by the propagator are put - * in the (output-only) newFacts vector. + * Propagate through the asserted circuit propagator. New information discovered by the propagator + * are put in the subsitutions vector used in construction. * * @return true iff conflict found */ - bool propagate(TNode in, bool polarity, std::vector<Node>& newFacts) CVC4_WARN_UNUSED_RESULT; + bool propagate() CVC4_WARN_UNUSED_RESULT; };/* class CircuitPropagator */ diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 836022bc2..01185281a 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -97,134 +97,29 @@ Node TheoryBool::getValue(TNode n) { } } -static void -findAtoms(TNode in, vector<TNode>& atoms, - hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) { - Kind k CVC4_UNUSED = in.getKind(); - Assert(kindToTheoryId(k) == THEORY_BOOL); - - stack< pair<TNode, TNode::iterator> > trail; - hash_set<TNode, TNodeHashFunction> seen; - trail.push(make_pair(in, in.begin())); - - while(!trail.empty()) { - pair<TNode, TNode::iterator>& pr = trail.top(); - Debug("simplify") << "looking at: " << pr.first << endl; - if(pr.second == pr.first.end()) { - trail.pop(); - } else { - if(pr.second == pr.first.begin()) { - Debug("simplify") << "first visit: " << pr.first << endl; - // first time we've visited this node? - if(seen.find(pr.first) == seen.end()) { - Debug("simplify") << "+ haven't seen it yet." << endl; - seen.insert(pr.first); - } else { - Debug("simplify") << "+ saw it before." << endl; - trail.pop(); - continue; - } - } - TNode n = *pr.second++; - if(seen.find(n) == seen.end()) { - Debug("simplify") << "back edge " << n << " to " << pr.first << endl; - backEdges[n].push_back(pr.first); - Kind nk = n.getKind(); - if(kindToTheoryId(nk) == THEORY_BOOL) { - trail.push(make_pair(n, n.begin())); - } else { - Debug("simplify") << "atom: " << n << endl; - atoms.push_back(n); - } - } - } - } -} +Theory::SolveStatus TheoryBool::solve(TNode in, SubstitutionMap& outSubstitutions) { -Node TheoryBool::simplify(TNode in, Substitutions& outSubstitutions) { - const unsigned prev = outSubstitutions.size(); - - if(kindToTheoryId(in.getKind()) != THEORY_BOOL) { - Assert(in.getMetaKind() == kind::metakind::VARIABLE && - in.getType().isBoolean()); - return in; + if (in.getKind() == kind::CONST_BOOLEAN && !in.getConst<bool>()) { + // If we get a false literal, we're in conflict + return SOLVE_STATUS_CONFLICT; } - // form back edges and atoms - vector<TNode> atoms; - hash_map<TNode, vector<TNode>, TNodeHashFunction> backEdges; - Debug("simplify") << "finding atoms..." << endl << push; - findAtoms(in, atoms, backEdges); - Debug("simplify") << pop << "done finding atoms..." << endl; - - hash_map<TNode, Node, TNodeHashFunction> simplified; - - vector<Node> newFacts; - CircuitPropagator circuit(atoms, backEdges); - Debug("simplify") << "propagate..." << endl; - if(circuit.propagate(in, true, newFacts)) { - Notice() << "Found a conflict in nonclausal Boolean reasoning" << endl; - return NodeManager::currentNM()->mkConst(false); - } - Debug("simplify") << "done w/ propagate..." << endl; - - for(vector<Node>::iterator i = newFacts.begin(), i_end = newFacts.end(); i != i_end; ++i) { - TNode a = *i; - if(a.getKind() == kind::NOT) { - if(a[0].getMetaKind() == kind::metakind::VARIABLE ) { - Debug("simplify") << "found bool unit ~" << a[0] << "..." << endl; - outSubstitutions.push_back(make_pair(a[0], NodeManager::currentNM()->mkConst(false))); - } else if(kindToTheoryId(a[0].getKind()) != THEORY_BOOL) { - Debug("simplify") << "simplifying: " << a << endl; - simplified[a] = d_valuation.simplify(a, outSubstitutions); - Debug("simplify") << "done simplifying, got: " << simplified[a] << endl; - } + // Add the substitution from the variable to it's value + if (in.getKind() == kind::NOT) { + if (in[0].getKind() == kind::VARIABLE) { + outSubstitutions.addSubstitution(in[0], NodeManager::currentNM()->mkConst<bool>(false)); } else { - if(a.getMetaKind() == kind::metakind::VARIABLE) { - Debug("simplify") << "found bool unit " << a << "..." << endl; - outSubstitutions.push_back(make_pair(a, NodeManager::currentNM()->mkConst(true))); - } else if(kindToTheoryId(a.getKind()) != THEORY_BOOL) { - Debug("simplify") << "simplifying: " << a << endl; - simplified[a] = d_valuation.simplify(a, outSubstitutions); - Debug("simplify") << "done simplifying, got: " << simplified[a] << endl; - } + return SOLVE_STATUS_UNSOLVED; } - } - - Debug("simplify") << "substituting in root..." << endl; - Node n = in.substitute(outSubstitutions.begin(), outSubstitutions.end()); - Debug("simplify") << "got: " << n << endl; - if(Debug.isOn("simplify")) { - Debug("simplify") << "new substitutions:" << endl; - copy(outSubstitutions.begin() + prev, outSubstitutions.end(), - ostream_iterator< pair<TNode, TNode> >(Debug("simplify"), "\n")); - Debug("simplify") << "done." << endl; - } - if(outSubstitutions.size() > prev) { - NodeBuilder<> b(kind::AND); - b << n; - for(Substitutions::iterator i = outSubstitutions.begin() + prev, - i_end = outSubstitutions.end(); - i != i_end; - ++i) { - if((*i).first.getType().isBoolean()) { - if((*i).second.getMetaKind() == kind::metakind::CONSTANT) { - if((*i).second.getConst<bool>()) { - b << (*i).first; - } else { - b << BooleanSimplification::negate((*i).first); - } - } else { - b << (*i).first.iffNode((*i).second); - } - } else { - b << (*i).first.eqNode((*i).second); - } + } else { + if (in.getKind() == kind::VARIABLE) { + outSubstitutions.addSubstitution(in, NodeManager::currentNM()->mkConst<bool>(true)); + } else { + return SOLVE_STATUS_UNSOLVED; } - n = b; } - Debug("simplify") << "final boolean simplification returned: " << n << endl; - return n; + + return SOLVE_STATUS_SOLVED; } diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 40bbd3308..ce9938b10 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -36,7 +36,7 @@ public: Node getValue(TNode n); - Node simplify(TNode in, Substitutions& outSubstitutions); + SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions); std::string identify() const { return std::string("TheoryBool"); } };/* class TheoryBool */ diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index c1be3b906..18aa71667 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -36,7 +36,31 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (n[0].getKind() == kind::NOT) return RewriteResponse(REWRITE_AGAIN, n[0][0]); break; } - case kind::IFF: { + case kind::OR: { + if (n.getNumChildren() == 2) { + if (n[0] == tt || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); + if (n[0] == ff) return RewriteResponse(REWRITE_AGAIN, n[1]); + if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0]); + } + break; + } + case kind::AND: { + if (n.getNumChildren() == 2) { + if (n[0] == ff || n[1] == ff) return RewriteResponse(REWRITE_DONE, ff); + if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); + if (n[1] == tt) return RewriteResponse(REWRITE_AGAIN, n[0]); + } + break; + } + case kind::IMPLIES: { + if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt); + if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff); + if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]); + if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + break; + } + case kind::IFF: + case kind::EQUAL: { // rewrite simple cases of IFF if(n[0] == tt) { // IFF true x @@ -62,10 +86,35 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { } break; } + case kind::XOR: { + // rewrite simple cases of XOR + if(n[0] == tt) { + // XOR true x + return RewriteResponse(REWRITE_AGAIN, n[1].notNode()); + } else if(n[1] == tt) { + // XCR x true + return RewriteResponse(REWRITE_AGAIN, n[0].notNode()); + } else if(n[0] == ff) { + // XOR false x + return RewriteResponse(REWRITE_AGAIN, n[1]); + } else if(n[1] == ff) { + // XOR x false + return RewriteResponse(REWRITE_AGAIN, n[0]); + } else if(n[0] == n[1]) { + // XOR x x + return RewriteResponse(REWRITE_DONE, ff); + } else if(n[0].getKind() == kind::NOT && n[0][0] == n[1]) { + // XOR (NOT x) x + return RewriteResponse(REWRITE_DONE, tt); + } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { + // XOR x (NOT x) + return RewriteResponse(REWRITE_DONE, tt); + } + break; + } case kind::ITE: { // non-Boolean-valued ITEs should have been removed in place of // a variable - Assert(n.getType().isBoolean()); // rewrite simple cases of ITE if(n[0] == tt) { // ITE true x y diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index ddfd2ab59..1c779bd79 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -26,47 +26,6 @@ namespace CVC4 { namespace theory { namespace builtin { -Node TheoryBuiltin::simplify(TNode in, Substitutions& outSubstitutions) { - if(in.getKind() == kind::EQUAL) { - Node lhs = d_valuation.simplify(in[0], outSubstitutions); - Node rhs = d_valuation.simplify(in[1], outSubstitutions); - Node n = lhs.eqNode(rhs); - if( n[0].getMetaKind() == kind::metakind::VARIABLE && - n[1].getMetaKind() == kind::metakind::CONSTANT ) { - Debug("simplify:builtin") << "found new substitution! " - << n[0] << " => " << n[1] << endl; - outSubstitutions.push_back(make_pair(n[0], n[1])); - // with our substitutions we've subsumed the equality - return NodeManager::currentNM()->mkConst(true); - } else if( n[1].getMetaKind() == kind::metakind::VARIABLE && - n[0].getMetaKind() == kind::metakind::CONSTANT ) { - Debug("simplify:builtin") << "found new substitution! " - << n[1] << " => " << n[0] << endl; - outSubstitutions.push_back(make_pair(n[1], n[0])); - // with our substitutions we've subsumed the equality - return NodeManager::currentNM()->mkConst(true); - } - } else if(in.getKind() == kind::NOT && in[0].getKind() == kind::DISTINCT) { - TNode::iterator found = in[0].end(); - for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) { - if((*i).getMetaKind() == kind::metakind::CONSTANT) { - found = i; - break; - } - } - if(found != in[0].end()) { - for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) { - if(i != found) { - outSubstitutions.push_back(make_pair(*i, *found)); - } - } - // with our substitutions we've subsumed the (NOT (DISTINCT...)) - return NodeManager::currentNM()->mkConst(true); - } - } - return in; -} - Node TheoryBuiltin::getValue(TNode n) { switch(n.getKind()) { diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index a97773dce..4e62401ff 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -31,7 +31,6 @@ class TheoryBuiltin : public Theory { public: TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) : Theory(THEORY_BUILTIN, c, out, valuation) {} - Node simplify(TNode in, Substitutions& outSubstitutions); Node getValue(TNode n); std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 8c2b59efa..27fadce0b 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -143,8 +143,6 @@ public: void check(Effort e); - //void presolve() { } - void propagate(Effort e) { } void explain(TNode n); diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp new file mode 100644 index 000000000..8657ed871 --- /dev/null +++ b/src/theory/substitutions.cpp @@ -0,0 +1,165 @@ +/********************* */ +/*! \file substitutions.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A substitution mapping for theory simplification + ** + ** A substitution mapping for theory simplification. + **/ + +#include "theory/substitutions.h" + +using namespace std; + +namespace CVC4 { +namespace theory { + +struct substitution_stack_element { + TNode node; + bool children_added; + substitution_stack_element(TNode node) + : node(node), children_added(false) {} +}; + +Node SubstitutionMap::internalSubstitute(TNode t, NodeMap& substitutionCache) { + + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << std::endl; + + // If nothing to substitute just return the node + if (substitutionCache.empty()) { + return t; + } + + // Do a topological sort of the subexpressions and substitute them + vector<substitution_stack_element> toVisit; + toVisit.push_back((TNode) t); + + while (!toVisit.empty()) + { + // The current node we are processing + substitution_stack_element& stackHead = toVisit.back(); + TNode current = stackHead.node; + + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << std::endl; + + // If node already in the cache we're done, pop from the stack + NodeMap::iterator find = substitutionCache.find(current); + if (find != substitutionCache.end()) { + toVisit.pop_back(); + continue; + } + + // Not yet substituted, so process + if (stackHead.children_added) { + // Children have been processed, so substitute + NodeBuilder<> builder(current.getKind()); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } + for (unsigned i = 0; i < current.getNumChildren(); ++ i) { + Assert(substitutionCache.find(current[i]) != substitutionCache.end()); + builder << substitutionCache[current[i]]; + } + // Mark the substitution and continue + Node result = builder; + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl; + substitutionCache[current] = result; + toVisit.pop_back(); + } else { + // Mark that we have added the children if any + if (current.getNumChildren() > 0) { + stackHead.children_added = true; + // We need to add the children + for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { + TNode childNode = *child_it; + NodeMap::iterator childFind = substitutionCache.find(childNode); + if (childFind == substitutionCache.end()) { + toVisit.push_back(childNode); + } + } + } else { + // No children, so we're done + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << std::endl; + substitutionCache[current] = current; + toVisit.pop_back(); + } + } + } + + // Return the substituted version + return substitutionCache[t]; +} + +void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { + Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl; + Assert(d_substitutions.find(x) == d_substitutions.end()); + + // Temporary substitution cache + NodeMap tempCache; + tempCache[x] = t; + + // Put in the new substitutions into the old ones + NodeMap::iterator it = d_substitutions.begin(); + NodeMap::iterator it_end = d_substitutions.end(); + for(; it != it_end; ++ it) { + it->second = internalSubstitute(it->second, tempCache); + } + + // Put the new substitution in + d_substitutions[x] = t; + + // Also invalidate the cache + if (invalidateCache) { + d_cacheInvalidated = true; + } +} + +bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) { + SubstitutionMap::NodeMap::const_iterator it = substitutions.begin(); + SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end(); + for (; it != it_end; ++ it) { + if (node.hasSubterm(it->first)) { + return false; + } + } + return true; +} + +Node SubstitutionMap::apply(TNode t) { + + Debug("substitution") << "SubstitutionMap::apply(" << t << ")" << std::endl; + + // Setup the cache + if (d_cacheInvalidated) { + d_substitutionCache = d_substitutions; + d_cacheInvalidated = false; + } + + // Perform the substitution + Node result = internalSubstitute(t, d_substitutionCache); + Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl; + + Assert(check(result, d_substitutions)); + + return result; +} + +void SubstitutionMap::print(ostream& out) const { + NodeMap::const_iterator it = d_substitutions.begin(); + NodeMap::const_iterator it_end = d_substitutions.end(); + for (; it != it_end; ++ it) { + out << it->first << " -> " << it->second << endl; + } +} + +} +} diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 32e1599ea..513300a32 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -34,7 +34,59 @@ namespace theory { * Valuation::simplify(). This is in its own header to avoid circular * dependences between those three. */ -typedef std::vector< std::pair<Node, Node> > Substitutions; +class SubstitutionMap { + +public: + + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + +private: + + /** The variables, in order of addition */ + NodeMap d_substitutions; + + /** Cache of the already performed substitutions */ + NodeMap d_substitutionCache; + + /** Has the cache been invalidated */ + bool d_cacheInvalidated; + + /** Internaal method that performs substitution */ + Node internalSubstitute(TNode t, NodeMap& substitutionCache); + +public: + + SubstitutionMap(): d_cacheInvalidated(true) {} + + /** + * Adds a substitution from x to t + */ + void addSubstitution(TNode x, TNode t, bool invalidateCache = true); + + + /** + * Apply the substitutions to the node. + */ + Node apply(TNode t); + + /** + * Apply the substitutions to the node. + */ + Node apply(TNode t) const { + return const_cast<SubstitutionMap*>(this)->apply(t); + } + + /** + * Print to the output stream + */ + void print(std::ostream& out) const; + +}; + +inline std::ostream& operator << (std::ostream& out, const SubstitutionMap& subst) { + subst.print(out); + return out; +} }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index e97e603e5..252d18844 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -141,7 +141,7 @@ protected: d_wasSharedTermFact = false; d_factsHead = d_factsHead + 1; Debug("theory") << "Theory::get() => " << fact - << "(" << d_facts.size() << " left)" << std::endl; + << " (" << d_facts.size() << " left)" << std::endl; d_out->newFact(fact); return fact; } @@ -407,19 +407,43 @@ public: */ virtual void staticLearning(TNode in, NodeBuilder<>& learned) { } + enum SolveStatus { + /** Atom has been solved */ + SOLVE_STATUS_SOLVED, + /** Atom has not been solved */ + SOLVE_STATUS_UNSOLVED, + /** Atom is inconsistent */ + SOLVE_STATUS_CONFLICT + }; + + /** + * Given a literal, add the solved substitutions to the map, if any. + * The method should return true if the literal can be safely removed. + */ + virtual SolveStatus solve(TNode in, SubstitutionMap& outSubstitutions) { + if (in.getKind() == kind::EQUAL) { + if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) { + outSubstitutions.addSubstitution(in[0], in[1]); + return SOLVE_STATUS_SOLVED; + } + if (in[1].getMetaKind() == kind::metakind::VARIABLE && !in[0].hasSubterm(in[1])) { + outSubstitutions.addSubstitution(in[1], in[0]); + } + if (in[0].getMetaKind() == kind::metakind::CONSTANT && in[1].getMetaKind() == kind::metakind::CONSTANT) { + if (in[0] != in[1]) { + return SOLVE_STATUS_CONFLICT; + } + } + } + + return SOLVE_STATUS_UNSOLVED; + } + /** - * Simplify a node in a theory-specific way. The node is a theory - * operation or its negation, or an equality between theory-typed - * terms or its negation. Add to "outSubstitutions" any - * replacements you want to make for the entire subterm; if you add - * [x,y] to the vector, the enclosing Boolean formula (call it - * "phi") will be replaced with (AND phi[x->y] (x = y)). Use - * Valuation::simplify() to simplify subterms (it maintains a cache - * and dispatches to the appropriate theory). + * Given an atom of the theory, that comes from the input formula, this is method can rewrite the atom + * into an equivalent form. This is only called just before an input atom to the engine. */ - virtual Node simplify(TNode in, Substitutions& outSubstitutions) { - return in; - } + virtual Node preprocess(TNode atom) { return atom; } /** * A Theory is called with presolve exactly one time per user @@ -457,6 +481,20 @@ inline std::ostream& operator<<(std::ostream& out, return out << theory.identify(); } +inline std::ostream& operator << (std::ostream& out, theory::Theory::SolveStatus status) { + switch (status) { + case theory::Theory::SOLVE_STATUS_SOLVED: + out << "SOLVE_STATUS_SOLVED"; break; + case theory::Theory::SOLVE_STATUS_UNSOLVED: + out << "SOLVE_STATUS_UNSOLVED"; break; + case theory::Theory::SOLVE_STATUS_CONFLICT: + out << "SOLVE_STATUS_CONFLICT"; break; + default: + Unhandled(); + } + return out; +} + }/* CVC4 namespace */ #endif /* __CVC4__THEORY__THEORY_H */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index db22d8981..fa885590b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -29,6 +29,8 @@ #include "theory/rewriter.h" #include "theory/theory_traits.h" +#include "util/ite_removal.h" + using namespace std; using namespace CVC4; @@ -46,9 +48,6 @@ typedef CVC4::expr::CDAttribute<RegisteredAttrTag, bool> RegisteredAttr; struct PreRegisteredAttrTag {}; typedef expr::Attribute<PreRegisteredAttrTag, bool> PreRegistered; -struct IteRewriteAttrTag {}; -typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr; - }/* CVC4::theory namespace */ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { @@ -125,11 +124,7 @@ void TheoryEngine::EngineOutputChannel::newFact(TNode fact) { // traversing a DAG as a tree and that can really blow up @CB if(! n.getAttribute(RegisteredAttr())) { n.setAttribute(RegisteredAttr(), true); - if (n.getKind() == kind::EQUAL) { - d_engine->theoryOf(n[0])->registerTerm(n); - } else { - d_engine->theoryOf(n)->registerTerm(n); - } + d_engine->theoryOf(n)->registerTerm(n); } } }/* Options::current()->theoryRegistration && !fact.getAttribute(RegisteredAttr()) */ @@ -167,24 +162,13 @@ TheoryEngine::~TheoryEngine() { delete d_sharedTermManager; } -struct preprocess_stack_element { +struct preregister_stack_element { TNode node; bool children_added; - preprocess_stack_element(TNode node) + preregister_stack_element(TNode node) : node(node), children_added(false) {} };/* struct preprocess_stack_element */ -Node TheoryEngine::preprocess(TNode node) { - // Make sure the node is type-checked first (some rewrites depend on - // typechecking having succeeded to be safe). - if(Options::current()->typeChecking) { - node.getType(true); - } - // Remove ITEs and rewrite the node - Node preprocessed = Rewriter::rewrite(removeITEs(node)); - return preprocessed; -} - void TheoryEngine::preRegister(TNode preprocessed) { // If we are pre-registered already we are done if (preprocessed.getAttribute(PreRegistered())) { @@ -192,10 +176,10 @@ void TheoryEngine::preRegister(TNode preprocessed) { } // Do a topological sort of the subexpressions and preregister them - vector<preprocess_stack_element> toVisit; + vector<preregister_stack_element> toVisit; toVisit.push_back((TNode) preprocessed); while (!toVisit.empty()) { - preprocess_stack_element& stackHead = toVisit.back(); + preregister_stack_element& stackHead = toVisit.back(); // The current node we are processing TNode current = stackHead.node; // If we already added all the children its time to register or just pop from the stack @@ -208,22 +192,11 @@ void TheoryEngine::preRegister(TNode preprocessed) { if(d_logic == "QF_AX") { d_theoryTable[theory::THEORY_ARRAY]->preRegisterTerm(current); } else { - TheoryId theoryLHS = Theory::theoryOf(current[0]); + Theory* theory = theoryOf(current); + TheoryId theoryLHS = theory->getId(); Debug("register") << "preregistering " << current << " with " << theoryLHS << std::endl; markActive(theoryLHS); - d_theoryTable[theoryLHS]->preRegisterTerm(current); -// TheoryId theoryRHS = Theory::theoryOf(current[1]); -// if (theoryLHS != theoryRHS) { -// markActive(theoryRHS); -// d_theoryTable[theoryRHS]->preRegisterTerm(current); -// Debug("register") << "preregistering " << current << " with " << theoryRHS << std::endl; -// } -// TheoryId typeTheory = Theory::theoryOf(current[0].getType()); -// if (typeTheory != theoryLHS && typeTheory != theoryRHS) { -// markActive(typeTheory); -// d_theoryTable[typeTheory]->preRegisterTerm(current); -// Debug("register") << "preregistering " << current << " with " << typeTheory << std::endl; -// } + theory->preRegisterTerm(current); } } else { TheoryId theory = Theory::theoryOf(current); @@ -297,68 +270,6 @@ void TheoryEngine::propagate() { CVC4_FOR_EACH_THEORY; } -/* Our goal is to tease out any ITE's sitting under a theory operator. */ -Node TheoryEngine::removeITEs(TNode node) { - Debug("ite") << "removeITEs(" << node << ")" << endl; - - /* The result may be cached already */ - Node cachedRewrite; - NodeManager *nodeManager = NodeManager::currentNM(); - if(nodeManager->getAttribute(node, theory::IteRewriteAttr(), cachedRewrite)) { - Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl; - return cachedRewrite.isNull() ? Node(node) : cachedRewrite; - } - - if(node.getKind() == kind::ITE){ - Assert( node.getNumChildren() == 3 ); - TypeNode nodeType = node.getType(); - if(!nodeType.isBoolean()){ - Node skolem = nodeManager->mkVar(nodeType); - Node newAssertion = - nodeManager->mkNode(kind::ITE, - node[0], - nodeManager->mkNode(kind::EQUAL, skolem, node[1]), - nodeManager->mkNode(kind::EQUAL, skolem, node[2])); - nodeManager->setAttribute(node, theory::IteRewriteAttr(), skolem); - - Debug("ite") << "removeITEs([" << node.getId() << "," << node << "," << nodeType << "])" - << "->" - << "[" << newAssertion.getId() << "," << newAssertion << "]" - << endl; - - Node preprocessed = preprocess(newAssertion); - d_propEngine->assertFormula(preprocessed); - - return skolem; - } - } - vector<Node> newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - // Make sure to push operator or it will be missing in new - // (reformed) node. This was crashing on the very simple input - // "(f (ite c 0 1))" - newChildren.push_back(node.getOperator()); - } - for(TNode::const_iterator it = node.begin(), end = node.end(); - it != end; - ++it) { - Node newChild = removeITEs(*it); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - if(somethingChanged) { - cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); - nodeManager->setAttribute(node, theory::IteRewriteAttr(), cachedRewrite); - return cachedRewrite; - } else { - nodeManager->setAttribute(node, theory::IteRewriteAttr(), Node::null()); - return node; - } -} - - Node TheoryEngine::getValue(TNode node) { kind::MetaKind metakind = node.getMetaKind(); // special case: prop engine handles boolean vars @@ -451,36 +362,91 @@ bool TheoryEngine::hasRegisterTerm(TheoryId th) const { } } -Node TheoryEngine::simplify(TNode in, theory::Substitutions& outSubstitutions) { - SimplifyCache::Scope cache(d_simplifyCache, in); - if(cache) { - outSubstitutions.insert(outSubstitutions.end(), - cache.get().second.begin(), - cache.get().second.end()); - return cache.get().first; - } +theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) { + TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; + Debug("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl; + Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut); + Debug("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl; + return solveStatus; +} + +struct preprocess_stack_element { + TNode node; + bool children_added; + preprocess_stack_element(TNode node) + : node(node), children_added(false) {} +};/* struct preprocess_stack_element */ - size_t prevSize = outSubstitutions.size(); - TNode atom = in.getKind() == kind::NOT ? in[0] : in; +Node TheoryEngine::preprocess(TNode assertion) { + + Debug("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl; + + // Do a topological sort of the subexpressions and substitute them + vector<preprocess_stack_element> toVisit; + toVisit.push_back(assertion); + + while (!toVisit.empty()) + { + // The current node we are processing + preprocess_stack_element& stackHead = toVisit.back(); + TNode current = stackHead.node; - theory::Theory* theory = theoryOf(atom); + Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << std::endl; - Debug("simplify") << push << "simplifying " << in << " to " << theory->identify() << std::endl; - Node n = theory->simplify(in, outSubstitutions); - Debug("simplify") << "got from " << theory->identify() << " : " << n << std::endl << pop; + // If node already in the cache we're done, pop from the stack + NodeMap::iterator find = d_atomPreprocessingCache.find(current); + if (find != d_atomPreprocessingCache.end()) { + toVisit.pop_back(); + continue; + } - atom = n.getKind() == kind::NOT ? n[0] : n; + // If this is an atom, we preprocess it with the theory + if (Theory::theoryOf(current) != THEORY_BOOL) { + d_atomPreprocessingCache[current] = theoryOf(current)->preprocess(current); + continue; + } - if(atom.getKind() == kind::EQUAL) { - theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType()); - Debug("simplify") << push << "simplifying " << n << " to " << typeTheory << std::endl; - n = d_theoryTable[typeTheory]->simplify(n, outSubstitutions); - Debug("simplify") << "got from " << d_theoryTable[typeTheory]->identify() << " : " << n << std::endl << pop; + // Not yet substituted, so process + if (stackHead.children_added) { + // Children have been processed, so substitute + NodeBuilder<> builder(current.getKind()); + if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { + builder << current.getOperator(); + } + for (unsigned i = 0; i < current.getNumChildren(); ++ i) { + Assert(d_atomPreprocessingCache.find(current[i]) != d_atomPreprocessingCache.end()); + builder << d_atomPreprocessingCache[current[i]]; + } + // Mark the substitution and continue + Node result = builder; + Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << std::endl; + d_atomPreprocessingCache[current] = result; + toVisit.pop_back(); + } else { + // Mark that we have added the children if any + if (current.getNumChildren() > 0) { + stackHead.children_added = true; + // We need to add the children + for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { + TNode childNode = *child_it; + NodeMap::iterator childFind = d_atomPreprocessingCache.find(childNode); + if (childFind == d_atomPreprocessingCache.end()) { + toVisit.push_back(childNode); + } + } + } else { + // No children, so we're done + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << std::endl; + d_atomPreprocessingCache[current] = current; + toVisit.pop_back(); + } + } } - cache(std::make_pair(n, theory::Substitutions(outSubstitutions.begin() + prevSize, outSubstitutions.end()))); - return n; + // Return the substituted version + return d_atomPreprocessingCache[assertion]; } + }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 852eea0c4..5b724a7c7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -29,6 +29,7 @@ #include "prop/prop_engine.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" +#include "theory/substitutions.h" #include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/valuation.h" @@ -36,6 +37,7 @@ #include "util/stats.h" #include "util/hash.h" #include "util/cache.h" +#include "util/ite_removal.h" namespace CVC4 { @@ -81,14 +83,10 @@ class TheoryEngine { bool d_needRegistration; /** - * The type of the simplification cache. - */ - typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache; - - /** - * A cache for simplification. + * Cache from proprocessing of atoms. */ - SimplifyCache d_simplifyCache; + typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap; + NodeMap d_atomPreprocessingCache; /** * An output channel for Theory that passes messages @@ -191,11 +189,6 @@ class TheoryEngine { context::CDO<bool> d_incomplete; /** - * Replace ITE forms in a node. - */ - Node removeITEs(TNode t); - - /** * Mark a theory active if it's not already. */ void markActive(theory::TheoryId th) { @@ -256,6 +249,12 @@ public: } /** + * Runs theory specific preprocesssing on the non-Boolean parts of the formula. + * This is only called on input assertions, after ITEs have been removed. + */ + Node preprocess(TNode node); + + /** * Return whether or not we are incomplete (in the current context). */ bool isIncomplete() { @@ -290,7 +289,11 @@ public: * of built-in type. */ inline theory::Theory* theoryOf(TNode node) { - return d_theoryTable[theory::Theory::theoryOf(node)]; + if (node.getKind() == kind::EQUAL) { + return d_theoryTable[theory::Theory::theoryOf(node[0])]; + } else { + return d_theoryTable[theory::Theory::theoryOf(node)]; + } } /** @@ -304,12 +307,9 @@ public: } /** - * Preprocess a node. This involves ITE removal and theory-specific - * rewriting. - * - * @param n the node to preprocess + * Solve the given literal with a theory that owns it. */ - Node preprocess(TNode n); + theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut); /** * Preregister a Theory atom with the responsible theory (or @@ -318,6 +318,15 @@ public: void preRegister(TNode preprocessed); /** + * Call the theories to perform one last rewrite on the theory atoms + * if they wish. This last rewrite is only performed on the input atoms. + * At this point it is ensured that atoms do not contain any Boolean + * strucure, i.e. there is no ITE nodes in them. + * + */ + Node preCheckRewrite(TNode node); + + /** * Assert the formula to the appropriate theory. * @param node the assertion */ @@ -339,19 +348,9 @@ public: //Debug("theory")<< "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays \n"; d_theoryTable[theory::THEORY_ARRAY]->assertFact(node); } else { - theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]); - Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl; - d_theoryTable[theoryLHS]->assertFact(node); -// theory::TheoryId theoryRHS = theory::Theory::theoryOf(atom[1]); -// if (theoryLHS != theoryRHS) { -// Debug("theory") << "asserting " << node << " to " << theoryRHS << std::endl; -// d_theoryTable[theoryRHS]->assertFact(node); -// } -// theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType()); -// if (typeTheory!= theoryLHS && typeTheory != theoryRHS) { -// Debug("theory") << "asserting " << node << " to " << typeTheory << std::endl; -// d_theoryTable[typeTheory]->assertFact(node); -// } + theory::Theory* theory = theoryOf(atom); + Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl; + theory->assertFact(node); } } else { theory::Theory* theory = theoryOf(atom); @@ -373,12 +372,6 @@ public: void staticLearning(TNode in, NodeBuilder<>& learned); /** - * Calls simplify() on all theories, accumulating their combined - * contributions in the "outSubstitutions" vector. - */ - Node simplify(TNode in, theory::Substitutions& outSubstitutions); - - /** * Calls presolve() on all active theories and returns true * if one of the theories discovers a conflict. */ @@ -398,7 +391,13 @@ public: } inline void newLemma(TNode node) { - d_propEngine->assertLemma(preprocess(node)); + // Remove the ITEs and assert to prop engine + std::vector<Node> additionalLemmas; + additionalLemmas.push_back(node); + RemoveITE::run(additionalLemmas); + for (unsigned i = 0; i < additionalLemmas.size(); ++ i) { + d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i])); + } } /** diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 604ae21e1..536255c2d 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -41,13 +41,5 @@ Node Valuation::getSatValue(TNode n) const{ } } -Node Valuation::simplify(TNode in, Substitutions& outSubstitutions) { - return d_engine->simplify(in, outSubstitutions); -} - -Node Valuation::rewrite(TNode in) { - return d_engine->preprocess(in); -} - }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index d46b9aab1..2346b6d32 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -51,20 +51,6 @@ public: */ Node getSatValue(TNode n) const; - /** - * Simplify a node. Intended to be used by a theory's simplify() - * function to simplify subterms (TheoryEngine will cache the - * results and make sure that the request is directed to the correct - * theory). - */ - Node simplify(TNode in, Substitutions& outSubstitutions); - - /** - * Rewrite a node. Intended to be used by a theory to have the - * TheoryEngine fully rewrite a node. - */ - Node rewrite(TNode in); - };/* class Valuation */ }/* CVC4::theory namespace */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index dc1da0659..83200a473 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -59,7 +59,9 @@ libutil_la_SOURCES = \ trans_closure.h \ trans_closure.cpp \ boolean_simplification.h \ - boolean_simplification.cpp + boolean_simplification.cpp \ + ite_removal.h \ + ite_removal.cpp libutil_la_LIBADD = \ @builddir@/libutilcudd.la diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp new file mode 100644 index 000000000..e9c5122b3 --- /dev/null +++ b/src/util/ite_removal.cpp @@ -0,0 +1,94 @@ +/********************* */ +/*! \file ite_removal.cpp + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of cardinality + ** + ** Simple class to represent a cardinality; used by the CVC4 type system + ** give the cardinality of sorts. + **/ + +#include <vector> + +#include "util/ite_removal.h" +#include "theory/rewriter.h" + +using namespace CVC4; +using namespace std; + +struct IteRewriteAttrTag {}; +typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr; + +void RemoveITE::run(std::vector<Node>& output) { + for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { + output[i] = run(output[i], output); + } +} + +Node RemoveITE::run(TNode node, std::vector<Node>& output) +{ + // Current node + Debug("ite") << "removeITEs(" << node << ")" << endl; + + // The result may be cached already + Node cachedRewrite; + NodeManager *nodeManager = NodeManager::currentNM(); + if(nodeManager->getAttribute(node, IteRewriteAttr(), cachedRewrite)) { + Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl; + return cachedRewrite.isNull() ? Node(node) : cachedRewrite; + } + + // If an ITE replace it + if(node.getKind() == kind::ITE) { + TypeNode nodeType = node.getType(); + if(!nodeType.isBoolean()) { + // Make the skolem to represent the ITE + Node skolem = nodeManager->mkVar(nodeType); + + // The new assertion + Node newAssertion = nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the skolem + nodeManager->setAttribute(node, IteRewriteAttr(), skolem); + + // Remove ITEs from the new assertion, rewrite it and push it to the output + output.push_back(run(newAssertion, output)); + + // The representation is now the skolem + return skolem; + } + } + + // If not an ITE, go deep + vector<Node> newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Remove the ITEs from the children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = run(*it, output); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren); + nodeManager->setAttribute(node, IteRewriteAttr(), cachedRewrite); + return cachedRewrite; + } else { + nodeManager->setAttribute(node, IteRewriteAttr(), Node::null()); + return node; + } +}; diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h new file mode 100644 index 000000000..b286665cc --- /dev/null +++ b/src/util/ite_removal.h @@ -0,0 +1,44 @@ +/********************* */ +/*! \file ite_removal.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of cardinality + ** + ** Simple class to represent a cardinality; used by the CVC4 type system + ** give the cardinality of sorts. + **/ + +#pragma once + +#include <vector> +#include "expr/node.h" + +namespace CVC4 { + +class RemoveITE { + +public: + + /** + * Removes the ITE nodes by introducing skolem variables. All additional assertions are pushed into assertions. + */ + static void run(std::vector<Node>& assertions); + + /** + * Removes the ITE from the node by introducing skolem variables. All additional assertions are pushed into assertions. + */ + static Node run(TNode node, std::vector<Node>& additionalAssertions); + +}; + + +} diff --git a/src/util/options.cpp b/src/util/options.cpp index 314d85718..ff028b6c6 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -69,7 +69,7 @@ Options::Options() : memoryMap(false), strictParsing(false), lazyDefinitionExpansion(false), - simplificationMode(INCREMENTAL_MODE), + simplificationMode(SIMPLIFICATION_MODE_BATCH), simplificationStyle(NO_SIMPLIFICATION_STYLE), interactive(false), interactiveSetByUser(false), @@ -142,19 +142,15 @@ Languages currently supported as arguments to the -L / --lang option:\n\ static const string simplificationHelp = "\ Simplification modes currently supported by the --simplification option:\n\ \n\ -batch\n\ +batch (default) \n\ + save up all ASSERTions; run nonclausal simplification and clausal\n\ (MiniSat) propagation for all of them only after reaching a querying command\n\ (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\ \n\ -incremental (default)\n\ +incremental\n\ + run nonclausal simplification and clausal propagation at each ASSERT\n\ (and at CHECKSAT/QUERY/SUBTYPE)\n\ \n\ -incremental-lazy-sat\n\ -+ run nonclausal simplification at each ASSERT, but delay clausification of\n\ - ASSERT until reaching a CHECKSAT/QUERY/SUBTYPE, then clausify them all\n\ -\n\ You can also specify the level of aggressiveness for the simplification\n\ (by repeating the --simplification option):\n\ \n\ @@ -454,11 +450,9 @@ throw(OptionException) { case SIMPLIFICATION_MODE: if(!strcmp(optarg, "batch")) { - simplificationMode = BATCH_MODE; + simplificationMode = SIMPLIFICATION_MODE_BATCH; } else if(!strcmp(optarg, "incremental")) { - simplificationMode = INCREMENTAL_MODE; - } else if(!strcmp(optarg, "incremental-lazy-sat")) { - simplificationMode = INCREMENTAL_LAZY_SAT_MODE; + simplificationMode = SIMPLIFICATION_MODE_INCREMENTAL; } else if(!strcmp(optarg, "aggressive")) { simplificationStyle = AGGRESSIVE_SIMPLIFICATION_STYLE; } else if(!strcmp(optarg, "toplevel")) { diff --git a/src/util/options.h b/src/util/options.h index a5e03d21b..06ca20073 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -106,10 +106,12 @@ struct CVC4_PUBLIC Options { /** Enumeration of simplification modes (when to simplify). */ typedef enum { - BATCH_MODE, - INCREMENTAL_MODE, - INCREMENTAL_LAZY_SAT_MODE + /** Simplify the assertions as they come in */ + SIMPLIFICATION_MODE_INCREMENTAL, + /** Simplify the assertions all together once a check is requested */ + SIMPLIFICATION_MODE_BATCH } SimplificationMode; + /** When to perform nonclausal simplifications. */ SimplificationMode simplificationMode; @@ -241,14 +243,11 @@ inline std::ostream& operator<<(std::ostream& out, inline std::ostream& operator<<(std::ostream& out, Options::SimplificationMode mode) { switch(mode) { - case Options::BATCH_MODE: - out << "BATCH_MODE"; - break; - case Options::INCREMENTAL_MODE: - out << "INCREMENTAL_MODE"; + case Options::SIMPLIFICATION_MODE_BATCH: + out << "SIMPLIFICATION_MODE_BATCH"; break; - case Options::INCREMENTAL_LAZY_SAT_MODE: - out << "INCREMENTAL_LAZY_SAT_MODE"; + case Options::SIMPLIFICATION_MODE_INCREMENTAL: + out << "SIMPLIFICATION_MODE_INCREMENTAL"; break; default: out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]"; diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 89df462e5..fb0abfe25 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop +SUBDIRS = . arith precedence uf uflra bv arrays datatypes lemmas push-pop preprocess TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 MAKEFLAGS = -k @@ -78,7 +78,6 @@ CVC_TESTS = \ # Regression tests derived from bug reports BUG_TESTS = \ - bug2.smt \ bug32.cvc \ bug49.smt \ bug161.smt \ diff --git a/test/regress/regress0/preprocess/Makefile b/test/regress/regress0/preprocess/Makefile new file mode 100644 index 000000000..c5843db5f --- /dev/null +++ b/test/regress/regress0/preprocess/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/preprocess + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am new file mode 100644 index 000000000..a4fe70946 --- /dev/null +++ b/test/regress/regress0/preprocess/Makefile.am @@ -0,0 +1,45 @@ +SUBDIRS = . + +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" + +# Regression tests for SMT inputs +SMT_TESTS = + +# Regression tests for SMT2 inputs +SMT2_TESTS = + +# Regression tests for PL inputs +CVC_TESTS = \ + preprocess_00.cvc \ + preprocess_01.cvc \ + preprocess_02.cvc \ + preprocess_03.cvc \ + preprocess_04.cvc \ + preprocess_05.cvc \ + preprocess_06.cvc \ + preprocess_07.cvc \ + preprocess_08.cvc \ + preprocess_09.cvc \ + preprocess_10.cvc \ + preprocess_11.cvc \ + preprocess_12.cvc + +# Regression tests derived from bug reports +BUG_TESTS = + +TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) + +EXTRA_DIST = $(TESTS) + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/preprocess/preprocess_00.cvc b/test/regress/regress0/preprocess/preprocess_00.cvc new file mode 100644 index 000000000..c91a8e775 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_00.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid + +a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; + +ASSERT (a5); + +QUERY (a0 OR a1 OR a2 OR a3 OR a4 OR a5 OR a6 OR a7 OR a8 OR a9); + +% EXIT: 20 + diff --git a/test/regress/regress0/preprocess/preprocess_01.cvc b/test/regress/regress0/preprocess/preprocess_01.cvc new file mode 100644 index 000000000..e4b2e7dcf --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_01.cvc @@ -0,0 +1,12 @@ +% EXPECT: unsat + +a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; + +ASSERT (a5); + +ASSERT NOT (a0 OR a1 OR a2 OR a3 OR a4 OR a5 OR a6 OR a7 OR a8 OR a9); + +CHECKSAT; + +% EXIT: 20 + diff --git a/test/regress/regress0/preprocess/preprocess_02.cvc b/test/regress/regress0/preprocess/preprocess_02.cvc new file mode 100644 index 000000000..7907d87ec --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_02.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid + +a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; + +ASSERT (NOT a5); + +QUERY NOT (a0 AND a1 AND a2 AND a3 AND a4 AND a5 AND a6 AND a7 AND a8 AND a9); + +% EXIT: 20 + diff --git a/test/regress/regress0/preprocess/preprocess_03.cvc b/test/regress/regress0/preprocess/preprocess_03.cvc new file mode 100644 index 000000000..e564936a6 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_03.cvc @@ -0,0 +1,11 @@ +% EXPECT: unsat + +a0, a1, a2, a3, a4, a5, a6, a7, a8, a9: BOOLEAN; + +ASSERT (NOT a5); +ASSERT (a0 AND a1 AND a2 AND a3 AND a4 AND a5 AND a6 AND a7 AND a8 AND a9); + +CHECKSAT; + +% EXIT: 20 + diff --git a/test/regress/regress0/preprocess/preprocess_04.cvc b/test/regress/regress0/preprocess/preprocess_04.cvc new file mode 100644 index 000000000..2728e0eb8 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_04.cvc @@ -0,0 +1,16 @@ +% EXPECT: unsat + +a0, a1, a2, a3, a4, a5, a6, a7, a8: BOOLEAN; + +ASSERT (NOT a1); +ASSERT (a4 AND a7); +ASSERT + IF (a0 AND a1 AND a2) + THEN (a3 AND a4 AND a5) + ELSE (a6 AND NOT a7 AND a8) + ENDIF; + +CHECKSAT; + +% EXIT: 20 + diff --git a/test/regress/regress0/preprocess/preprocess_05.cvc b/test/regress/regress0/preprocess/preprocess_05.cvc new file mode 100644 index 000000000..7e337bb13 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_05.cvc @@ -0,0 +1,16 @@ +% EXPECT: sat + +a0, a1, a2, a3, a4, a5, a6, a7, a8: BOOLEAN; + +ASSERT (NOT a1); +ASSERT (a4 AND a7); +ASSERT + IF (a0 AND a1 AND a2) + THEN (a3 AND a4 AND a5) + ELSE (a6 AND a7 AND a8) + ENDIF; + +CHECKSAT; + +% EXIT: 10 + diff --git a/test/regress/regress0/preprocess/preprocess_06.cvc b/test/regress/regress0/preprocess/preprocess_06.cvc new file mode 100644 index 000000000..e9631b3ac --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_06.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid + +a0, a1, a2, a3, a4, a5: BOOLEAN; + +ASSERT (a0 => a1); +ASSERT (a1 => a2); +ASSERT (a2 => a3); +ASSERT (a3 => a4); +ASSERT (a4 => a5); +ASSERT a0; + +QUERY (a0 <=> a5); + +% EXIT: 20 + diff --git a/test/regress/regress0/preprocess/preprocess_07.cvc b/test/regress/regress0/preprocess/preprocess_07.cvc new file mode 100644 index 000000000..57ccc6ef8 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_07.cvc @@ -0,0 +1,11 @@ +% EXPECT: sat + +a0, a1, a2, a3, a4, a5: BOOLEAN; + +ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5)); +ASSERT (a4); + +CHECKSAT; + +% EXIT: 10 + diff --git a/test/regress/regress0/preprocess/preprocess_08.cvc b/test/regress/regress0/preprocess/preprocess_08.cvc new file mode 100644 index 000000000..6e0edc5a9 --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_08.cvc @@ -0,0 +1,11 @@ +% EXPECT: sat + +a0, a1, a2, a3, a4, a5: BOOLEAN; + +ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5)); +ASSERT (NOT a1); + +CHECKSAT; + +% EXIT: 10 + diff --git a/test/regress/regress0/preprocess/preprocess_09.cvc b/test/regress/regress0/preprocess/preprocess_09.cvc new file mode 100644 index 000000000..8b62bbafa --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_09.cvc @@ -0,0 +1,15 @@ +% EXPECT: sat + +a0, a1, a2, a3, a4, a5: BOOLEAN; + +ASSERT ((a0 AND a1 AND a2) <=> (a3 OR a4 OR a5)); +ASSERT (a0); +ASSERT (a1); +ASSERT (a2); +ASSERT (NOT a3); +ASSERT (NOT a5); + +CHECKSAT; + +% EXIT: 10 + diff --git a/test/regress/regress0/preprocess/preprocess_10.cvc b/test/regress/regress0/preprocess/preprocess_10.cvc new file mode 100644 index 000000000..d3b5bfe7e --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_10.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat +x: REAL; +b: BOOLEAN; + +ASSERT (x = IF b THEN 10 ELSE -10 ENDIF); +ASSERT b; + +CHECKSAT; + +% EXIT: 10 + + diff --git a/test/regress/regress0/preprocess/preprocess_11.cvc b/test/regress/regress0/preprocess/preprocess_11.cvc new file mode 100644 index 000000000..13a8f532c --- /dev/null +++ b/test/regress/regress0/preprocess/preprocess_11.cvc @@ -0,0 +1,11 @@ +% EXPECT: sat + +x: REAL; +y: REAL; + +ASSERT ((0 = IF TRUE THEN x ELSE 1 ENDIF) AND (0 = IF (x = 0) THEN 0 ELSE 1 ENDIF) AND (x = IF TRUE THEN y ELSE 0 ENDIF) AND (0 = IF TRUE THEN 0 ELSE 0 ENDIF)); + +CHECKSAT; + +% EXIT: 10 + diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 3a57ada3f..85c3cb9c9 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -8,13 +8,11 @@ MAKEFLAGS = -k # put it below in "TESTS +=" # Regression tests for SMT inputs -CVC_TESTS = \ - test.00.cvc +CVC_TESTS = TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) -EXTRA_DIST = $(TESTS) \ - test.01.cvc +EXTRA_DIST = $(TESTS) # synonyms for "check" in this directory .PHONY: regress regress0 test |