From 353c6d5c3770365f0dffcbdf697199bed156cf50 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Fri, 24 Sep 2010 15:03:28 +0000 Subject: [PATCH] basic union find for bitvectors --- src/theory/bv/Makefile.am | 4 +- src/theory/bv/equality_engine.cpp | 5 + src/theory/bv/equality_engine.h | 564 ++++++++++++++++++ src/theory/bv/theory_bv.cpp | 75 ++- src/theory/bv/theory_bv.h | 28 +- src/theory/bv/theory_bv_rewrite_rules.cpp | 36 ++ src/theory/bv/theory_bv_rewrite_rules.h | 10 + src/theory/bv/theory_bv_utils.h | 4 + src/theory/theory_engine.h | 2 +- test/regress/regress0/bv/core/Makefile.am | 74 +-- .../regress0/bv/core/bv_eq_diamond10.smt | 33 + .../regress0/bv/core/bv_eq_diamond11.smt | 35 ++ .../regress0/bv/core/bv_eq_diamond12.smt | 37 ++ .../regress0/bv/core/bv_eq_diamond13.smt | 39 ++ .../regress0/bv/core/bv_eq_diamond14.smt | 41 ++ .../regress0/bv/core/bv_eq_diamond15.smt | 43 ++ .../regress0/bv/core/bv_eq_diamond16.smt | 45 ++ .../regress0/bv/core/bv_eq_diamond17.smt | 47 ++ test/regress/regress0/bv/core/equality-00.cvc | 4 + test/regress/regress0/bv/core/equality-00.smt | 10 + test/regress/regress0/bv/core/equality-01.cvc | 5 + test/regress/regress0/bv/core/equality-01.smt | 12 + test/regress/regress0/bv/core/equality-02.cvc | 15 + test/regress/regress0/bv/core/equality-02.smt | 20 + test/regress/regress0/bv/core/equality-03.cvc | 10 + test/regress/regress0/bv/core/equality-03.smt | 27 + test/regress/regress0/bv/core/equality-04.smt | 25 + 27 files changed, 1206 insertions(+), 44 deletions(-) create mode 100644 src/theory/bv/equality_engine.cpp create mode 100644 src/theory/bv/equality_engine.h create mode 100644 test/regress/regress0/bv/core/bv_eq_diamond10.smt create mode 100644 test/regress/regress0/bv/core/bv_eq_diamond11.smt create mode 100644 test/regress/regress0/bv/core/bv_eq_diamond12.smt create mode 100644 test/regress/regress0/bv/core/bv_eq_diamond13.smt create mode 100644 test/regress/regress0/bv/core/bv_eq_diamond14.smt create mode 100644 test/regress/regress0/bv/core/bv_eq_diamond15.smt create mode 100644 test/regress/regress0/bv/core/bv_eq_diamond16.smt create mode 100644 test/regress/regress0/bv/core/bv_eq_diamond17.smt create mode 100644 test/regress/regress0/bv/core/equality-00.cvc create mode 100644 test/regress/regress0/bv/core/equality-00.smt create mode 100644 test/regress/regress0/bv/core/equality-01.cvc create mode 100644 test/regress/regress0/bv/core/equality-01.smt create mode 100644 test/regress/regress0/bv/core/equality-02.cvc create mode 100644 test/regress/regress0/bv/core/equality-02.smt create mode 100644 test/regress/regress0/bv/core/equality-03.cvc create mode 100644 test/regress/regress0/bv/core/equality-03.smt create mode 100644 test/regress/regress0/bv/core/equality-04.smt diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index ad858ab53..c07bf018e 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -11,6 +11,8 @@ libbv_la_SOURCES = \ theory_bv_utils.h \ theory_bv_rewrite_rules.h \ theory_bv_rewrite_rules.cpp \ - theory_bv_type_rules.h + theory_bv_type_rules.h \ + equality_engine.h \ + equality_engine.cpp EXTRA_DIST = kinds diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp new file mode 100644 index 000000000..8f75f5e86 --- /dev/null +++ b/src/theory/bv/equality_engine.cpp @@ -0,0 +1,5 @@ +#include "equality_engine.h" + +using namespace CVC4::theory::bv; + +const size_t NodeIdTraits::null = ((size_t)(-1) << (sizeof(size_t)*8 - NodeIdTraits::s_id_bits)) >> (sizeof(size_t)*8 - NodeIdTraits::s_id_bits); diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h new file mode 100644 index 000000000..03895a598 --- /dev/null +++ b/src/theory/bv/equality_engine.h @@ -0,0 +1,564 @@ +#include "cvc4_private.h" + +#pragma once + +#include +#include + +#include "expr/node.h" +#include "context/cdo.h" +#include "util/output.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +struct NodeIdTraits { + /** The null id */ + static const size_t null; // Defined in the cpp file (GCC bug) + /** Number of bits we use for the id */ + static const size_t s_id_bits = 24; + /** Number of bits we use for the size the equivalence class */ + static const size_t s_size_bits = 16; +}; + +class EqualityNode { + +public: + + /** The size of this equivalence class (if it's a representative) */ + size_t d_size : NodeIdTraits::s_size_bits; + + /** The id (in the eq-manager) of the representative equality node */ + size_t d_findId : NodeIdTraits::s_id_bits; + + /** The next equality node in this class */ + size_t d_nextId : NodeIdTraits::s_id_bits; + +public: + + /** + * Creates a new node, which is in a list of it's own. + */ + EqualityNode(size_t nodeId = NodeIdTraits::null) + : d_size(1), d_findId(nodeId), d_nextId(nodeId) {} + + inline void init(size_t nodeId) { + d_size = 1; + d_findId = d_nextId = nodeId; + } + + /** + * Returns the next node in the class circural list. + */ + inline size_t getNext() const { + return d_nextId; + } + + /** + * Returns the size of this equivalence class (only valid if this is the representative). + */ + inline 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 + inline void merge(EqualityNode& other) { + size_t tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp; + if (addSize) { + Assert(d_size + other.d_size > d_size); + d_size += other.d_size; + } else { + Assert(d_size > other.d_size); + d_size -= other.d_size; + } + } + + /** + * Returns the class representative. + */ + inline size_t getFind() const { return d_findId; } + + /** + * Set the class representative. + */ + inline void setFind(size_t findId) { d_findId = findId; } + +}; + + +template +class EqualityEngine { + + /** The class to notify when a representative changes for a term */ + NotifyClass d_notify; + + /** Map from nodes to their ids */ + __gnu_cxx::hash_map d_nodeIds; + + /** Map from ids to the nodes */ + std::vector d_nodes; + + /** Map from ids to the equality nodes */ + std::vector d_equalityNodes; + + /** Number of asserted equalities we have so far */ + context::CDO d_assertedEqualitiesCount; + + /** + * We keep a list of asserted equalities. Not among original terms, but + * among the class representatives. + */ + struct Equality { + /** Left hand side of the equality */ + size_t lhs : NodeIdTraits::s_id_bits; + /** Right hand side of the equality */ + size_t rhs : NodeIdTraits::s_id_bits; + /** Equality constructor */ + Equality(size_t lhs = NodeIdTraits::null, size_t rhs = NodeIdTraits::null) + : lhs(lhs), rhs(rhs) {} + }; + + /** The ids of the classes we have merged */ + std::vector d_assertedEqualities; + + /** + * An edge in the equality graph. This graph is an undirected graph (both edges added) + * containing the actual asserted equalities. + */ + class EqualityEdge { + + // The id of the RHS of this equality + size_t d_nodeId : NodeIdTraits::s_id_bits; + // The next edge + size_t d_nextId : NodeIdTraits::s_id_bits; + + public: + + EqualityEdge(size_t nodeId = NodeIdTraits::null, size_t nextId = NodeIdTraits::null) + : d_nodeId(nodeId), d_nextId(nextId) {} + + /** Returns the id of the next edge */ + inline size_t getNext() const { return d_nextId; } + + /** Returns the id of the target edge node */ + inline size_t getNodeId() const { return d_nodeId; } + }; + + /** + * All the equality edges (twice as many as the number of asserted equalities. If an equality + * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index + * of one of the edges you can reconstruct the original equality. + */ + std::vector d_equalityEdges; + + /** + * Map from a node to it's first edge in the equality graph. Edges are added to the front of the + * list which makes the insertion/backtracking easy. + */ + std::vector d_equalityGraph; + + /** Add an edge to the equality graph */ + inline void addGraphEdge(size_t t1, size_t t2); + + /** Returns the equality node of the given node */ + inline EqualityNode& getEqualityNode(TNode node); + + /** Returns the equality node of the given node */ + inline EqualityNode& getEqualityNode(size_t nodeId); + + /** Returns the id of the node */ + inline size_t getNodeId(TNode node) const; + + /** Merge the class2 into class1 */ + void merge(EqualityNode& class1, EqualityNode& class2); + + /** Undo the mereg of class2 into class1 */ + void undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id); + + /** Backtrack the information if necessary */ + void backtrack(); + + /** + * Data used in the BFS search through the equality graph. + */ + struct BfsData { + // The current node + size_t nodeId : NodeIdTraits::s_id_bits; + // The index of the edge we traversed + size_t edgeId : NodeIdTraits::s_id_bits; + // Index in the queue of the previous node. Shouldn't be too much of them, at most the size + // of the biggest equivalence class + size_t previousIndex : NodeIdTraits::s_size_bits; + + BfsData(size_t nodeId = NodeIdTraits::null, size_t edgeId = NodeIdTraits::null, size_t prev = 0) + : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {} + }; + + /** + * Trigger that will + */ + struct Trigger { + size_t class1Id : NodeIdTraits::s_id_bits; + size_t class2Id : NodeIdTraits::s_id_bits; + }; + + +public: + + /** + * Initialize the equalty engine, given the owning class. This will initialize the notifier with + * the owner information. + */ + EqualityEngine(OwnerClass& owner, context::Context* context) + : d_notify(owner), d_assertedEqualitiesCount(context, 0) {} + + /** + * Adds a term to the term database. Returns the internal id of the term. + */ + size_t addTerm(TNode t); + + /** + * Check whether the node is already in the database. + */ + inline bool hasTerm(TNode t) const; + + /** + * Adds an equality t1 = t2 to the database. + */ + void addEquality(TNode t1, TNode t2); + + /** + * Returns the representative of the term t. + */ + inline TNode getRepresentative(TNode t) const; + + /** + * Returns true if the two nodes are in the same class. + */ + inline bool areEqual(TNode t1, TNode t2) const; + + /** + * 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). + */ + void getExplanation(TNode t1, TNode t2, std::vector& equalities) const; + + /** + * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with + * (t1, t2). + */ + void addTrigger(TNode t1, TNode t2); + +}; + +template +size_t EqualityEngine::addTerm(TNode t) { + + Debug("equality") << "addTerm(" << t << ")" << std::endl; + + // If term already added, retrurn it's id + if (hasTerm(t)) return getNodeId(t); + + // Register the new id of the term + size_t newId = d_nodes.size(); + d_nodeIds[t] = newId; + // Add the node to it's position + d_nodes.push_back(t); + // Add it to the equality graph + d_equalityGraph.push_back(NodeIdTraits::null); + // Add the equality node to the nodes + if (d_equalityNodes.size() <= newId) { + d_equalityNodes.resize(newId + 100); + } + d_equalityNodes[newId].init(newId); + // Return the id of the term + return newId; +} + +template +bool EqualityEngine::hasTerm(TNode t) const { + return d_nodeIds.find(t) != d_nodeIds.end(); +} + +template +size_t EqualityEngine::getNodeId(TNode node) const { + Assert(hasTerm(node)); + return (*d_nodeIds.find(node)).second; +} + +template +EqualityNode& EqualityEngine::getEqualityNode(TNode t) { + return getEqualityNode(getNodeId(t)); +} + +template +EqualityNode& EqualityEngine::getEqualityNode(size_t nodeId) { + Assert(nodeId < d_equalityNodes.size()); + return d_equalityNodes[nodeId]; +} + +template +void EqualityEngine::addEquality(TNode t1, TNode t2) { + + Debug("equality") << "addEquality(" << t1 << "," << t2 << ")" << std::endl; + + // Backtrack if necessary + backtrack(); + + // Add the terms if they are not already in the database + size_t t1Id = getNodeId(t1); + size_t t2Id = getNodeId(t2); + + // Get the representatives + size_t t1classId = getEqualityNode(t1Id).getFind(); + size_t t2classId = getEqualityNode(t2Id).getFind(); + + // If already the same, we're done + if (t1classId == t2classId) return; + + // Get the nodes of the representatives + EqualityNode& node1 = getEqualityNode(t1classId); + EqualityNode& node2 = getEqualityNode(t2classId); + + Assert(node1.getFind() == t1classId); + Assert(node2.getFind() == t2classId); + + // Depending on the size, merge them + if (node1.getSize() < node2.getSize()) { + merge(node2, node1); + d_assertedEqualities.push_back(Equality(t2classId, t1classId)); + } else { + merge(node1, node2); + d_assertedEqualities.push_back(Equality(t1classId, t2classId)); + } + + // Add the actuall equality to the equality graph + addGraphEdge(t1Id, t2Id); + + Assert(2*d_assertedEqualities.size() == d_equalityEdges.size()); + + // One more equality added + d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; +} + +template +TNode EqualityEngine::getRepresentative(TNode t) const { + + Debug("equality") << "getRepresentative(" << t << ")" << std::endl; + + Assert(hasTerm(t)); + + // Both following commands are semantically const + const_cast(this)->backtrack(); + size_t representativeId = const_cast(this)->getEqualityNode(t).getFind(); + + Debug("equality") << "getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl; + + return d_nodes[representativeId]; +} + +template +bool EqualityEngine::areEqual(TNode t1, TNode t2) const { + Debug("equality") << "areEqual(" << t1 << "," << t2 << ")" << std::endl; + + Assert(hasTerm(t1)); + Assert(hasTerm(t2)); + + // Both following commands are semantically const + const_cast(this)->backtrack(); + size_t rep1 = const_cast(this)->getEqualityNode(t1).getFind(); + size_t rep2 = const_cast(this)->getEqualityNode(t2).getFind(); + + Debug("equality") << "areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl; + + return rep1 == rep2; +} + +template +void EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2) { + + Debug("equality") << "merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; + + size_t class1Id = class1.getFind(); + size_t class2Id = class2.getFind(); + + // Update class2 representative information + size_t currentId = class2Id; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + + // Update it's find to class1 id + currentNode.setFind(class1Id); + + // Move to the next node + currentId = currentNode.getNext(); + + } while (currentId != class2Id); + + // Now merge the lists + class1.merge(class2); +} + +template +void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, size_t class2Id) { + + Debug("equality") << "undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl; + + // Now unmerge the lists (same as merge) + class1.merge(class2); + + // Update class2 representative information + size_t currentId = class2Id; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + + // Update it's find to class1 id + currentNode.setFind(class2Id); + + // Move to the next node + currentId = currentNode.getNext(); + + } while (currentId != class2Id); + +} + +template +void EqualityEngine::backtrack() { + + // If we need to backtrack then do it + if (d_assertedEqualitiesCount < d_assertedEqualities.size()) { + + Debug("equality") << "backtrack(): nodes" << std::endl; + + for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) { + // Get the ids of the merged classes + Equality& eq = d_assertedEqualities[i]; + // Undo the merge + undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs); + } + + d_assertedEqualities.resize(d_assertedEqualitiesCount); + + Debug("equality") << "backtrack(): edges" << std::endl; + + for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) { + EqualityEdge& edge1 = d_equalityEdges[i]; + EqualityEdge& edge2 = d_equalityEdges[i | 1]; + d_equalityGraph[edge2.getNodeId()] = edge1.getNext(); + d_equalityGraph[edge1.getNodeId()] = edge2.getNext(); + } + + d_equalityEdges.resize(2 * d_assertedEqualitiesCount); + } + +} + +template +void EqualityEngine::addGraphEdge(size_t t1, size_t t2) { + size_t edge = d_equalityEdges.size(); + d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1])); + d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2])); + d_equalityGraph[t1] = edge; + d_equalityGraph[t2] = edge | 1; +} + +template +void EqualityEngine::getExplanation(TNode t1, TNode t2, std::vector& equalities) const { + Assert(equalities.empty()); + Assert(t1 != t2); + Assert(getRepresentative(t1) == getRepresentative(t2)); + + Debug("equality") << "getExplanation(" << t1 << "," << t2 << ")" << std::endl; + + const_cast(this)->backtrack(); + + // Queue for the BFS containing nodes + std::vector bfsQueue; + + // The id's of the nodes + size_t t1Id = getNodeId(t1); + size_t t2Id = getNodeId(t2); + + // Find a path from t1 to t2 in the graph (BFS) + bfsQueue.push_back(BfsData(t1Id, NodeIdTraits::null, 0)); + size_t currentIndex = 0; + while (true) { + // There should always be a path, and every node can be visited only once (tree) + Assert(currentIndex < bfsQueue.size()); + + // The next node to visit + BfsData& current = bfsQueue[currentIndex]; + size_t currentNode = current.nodeId; + + Debug("equality") << "getExplanation(): currentNode: " << currentNode << std::endl; + + // Go through the equality edges of this node + size_t currentEdge = d_equalityGraph[currentNode]; + + while (currentEdge != NodeIdTraits::null) { + Debug("equality") << "getExplanation(): currentEdge: " << currentEdge << std::endl; + + // Get the edge + const EqualityEdge& edge = d_equalityEdges[currentEdge]; + + // Did we find the path + if (edge.getNodeId() == t2Id) { + + Debug("equality") << "getExplanation(): path found: " << std::endl; + + // Reconstruct the path + do { + // Get the left and right hand side from the edge + size_t firstEdge = (currentEdge >> 1) << 1; + size_t secondEdge = (currentEdge | 1); + TNode lhs = d_nodes[d_equalityEdges[secondEdge].getNodeId()]; + TNode rhs = d_nodes[d_equalityEdges[firstEdge].getNodeId()]; + // Add the actual equality to the vector + equalities.push_back(lhs.eqNode(rhs)); + + Debug("equality") << "getExplanation(): adding: " << lhs.eqNode(rhs) << std::endl; + + // Go to the previous + currentEdge = bfsQueue[currentIndex].edgeId; + currentIndex = bfsQueue[currentIndex].previousIndex; + } while (currentEdge != NodeIdTraits::null); + + // Done + return; + } + + // Push to the visitation queue if it's not the backward edge + if ((currentEdge | 1) != (current.edgeId | 1)) { + bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex)); + } + + // Go to the next edge + currentEdge = edge.getNext(); + } + + // Go to the next node to visit + ++ currentIndex; + } +} + +template +void EqualityEngine::addTrigger(TNode t1, TNode t2) { + + + +} + + + +} // Namespace bv +} // Namespace theory +} // Namespace CVC4 + diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 849740c9a..e08c19dbd 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -7,9 +7,19 @@ using namespace CVC4::theory; using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; +void TheoryBV::preRegisterTerm(TNode node) { + + Debug("bitvector") << "TheoryBV::preRegister(" << node << ")" << std::endl; + + if (node.getKind() == kind::EQUAL) { + d_eqEngine.addTerm(node[0]); + d_eqEngine.addTerm(node[1]); + } +} + RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) { - Debug("bitvector") << "postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ")" << std::endl; + Debug("bitvector") << "TheoryBV::postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ")" << std::endl; Node result; @@ -43,8 +53,12 @@ RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) { >::apply(node); break; case kind::EQUAL: - if (node[0] == node[1]) result = mkTrue(); - else result = node; + result = LinearRewriteStrategy< + // Two distinct values rewrite to false + CoreRewriteRules::FailEq, + // If both sides are equal equality is true + CoreRewriteRules::SimplifyEq + >::apply(node); break; default: // TODO: figure out when this is an operator @@ -54,7 +68,60 @@ RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) { } } - Debug("bitvector") << "postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ") => " << result << std::endl; + Debug("bitvector") << "TheoryBV::postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ") => " << result << std::endl; return RewriteComplete(result); } + + +void TheoryBV::check(Effort e) { + + Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl; + + while(!done()) { + + // Get the assertion + TNode assertion = get(); + + Debug("bitvector") << "TheoryBV::check(" << e << "): asserting: " << assertion << std::endl; + + // Do the right stuff + switch (assertion.getKind()) { + case kind::EQUAL: + d_eqEngine.addEquality(assertion[0], assertion[1]); + break; + case kind::NOT: { + TNode equality = assertion[0]; + if (d_eqEngine.areEqual(equality[0], equality[1])) { + vector assertions; + d_eqEngine.getExplanation(equality[0], equality[1], assertions); + // We can assume that the explanation is bigger than one node + assertions.push_back(assertion); + d_out->conflict(mkAnd(assertions)); + } else { + d_disequalities.push_back(assertion); + } + break; + } + default: + Unhandled(); + } + } + + // In full effort go back and check the disequalities + if (true) { + Debug("bitvector") << "TheoryBV::check(" << e << "): checking disequalities" << std::endl; + + for (unsigned i = 0; i < d_disequalities.size(); ++ i) { + TNode assertion = d_disequalities[i]; + TNode equality = assertion[0]; + if (d_eqEngine.areEqual(equality[0], equality[1])) { + vector assertions; + d_eqEngine.getExplanation(equality[0], equality[1], assertions); + assertions.push_back(assertion); + // We can assume that the explanation is bigger than one node + d_out->conflict(mkAnd(assertions)); + } + } + } +} diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index ee331af02..912c453b4 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -23,19 +23,41 @@ #include "theory/theory.h" #include "context/context.h" +#include "context/cdlist.h" +#include "equality_engine.h" namespace CVC4 { namespace theory { namespace bv { class TheoryBV : public Theory { + public: + + class EqualityNotify { + TheoryBV& d_theoryBV; + public: + EqualityNotify(TheoryBV& theoryBV) + : d_theoryBV(theoryBV) {} + }; + +private: + + /** Equality reasoning engine */ + EqualityEngine d_eqEngine; + + /** The disequalities */ + context::CDList d_disequalities; + +public: + TheoryBV(int id, context::Context* c, OutputChannel& out) : - Theory(id, c, out) { + Theory(id, c, out), d_eqEngine(*this, c), d_disequalities(c) { } - void preRegisterTerm(TNode n) { } + + void preRegisterTerm(TNode n); void registerTerm(TNode n) { } - void check(Effort e) {} + void check(Effort e); void propagate(Effort e) {} void explain(TNode n, Effort e) { } RewriteResponse postRewrite(TNode n, bool topLevel); diff --git a/src/theory/bv/theory_bv_rewrite_rules.cpp b/src/theory/bv/theory_bv_rewrite_rules.cpp index 5473768bb..8c5dfc415 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.cpp +++ b/src/theory/bv/theory_bv_rewrite_rules.cpp @@ -245,5 +245,41 @@ Node CoreRewriteRules::ExtractExtract::apply(Node node) { Debug("bitvector") << "ExtractExtract(" << node << ") => " << result << endl; return result; +} +bool CoreRewriteRules::FailEq::applies(Node node) { + if (node.getKind() != kind::EQUAL) return false; + if (node[0].getKind() != kind::CONST_BITVECTOR) return false; + if (node[1].getKind() != kind::CONST_BITVECTOR) return false; + return node[0] != node[1]; } + +Node CoreRewriteRules::FailEq::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "FailEq(" << node << ")" << endl; + + Node result = mkFalse(); + + Debug("bitvector") << "FailEq(" << node << ") => " << result << endl; + + return result; +} + +bool CoreRewriteRules::SimplifyEq::applies(Node node) { + if (node.getKind() != kind::EQUAL) return false; + return node[0] == node[1]; +} + +Node CoreRewriteRules::SimplifyEq::apply(Node node) { + Assert(applies(node)); + + Debug("bitvector") << "FailEq(" << node << ")" << endl; + + Node result = mkTrue(); + + Debug("bitvector") << "FailEq(" << node << ") => " << result << endl; + + return result; +} + diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 48696ce33..ea396e32c 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -50,6 +50,16 @@ struct CoreRewriteRules { static bool applies(Node node); }; + struct FailEq { + static Node apply(Node node); + static bool applies(Node node); + }; + + struct SimplifyEq { + static Node apply(Node node); + static bool applies(Node node); + }; + }; template diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index fa948465d..ce8298702 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -28,6 +28,10 @@ inline Node mkFalse() { return NodeManager::currentNM()->mkConst(false); } +inline Node mkAnd(std::vector& children) { + return NodeManager::currentNM()->mkNode(kind::AND, children); +} + inline Node mkExtract(TNode node, unsigned high, unsigned low) { Node extractOp = NodeManager::currentNM()->mkConst(BitVectorExtract(high, low)); std::vector children; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index cc0e663fa..074d40d05 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -332,7 +332,7 @@ public: d_uf->check(effort); d_arith->check(effort); d_arrays->check(effort); - //d_bv->check(effort); + d_bv->check(effort); } catch(const theory::Interrupted&) { Debug("theory") << "TheoryEngine::check() => conflict" << std::endl; } diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 0624c00f1..5b8e6d7d3 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -4,41 +4,45 @@ TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - concat-merge-0.smt \ - concat-merge-1.smt \ - concat-merge-2.smt \ - concat-merge-3.smt \ - extract-concat-0.smt \ - extract-concat-1.smt \ - extract-concat-2.smt \ - extract-concat-3.smt \ - extract-concat-4.smt \ - extract-concat-5.smt \ - extract-concat-6.smt \ - extract-concat-7.smt \ - extract-concat-8.smt \ - extract-concat-9.smt \ - extract-concat-10.smt \ - extract-concat-11.smt \ - extract-constant.smt \ - extract-extract-0.smt \ - extract-extract-1.smt \ - extract-extract-2.smt \ - extract-extract-3.smt \ - extract-extract-4.smt \ - extract-extract-5.smt \ - extract-extract-6.smt \ - extract-extract-7.smt \ - extract-extract-8.smt \ - extract-extract-9.smt \ - extract-extract-10.smt \ - extract-extract-11.smt \ - extract-whole-0.smt \ - extract-whole-1.smt \ - extract-whole-2.smt \ - extract-whole-3.smt \ - extract-whole-4.smt - + concat-merge-0.smt \ + concat-merge-1.smt \ + concat-merge-2.smt \ + concat-merge-3.smt \ + extract-concat-0.smt \ + extract-concat-1.smt \ + extract-concat-2.smt \ + extract-concat-3.smt \ + extract-concat-4.smt \ + extract-concat-5.smt \ + extract-concat-6.smt \ + extract-concat-7.smt \ + extract-concat-8.smt \ + extract-concat-9.smt \ + extract-concat-10.smt \ + extract-concat-11.smt \ + extract-constant.smt \ + extract-extract-0.smt \ + extract-extract-1.smt \ + extract-extract-2.smt \ + extract-extract-3.smt \ + extract-extract-4.smt \ + extract-extract-5.smt \ + extract-extract-6.smt \ + extract-extract-7.smt \ + extract-extract-8.smt \ + extract-extract-9.smt \ + extract-extract-10.smt \ + extract-extract-11.smt \ + extract-whole-0.smt \ + extract-whole-1.smt \ + extract-whole-2.smt \ + extract-whole-3.smt \ + extract-whole-4.smt \ + equality-00.smt \ + equality-01.smt \ + equality-02.smt \ + bv_eq_diamond10.smt + EXTRA_DIST = $(TESTS) # synonyms for "check" diff --git a/test/regress/regress0/bv/core/bv_eq_diamond10.smt b/test/regress/regress0/bv/core/bv_eq_diamond10.smt new file mode 100644 index 000000000..6d8042512 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond10.smt @@ -0,0 +1,33 @@ +(benchmark eq_diamond10 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(not (= x0 x9)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond11.smt b/test/regress/regress0/bv/core/bv_eq_diamond11.smt new file mode 100644 index 000000000..cf9dccf07 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond11.smt @@ -0,0 +1,35 @@ +(benchmark eq_diamond11 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(not (= x0 x10)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond12.smt b/test/regress/regress0/bv/core/bv_eq_diamond12.smt new file mode 100644 index 000000000..97f7159c7 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond12.smt @@ -0,0 +1,37 @@ +(benchmark eq_diamond12 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(not (= x0 x11)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond13.smt b/test/regress/regress0/bv/core/bv_eq_diamond13.smt new file mode 100644 index 000000000..9e25875e1 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond13.smt @@ -0,0 +1,39 @@ +(benchmark eq_diamond13 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(not (= x0 x12)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond14.smt b/test/regress/regress0/bv/core/bv_eq_diamond14.smt new file mode 100644 index 000000000..9eae02e30 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond14.smt @@ -0,0 +1,41 @@ +(benchmark eq_diamond14 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(not (= x0 x13)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond15.smt b/test/regress/regress0/bv/core/bv_eq_diamond15.smt new file mode 100644 index 000000000..ed28883a5 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond15.smt @@ -0,0 +1,43 @@ +(benchmark eq_diamond15 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32]) +(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) +(not (= x0 x14)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond16.smt b/test/regress/regress0/bv/core/bv_eq_diamond16.smt new file mode 100644 index 000000000..4e81c3c31 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond16.smt @@ -0,0 +1,45 @@ +(benchmark eq_diamond16 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32]) +(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32]) +(x15 BitVec[32]) (y15 BitVec[32]) (z15 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) +(or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) +(not (= x0 x15)))) diff --git a/test/regress/regress0/bv/core/bv_eq_diamond17.smt b/test/regress/regress0/bv/core/bv_eq_diamond17.smt new file mode 100644 index 000000000..b65e035e5 --- /dev/null +++ b/test/regress/regress0/bv/core/bv_eq_diamond17.smt @@ -0,0 +1,47 @@ +(benchmark eq_diamond17 +:source{ +Generating minimum transitivity constraints in P-time for deciding Equality Logic, +Ofer Strichman and Mirron Rozanov, +SMT Workshop 2005. + +Translator: Leonardo de Moura. } +:status unsat +:category { crafted } +:logic QF_BV +:difficulty { 0 } +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +(x10 BitVec[32]) (y10 BitVec[32]) (z10 BitVec[32]) +(x11 BitVec[32]) (y11 BitVec[32]) (z11 BitVec[32]) +(x12 BitVec[32]) (y12 BitVec[32]) (z12 BitVec[32]) +(x13 BitVec[32]) (y13 BitVec[32]) (z13 BitVec[32]) +(x14 BitVec[32]) (y14 BitVec[32]) (z14 BitVec[32]) +(x15 BitVec[32]) (y15 BitVec[32]) (z15 BitVec[32]) +(x16 BitVec[32]) (y16 BitVec[32]) (z16 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10))) +(or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11))) +(or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12))) +(or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13))) +(or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14))) +(or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15))) +(or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16))) +(not (= x0 x16)))) diff --git a/test/regress/regress0/bv/core/equality-00.cvc b/test/regress/regress0/bv/core/equality-00.cvc new file mode 100644 index 000000000..e02c616ad --- /dev/null +++ b/test/regress/regress0/bv/core/equality-00.cvc @@ -0,0 +1,4 @@ +x, y, z : BITVECTOR(32); +ASSERT(x = y); +ASSERT(y = z); +QUERY(x = z); \ No newline at end of file diff --git a/test/regress/regress0/bv/core/equality-00.smt b/test/regress/regress0/bv/core/equality-00.smt new file mode 100644 index 000000000..dabdae5f9 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-00.smt @@ -0,0 +1,10 @@ +(benchmark B_ + :status unsat + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :extrafuns ((z BitVec[32])) + :assumption (= x y) + :assumption (= y z) + :formula (not (= x z)) +) diff --git a/test/regress/regress0/bv/core/equality-01.cvc b/test/regress/regress0/bv/core/equality-01.cvc new file mode 100644 index 000000000..e56af23dd --- /dev/null +++ b/test/regress/regress0/bv/core/equality-01.cvc @@ -0,0 +1,5 @@ +x, y, z, w: BITVECTOR(32); +ASSERT(x = y); +ASSERT(y = z); +ASSERT(z = w); +QUERY(x = w); \ No newline at end of file diff --git a/test/regress/regress0/bv/core/equality-01.smt b/test/regress/regress0/bv/core/equality-01.smt new file mode 100644 index 000000000..48506d2b9 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-01.smt @@ -0,0 +1,12 @@ +(benchmark B_ + :status unsat + :logic QF_BV + :extrafuns ((x BitVec[32])) + :extrafuns ((y BitVec[32])) + :extrafuns ((z BitVec[32])) + :extrafuns ((w BitVec[32])) + :assumption (= x y) + :assumption (= y z) + :assumption (= z w) + :formula (not (= x w)) +) diff --git a/test/regress/regress0/bv/core/equality-02.cvc b/test/regress/regress0/bv/core/equality-02.cvc new file mode 100644 index 000000000..e8f51d61a --- /dev/null +++ b/test/regress/regress0/bv/core/equality-02.cvc @@ -0,0 +1,15 @@ +x0, x1, x2, x3 : BITVECTOR(32); +y0, y1, y2, y3 : BITVECTOR(32); + +ASSERT (x0 = x1); +ASSERT (x1 = x2); +ASSERT (x2 = x3); + +ASSERT (y0 = y1); +ASSERT (y1 = y2); +ASSERT (y2 = y3); + +ASSERT (x0 = y0); + +QUERY (x3 = y3); + diff --git a/test/regress/regress0/bv/core/equality-02.smt b/test/regress/regress0/bv/core/equality-02.smt new file mode 100644 index 000000000..ee011ceb4 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-02.smt @@ -0,0 +1,20 @@ +(benchmark B_ + :status unsat + :logic QF_BV + :extrafuns ((x0 BitVec[32])) + :extrafuns ((x1 BitVec[32])) + :extrafuns ((x2 BitVec[32])) + :extrafuns ((x3 BitVec[32])) + :extrafuns ((y0 BitVec[32])) + :extrafuns ((y1 BitVec[32])) + :extrafuns ((y2 BitVec[32])) + :extrafuns ((y3 BitVec[32])) + :assumption (= x0 x1) + :assumption (= x1 x2) + :assumption (= x2 x3) + :assumption (= y0 y1) + :assumption (= y1 y2) + :assumption (= y2 y3) + :assumption (= x0 y0) + :formula (not (= x3 y3)) +) diff --git a/test/regress/regress0/bv/core/equality-03.cvc b/test/regress/regress0/bv/core/equality-03.cvc new file mode 100644 index 000000000..d2f18682c --- /dev/null +++ b/test/regress/regress0/bv/core/equality-03.cvc @@ -0,0 +1,10 @@ +x0, x1, x2: BITVECTOR(32); +y0, y1, y2: BITVECTOR(32); +a0, a1, a2, a3 : BITVECTOR(32); + +ASSERT (a0 = x0 AND x0 = a1) XOR (a0 = y0 AND y0 = a1); +ASSERT (a1 = x1 AND x1 = a2) XOR (a1 = y1 AND y1 = a2); +ASSERT (a2 = x2 AND x2 = a3) XOR (a2 = y2 AND y2 = a3); + +QUERY (a0 = a3); + diff --git a/test/regress/regress0/bv/core/equality-03.smt b/test/regress/regress0/bv/core/equality-03.smt new file mode 100644 index 000000000..4141c7293 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-03.smt @@ -0,0 +1,27 @@ +(benchmark B_ + :source { +Source unknown +} + :status unknown + :difficulty { unknown } + :category { unknown } + :logic QF_BV + :extrafuns ((x0 BitVec[32])) + :extrafuns ((x1 BitVec[32])) + :extrafuns ((x2 BitVec[32])) + :extrafuns ((y0 BitVec[32])) + :extrafuns ((y1 BitVec[32])) + :extrafuns ((y2 BitVec[32])) + :extrafuns ((a0 BitVec[32])) + :extrafuns ((a1 BitVec[32])) + :extrafuns ((a2 BitVec[32])) + :extrafuns ((a3 BitVec[32])) + :assumption +(xor (and (= a0 x0) (= x0 a1)) (and (= a0 y0) (= y0 a1))) + :assumption +(xor (and (= a1 x1) (= x1 a2)) (and (= a1 y1) (= y1 a2))) + :assumption +(xor (and (= a2 x2) (= x2 a3)) (and (= a2 y2) (= y2 a3))) + :formula +(not (= a0 a3)) +) diff --git a/test/regress/regress0/bv/core/equality-04.smt b/test/regress/regress0/bv/core/equality-04.smt new file mode 100644 index 000000000..78adf0477 --- /dev/null +++ b/test/regress/regress0/bv/core/equality-04.smt @@ -0,0 +1,25 @@ +(benchmark eq_diamond10 +:status unsat +:logic QF_BV +:extrafuns ((x0 BitVec[32]) (y0 BitVec[32]) (z0 BitVec[32]) +(x1 BitVec[32]) (y1 BitVec[32]) (z1 BitVec[32]) +(x2 BitVec[32]) (y2 BitVec[32]) (z2 BitVec[32]) +(x3 BitVec[32]) (y3 BitVec[32]) (z3 BitVec[32]) +(x4 BitVec[32]) (y4 BitVec[32]) (z4 BitVec[32]) +(x5 BitVec[32]) (y5 BitVec[32]) (z5 BitVec[32]) +(x6 BitVec[32]) (y6 BitVec[32]) (z6 BitVec[32]) +(x7 BitVec[32]) (y7 BitVec[32]) (z7 BitVec[32]) +(x8 BitVec[32]) (y8 BitVec[32]) (z8 BitVec[32]) +(x9 BitVec[32]) (y9 BitVec[32]) (z9 BitVec[32]) +) +:formula (and +(or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) +(or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2))) +(or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3))) +(or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4))) +(or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5))) +(or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6))) +(or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7))) +(or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8))) +(or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9))) +(not (= x0 x9)))) -- 2.30.2