diff options
author | lianah <lianahady@gmail.com> | 2013-03-18 19:10:47 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-18 19:10:47 -0400 |
commit | b7054f0e092f54c9e385f4b55a81173602b74b42 (patch) | |
tree | 3d0d81d72f768773d055ed9667a72c2067ea297c /src/theory/bv | |
parent | 25ac2c8f4b45e2b299895e97a30790fbf46cf79f (diff) |
more work on inequality reasoning for bv
Diffstat (limited to 'src/theory/bv')
-rw-r--r-- | src/theory/bv/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/bv/bv_inequality_graph.h | 22 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory.h | 5 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bv_subtheory_inequality.h | 11 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 1 |
6 files changed, 31 insertions, 14 deletions
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 686cc7e83..419acf6ba 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -13,12 +13,12 @@ libbv_la_SOURCES = \ bitblaster.h \ bitblaster.cpp \ bv_subtheory.h \ - bv_subtheory_eq.h \ - bv_subtheory_eq.cpp \ bv_subtheory_core.h \ bv_subtheory_core.cpp \ bv_subtheory_bitblast.h \ bv_subtheory_bitblast.cpp \ + bv_subtheory_inequality.h \ + bv_subtheory_inequality.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 2ac22bb5b..c319ba5f4 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -35,6 +35,24 @@ typedef unsigned ReasonId; class InequalityGraph { context::Context d_context; + + struct InequalityEdge { + TermId next; + ReasonId reason; + InequalityEdge(TermId n, ReasonId r) + : next(n) + reason(r) + {} + }; + + class InequalityNode { + TermId d_id; + unsigned d_bitwidth; + bool d_isConstant; + BitVector d_value; + }; + std::vector<InequalityNode> d_nodes; + std::vector< std::vector<InequalityEdge> > d_nodeEdges; public: @@ -44,7 +62,9 @@ public: bool addInequality(TermId a, TermId b, ReasonId reason); bool propagate(); bool areLessThan(TermId a, TermId b); - void getConflict(std::vector<ReasonId>& conflict); + void getConflict(std::vector<ReasonId>& conflict); + TermId addTerm(unsigned bitwidth); + TermId addTerm(const BitVector& value); }; } diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h index 9e7566ebb..73050ea73 100644 --- a/src/theory/bv/bv_subtheory.h +++ b/src/theory/bv/bv_subtheory.h @@ -61,6 +61,7 @@ const bool d_useSatPropagation = true; // forward declaration class TheoryBV; +typedef context::CDQueue<TNode> AssertionQueue; /** * Abstract base class for bit-vector subtheory solvers * @@ -74,7 +75,7 @@ protected: /** The bit-vector theory */ TheoryBV* d_bv; - context::CDQueue<TNode> d_assertionQueue; + AssertionQueue d_assertionQueue; context::CDO<uint32_t> d_assertionIndex; public: @@ -88,7 +89,7 @@ public: virtual bool check(Theory::Effort e) = 0; virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0; virtual void preRegister(TNode node) {} - virtual void propagate(Effort e) {} + virtual void propagate(Theory::Effort e) {} virtual void collectModelInfo(TheoryModel* m) = 0; bool done() { return d_assertionQueue.size() == d_assertionIndex; } TNode get() { diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 7ccef5ff1..3172a8c33 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -33,6 +33,6 @@ void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) { } -bool InequalitySolver::propagate(Theory::Effort e) { +void InequalitySolver::propagate(Theory::Effort e) { } diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h index 63f9af9e4..71c6d0d4e 100644 --- a/src/theory/bv/bv_subtheory_inequality.h +++ b/src/theory/bv/bv_subtheory_inequality.h @@ -19,18 +19,15 @@ #ifndef __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H #define __CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H -#include "context/context.h" -#include "context/cdqueue.h" -#include "theory/uf/equality_engine.h" -#include "theory/theory.h" - +#include "theory/bv/theory_bv.h" +#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { namespace bv { -class InequalitySolver { +class InequalitySolver: public SubtheorySolver { public: @@ -39,7 +36,7 @@ public: {} bool check(Theory::Effort e); - void propagate(Effort e); + void propagate(Theory::Effort e); void explain(TNode literal, std::vector<TNode>& assumptions); }; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index d457571e2..85077f10d 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -26,7 +26,6 @@ #include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" #include "theory/bv/bv_subtheory.h" -#include "theory/bv/bv_subtheory_eq.h" #include "theory/bv/bv_subtheory_core.h" #include "theory/bv/bv_subtheory_bitblast.h" #include "theory/bv/slicer.h" |