*/
ApplicationIdsMap d_applicationLookup;
- /** Map from ids to the nodes */
- std::vector<TNode> d_nodes;
+ /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */
+ std::vector<Node> d_nodes;
/** A context-dependents count of nodes */
context::CDO<size_t> d_nodesCount;
/** Memory for the use-list nodes */
std::vector<UseListNode> d_useListNodes;
- /** 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
* among the class representatives.
/**
* Vector of original equalities of the triggers.
*/
- std::vector<TNode> d_equalityTriggersOriginal;
+ std::vector<Node> d_equalityTriggersOriginal;
/**
* Context dependent count of triggers
/**
* Get an explanation of the equality t1 = t2. Returns the asserted equalities that
* imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
- * else. TODO: mark the phantom equalities (skolems).
+ * else.
*/
void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const;
d_notify(notify),
d_nodesCount(context, 0),
d_assertedEqualitiesCount(context, 0),
- d_useListNodeSize(context, 0),
d_equalityTriggersCount(context, 0),
d_stats(name)
{
}
// Add to the use lists
- d_equalityNodes[t1].usedIn(funId, d_useListNodes);
- d_equalityNodes[t2].usedIn(funId, d_useListNodes);
- d_useListNodeSize = d_useListNodes.size();
+ d_equalityNodes[t1ClassId].usedIn(funId, d_useListNodes);
+ d_equalityNodes[t2ClassId].usedIn(funId, d_useListNodes);
// Return the new id
Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl;
d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
}
+ if (d_equalityTriggers.size() > d_equalityTriggersCount) {
+ // Unlink the triggers from the lists
+ for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) {
+ const Trigger& trigger = d_equalityTriggers[i];
+ d_nodeTriggers[trigger.classId] = trigger.nextTrigger;
+ }
+ // Get rid of the triggers
+ d_equalityTriggers.resize(d_equalityTriggersCount);
+ d_equalityTriggersOriginal.resize(d_equalityTriggersCount);
+ }
+
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) {
+ for(int i = d_nodes.size() - 1, i_end = (int)d_nodesCount; i >= i_end; -- i) {
// Remove from the node -> id map
+ Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl;
d_nodeIds.erase(d_nodes[i]);
const FunctionApplication& app = d_applications[i];
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);
}
}
d_equalityTriggersCount = d_equalityTriggersCount + 2;
// Add the trigger to the trigger graph
- d_nodeTriggers[t1Id] = t1NewTriggerId;
- d_nodeTriggers[t2Id] = t2NewTriggerId;
+ d_nodeTriggers[t1classId] = t1NewTriggerId;
+ d_nodeTriggers[t2classId] = t2NewTriggerId;
// If the trigger is already on, we propagate
if (t1classId == t2classId) {
if (d_conflict) {
Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl;
d_out->conflict(d_conflictNode);
- d_literalsToPropagate.clear();
}
// Otherwise we propagate in order to detect a weird conflict like
void TheoryUF::propagate(Effort level) {
Debug("uf") << "TheoryUF::propagate()" << std::endl;
if (!d_conflict) {
- for (unsigned i = 0; i < d_literalsToPropagate.size(); ++ i) {
- TNode literal = d_literalsToPropagate[i];
+ for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+ TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
bool satValue;
if (!d_valuation.hasSatValue(literal, satValue)) {
}
}
}
- d_literalsToPropagate.clear();
}
void TheoryUF::preRegisterTerm(TNode node) {
namespace uf {
class TheoryUF : public Theory {
-
public:
class NotifyClass {
void explain(TNode literal, std::vector<TNode>& assumptions);
/** Literals to propagate */
- std::vector<TNode> d_literalsToPropagate;
+ context::CDList<TNode> d_literalsToPropagate;
+
+ /** Index of the next literal to propagate */
+ context::CDO<unsigned> d_literalsToPropagateIndex;
+
/** True node for predicates = true */
Node d_true;
d_notify(*this),
d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"),
d_knownFacts(ctxt),
- d_conflict(ctxt, false)
+ d_conflict(ctxt, false),
+ d_literalsToPropagate(ctxt),
+ d_literalsToPropagateIndex(ctxt, 0)
{
// The kinds we are treating as function application in congruence
d_equalityEngine.addFunctionKind(kind::APPLY_UF);