summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/main/main.cpp2
-rw-r--r--src/parser/cvc/cvc_input.h2
-rw-r--r--src/parser/parser_builder.cpp1
-rw-r--r--src/parser/smt/smt_input.h2
-rw-r--r--src/prop/cnf_stream.cpp3
-rw-r--r--src/prop/minisat/core/Solver.cc12
-rw-r--r--src/prop/minisat/core/Solver.h13
-rw-r--r--src/prop/sat.cpp4
-rw-r--r--src/prop/sat.h11
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/theory.h2
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/theory_engine.h72
-rw-r--r--src/theory/uf/equality_engine.h43
-rw-r--r--src/theory/uf/equality_engine_impl.h47
-rw-r--r--src/theory/uf/theory_uf.cpp1
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<VarIntroInfo> 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<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
+ typedef context::CDMap<TNode, theory::Theory::Set, TNodeHashFunction> 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<typename memory_class>
+ void removeTopFromUseList(memory_class& memory) {
+ Assert ((int)d_useList == (int)memory.size() - 1);
+ d_useList = memory.back().getNext();
+ memory.pop_back();
+ }
};
template <typename NotifyClass>
@@ -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<TNode> d_nodes;
- /** Map from ids to the nodes */
+ /** A context-dependents count of nodes */
+ context::CDO<size_t> d_nodesCount;
+
+ /** Map from ids to the applications */
std::vector<FunctionApplication> d_applications;
/** Map from ids to the equality nodes */
std::vector<EqualityNode> d_equalityNodes;
+ /** Number of asserted equalities we have so far */
+ context::CDO<size_t> d_assertedEqualitiesCount;
+
/** Memory for the use-list nodes */
std::vector<UseListNode> d_useListNodes;
- /** Number of asserted equalities we have so far */
- context::CDO<size_t> d_assertedEqualitiesCount;
+ /** Context dependent size of the use-list memory */
+ context::CDO<size_t> 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).
*/
@@ -432,6 +447,11 @@ private:
std::vector<TNode> d_equalityTriggersOriginal;
/**
+ * Context dependent count of triggers
+ */
+ context::CDO<size_t> 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<NotifyClass>::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<NotifyClass>::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<NotifyClass>::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<NotifyClass>::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 <typename NotifyClass>
@@ -601,6 +637,9 @@ void EqualityEngine<NotifyClass>::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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback