}
void SimplifyCommand::invoke(SmtEngine* smtEngine) {
- d_result = smtEngine->simplify(d_term);
+#warning TODO: what is this
}
Expr SimplifyCommand::getResult() const {
*/
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;
if(*i == node) {
nb << replacement;
} else {
- (*i).substitute(node, replacement, cache);
+ nb << (*i).substitute(node, replacement, cache);
}
}
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
// 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;
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;
}
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) {
d_cnfStream->convertAndAssert(node, true, false);
}
-
void PropEngine::printSatisfyingAssignment(){
const CnfStream::TranslationCache& transCache =
d_cnfStream->getTranslationCache();
#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"
#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 {
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
}
d_assignments = NULL;
- d_haveAdditions = false;
+ d_problemExtended = false;
d_queryMade = false;
}
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" ||
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();
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();
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") {
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();
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) {
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 {
iend = n.end();
i != iend;
++i) {
- Node expanded = this->expandDefinitions(*i, cache);
+ Node expanded = expandDefinitions(*i, cache);
Debug("expand") << "exchld: " << expanded << endl;
nb << expanded;
}
}
}
-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
}
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) {
}
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 "
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);
}
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)
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.";
}
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);
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));
}
}
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 "
}
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);
++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
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.";
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)");
}
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)");
}
}
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();
}
* 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
rewriter_attributes.h \
rewriter.cpp \
substitutions.h \
+ substitutions.cpp \
valuation.h \
valuation.cpp
RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
Assert(isAtom(atom));
+
NodeManager* currNM = NodeManager::currentNM();
if(atom.getKind() == kind::EQUAL) {
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];
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:
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;
}
}
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;
}
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);
+ }
+ }
}
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;
+ }
+}
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:
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) {
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"); }
#include "theory/booleans/circuit_propagator.h"
#include "util/utility.h"
+#include <stack>
#include <vector>
#include <algorithm>
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 */
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
* 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. */
};/* 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 */
}
}
-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;
}
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 */
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
}
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
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()) {
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 */
void check(Effort e);
- //void presolve() { }
-
void propagate(Effort e) { }
void explain(TNode n);
--- /dev/null
+/********************* */
+/*! \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;
+ }
+}
+
+}
+}
* 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 */
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;
}
*/
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
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 */
#include "theory/rewriter.h"
#include "theory/theory_traits.h"
+#include "util/ite_removal.h"
+
using namespace std;
using namespace CVC4;
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) {
// 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()) */
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())) {
}
// 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
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);
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
}
}
-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 */
#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"
#include "util/stats.h"
#include "util/hash.h"
#include "util/cache.h"
+#include "util/ite_removal.h"
namespace CVC4 {
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
*/
context::CDO<bool> d_incomplete;
- /**
- * Replace ITE forms in a node.
- */
- Node removeITEs(TNode t);
-
/**
* Mark a theory active if it's not already.
*/
return d_propEngine;
}
+ /**
+ * 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).
*/
* 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)];
+ }
}
/**
}
/**
- * 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
*/
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
//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);
*/
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.
}
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]));
+ }
}
/**
}
}
-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 */
*/
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 */
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
--- /dev/null
+/********************* */
+/*! \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;
+ }
+};
--- /dev/null
+/********************* */
+/*! \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);
+
+};
+
+
+}
memoryMap(false),
strictParsing(false),
lazyDefinitionExpansion(false),
- simplificationMode(INCREMENTAL_MODE),
+ simplificationMode(SIMPLIFICATION_MODE_BATCH),
simplificationStyle(NO_SIMPLIFICATION_STYLE),
interactive(false),
interactiveSetByUser(false),
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\
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")) {
/** 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;
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) << "]";
-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
# Regression tests derived from bug reports
BUG_TESTS = \
- bug2.smt \
bug32.cvc \
bug49.smt \
bug161.smt \
--- /dev/null
+topdir = ../../../..
+srcdir = test/regress/regress0/preprocess
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
--- /dev/null
+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:
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% 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
+
--- /dev/null
+% EXPECT: sat
+x: REAL;
+b: BOOLEAN;
+
+ASSERT (x = IF b THEN 10 ELSE -10 ENDIF);
+ASSERT b;
+
+CHECKSAT;
+
+% EXIT: 10
+
+
--- /dev/null
+% 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
+
# 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
projects / cvc5.git / commitdiff