diff options
author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
commit | 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch) | |
tree | 040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/theory/bv/theory_bv.h | |
parent | 4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff) |
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally
* added more bv regressions
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 36ba17b52..d147c8bb5 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -24,6 +24,7 @@ #include "theory/theory.h" #include "context/context.h" #include "context/cdlist.h" +#include "context/cdhashset.h" #include "theory/bv/theory_bv_utils.h" #include "util/stats.h" @@ -41,7 +42,6 @@ class Bitblaster; class TheoryBV : public Theory { -public: private: @@ -54,7 +54,11 @@ private: /** Bitblaster */ Bitblaster* d_bitblaster; Node d_true; - + + /** Context dependent set of atoms we already propagated */ + context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet; + + bool hasBeenPropagated(TNode node); public: TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); @@ -66,7 +70,7 @@ public: void check(Effort e); - void propagate(Effort e) { } + void propagate(Effort e); Node explain(TNode n); |