pStatistics->flushStatistics(*options.err);
}
exit(1);
- } catch(bad_alloc) {
+ } catch(bad_alloc&) {
#ifdef CVC4_COMPETITION_MODE
*options.out << "unknown" << endl;
#endif
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() {
break;
default:
parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
+ break;
}
if( d_checksEnabled ) {
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() {
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 {
//Node atomic = handleNonAtomicNode(node);
//return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
}
+ break;
}
}
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;
}
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);
+ }
}
}
/** 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:
//
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);
}
return Minisat::var(lit);
}
+inline SatLiteral variableToLiteral(SatVariable var) {
+ return Minisat::mkLit(var);
+}
+
inline bool literalSign(SatLiteral lit) {
return Minisat::sign(lit);
}
TheoryEngine* theoryEngine,
context::Context* context);
- ~SatSolver();
+ virtual ~SatSolver();
bool solve();
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);
public:
TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation);
- ~TheoryArith();
+ virtual ~TheoryArith();
/**
* Does non-context dependent setup for a node connected to a theory.
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);
}
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;
/**
* 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;
/**
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) {
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;
}
}
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));
/**
* 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) {}
/**
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>
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;
}
};
/** 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
/** 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).
*/
*/
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.
* 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;
// 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
// 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;
// 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;
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>
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;
d_equalityEngine.addTriggerEquality(node, d_true, node);
d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
}
+ break;
default:
// Variables etc
d_equalityEngine.addTerm(node);
projects / cvc5.git / commitdiff