summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblast/simple_bitblaster.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bitblast/simple_bitblaster.h')
-rw-r--r--src/theory/bv/bitblast/simple_bitblaster.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index ebbb2891f..ec0899145 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -53,6 +53,8 @@ class BBSimple : public TBitblaster<Node>
/** Create 'bits' for variable 'var'. */
void makeVariable(TNode var, Bits& bits) override;
+ /** Add d_variables to termSet. */
+ void computeRelevantTerms(std::set<Node>& termSet);
/** Collect model values for all relevant terms given in 'relevantTerms'. */
bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback