summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblast/eager_bitblaster.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bitblast/eager_bitblaster.h')
-rw-r--r--src/theory/bv/bitblast/eager_bitblaster.h4
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index fbf1a4ddb..3e6190d76 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -36,7 +36,7 @@ class TheoryBV;
class EagerBitblaster : public TBitblaster<Node>
{
public:
- EagerBitblaster(TheoryBV* theory_bv);
+ EagerBitblaster(TheoryBV* theory_bv, context::Context* context);
~EagerBitblaster();
void addAtom(TNode atom);
@@ -51,10 +51,12 @@ class EagerBitblaster : public TBitblaster<Node>
bool assertToSat(TNode node, bool propagate = true);
bool solve();
+ bool solve(const std::vector<Node>& assumptions);
bool collectModelInfo(TheoryModel* m, bool fullModel);
void setProofLog(BitVectorProof* bvp);
private:
+ context::Context* d_context;
std::unique_ptr<context::Context> d_nullContext;
typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback