diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 3a43eb83d..cf6178fdb 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -280,6 +280,11 @@ class SynthConjecture /** the asserted (negated) conjecture */ Node d_quant; + /** + * The side condition for solving the conjecture, after conversion to deep + * embedding. + */ + Node d_embedSideCondition; /** (negated) conjecture after simplification */ Node d_simp_quant; /** (negated) conjecture after simplification, conversion to deep embedding */ @@ -363,6 +368,8 @@ class SynthConjecture * output channel, which we refer to as a "stream exclusion lemma". */ void printAndContinueStream(); + /** exclude the current solution */ + void excludeCurrentSolution(); /** * Whether we have guarded a stream exclusion lemma when using sygusStream. * This is an optimization that allows us to guard only the first stream |