From: Morgan Deters Date: Fri, 30 Sep 2011 02:29:00 +0000 (+0000) Subject: fixes to incremental simplification, cnf routines, other stuff in preparation of... X-Git-Tag: cvc5-1.0.0~8445 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5fad8e60577136632f12b05fc07336b77fbabe7b;p=cvc5.git fixes to incremental simplification, cnf routines, other stuff in preparation of user push/pop in SAT solver --- diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 5b8e4c3f3..4e557d416 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -103,17 +103,22 @@ bool CnfStream::isTranslated(TNode n) const { return find != d_translationCache.end() && find->second.level >= 0; } -bool CnfStream::hasLiteral(TNode n) const { +bool CnfStream::hasEverHadLiteral(TNode n) const { TranslationCache::const_iterator find = d_translationCache.find(n); return find != d_translationCache.end(); } +bool CnfStream::currentlyHasLiteral(TNode n) const { + TranslationCache::const_iterator find = d_translationCache.find(n); + return find != d_translationCache.end() && (*find).second.level != -1; +} + SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl; // Get the literal for this node SatLiteral lit; - if (!hasLiteral(node)) { + if (!hasEverHadLiteral(node)) { // If no literal, well make one lit = variableToLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; @@ -599,13 +604,16 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl; - if(hasLiteral(node)) { + /* + if(currentlyHasLiteral(node)) { Debug("cnf") << "==> fortunate literal detected!" << endl; ++d_fortunateLiterals; SatLiteral lit = getLiteral(node); //d_satSolver->renewVar(lit); assertClause(node, negated ? ~lit : lit); + return; } + */ switch(node.getKind()) { case AND: diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index ecb0fd2fb..3ef636811 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -215,12 +215,16 @@ public: TNode getNode(const SatLiteral& literal); /** - * Returns true if the node has an assigned literal (it might not be translated). - * Caches the pair of the node and the literal corresponding to the - * translation. + * Returns true iff the node has an assigned literal (it might not be translated). * @param node the node */ - bool hasLiteral(TNode node) const; + bool hasEverHadLiteral(TNode node) const; + + /** + * Returns true iff the node has an assigned literal and it's translated. + * @param node the node + */ + bool currentlyHasLiteral(TNode node) const; /** * Returns the literal that represents the given node in the SAT CNF diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index c8e4083b1..7b4155bde 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -167,7 +167,7 @@ Node PropEngine::getValue(TNode node) { } bool PropEngine::isSatLiteral(TNode node) { - return d_cnfStream->hasLiteral(node); + return d_cnfStream->hasEverHadLiteral(node); } bool PropEngine::hasValue(TNode node, bool& value) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 86d06520a..42b21b79a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -107,6 +107,9 @@ class SmtEnginePrivate { /** Learned literals */ vector d_nonClausalLearnedLiterals; + /** A circuit propagator for non-clausal propositional deduction */ + booleans::CircuitPropagator d_propagator; + /** Assertions to push to sat */ vector d_assertionsToCheck; @@ -140,6 +143,8 @@ public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), + d_nonClausalLearnedLiterals(), + d_propagator(smt.d_userContext, d_nonClausalLearnedLiterals, true, true), d_topLevelSubstitutions(smt.d_userContext) { } @@ -244,6 +249,8 @@ SmtEngine::~SmtEngine() { StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime); StatisticsRegistry::unregisterStat(&d_staticLearningTime); + // Deletion order error: circuit propagator has some unsafe TNodes ?! + // delete d_private; delete d_userContext; delete d_theoryEngine; @@ -559,7 +566,7 @@ void SmtEnginePrivate::staticLearning() { void SmtEnginePrivate::nonClausalSimplify() { - TimerStat::CodeTimer nonclauselTimer(d_smt.d_nonclausalSimplificationTime); + TimerStat::CodeTimer nonclausalTimer(d_smt.d_nonclausalSimplificationTime); Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl; @@ -571,19 +578,16 @@ void SmtEnginePrivate::nonClausalSimplify() { theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); } - d_nonClausalLearnedLiterals.clear(); - booleans::CircuitPropagator propagator(d_nonClausalLearnedLiterals, true, true); - // Assert all the assertions to the propagator Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "asserting to propagator" << endl; for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - propagator.assert(d_assertionsToPreprocess[i]); + d_propagator.assert(d_assertionsToPreprocess[i]); } Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "propagating" << endl; - if (propagator.propagate()) { + if (d_propagator.propagate()) { // If in conflict, just return false Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "conflict in non-clausal propagation" << endl; @@ -1082,22 +1086,25 @@ void SmtEngine::pop() { << d_userContext->getLevel() << endl; // FIXME: should we reset d_status here? // SMT-LIBv2 spec seems to imply no, but it would make sense to.. + // Still, we want the right exit status after any final sequence + // of pops... hm. } -void SmtEngine::internalPop() { - Trace("smt") << "internalPop()" << endl; - d_propEngine->pop(); - d_userContext->pop(); +void SmtEngine::internalPush() { + Trace("smt") << "SmtEngine::internalPush()" << endl; + if(Options::current()->incrementalSolving) { + d_private->processAssertions(); + d_userContext->push(); + d_propEngine->push(); + } } -void SmtEngine::internalPush() { - Trace("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(); +void SmtEngine::internalPop() { + Trace("smt") << "SmtEngine::internalPop()" << endl; + if(Options::current()->incrementalSolving) { + d_propEngine->pop(); + d_userContext->pop(); + } } StatisticsRegistry* SmtEngine::getStatisticsRegistry() const { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7a5f39056..f5036bed7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -137,7 +137,7 @@ class CVC4_PUBLIC SmtEngine { /** * Whether or not a query() or checkSat() has already been made through - * this SmtEngine. If true, and d_incrementalSolving is false, then + * this SmtEngine. If true, and incrementalSolving is false, then * attempting an additional query() or checkSat() will fail with a * ModalException. */ diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 9593f7735..e1e3073ce 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -28,6 +28,9 @@ #include "context/context.h" #include "util/hash.h" #include "expr/node.h" +#include "context/cdset.h" +#include "context/cdmap.h" +#include "context/cdo.h" namespace CVC4 { namespace theory { @@ -72,20 +75,50 @@ private: /** The propagation queue */ std::vector d_propagationQueue; + /** A context-notify object that clears out stale data. */ + template + class DataClearer : context::ContextNotifyObj { + T& d_data; + public: + DataClearer(context::Context* context, T& data) : + context::ContextNotifyObj(context), + d_data(data) { + } + + void notify() { + Trace("circuit-prop") << "CircuitPropagator::DataClearer: clearing data " + << "(size was " << d_data.size() << ")" << std::endl; + d_data.clear(); + } + };/* class DataClearer */ + + /** + * We have a propagation queue "clearer" object for when the user + * context pops. Normally the propagation queue should be empty, + * but this keeps us safe in case there's still some rubbish around + * on the queue. + */ + DataClearer< std::vector > d_propagationQueueClearer; + /** Are we in conflict */ - bool d_conflict; + context::CDO d_conflict; /** Map of substitutions */ std::vector& d_learnedLiterals; + /** + * Similar data clearer for learned literals. + */ + DataClearer< std::vector > d_learnedLiteralClearer; + /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far - std::hash_set d_seen; + context::CDSet d_seen; /** * Assignment status of each node. */ - typedef std::hash_map AssignmentMap; + typedef context::CDMap AssignmentMap; AssignmentMap d_state; /** @@ -93,7 +126,7 @@ private: */ void assignAndEnqueue(TNode n, bool value) { - Debug("circuit-prop") << "CircuitPropagator::assign(" << n << ", " << (value ? "true" : "false") << ")" << std::endl; + Trace("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 @@ -136,8 +169,9 @@ private: /** Get Node assignment in circuit. Assert-fails if Node is unassigned. */ 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; + AssignmentMap::iterator i = d_state.find(n); + Assert(i != d_state.end() && (*i).second != UNASSIGNED); + return (*i).second == ASSIGNED_TO_TRUE; } /** Predicate for use in STL functions. */ @@ -186,17 +220,25 @@ private: void propagateBackward(TNode parent, bool assignment); /** Whether to perform forward propagation */ - bool d_forwardPropagation; + const bool d_forwardPropagation; + /** Whether to perform backward propagation */ - bool d_backwardPropagation; + const bool d_backwardPropagation; public: /** - * Construct a new CircuitPropagator with the given atoms and backEdges. + * Construct a new CircuitPropagator. */ - CircuitPropagator(std::vector& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) : - d_conflict(false), + CircuitPropagator(context::Context* context, std::vector& outLearnedLiterals, + bool enableForward = true, bool enableBackward = true) : + d_backEdges(), + d_propagationQueue(), + d_propagationQueueClearer(context, d_propagationQueue), + d_conflict(context, false), d_learnedLiterals(outLearnedLiterals), + d_learnedLiteralClearer(context, outLearnedLiterals), + d_seen(context), + d_state(context), d_forwardPropagation(enableForward), d_backwardPropagation(enableBackward) { } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index fb0abfe25..948731057 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -74,7 +74,8 @@ CVC_TESTS = \ wiki.18.cvc \ wiki.19.cvc \ wiki.20.cvc \ - wiki.21.cvc + wiki.21.cvc \ + simplification_bug3.cvc # Regression tests derived from bug reports BUG_TESTS = \ diff --git a/test/regress/regress0/simplification_bug3.cvc b/test/regress/regress0/simplification_bug3.cvc new file mode 100644 index 000000000..26efad5b6 --- /dev/null +++ b/test/regress/regress0/simplification_bug3.cvc @@ -0,0 +1,8 @@ +% COMMAND-LINE: --simplification=incremental +x, y: BOOLEAN; +ASSERT x OR y; +ASSERT NOT x; +ASSERT NOT y; +% EXPECT: unsat +CHECKSAT; +% EXIT: 20