From 90267f8729799f44c6fb33ace11b971a16e78dff Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 2 Sep 2011 12:39:23 +0000 Subject: [PATCH] * Changing pre-registration to be context dependent -- it is called from the SAT solver on every backtrack * Updated UF to handle the context dependent pre-registration * Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool --- src/main/main.cpp | 2 +- src/parser/cvc/cvc_input.h | 2 +- src/parser/parser_builder.cpp | 1 + src/parser/smt/smt_input.h | 2 +- src/prop/cnf_stream.cpp | 3 +- src/prop/minisat/core/Solver.cc | 12 +++++ src/prop/minisat/core/Solver.h | 13 ++++- src/prop/sat.cpp | 4 ++ src/prop/sat.h | 11 ++++- src/theory/arith/theory_arith.h | 2 +- src/theory/theory.h | 2 +- src/theory/theory_engine.cpp | 2 +- src/theory/theory_engine.h | 72 +++++++++------------------- src/theory/uf/equality_engine.h | 43 +++++++++++++---- src/theory/uf/equality_engine_impl.h | 47 ++++++++++++++++-- src/theory/uf/theory_uf.cpp | 1 + 16 files changed, 149 insertions(+), 70 deletions(-) diff --git a/src/main/main.cpp b/src/main/main.cpp index c21a7bdac..1423befb6 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -112,7 +112,7 @@ int main(int argc, char* argv[]) { pStatistics->flushStatistics(*options.err); } exit(1); - } catch(bad_alloc) { + } catch(bad_alloc&) { #ifdef CVC4_COMPETITION_MODE *options.out << "unknown" << endl; #endif diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h index 45a0edf95..efe0a522f 100644 --- a/src/parser/cvc/cvc_input.h +++ b/src/parser/cvc/cvc_input.h @@ -51,7 +51,7 @@ public: CvcInput(AntlrInputStream& inputStream); /** Destructor. Frees the lexer and the parser. */ - ~CvcInput(); + virtual ~CvcInput(); /** Get the language that this Input is reading. */ InputLanguage getLanguage() const throw() { diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 9773445ed..d4725c4bc 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -89,6 +89,7 @@ Parser *ParserBuilder::build() break; default: parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); + break; } if( d_checksEnabled ) { diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h index 0ab382c73..2fb037f06 100644 --- a/src/parser/smt/smt_input.h +++ b/src/parser/smt/smt_input.h @@ -53,7 +53,7 @@ public: SmtInput(AntlrInputStream& inputStream); /** Destructor. Frees the lexer and the parser. */ - ~SmtInput(); + virtual ~SmtInput(); /** Get the language that this Input is reading. */ InputLanguage getLanguage() const throw() { diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 629e44e3e..9b0c4847b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -98,7 +98,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) { SatLiteral lit; if (!hasLiteral(node)) { // If no literal, well make one - lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral)); + lit = variableToLiteral(d_satSolver->newVar(theoryLiteral)); d_translationCache[node].literal = lit; d_translationCache[node.notNode()].literal = ~lit; } else { @@ -411,6 +411,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { //Node atomic = handleNonAtomicNode(node); //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic); } + break; } } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 7ca117c2e..711379519 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -148,6 +148,11 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom) setDecisionVar(v, dvar); + // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks + if (theoryAtom) { + variables_to_register.push(VarIntroInfo(v, decisionLevel())); + } + return v; } @@ -295,6 +300,13 @@ void Solver::cancelUntil(int level) { qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); + + // Register variables that have not been registered yet + int currentLevel = decisionLevel(); + for(int i = variables_to_register.size() - 1; i >= 0 && variables_to_register[i].level > currentLevel; --i) { + variables_to_register[i].level = currentLevel; + proxy->variableNotify(variables_to_register[i].var); + } } } diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 1141e53c4..4c6e98a2e 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -80,12 +80,23 @@ protected: /** True if we are currently solving. */ bool minisat_busy; + // Information about registration of variables + struct VarIntroInfo { + Var var; + int level; + VarIntroInfo(Var var, int level) + : var(var), level(level) {} + }; + + /** Variables to re-register with theory solvers on backtracks */ + vec variables_to_register; + public: // Constructor/Destructor: // Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false); - CVC4_PUBLIC ~Solver(); + CVC4_PUBLIC virtual ~Solver(); // Problem specification: // diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp index 62558cac1..a7eced6f2 100644 --- a/src/prop/sat.cpp +++ b/src/prop/sat.cpp @@ -27,6 +27,10 @@ namespace CVC4 { namespace prop { +void SatSolver::variableNotify(SatVariable var) { + d_theoryEngine->preRegister(getNode(variableToLiteral(var))); +} + void SatSolver::theoryCheck(theory::Theory::Effort effort) { d_theoryEngine->check(effort); } diff --git a/src/prop/sat.h b/src/prop/sat.h index 2521f3ee7..39977a96b 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -70,6 +70,10 @@ inline SatVariable literalToVariable(SatLiteral lit) { return Minisat::var(lit); } +inline SatLiteral variableToLiteral(SatVariable var) { + return Minisat::mkLit(var); +} + inline bool literalSign(SatLiteral lit) { return Minisat::sign(lit); } @@ -208,7 +212,7 @@ public: TheoryEngine* theoryEngine, context::Context* context); - ~SatSolver(); + virtual ~SatSolver(); bool solve(); @@ -242,6 +246,11 @@ public: void removeClausesAboveLevel(int level); + /** + * Notifies of a new variable at a decision level. + */ + void variableNotify(SatVariable var); + void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 8213dd47a..0c15c824c 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -133,7 +133,7 @@ private: public: TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation); - ~TheoryArith(); + virtual ~TheoryArith(); /** * Does non-context dependent setup for a node connected to a theory. diff --git a/src/theory/theory.h b/src/theory/theory.h index 2256c4462..d859c60d8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -480,7 +480,7 @@ public: return set | (1 << theory); } - /** Check if the set containt the theory */ + /** Check if the set contains the theory */ static inline bool setContains(TheoryId theory, Set set) { return set & (1 << theory); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7447726b4..e604c45df 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -50,7 +50,7 @@ TheoryEngine::TheoryEngine(context::Context* ctxt) : d_hasShutDown(false), d_incomplete(ctxt, false), d_statistics(), - d_preRegistrationVisitor(*this) { + d_preRegistrationVisitor(*this, ctxt) { for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { d_theoryTable[theoryId] = NULL; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ea3fe95c1..662a4925a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -441,7 +441,7 @@ private: /** * Cache from proprocessing of atoms. */ - typedef std::hash_map TNodeVisitedMap; + typedef context::CDMap TNodeVisitedMap; TNodeVisitedMap d_visited; /** @@ -453,14 +453,14 @@ private: std::stringstream ss; TNodeVisitedMap::const_iterator it = d_visited.begin(); for (; it != d_visited.end(); ++ it) { - ss << it->first << ": " << theory::Theory::setToString(it->second) << std::endl; + ss << (*it).first << ": " << theory::Theory::setToString((*it).second) << std::endl; } return ss.str(); } public: - PreRegisterVisitor(TheoryEngine& engine): d_engine(engine), d_theories(0) {} + PreRegisterVisitor(TheoryEngine& engine, context::Context* context): d_engine(engine), d_visited(context), d_theories(0){} bool alreadyVisited(TNode current, TNode parent) { @@ -476,21 +476,18 @@ private: return false; } + Theory::Set theories = (*find).second; + TheoryId currentTheoryId = Theory::theoryOf(current); - if (Theory::setContains(currentTheoryId, find->second)) { + TheoryId parentTheoryId = Theory::theoryOf(parent); + + if (Theory::setContains(currentTheoryId, theories)) { // The current theory has already visited it, so now it depends on the parent - TheoryId parentTheoryId = Theory::theoryOf(parent); - if (parentTheoryId == currentTheoryId) { - // If it's the same theory, we've visited it already - Debug("register::internal") << "2:true" << std::endl; - return true; - } - // If not the same theory, we might have visited it, just check - Debug("register::internal") << (Theory::setContains(parentTheoryId, find->second) ? "3:true" : "3:false") << std::endl; - return Theory::setContains(parentTheoryId, find->second); + Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl; + return Theory::setContains(parentTheoryId, theories); } else { // If the current theory is not registered, it still needs to be visited - Debug("register::internal") << "4:false" << std::endl; + Debug("register::internal") << "2:false" << std::endl; return false; } } @@ -506,44 +503,21 @@ private: TheoryId currentTheoryId = Theory::theoryOf(current); TheoryId parentTheoryId = Theory::theoryOf(parent); - if (currentTheoryId == parentTheoryId) { - // If it's the same theory we just add it - TNodeVisitedMap::iterator find = d_visited.find(current); - if (find == d_visited.end()) { - d_visited[current] = Theory::setInsert(currentTheoryId); - } else { - find->second = Theory::setInsert(currentTheoryId, find->second); - } - // Visit it + Theory::Set theories = d_visited[current]; + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl; + if (!Theory::setContains(currentTheoryId, theories)) { + d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories); d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); - // Mark the theory as active d_theories = Theory::setInsert(currentTheoryId, d_theories); - } else { - // If two theories, one might have visited it already - // If it's the same theory we just add it - TNodeVisitedMap::iterator find = d_visited.find(current); - if (find == d_visited.end()) { - // If not in the map at all, we just add both - d_visited[current] = Theory::setInsert(parentTheoryId, Theory::setInsert(currentTheoryId)); - // And visit both - d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); - d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current); - // Mark both theories as active - d_theories = Theory::setInsert(currentTheoryId, d_theories); - d_theories = Theory::setInsert(parentTheoryId, d_theories); - } else { - if (!Theory::setContains(currentTheoryId, find->second)) { - find->second = Theory::setInsert(currentTheoryId, find->second); - d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); - d_theories = Theory::setInsert(currentTheoryId, d_theories); - } - if (!Theory::setContains(parentTheoryId, find->second)) { - find->second = Theory::setInsert(parentTheoryId, find->second); - d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current); - d_theories = Theory::setInsert(parentTheoryId, d_theories); - } - } + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; + } + if (!Theory::setContains(parentTheoryId, theories)) { + d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories); + d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(parentTheoryId, d_theories); + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; } + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl; Assert(d_visited.find(current) != d_visited.end()); Assert(alreadyVisited(current, parent)); diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index bb5c46945..4f3879560 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -100,7 +100,7 @@ public: /** * Creates a new node, which is in a list of it's own. */ - UseListNode(EqualityNodeId nodeId, UseListNodeId nextId) + UseListNode(EqualityNodeId nodeId = null_id, UseListNodeId nextId = null_uselist_id) : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {} /** @@ -198,6 +198,15 @@ public: d_useList = newUseId; } + /** + * For backtracking: remove the first element from the uselist and pop the memory. + */ + template + void removeTopFromUseList(memory_class& memory) { + Assert ((int)d_useList == (int)memory.size() - 1); + d_useList = memory.back().getNext(); + memory.pop_back(); + } }; template @@ -241,7 +250,7 @@ public: bool operator == (const FunctionApplication& other) const { return a == other.a && b == other.b; } - bool isApplication() { + bool isApplication() const { return a != null_id && b != null_id; } }; @@ -278,17 +287,23 @@ private: /** Map from ids to the nodes */ std::vector d_nodes; - /** Map from ids to the nodes */ + /** A context-dependents count of nodes */ + context::CDO d_nodesCount; + + /** Map from ids to the applications */ std::vector d_applications; /** Map from ids to the equality nodes */ std::vector d_equalityNodes; + /** Number of asserted equalities we have so far */ + context::CDO d_assertedEqualitiesCount; + /** Memory for the use-list nodes */ std::vector d_useListNodes; - /** Number of asserted equalities we have so far */ - context::CDO d_assertedEqualitiesCount; + /** Context dependent size of the use-list memory */ + context::CDO d_useListNodeSize; /** * We keep a list of asserted equalities. Not among original terms, but @@ -415,12 +430,12 @@ private: /** Next trigger for class 1 */ TriggerId nextTrigger; - Trigger(EqualityNodeId classId, TriggerId nextTrigger) + Trigger(EqualityNodeId classId = null_id, TriggerId nextTrigger = null_trigger) : classId(classId), nextTrigger(nextTrigger) {} }; /** - * Vector of triggers (persistent and not-backtrackable). Triggers come in pairs for an + * Vector of triggers. Triggers come in pairs for an * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When * updating triggers we always know where the other one is (^1). */ @@ -431,6 +446,11 @@ private: */ std::vector d_equalityTriggersOriginal; + /** + * Context dependent count of triggers + */ + context::CDO d_equalityTriggersCount; + /** * Trigger lists per node. The begin id changes as we merge, but the end always points to * the actual end of the triggers for this node. @@ -493,7 +513,14 @@ public: * the owner information. */ EqualityEngine(NotifyClass& notify, context::Context* context, std::string name) - : ContextNotifyObj(context), d_notify(notify), d_assertedEqualitiesCount(context, 0), d_stats(name) { + : ContextNotifyObj(context), + d_notify(notify), + d_nodesCount(context, 0), + d_assertedEqualitiesCount(context, 0), + d_useListNodeSize(context, 0), + d_equalityTriggersCount(context, 0), + d_stats(name) + { Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl; Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl; Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl; diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index cc73e1917..1dd9963f7 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -41,19 +41,20 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, E // Get another id for this EqualityNodeId funId = newNode(original, true); - FunctionApplication fun(t1, t2); - d_applications[funId] = fun; - - // The function application we're creating + // The function application we're creating EqualityNodeId t1ClassId = getEqualityNode(t1).getFind(); EqualityNodeId t2ClassId = getEqualityNode(t2).getFind(); FunctionApplication funNormalized(t1ClassId, t2ClassId); + // We add the normalized version, the term needs to be re-added on each backtrack + d_applications[funId] = funNormalized; + // Add the lookup data, if it's not already there typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); if (find == d_applicationLookup.end()) { // When we backtrack, if the lookup is not there anymore, we'll add it again Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl; + // Mark the normalization to the lookup d_applicationLookup[funNormalized] = funId; } else { // If it's there, we need to merge these two @@ -65,6 +66,7 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, E // Add to the use lists d_equalityNodes[t1].usedIn(funId, d_useListNodes); d_equalityNodes[t2].usedIn(funId, d_useListNodes); + d_useListNodeSize = d_useListNodes.size(); // Return the new id Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl; @@ -93,6 +95,9 @@ EqualityNodeId EqualityEngine::newNode(TNode node, bool isApplicati // Add the equality node to the nodes d_equalityNodes.push_back(EqualityNode(newId)); + // Increase the counters + d_nodesCount = d_nodesCount + 1; + Debug("equality") << "EqualityEngine::newNode(" << node << ", " << (isApplication ? "function" : "regular") << ") => " << newId << std::endl; return newId; @@ -433,6 +438,37 @@ void EqualityEngine::backtrack() { d_equalityEdges.resize(2 * d_assertedEqualitiesCount); } + + if (d_nodes.size() > d_nodesCount) { + // Go down the nodes, check the application nodes and remove them from use-lists + for(int i = d_nodes.size() - 1, i_end = (int)d_nodesCount; i >= i_end; ++ i) { + // Remove from the node -> id map + d_nodeIds.erase(d_nodes[i]); + + const FunctionApplication& app = d_applications[i]; + if (app.isApplication()) { + // Remove from the applications map + d_applicationLookup.erase(app); + // Remove b from use-list + getEqualityNode(app.b).removeTopFromUseList(d_useListNodes); + // Remove a from use-list + getEqualityNode(app.a).removeTopFromUseList(d_useListNodes); + } + } + + // Now get rid of the nodes and the rest + d_nodes.resize(d_nodesCount); + d_applications.resize(d_nodesCount); + d_nodeTriggers.resize(d_nodesCount); + d_equalityGraph.resize(d_nodesCount); + d_equalityNodes.resize(d_nodesCount); + d_useListNodes.resize(d_useListNodeSize); + } + + if (d_equalityTriggers.size() > d_equalityTriggersCount) { + d_equalityTriggers.resize(d_equalityTriggersCount); + d_equalityTriggersOriginal.resize(d_equalityTriggersCount); + } } template @@ -601,6 +637,9 @@ void EqualityEngine::addTriggerEquality(TNode t1, TNode t2, TNode t d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId)); d_equalityTriggersOriginal.push_back(trigger); + // Update the counters + d_equalityTriggersCount = d_equalityTriggersCount + 2; + // Add the trigger to the trigger graph d_nodeTriggers[t1Id] = t1NewTriggerId; d_nodeTriggers[t2Id] = t2NewTriggerId; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index a3eeec633..3c8d59d08 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -153,6 +153,7 @@ void TheoryUF::preRegisterTerm(TNode node) { d_equalityEngine.addTriggerEquality(node, d_true, node); d_equalityEngine.addTriggerEquality(node, d_false, node.notNode()); } + break; default: // Variables etc d_equalityEngine.addTerm(node); -- 2.30.2