diff options
Diffstat (limited to 'src/theory/bv/bitblaster.h')
| -rw-r--r-- | src/theory/bv/bitblaster.h | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h index ada9802bd..3aee0ee1a 100644 --- a/src/theory/bv/bitblaster.h +++ b/src/theory/bv/bitblaster.h @@ -51,6 +51,7 @@ class BVSatSolverInterface; namespace theory { class OutputChannel; +class TheoryModel; namespace bv { @@ -82,7 +83,8 @@ class Bitblaster { }; typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction > TermDefMap; - typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet; + typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet; typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*); typedef Node (*AtomBBStrategy) (TNode, Bitblaster*); @@ -95,7 +97,7 @@ class Bitblaster { // caches and mappings TermDefMap d_termCache; AtomSet d_bitblastedAtoms; - + VarSet d_variables; context::CDList<prop::SatLiteral> d_assertedAtoms; /**< context dependent list storing the atoms currently asserted by the DPLL SAT solver. */ @@ -136,7 +138,29 @@ public: void explain(TNode atom, std::vector<TNode>& explanation); EqualityStatus getEqualityStatus(TNode a, TNode b); - + /** + * Return a constant Node representing the value of a variable + * in the current model. + * @param a + * + * @return + */ + Node getVarValue(TNode a); + /** + * Adds a constant value for each bit-blasted variable in the model. + * + * @param m the model + */ + void collectModelInfo(TheoryModel* m); + /** + * Stores the variable (or non-bv term) and its corresponding bits. + * + * @param var + * @param bits + */ + void storeVariable(TNode var) { + d_variables.insert(var); + } private: |