summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/synth_conjecture.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.h6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 9cc488fd2..d7635c816 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -21,6 +21,7 @@
#include <memory>
+#include "smt/env_obj.h"
#include "theory/quantifiers/expr_miner_manager.h"
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
#include "theory/quantifiers/sygus/cegis.h"
@@ -51,10 +52,11 @@ class EnumValueManager;
* determines which approach and optimizations are applicable to the
* conjecture, and has interfaces for implementing them.
*/
-class SynthConjecture
+class SynthConjecture : protected EnvObj
{
public:
- SynthConjecture(QuantifiersState& qs,
+ SynthConjecture(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback