, d_nodesCount(context, 0)
, d_assertedEqualitiesCount(context, 0)
, d_equalityTriggersCount(context, 0)
+, d_nodesThatEvaluateSize(context, 0)
, d_stats(name)
+, d_inPropagate(false)
, d_triggerDatabaseSize(context, 0)
, d_triggerTermSetUpdatesSize(context, 0)
, d_deducedDisequalitiesSize(context, 0)
, d_nodesCount(context, 0)
, d_assertedEqualitiesCount(context, 0)
, d_equalityTriggersCount(context, 0)
+, d_nodesThatEvaluateSize(context, 0)
, d_stats(name)
+, d_inPropagate(false)
, d_triggerDatabaseSize(context, 0)
, d_triggerTermSetUpdatesSize(context, 0)
, d_deducedDisequalitiesSize(context, 0)
// Add the lookup data, if it's not already there
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") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl;
// Mark the normalization to the lookup
storeApplicationLookup(funNormalized, funId);
- // If an equality over constants we merge to false
- if (isEquality) {
- if (d_isConstant[t1ClassId] && d_isConstant[t2ClassId] && t1ClassId != t2ClassId) {
- Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl;
- Assert(d_nodes[funId].getKind() == kind::EQUAL);
- enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()), false);
- // Also enqueue the symmetric one
- TNode eq = d_nodes[funId];
- Node symmetricEq = eq[1].eqNode(eq[0]);
- if (hasTerm(symmetricEq)) {
- EqualityNodeId symmFunId = getNodeId(symmetricEq);
- enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()), false);
- }
- }
- if (t1ClassId == t2ClassId) {
- enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()), false);
- }
- }
} else {
// If it's there, we need to merge these two
Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl;
d_nodeIndividualTrigger.push_back(+null_set_id);
// Mark non-constant by default
d_isConstant.push_back(false);
+ // Makr non-evaluate by default
+ d_evaluates.push_back(false);
// Mark Boolean nodes
d_isBoolean.push_back(false);
// Mark the node as internal by default
return newId;
}
+void EqualityEngine::addFunctionKind(Kind fun, bool interpreted) {
+ d_congruenceKinds |= fun;
+ if (interpreted) {
+ Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl;
+ d_congruenceKindsInterpreted |= fun;
+ }
+}
+
void EqualityEngine::addTerm(TNode t) {
Debug("equality") << d_name << "::eq::addTerm(" << t << ")" << std::endl;
if (t.getKind() == kind::EQUAL) {
addTerm(t[0]);
addTerm(t[1]);
- result = newApplicationNode(t, getNodeId(t[0]), getNodeId(t[1]), true);
+ EqualityNodeId t0id = getNodeId(t[0]);
+ EqualityNodeId t1id = getNodeId(t[1]);
+ result = newApplicationNode(t, t0id, t1id, true);
d_isInternal[result] = false;
+
} else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) {
- // Add the operator
TNode tOp = t.getOperator();
+ // Add the operator
addTerm(tOp);
- // Add all the children and Curryfy
result = getNodeId(tOp);
d_isInternal[result] = true;
+ d_isConstant[result] = isInterpretedFunctionKind(t.getKind());
+ d_evaluates[result] = isInterpretedFunctionKind(t.getKind());
+ // Add all the children and Curryfy
for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
// Add the child
addTerm(t[i]);
result = newApplicationNode(t, result, getNodeId(t[i]), false);
}
d_isInternal[result] = false;
- d_isConstant[result] = t.isConst();
+ if (t.isConst()) {
+ d_isConstant[result] = true;
+ d_evaluates[result] = true;
+ }
} else {
// Otherwise we just create the new id
result = newNode(t);
+ // Is this an operator
d_isInternal[result] = false;
- d_isConstant[result] = t.isConst();
+ if (t.isConst()) {
+ d_isConstant[result] = true;
+ d_evaluates[result] = true;
+ }
}
if (t.getType().isBoolean()) {
d_masterEqualityEngine->addTerm(t);
}
+ // Empty the queue
propagate();
+ Assert(hasTerm(t));
+
Debug("equality") << d_name << "::eq::addTerm(" << t << ") => " << result << std::endl;
}
} else {
// There is no representative, so we can add one, we remove this when backtracking
storeApplicationLookup(funNormalized, funId);
- // Note: both checks below we don't need to do in the above case as the normalized lookup
- // has already been checked for this
- // Now, if we're constant and it's an equality, check if the other guy is also a constant
- if (fun.isEquality) {
- // If the equation normalizes to two constants, it's disequal
- if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) {
- Assert(d_nodes[funId].getKind() == kind::EQUAL);
- enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()), false);
- // Also enqueue the symmetric one
- TNode eq = d_nodes[funId];
- Node symmetricEq = eq[1].eqNode(eq[0]);
- if (hasTerm(symmetricEq)) {
- EqualityNodeId symmFunId = getNodeId(symmetricEq);
- enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()), false);
- }
- }
- // If the function normalizes to a = a, we merge it with true, we check that its not
- // already there so as not to enqueue multiple times when several things get merged
- if (aNormalized == bNormalized && getEqualityNode(funId).getFind() != d_trueId) {
- enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()), false);
- }
- }
}
// Go to the next one in the use list
d_applicationLookups.resize(d_applicationLookupsCount);
}
+ if (d_nodesThatEvaluate.size() > d_nodesThatEvaluateSize) {
+ for(int i = d_nodesThatEvaluate.size() - 1, i_end = (int)d_nodesThatEvaluateSize; i >= i_end; --i) {
+ d_evaluates[d_nodesThatEvaluate[i]] = false;
+ }
+ }
+
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) {
d_nodeTriggers.resize(d_nodesCount);
d_nodeIndividualTrigger.resize(d_nodesCount);
d_isConstant.resize(d_nodesCount);
+ d_evaluates.resize(d_nodesCount);
d_isBoolean.resize(d_nodesCount);
d_isInternal.resize(d_nodesCount);
d_equalityGraph.resize(d_nodesCount);
d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize);
d_deducedDisequalities.resize(d_deducedDisequalitiesSize);
}
+
}
void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
equalities.push_back(d_equalityEdges[currentEdge].getReason());
break;
case MERGED_THROUGH_REFLEXIVITY: {
- // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
+ // x1 == x1
Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode;
const FunctionApplication& eq = d_applications[eqId].original;
break;
}
case MERGED_THROUGH_CONSTANTS: {
- // (a = b) == false because a and b are different constants
- Debug("equality") << d_name << "::eq::getExplanation(): due to constants, going deeper" << std::endl;
- EqualityNodeId eqId = currentNode == d_falseId ? edgeNode : currentNode;
- const FunctionApplication& eq = d_applications[eqId].original;
- Assert(eq.isEquality, "Must be an equality");
-
+ // f(c1, ..., cn) = c semantically, we can just ignore it
+ Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl;
Debug("equality") << push;
- // Explain why a is a constant
- Assert(isConstant(eq.a));
- getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities);
- // Explain why b is a constant
- Assert(isConstant(eq.b));
- getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities);
+
+ // Get the node we interpreted
+ TNode interpreted = d_nodes[currentNode];
+ if (interpreted.isConst()) {
+ interpreted = d_nodes[edgeNode];
+ }
+
+ // Explain why a is a constant by explaining each argument
+ for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) {
+ EqualityNodeId childId = getNodeId(interpreted[i]);
+ Assert(isConstant(childId));
+ getExplanation(childId, getEqualityNode(childId).getFind(), equalities);
+ }
+
Debug("equality") << pop;
- // If the constants were merged, we're in trouble
- Assert(getEqualityNode(eq.a).getFind() != getEqualityNode(eq.b).getFind());
break;
}
Debug("equality") << d_name << "::eq::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
}
+Node EqualityEngine::evaluateTerm(TNode node) {
+ Debug("equality::evaluation") << d_name << "::eq::evaluateTerm(" << node << ")" << std::endl;
+ NodeBuilder<> builder;
+ builder << node.getKind();
+ if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << node.getOperator();
+ }
+ for (unsigned i = 0; i < node.getNumChildren(); ++ i) {
+ TNode child = node[i];
+ TNode childRep = getRepresentative(child);
+ Debug("equality::evaluation") << d_name << "::eq::evaluateTerm: " << child << " -> " << childRep << std::endl;
+ Assert(childRep.isConst());
+ builder << childRep;
+ }
+ Node newNode = builder;
+ return Rewriter::rewrite(newNode);
+}
+
+void EqualityEngine::processEvaluationQueue() {
+
+ Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): start" << std::endl;
+
+ while (!d_evaluationQueue.empty()) {
+ // Get the node
+ EqualityNodeId id = d_evaluationQueue.front();
+ d_evaluationQueue.pop();
+
+ // Replace the children with their representatives (must be constants)
+ Node nodeEvaluated = evaluateTerm(d_nodes[id]);
+ Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): " << d_nodes[id] << " evaluates to " << nodeEvaluated << std::endl;
+ Assert(nodeEvaluated.isConst());
+ addTerm(nodeEvaluated);
+ EqualityNodeId nodeEvaluatedId = getNodeId(nodeEvaluated);
+
+ // Enqueue the semantic equality
+ enqueue(MergeCandidate(id, nodeEvaluatedId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+ }
+
+ Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): done" << std::endl;
+}
+
+void EqualityEngine::evaluateApplication(const FunctionApplication& funNormalized, EqualityNodeId funId) {
+
+ // Evaluate special for equality and other
+ if (!funNormalized.isEquality) {
+ // We can't add new terms
+ d_evaluationQueue.push(funId);
+ } else {
+ if (funNormalized.a != funNormalized.b) {
+ // We don't enqueue fun -> true, as this is convered with reflexivity
+ enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+ }
+ }
+}
+
void EqualityEngine::propagate() {
+ if (d_inPropagate) {
+ // We're already in propagate, go back
+ return;
+ }
+
+ // Make sure we don't get in again
+ ScopedBool inPropagate(d_inPropagate, true);
+
Debug("equality") << d_name << "::eq::propagate()" << std::endl;
- while (!d_propagationQueue.empty()) {
-
- // The current merge candidate
- const MergeCandidate current = d_propagationQueue.front();
- d_propagationQueue.pop_front();
+ while (!d_propagationQueue.empty() || !d_evaluationQueue.empty()) {
if (d_done) {
// If we're done, just empty the queue
+ while (!d_propagationQueue.empty()) d_propagationQueue.pop_front();
+ while (!d_evaluationQueue.empty()) d_evaluationQueue.pop();
continue;
}
+
+ // Process any evaluation requests
+ if (!d_evaluationQueue.empty()) {
+ processEvaluationQueue();
+ continue;
+ }
+
+ // The current merge candidate
+ const MergeCandidate current = d_propagationQueue.front();
+ d_propagationQueue.pop_front();
// Get the representatives
EqualityNodeId t1classId = getEqualityNode(current.t1Id).getFind();
Debug("equality::backtrack") << "d_applicationLookupsCount = " << d_applicationLookupsCount << std::endl;
Debug("equality::backtrack") << "d_applicationLookups.size() = " << d_applicationLookups.size() << std::endl;
Assert(d_applicationLookupsCount == d_applicationLookups.size());
+
+ // If an equality over constants we merge to false
+ if (funNormalized.isEquality && funNormalized.a == funNormalized.b) {
+ enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));
+ }
+
+ // Now check for application evaluation
+ if (!d_evaluates[funId]) {
+ if (d_evaluates[funNormalized.a] && d_evaluates[funNormalized.b]) {
+ // Depending on the "internal"
+ if (d_isInternal[funId]) {
+ setEvaluates(funId);
+ } else {
+ evaluateApplication(funNormalized, funId);
+ }
+ }
+ }
}
void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) {
/** The map of kinds to be treated as function applications */
KindMap d_congruenceKinds;
+ /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */
+ KindMap d_congruenceKindsInterpreted;
+
/** Map from nodes to their ids */
__gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
*/
std::vector<bool> d_isConstant;
+ /**
+ * Map from ids to whether they evaluate. A node evaluates
+ * (1) if it is a constant
+ * (2) if it is internal and it's children evaluate
+ * (3) if it is non-internal and it's children are constants
+ *
+ * Example:
+ *
+ * f(x) + g(y)
+ *
+ * If f and g are interpreted, in the context x = 0, the nodes
+ * f(x) and g(y) evaluate, but not f(x) + g(y). The term f(x) + g(y)
+ * evaluates if we evaluate f(0) and g(0) to constants c1 and c2.
+ */
+ std::vector<bool> d_evaluates;
+
+ /**
+ * For nodes that we need to postpone evaluation.
+ */
+ std::queue<EqualityNodeId> d_evaluationQueue;
+
+ /**
+ * Evaluate all terms in the evaluation queue.
+ */
+ void processEvaluationQueue();
+
+ /**
+ * Check whether the node evaluates in the current context
+ */
+ bool evaluates(EqualityNodeId id) const {
+ return d_evaluates[id];
+ }
+
+ /** Vector of nodes that evaluate. */
+ std::vector<EqualityNodeId> d_nodesThatEvaluate;
+
+ /** Size of the nodes that evaluate vector. */
+ context::CDO<unsigned> d_nodesThatEvaluateSize;
+
+ /** Set the node evaluate flag */
+ void setEvaluates(EqualityNodeId id) {
+ Assert(!d_evaluates[id]);
+ d_evaluates[id] = true;
+ d_nodesThatEvaluate.push_back(id);
+ d_nodesThatEvaluateSize = d_nodesThatEvaluate.size();
+ }
+
+ /**
+ * Propagate something that evaluates.
+ * @param fragile if true, no new terms are added, but
+ */
+ void evaluateApplication(const FunctionApplication& funNormalized, EqualityNodeId funId);
+
+ /**
+ * Returns the evaluation of the term when all (direct) children are replaced with
+ * the constant representatives.
+ */
+ Node evaluateTerm(TNode node);
+
/**
* Returns true if it's a constant
*/
/** Enqueue to the propagation queue */
void enqueue(const MergeCandidate& candidate, bool back = true);
-
+
/** Do the propagation */
void propagate();
+ /** Are we in propagate */
+ bool d_inPropagate;
+
/**
* 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
/**
* Add a kind to treat as function applications.
*/
- void addFunctionKind(Kind fun) {
- d_congruenceKinds |= fun;
- }
+ void addFunctionKind(Kind fun, bool interpreted = false);
/**
* Returns true if this kind is used for congruence closure.
*/
- bool isFunctionKind(Kind fun) {
+ bool isFunctionKind(Kind fun) const {
return d_congruenceKinds.tst(fun);
}
/**
- * Adds a function application term to the database.
+ * Returns true if this kind is used for congruencce closure + evaluation of constants.
*/
+ bool isInterpretedFunctionKind(Kind fun) const {
+ return d_congruenceKindsInterpreted.tst(fun);
+ }
/**
* Check whether the node is already in the database.
projects / cvc5.git / commitdiff