diff options
Diffstat (limited to 'src/theory/bv/bv_sat.h')
| -rw-r--r-- | src/theory/bv/bv_sat.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index 647e4fe9f..2422da0b7 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -82,7 +82,9 @@ class Bitblaster { currently asserted by the DPLL SAT solver. */ /// helper methods + public: bool hasBBAtom(TNode node); + private: bool hasBBTerm(TNode node); void getBBTerm(TNode node, Bits& bits); @@ -101,6 +103,7 @@ class Bitblaster { Node bbOptimize(TNode node); void bbAtom(TNode node); + void addAtom(TNode atom); // division is bitblasted in terms of constraints // so it needs to use private bitblaster interface void bbUdiv(TNode node, Bits& bits); @@ -116,7 +119,7 @@ public: bool solve(bool quick_solve = false); void bitblast(TNode node); void getConflict(std::vector<TNode>& conflict); - void addAtom(TNode atom); + bool getPropagations(std::vector<TNode>& propagations); void explainPropagation(TNode atom, std::vector<Node>& explanation); private: |