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, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 33fff6844..8ae30f636 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -34,6 +34,8 @@ namespace CVC4 {
namespace theory {
namespace quantifiers {
+class SynthEngine;
+
/**
* A base class for generating values for actively-generated enumerators.
* At a high level, the job of this class is to accept a stream of "abstract
@@ -68,7 +70,7 @@ class EnumValGenerator
class SynthConjecture
{
public:
- SynthConjecture(QuantifiersEngine* qe);
+ SynthConjecture(QuantifiersEngine* qe, SynthEngine* p);
~SynthConjecture();
/** presolve */
void presolve();
@@ -165,6 +167,8 @@ class SynthConjecture
private:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
+ /** pointer to the synth engine that owns this */
+ SynthEngine* d_parent;
/** term database sygus of d_qe */
TermDbSygus* d_tds;
/** The feasible guard. */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback