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
--- /dev/null
+#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);
--- /dev/null
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+#include <ext/hash_map>
+
+#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<bool addSize>
+ 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 <typename OwnerClass, typename NotifyClass>
+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<TNode, size_t, TNodeHashFunction> d_nodeIds;
+
+ /** Map from ids to the nodes */
+ std::vector<Node> d_nodes;
+
+ /** Map from ids to the equality nodes */
+ std::vector<EqualityNode> d_equalityNodes;
+
+ /** Number of asserted equalities we have so far */
+ context::CDO<size_t> d_assertedEqualitiesCount;
+
+ /**
+ * 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<Equality> 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<EqualityEdge> 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<size_t> 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<TNode>& 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 <typename OwnerClass, typename NotifyClass>
+size_t EqualityEngine<OwnerClass, NotifyClass>::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 <typename OwnerClass, typename NotifyClass>
+bool EqualityEngine<OwnerClass, NotifyClass>::hasTerm(TNode t) const {
+ return d_nodeIds.find(t) != d_nodeIds.end();
+}
+
+template <typename OwnerClass, typename NotifyClass>
+size_t EqualityEngine<OwnerClass, NotifyClass>::getNodeId(TNode node) const {
+ Assert(hasTerm(node));
+ return (*d_nodeIds.find(node)).second;
+}
+
+template <typename OwnerClass, typename NotifyClass>
+EqualityNode& EqualityEngine<OwnerClass, NotifyClass>::getEqualityNode(TNode t) {
+ return getEqualityNode(getNodeId(t));
+}
+
+template <typename OwnerClass, typename NotifyClass>
+EqualityNode& EqualityEngine<OwnerClass, NotifyClass>::getEqualityNode(size_t nodeId) {
+ Assert(nodeId < d_equalityNodes.size());
+ return d_equalityNodes[nodeId];
+}
+
+template <typename OwnerClass, typename NotifyClass>
+void EqualityEngine<OwnerClass, NotifyClass>::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 <typename OwnerClass, typename NotifyClass>
+TNode EqualityEngine<OwnerClass, NotifyClass>::getRepresentative(TNode t) const {
+
+ Debug("equality") << "getRepresentative(" << t << ")" << std::endl;
+
+ Assert(hasTerm(t));
+
+ // Both following commands are semantically const
+ const_cast<EqualityEngine*>(this)->backtrack();
+ size_t representativeId = const_cast<EqualityEngine*>(this)->getEqualityNode(t).getFind();
+
+ Debug("equality") << "getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
+
+ return d_nodes[representativeId];
+}
+
+template <typename OwnerClass, typename NotifyClass>
+bool EqualityEngine<OwnerClass, NotifyClass>::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<EqualityEngine*>(this)->backtrack();
+ size_t rep1 = const_cast<EqualityEngine*>(this)->getEqualityNode(t1).getFind();
+ size_t rep2 = const_cast<EqualityEngine*>(this)->getEqualityNode(t2).getFind();
+
+ Debug("equality") << "areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl;
+
+ return rep1 == rep2;
+}
+
+template <typename OwnerClass, typename NotifyClass>
+void EqualityEngine<OwnerClass, NotifyClass>::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<true>(class2);
+}
+
+template <typename OwnerClass, typename NotifyClass>
+void EqualityEngine<OwnerClass, NotifyClass>::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<false>(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 <typename OwnerClass, typename NotifyClass>
+void EqualityEngine<OwnerClass, NotifyClass>::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 <typename OwnerClass, typename NotifyClass>
+void EqualityEngine<OwnerClass, NotifyClass>::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 <typename OwnerClass, typename NotifyClass>
+void EqualityEngine<OwnerClass, NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
+ Assert(equalities.empty());
+ Assert(t1 != t2);
+ Assert(getRepresentative(t1) == getRepresentative(t2));
+
+ Debug("equality") << "getExplanation(" << t1 << "," << t2 << ")" << std::endl;
+
+ const_cast<EqualityEngine*>(this)->backtrack();
+
+ // Queue for the BFS containing nodes
+ std::vector<BfsData> 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 <typename OwnerClass, typename NotifyClass>
+void EqualityEngine<OwnerClass, NotifyClass>::addTrigger(TNode t1, TNode t2) {
+
+
+
+}
+
+
+
+} // Namespace bv
+} // Namespace theory
+} // Namespace CVC4
+
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;
>::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
}
}
- 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<TNode> 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<TNode> 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));
+ }
+ }
+ }
+}
#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<TheoryBV, EqualityNotify> d_eqEngine;
+
+ /** The disequalities */
+ context::CDList<TNode> 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);
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;
+}
+
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<Kind kind, typename Rule>
return NodeManager::currentNM()->mkConst<bool>(false);
}
+inline Node mkAnd(std::vector<TNode>& children) {
+ return NodeManager::currentNM()->mkNode(kind::AND, children);
+}
+
inline Node mkExtract(TNode node, unsigned high, unsigned low) {
Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
std::vector<Node> children;
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;
}
# 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"
--- /dev/null
+(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))))
--- /dev/null
+(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))))
--- /dev/null
+(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))))
--- /dev/null
+(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))))
--- /dev/null
+(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))))
--- /dev/null
+(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))))
--- /dev/null
+(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))))
--- /dev/null
+(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))))
--- /dev/null
+x, y, z : BITVECTOR(32);
+ASSERT(x = y);
+ASSERT(y = z);
+QUERY(x = z);
\ No newline at end of file
--- /dev/null
+(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))
+)
--- /dev/null
+x, y, z, w: BITVECTOR(32);
+ASSERT(x = y);
+ASSERT(y = z);
+ASSERT(z = w);
+QUERY(x = w);
\ No newline at end of file
--- /dev/null
+(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))
+)
--- /dev/null
+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);
+
--- /dev/null
+(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))
+)
--- /dev/null
+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);
+
--- /dev/null
+(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))
+)
--- /dev/null
+(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))))
projects / cvc5.git / commitdiff