diff options
Diffstat (limited to 'src/theory/bv/bv_sat.h')
-rw-r--r-- | src/theory/bv/bv_sat.h | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h index c0f3b75ed..647e4fe9f 100644 --- a/src/theory/bv/bv_sat.h +++ b/src/theory/bv/bv_sat.h @@ -97,6 +97,8 @@ class Bitblaster { void initAtomBBStrategies(); void initTermBBStrategies(); + // returns a node that might be easier to bitblast + Node bbOptimize(TNode node); void bbAtom(TNode node); // division is bitblasted in terms of constraints @@ -110,17 +112,20 @@ public: public: Bitblaster(context::Context* c); ~Bitblaster(); - void assertToSat(TNode node); - bool solve(); + bool assertToSat(TNode node, bool propagate = true); + 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: class Statistics { public: - IntStat d_numTermClauses, d_numAtomClauses; + IntStat d_numTermClauses, d_numAtomClauses; + IntStat d_numTerms, d_numAtoms; TimerStat d_bitblastTimer; Statistics(); ~Statistics(); |