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;
+
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
+
addTerm(d_true);
addTerm(d_false);
+ d_trueId = getNodeId(d_true);
+ d_falseId = getNodeId(d_false);
+
d_triggerDatabaseAllocatedSize = 100000;
d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
}
EqualityEngine::EqualityEngine(context::Context* context, std::string name)
: ContextNotifyObj(context)
, d_context(context)
+, d_done(context, false)
, d_performNotify(true)
, d_notify(s_notifyNone)
, d_applicationLookupsCount(context, 0)
, d_nodesCount(context, 0)
, d_assertedEqualitiesCount(context, 0)
, d_equalityTriggersCount(context, 0)
-, d_constantRepresentativesSize(context, 0)
-, d_constantsSize(context, 0)
, d_stats(name)
, d_triggerDatabaseSize(context, 0)
, d_triggerTermSetUpdatesSize(context, 0)
EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* context, std::string name)
: ContextNotifyObj(context)
, d_context(context)
+, d_done(context, false)
, d_performNotify(true)
, d_notify(notify)
, d_applicationLookupsCount(context, 0)
, d_nodesCount(context, 0)
, d_assertedEqualitiesCount(context, 0)
, d_equalityTriggersCount(context, 0)
-, d_constantRepresentativesSize(context, 0)
-, d_constantsSize(context, 0)
, d_stats(name)
, d_triggerDatabaseSize(context, 0)
, d_triggerTermSetUpdatesSize(context, 0)
}
void EqualityEngine::enqueue(const MergeCandidate& candidate) {
- Debug("equality") << "EqualityEngine::enqueue(" << candidate.toString(*this) << ")" << std::endl;
d_propagationQueue.push(candidate);
}
-EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2) {
+EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) {
Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl;
++ d_stats.functionTermsCount;
// Get another id for this
EqualityNodeId funId = newNode(original);
- FunctionApplication funOriginal(t1, t2);
+ FunctionApplication funOriginal(isEquality, t1, t2);
// The function application we're creating
EqualityNodeId t1ClassId = getEqualityNode(t1).getFind();
EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
- FunctionApplication funNormalized(t1ClassId, t2ClassId);
+ FunctionApplication funNormalized(isEquality, t1ClassId, t2ClassId);
// We add the original version
d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized);
Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl;
// Mark the normalization to the lookup
storeApplicationLookup(funNormalized, funId);
+ // If an equality, we do some extra reasoning
+ if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) {
+ if (t1ClassId != t2ClassId) {
+ Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl;
+ enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+ }
+ }
} else {
// If it's there, we need to merge these two
Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl;
enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
- propagate();
}
// Add to the use lists
// Mark the no-individual trigger
d_nodeIndividualTrigger.push_back(+null_set_id);
// Mark non-constant by default
- d_constantRepresentative.push_back(node.isConst() ? newId : +null_id);
+ d_isConstant.push_back(node.isConst());
+ // Mark Boolean nodes
+ d_isBoolean.push_back(false);
// Add the equality node to the nodes
d_equalityNodes.push_back(EqualityNode(newId));
Debug("equality") << "EqualityEngine::newNode(" << node << ") => " << newId << std::endl;
- // If the node is a constant, assert all the dis-eqalities
- if (node.isConst() && node.getKind() != kind::CONST_BOOLEAN) {
-
- TypeNode nodeType = node.getType();
- for (unsigned i = 0; i < d_constants.size(); ++ i) {
- TNode constant = d_constants[i];
- if (constant.getType().isComparableTo(nodeType)) {
- Debug("equality::constants") << "adding const dis-equality " << node << " != " << constant << std::endl;
- assertEquality(node.eqNode(constant), false, d_true);
- }
- }
-
- d_constants.push_back(node);
- d_constantsSize = d_constantsSize + 1;
-
- propagate();
- }
-
return newId;
}
EqualityNodeId result;
- // If a function application we go in
- if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()])
- {
+ if (t.getKind() == kind::EQUAL) {
+ addTerm(t[0]);
+ addTerm(t[1]);
+ result = newApplicationNode(t, getNodeId(t[0]), getNodeId(t[1]), true);
+ } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) {
// Add the operator
TNode tOp = t.getOperator();
addTerm(tOp);
// Add the child
addTerm(t[i]);
// Add the application
- result = newApplicationNode(t, result, getNodeId(t[i]));
+ result = newApplicationNode(t, result, getNodeId(t[i]), false);
}
} else {
// Otherwise we just create the new id
result = newNode(t);
}
+ if (t.getType().isBoolean()) {
+ // We set this here as this only applies to actual terms, not the
+ // intermediate application terms
+ d_isBoolean[result] = true;
+ }
+
+ propagate();
+
Debug("equality") << "EqualityEngine::addTerm(" << t << ") => " << result << std::endl;
}
EqualityNodeId class1Id = class1.getFind();
EqualityNodeId class2Id = class2.getFind();
+ // Check for constant merges
+ bool isConstant = d_isConstant[class1Id];
+ if (isConstant && d_isConstant[class2Id]) {
+ if (d_performNotify) {
+ if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) {
+ // Now merge the so that backtracking is OK
+ class1.merge<true>(class2);
+ return false;
+ }
+ }
+ }
// Update class2 representative information
Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl;
EqualityNodeId currentId = class2Id;
} while (currentId != class2Id);
- // Update class2 table lookup and information
- Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
- do {
- // Get the current node
- EqualityNode& currentNode = getEqualityNode(currentId);
- Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
+ // Update class2 table lookup and information if not a boolean
+ // since booleans can't be in an application
+ if (!d_isBoolean[class2Id]) {
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
+ do {
+ // Get the current node
+ EqualityNode& currentNode = getEqualityNode(currentId);
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
- // Go through the uselist and check for congruences
- UseListNodeId currentUseId = currentNode.getUseList();
- while (currentUseId != null_uselist_id) {
- // Get the node of the use list
- UseListNode& useNode = d_useListNodes[currentUseId];
- // Get the function application
- EqualityNodeId funId = useNode.getApplicationId();
- Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
- const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
- // Check if there is an application with find arguments
- EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
- EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
- FunctionApplication funNormalized(aNormalized, bNormalized);
- ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
- if (find != d_applicationLookup.end()) {
- // Applications fun and the funNormalized can be merged due to congruence
- if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) {
- enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
+ // Go through the uselist and check for congruences
+ UseListNodeId currentUseId = currentNode.getUseList();
+ while (currentUseId != null_uselist_id) {
+ // Get the node of the use list
+ UseListNode& useNode = d_useListNodes[currentUseId];
+ // Get the function application
+ EqualityNodeId funId = useNode.getApplicationId();
+ Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
+ const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
+ // Check if there is an application with find arguments
+ EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
+ EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
+ FunctionApplication funNormalized(fun.isEquality, aNormalized, bNormalized);
+ ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
+ if (find != d_applicationLookup.end()) {
+ // Applications fun and the funNormalized can be merged due to congruence
+ if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) {
+ enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
+ }
+ } else {
+ // There is no representative, so we can add one, we remove this when backtracking
+ storeApplicationLookup(funNormalized, funId);
+ // Now, if we're constant and it's an equality, check if the other guy is also a constant
+ if (isConstant && funNormalized.isEquality) {
+ if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) {
+ // both constants
+ if (funNormalized.a != funNormalized.b) {
+ enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+ }
+ }
+ }
}
- } else {
- // There is no representative, so we can add one, we remove this when backtracking
- storeApplicationLookup(funNormalized, funId);
+
+ // Go to the next one in the use list
+ currentUseId = useNode.getNext();
}
- // Go to the next one in the use list
- currentUseId = useNode.getNext();
- }
-
- // Move to the next node
- currentId = currentNode.getNext();
- } while (currentId != class2Id);
-
+
+ // Move to the next node
+ currentId = currentNode.getNext();
+ } while (currentId != class2Id);
+ }
+
// Now merge the lists
class1.merge<true>(class2);
-
- // Check for constants
- EqualityNodeId class2constId = d_constantRepresentative[class2Id];
- if (class2constId != +null_id) {
- EqualityNodeId class1constId = d_constantRepresentative[class1Id];
- if (class1constId != +null_id) {
- if (d_performNotify) {
- TNode const1 = d_nodes[class1constId];
- TNode const2 = d_nodes[class2constId];
- if (!d_notify.eqNotifyConstantTermMerge(const1, const2)) {
- return false;
- }
- }
- } else {
- // If the class we're merging in is constant, mark the representative as constant
- d_constantRepresentative[class1Id] = d_constantRepresentative[class2Id];
- d_constantRepresentatives.push_back(class1Id);
- d_constantRepresentativesSize = d_constantRepresentativesSize + 1;
- }
- }
-
+
// Notify the trigger term merges
TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id];
if (class2triggerRef != +null_set_id) {
d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize);
}
- if (d_constantRepresentatives.size() > d_constantRepresentativesSize) {
- // Unset the constant representatives
- for (int i = d_constantRepresentatives.size() - 1, i_end = d_constantRepresentativesSize; i >= i_end; -- i) {
- d_constantRepresentative[d_constantRepresentatives[i]] = +null_id;
- }
- d_constantRepresentatives.resize(d_constantRepresentativesSize);
- }
-
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) {
d_applications.resize(d_nodesCount);
d_nodeTriggers.resize(d_nodesCount);
d_nodeIndividualTrigger.resize(d_nodesCount);
- d_constantRepresentative.resize(d_nodesCount);
+ d_isConstant.resize(d_nodesCount);
+ d_isBoolean.resize(d_nodesCount);
d_equalityGraph.resize(d_nodesCount);
d_equalityNodes.resize(d_nodesCount);
}
-
- d_constants.resize(d_constantsSize);
}
void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) {
addTerm(p);
// Get the explanation
- getExplanation(getNodeId(p), getNodeId(polarity ? d_true : d_false), assertions);
+ getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions);
}
void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const {
Debug("equality") << "EqualityEngine::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl;
- Assert(getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind());
+ // We can only explain the nodes that got merged (or between
+ // constants since they didn't get merged but we stil added the
+ // edge in the graph equality
+ Assert(getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind() ||
+ (d_isConstant[getEqualityNode(t1Id).getFind()] && d_isConstant[getEqualityNode(t2Id).getFind()]));
// If the nodes are the same, we're done
if (t1Id == t2Id) return;
Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
// Add the actual equality to the vector
- if (reasonType == MERGED_THROUGH_CONGRUENCE) {
+ switch (reasonType) {
+ case MERGED_THROUGH_CONGRUENCE: {
// f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl;
const FunctionApplication& f1 = d_applications[currentNode].original;
getExplanation(f1.a, f2.a, equalities);
getExplanation(f1.b, f2.b, equalities);
Debug("equality") << pop;
- } else {
+ break;
+ }
+ case MERGED_THROUGH_EQUALITY:
// Construct the equality
Debug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
equalities.push_back(d_equalityEdges[currentEdge].getReason());
+ break;
+ case MERGED_THROUGH_CONSTANTS: {
+ // (a = b) == false bacause a and b are different constants
+ Debug("equality") << "EqualityEngine::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");
+
+ Debug("equality") << push;
+ // Explain why a is a constant
+ getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities);
+ // Explain why b is a constant
+ getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities);
+ Debug("equality") << pop;
+
+ break;
}
-
+ default:
+ Unreachable();
+ }
+
// Go to the previous
currentEdge = bfsQueue[currentIndex].edgeId;
currentIndex = bfsQueue[currentIndex].previousIndex;
+
} while (currentEdge != null_id);
// Done
Debug("equality") << "EqualityEngine::propagate()" << std::endl;
- bool done = false;
while (!d_propagationQueue.empty()) {
// The current merge candidate
const MergeCandidate current = d_propagationQueue.front();
d_propagationQueue.pop();
- if (done) {
+ if (d_done) {
// If we're done, just empty the queue
continue;
}
// One more equality added
d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
- // Depending on the merge preference (such as size), merge them
+ // Depending on the merge preference (such as size, or being a constant), merge them
std::vector<TriggerId> triggers;
- if (node2.getSize() > node1.getSize()) {
+ if (node2.getSize() > node1.getSize() || d_isConstant[t2classId]) {
Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
d_assertedEqualities.push_back(Equality(t2classId, t1classId));
- done = !merge(node2, node1, triggers);
+ if (!merge(node2, node1, triggers)) {
+ d_done = true;
+ }
} else {
Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl;
d_assertedEqualities.push_back(Equality(t1classId, t2classId));
- done = !merge(node1, node2, triggers);
+ if (!merge(node1, node2, triggers)) {
+ d_done = true;
+ }
}
// Notify the triggers
- if (d_performNotify && !done) {
- for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !done; ++ trigger_i) {
+ if (d_performNotify && !d_done) {
+ for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) {
const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]];
// Notify the trigger and exit if it fails
if (triggerInfo.trigger.getKind() == kind::EQUAL) {
- done = !d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity);
+ if (!d_notify.eqNotifyTriggerEquality(triggerInfo.trigger, triggerInfo.polarity)) {
+ d_done = true;
+ }
} else {
- done = !d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity);
+ if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.trigger, triggerInfo.polarity)) {
+ d_done = true;
+ }
}
}
}
#include <queue>
#include <vector>
#include <ext/hash_map>
-#include <sstream>
#include "expr/node.h"
#include "expr/kind_map.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
+#include "theory/uf/equality_engine_types.h"
+
namespace CVC4 {
namespace theory {
namespace eq {
-/** Id of the node */
-typedef size_t EqualityNodeId;
-
-/** Id of the use list */
-typedef size_t UseListNodeId;
-
-/** The trigger ids */
-typedef size_t TriggerId;
-
-/** The equality edge ids */
-typedef size_t EqualityEdgeId;
-
-/** The null node */
-static const EqualityNodeId null_id = (size_t)(-1);
-
-/** The null use list node */
-static const EqualityNodeId null_uselist_id = (size_t)(-1);
-
-/** The null trigger */
-static const TriggerId null_trigger = (size_t)(-1);
-
-/** The null edge id */
-static const EqualityEdgeId null_edge = (size_t)(-1);
-
-/**
- * A reason for a merge. Either an equality x = y, or a merge of two
- * function applications f(x1, x2), f(y1, y2)
- */
-enum MergeReasonType {
- MERGED_THROUGH_CONGRUENCE,
- MERGED_THROUGH_EQUALITY
-};
-
-inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
- switch (reason) {
- case MERGED_THROUGH_CONGRUENCE:
- out << "c";
- break;
- case MERGED_THROUGH_EQUALITY:
- out << "e";
- break;
- default:
- Unreachable();
- }
- return out;
-}
-
-/** A node in the uselist */
-class UseListNode {
-
-private:
-
- /** The id of the application node where this representative is at */
- EqualityNodeId d_applicationId;
-
- /** The next one in the class */
- UseListNodeId d_nextUseListNodeId;
-
-public:
-
- /**
- * Creates a new node, which is in a list of it's own.
- */
- UseListNode(EqualityNodeId nodeId = null_id, UseListNodeId nextId = null_uselist_id)
- : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {}
-
- /**
- * Returns the next node in the circular list.
- */
- UseListNodeId getNext() const {
- return d_nextUseListNodeId;
- }
-
- /**
- * Returns the id of the function application.
- */
- EqualityNodeId getApplicationId() const {
- return d_applicationId;
- }
-};
-
-
-class EqualityNode {
-
-private:
-
- /** The size of this equivalence class (if it's a representative) */
- size_t d_size;
-
- /** The id (in the eq-manager) of the representative equality node */
- EqualityNodeId d_findId;
-
- /** The next equality node in this class */
- EqualityNodeId d_nextId;
-
- /** The use list of this node */
- UseListNodeId d_useList;
-
-public:
-
- /**
- * Creates a new node, which is in a list of it's own.
- */
- EqualityNode(EqualityNodeId nodeId = null_id)
- : d_size(1),
- d_findId(nodeId),
- d_nextId(nodeId),
- d_useList(null_uselist_id)
- {}
-
- /**
- * Retuerns the uselist.
- */
- UseListNodeId getUseList() const {
- return d_useList;
- }
-
- /**
- * Returns the next node in the class circular list.
- */
- EqualityNodeId getNext() const {
- return d_nextId;
- }
-
- /**
- * Returns the size of this equivalence class (only valid if this is the representative).
- */
- size_t getSize() const {
- return d_size;
- }
-
- /**
- * Merges the two lists. If add size is true the size of this node is increased by the size of
- * the other node, otherwise the size is decreased by the size of the other node.
- */
- template<bool addSize>
- void merge(EqualityNode& other) {
- EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
- if (addSize) {
- d_size += other.d_size;
- } else {
- d_size -= other.d_size;
- }
- }
-
- /**
- * Returns the class representative.
- */
- EqualityNodeId getFind() const { return d_findId; }
-
- /**
- * Set the class representative.
- */
- void setFind(EqualityNodeId findId) { d_findId = findId; }
-
- /**
- * Note that this node is used in a function a application funId.
- */
- template<typename memory_class>
- void usedIn(EqualityNodeId funId, memory_class& memory) {
- UseListNodeId newUseId = memory.size();
- memory.push_back(UseListNode(funId, d_useList));
- 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();
- }
-};
-
/**
* Interface for equality engine notifications. All the notifications
* are safe as TNodes, but not necessarily for negations.
}
};
- /**
- * f(a,b)
- */
- struct FunctionApplication {
- EqualityNodeId a, b;
- FunctionApplication(EqualityNodeId a = null_id, EqualityNodeId b = null_id):
- a(a), b(b) {}
- bool operator == (const FunctionApplication& other) const {
- return a == other.a && b == other.b;
- }
- bool isApplication() const {
- return a != null_id && b != null_id;
- }
- };
-
- struct FunctionApplicationHashFunction {
- size_t operator () (const FunctionApplication& app) const {
- size_t hash = 0;
- hash = 0x9e3779b9 + app.a;
- hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2);
- return hash;
- }
- };
-
/**
* Store the application lookup, with enough information to backtrack
*/
/** The context we are using */
context::Context* d_context;
+ /** If we are done, we don't except any new assertions */
+ context::CDO<bool> d_done;
+
/** Whether to notify or not (temporarily disabled on equality checks) */
bool d_performNotify;
std::vector<FunctionApplication> d_applicationLookups;
/** Number of application lookups, for backtracking. */
- context::CDO<size_t> d_applicationLookupsCount;
+ context::CDO<DefaultSizeType> d_applicationLookupsCount;
/** 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;
+ context::CDO<DefaultSizeType> d_nodesCount;
/**
* At time of addition a function application can already normalize to something, so
std::vector<EqualityNode> d_equalityNodes;
/** Number of asserted equalities we have so far */
- context::CDO<size_t> d_assertedEqualitiesCount;
+ context::CDO<DefaultSizeType> d_assertedEqualitiesCount;
/** Memory for the use-list nodes */
std::vector<UseListNode> d_useListNodes;
/**
* Context dependent count of triggers
*/
- context::CDO<size_t> d_equalityTriggersCount;
+ context::CDO<DefaultSizeType> d_equalityTriggersCount;
/**
* Trigger lists per node. The begin id changes as we merge, but the end always points to
std::vector<TriggerId> d_nodeTriggers;
/**
- * Map from ids to the id of the constant that is the representative.
+ * Map from ids to wheather they are constants (constants are always
+ * representatives of their class.
*/
- std::vector<EqualityNodeId> d_constantRepresentative;
+ std::vector<bool> d_isConstant;
/**
- * Size of the constant representatives list.
+ * Map from ids to wheather they are Boolean.
*/
- context::CDO<unsigned> d_constantRepresentativesSize;
-
- /** The list of representatives that became constant. */
- std::vector<EqualityNodeId> d_constantRepresentatives;
-
- /** List of all the constants. */
- std::vector<TNode> d_constants;
-
- /** Size of the constants list */
- context::CDO<unsigned> d_constantsSize;
+ std::vector<bool> d_isBoolean;
/**
* Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId.
Statistics d_stats;
/** Add a new function application node to the database, i.e APP t1 t2 */
- EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2);
+ EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality);
/** Add a new node to the database */
EqualityNodeId newNode(TNode t);
- struct MergeCandidate {
- EqualityNodeId t1Id, t2Id;
- MergeReasonType type;
- TNode reason;
- MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason):
- t1Id(x), t2Id(y), type(type), reason(reason) {}
-
- std::string toString(EqualityEngine& eqEngine) const {
- std::stringstream ss;
- ss << eqEngine.d_nodes[t1Id] << " = " << eqEngine.d_nodes[t2Id] << ", " << type;
- return ss.str();
- }
- };
-
/** Propagation queue */
std::queue<MergeCandidate> d_propagationQueue;
/** The true node */
Node d_true;
+ /** True node id */
+ EqualityNodeId d_trueId;
+
/** The false node */
Node d_false;
+ /** False node id */
+ EqualityNodeId d_falseId;
/**
* Adds an equality of terms t1 and t2 to the database.
char* d_triggerDatabase;
/** Allocated size of the trigger term database */
- size_t d_triggerDatabaseAllocatedSize ;
+ DefaultSizeType d_triggerDatabaseAllocatedSize ;
/** Reference for the trigger terms set */
- typedef size_t TriggerTermSetRef;
+ typedef DefaultSizeType TriggerTermSetRef;
/** Null reference */
- static const TriggerTermSetRef null_set_id = (size_t)(-1);
+ static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1);
/** Create new trigger term set based on the internally set information */
TriggerTermSetRef newTriggerTermSet();
}
/** Used part of the trigger term database */
- context::CDO<size_t> d_triggerDatabaseSize;
+ context::CDO<DefaultSizeType> d_triggerDatabaseSize;
struct TriggerSetUpdate {
EqualityNodeId classId;
--- /dev/null
+/********************* */
+/*! \file equality_engine_types.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#include <string>
+#include <iostream>
+#include <sstream>
+
+namespace CVC4 {
+namespace theory {
+namespace eq {
+
+/** Default type for the size of the sizes (size_t replacement) */
+typedef uint32_t DefaultSizeType;
+
+/** Id of the node */
+typedef DefaultSizeType EqualityNodeId;
+
+/** Id of the use list */
+typedef DefaultSizeType UseListNodeId;
+
+/** The trigger ids */
+typedef DefaultSizeType TriggerId;
+
+/** The equality edge ids */
+typedef DefaultSizeType EqualityEdgeId;
+
+/** The null node */
+static const EqualityNodeId null_id = (EqualityNodeId)(-1);
+
+/** The null use list node */
+static const EqualityNodeId null_uselist_id = (EqualityNodeId)(-1);
+
+/** The null trigger */
+static const TriggerId null_trigger = (TriggerId)(-1);
+
+/** The null edge id */
+static const EqualityEdgeId null_edge = (EqualityEdgeId)(-1);
+
+/**
+ * A reason for a merge. Either an equality x = y, a merge of two
+ * function applications f(x1, x2), f(y1, y2) due to congruence,
+ * or a merge of an equality to false due to both sides being
+ * (different) constants.
+ */
+enum MergeReasonType {
+ /** Terms were merged due to application of congruence closure */
+ MERGED_THROUGH_CONGRUENCE,
+ /** Terms were merged due to application of pure equality */
+ MERGED_THROUGH_EQUALITY,
+ /** Equality was merged to false, due to both sides of equality being a constant */
+ MERGED_THROUGH_CONSTANTS,
+};
+
+inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
+ switch (reason) {
+ case MERGED_THROUGH_CONGRUENCE:
+ out << "congruence";
+ break;
+ case MERGED_THROUGH_EQUALITY:
+ out << "pure equality";
+ break;
+ case MERGED_THROUGH_CONSTANTS:
+ out << "constants disequal";
+ break;
+ default:
+ Unreachable();
+ }
+ return out;
+}
+
+/**
+ * A candidate for merging two equivalence classes, with the necessary
+ * additional information.
+ */
+struct MergeCandidate {
+ EqualityNodeId t1Id, t2Id;
+ MergeReasonType type;
+ TNode reason;
+ MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason):
+ t1Id(x), t2Id(y), type(type), reason(reason) {}
+};
+
+/**
+ * We mantaint uselist where a node appears in, and this is the node
+ * of such a list.
+ */
+class UseListNode {
+
+private:
+
+ /** The id of the application node where this representative is at */
+ EqualityNodeId d_applicationId;
+
+ /** The next one in the class */
+ UseListNodeId d_nextUseListNodeId;
+
+public:
+
+ /**
+ * Creates a new node, which is in a list of it's own.
+ */
+ UseListNode(EqualityNodeId nodeId = null_id, UseListNodeId nextId = null_uselist_id)
+ : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {}
+
+ /**
+ * Returns the next node in the circular list.
+ */
+ UseListNodeId getNext() const {
+ return d_nextUseListNodeId;
+ }
+
+ /**
+ * Returns the id of the function application.
+ */
+ EqualityNodeId getApplicationId() const {
+ return d_applicationId;
+ }
+};
+
+/**
+ * Main class for representing nodes in the equivalence class. The
+ * nodes are a circular list, with the representative carrying the
+ * size. Each individual node carries with itself the uselist of
+ * functino applications it appears in and the list of asserted
+ * disequalities it belongs to. In order to get these lists one must
+ * traverse the entire class and pick up all the individual lists.
+ */
+class EqualityNode {
+
+private:
+
+ /** The size of this equivalence class (if it's a representative) */
+ DefaultSizeType d_size;
+
+ /** The id (in the eq-manager) of the representative equality node */
+ EqualityNodeId d_findId;
+
+ /** The next equality node in this class */
+ EqualityNodeId d_nextId;
+
+ /** The use list of this node */
+ UseListNodeId d_useList;
+
+public:
+
+ /**
+ * Creates a new node, which is in a list of it's own.
+ */
+ EqualityNode(EqualityNodeId nodeId = null_id)
+ : d_size(1),
+ d_findId(nodeId),
+ d_nextId(nodeId),
+ d_useList(null_uselist_id)
+ {}
+
+ /**
+ * Returns the function uselist.
+ */
+ UseListNodeId getUseList() const {
+ return d_useList;
+ }
+
+ /**
+ * Returns the next node in the class circular list.
+ */
+ EqualityNodeId getNext() const {
+ return d_nextId;
+ }
+
+ /**
+ * Returns the size of this equivalence class (only valid if this is the representative).
+ */
+ DefaultSizeType getSize() const {
+ return d_size;
+ }
+
+ /**
+ * Merges the two lists. If add size is true the size of this node is increased by the size of
+ * the other node, otherwise the size is decreased by the size of the other node.
+ */
+ template<bool addSize>
+ void merge(EqualityNode& other) {
+ EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp;
+ if (addSize) {
+ d_size += other.d_size;
+ } else {
+ d_size -= other.d_size;
+ }
+ }
+
+ /**
+ * Returns the class representative.
+ */
+ EqualityNodeId getFind() const { return d_findId; }
+
+ /**
+ * Set the class representative.
+ */
+ void setFind(EqualityNodeId findId) { d_findId = findId; }
+
+ /**
+ * Note that this node is used in a function application funId, or
+ * a negatively asserted equality (dis-equality) with funId.
+ */
+ template<typename memory_class>
+ void usedIn(EqualityNodeId funId, memory_class& memory) {
+ UseListNodeId newUseId = memory.size();
+ memory.push_back(UseListNode(funId, d_useList));
+ 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();
+ }
+};
+
+/**
+ * Represents the function APPLY a b. If isEquality is true then it
+ * represents the predicate (a = b). Note that since one can not
+ * construct the equality over function terms, the equality and hash
+ * function below are still well defined.
+ */
+struct FunctionApplication {
+ bool isEquality;
+ EqualityNodeId a, b;
+ FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id)
+ : isEquality(isEquality), a(a), b(b) {}
+ bool operator == (const FunctionApplication& other) const {
+ return a == other.a && b == other.b;
+ }
+ bool isApplication() const {
+ return a != null_id && b != null_id;
+ }
+};
+
+struct FunctionApplicationHashFunction {
+ size_t operator () (const FunctionApplication& app) const {
+ size_t hash = 0;
+ hash = 0x9e3779b9 + app.a;
+ hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2);
+ return hash;
+ }
+};
+
+} // namespace eq
+} // namespace theory
+} // namespace CVC4
+
projects / cvc5.git / commitdiff