From adad8844eeae9d5fc3b4de1941a64ad428998088 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Tue, 19 Mar 2013 00:51:17 -0400 Subject: [PATCH] implementing more inequality graph stuff; work in progress doesn't compile --- src/theory/bv/Makefile.am | 2 + src/theory/bv/bv_inequality_graph.h | 83 ++++++++++++++++++++--- src/theory/bv/bv_subtheory_inequality.cpp | 28 +++++++- src/theory/bv/bv_subtheory_inequality.h | 9 +-- 4 files changed, 104 insertions(+), 18 deletions(-) diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 419acf6ba..29284ff5a 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -19,6 +19,8 @@ libbv_la_SOURCES = \ bv_subtheory_bitblast.cpp \ bv_subtheory_inequality.h \ bv_subtheory_inequality.cpp \ + bv_inequality_graph.h \ + bv_inequality_graph.cpp \ bitblast_strategies.h \ bitblast_strategies.cpp \ slicer.h \ diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index c319ba5f4..2c7d3f8a3 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -33,14 +33,17 @@ namespace bv { typedef unsigned TermId; typedef unsigned ReasonId; + class InequalityGraph { - context::Context d_context; + + + context::Context* d_context; struct InequalityEdge { TermId next; ReasonId reason; InequalityEdge(TermId n, ReasonId r) - : next(n) + : next(n), reason(r) {} }; @@ -50,21 +53,79 @@ class InequalityGraph { unsigned d_bitwidth; bool d_isConstant; BitVector d_value; + public: + InequalityNode(TermId id, unsigned bitwidth, bool isConst = false) + : d_id(id), + d_bitwidth(bitwidth), + d_isConstant(isConst), + d_value(BitVector(bitwidth, 0u)) + {} + TermId getId() const { return d_id; } + unsigned getBitwidth() const { return d_bitwidth; } + bool isConstant() const { return d_isConstant; } + const BitVector& getValue() const { return d_value; } }; - std::vector d_nodes; - std::vector< std::vector > d_nodeEdges; + + struct PQueueElement { + TermId id; + BitVector min_value; + PQueueElement(TermId id, BitVector min) + : id(id), + min_value(min) + {} + bool operator< (const PQueueElement& other) const { + return min_value < other.min_value; + } + }; + typedef __gnu_cxx::hash_map ReasonToIdMap; + typedef __gnu_cxx::hash_map TermNodeToIdMap; + + typedef std::vector Edges; + typedef __gnu_cxx::hash_set TermIdSet; + + typedef std::queue BFSQueue; + + + std::vector d_ineqNodes; + + std::vector< Edges > d_ineqEdges; + std::vector< Edges > d_parentEdges; + + std::vector d_reasonNodes; + std::vector d_termNodes; + ReasonToIdMap d_reasonToIdMap; + TermNodeToIdMap d_termNodeToIdMap; + + TermId registerTerm(TNode term); + ReasonId registerReason(TNode reason); + TNode getReason(ReasonId id) const; + TNode getTerm(TermId id) const; + + Edges& getOutEdges(TermId id) { Assert (id < d_ineqEdges.size()); return d_ineqEdges[id]; } + Edges& getInEdges(TermId id) { Assert (id < d_parentEdges.size()); return d_parentEdges[id]; } + InequalityNode& getInequalityNode(TermId id) { Assert (id < d_ineqNodes.size()); return d_ineqNodes[id]; } + const BitVector& getValue(TermId id) const { return getInequalityNode().getValue(); } + bool addInequalityInternal(TermId a, TermId b, ReasonId reason); + bool areLessThanInternal(TermId a, TermId b); + void getConflictInternal(std::vector& conflict); + + context::CDO d_inConflict; + context::CDList d_conflict; + void setConflict(const std::vector& conflict); public: InequalityGraph(context::Context* c) - : d_context(c) + : d_context(c), + d_ineqNodes(), + d_ineqEdges(), + d_parentEdges(), + d_inConflict(c, false), + d_conflict(c) {} - bool addInequality(TermId a, TermId b, ReasonId reason); - bool propagate(); - bool areLessThan(TermId a, TermId b); - void getConflict(std::vector& conflict); - TermId addTerm(unsigned bitwidth); - TermId addTerm(const BitVector& value); + bool addInequality(TNode a, TNode b, TNode reason); + bool areLessThan(TNode a, TNode b); + void getConflict(std::vector& conflict); }; } diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 3172a8c33..ff1287b3d 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -27,12 +27,34 @@ using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; bool InequalitySolver::check(Theory::Effort e) { - + bool ok = true; + while (!done() && ok) { + TNode fact = get(); + if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) { + TNode a = fact[0][1]; + TNode b = fact[0][0]; + ok = d_inequalityGraph.addInequality(a, b, fact); + } + if (fact.getKind() == kind::BITVECTOR_ULT) { + TNode a = fact[0]; + Tnode b = fact[0]; + ok = d_inequalityGraph.addInequality(a, b, fact); + } + } + if (!ok) { + std::vector conflict; + d_inequalityGraph.getConflict(conflict); + d_bv->setConflict(utils::mkConjunction(conflict)); + return false; + } + return true; } + void InequalitySolver::explain(TNode literal, std::vector& assumptions) { - + Assert (false); } void InequalitySolver::propagate(Theory::Effort e) { - + Assert (false); } + diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 71c6d0d4e..445d5532d 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -21,18 +21,19 @@ #include "theory/bv/theory_bv.h" #include "theory/bv/bv_subtheory.h" +#include "theory/bv/bv_inequality_graph.h" + namespace CVC4 { namespace theory { - - namespace bv { class InequalitySolver: public SubtheorySolver { - + InequalityGraph d_inequalityGraph; public: InequalitySolver(context::Context* c, TheoryBV* bv) - : SubtheorySolver(c, bv) + : SubtheorySolver(c, bv), + d_inequalityGraph() {} bool check(Theory::Effort e); -- 2.30.2