diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 37 |
1 files changed, 22 insertions, 15 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index d5ace4dfe..ef1b4459f 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -83,9 +83,19 @@ class SynthConjecture */ void doSingleInvCheck(std::vector<Node>& lems); /** do syntax-guided enumerative check + * * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. + * + * The method returns true if this conjecture is finished trying solutions + * for the given call to SynthEngine::check. + * + * Notice that we make multiple calls to doCheck on one call to + * SynthEngine::check. For example, if we are using an actively-generated + * enumerator, one enumerated (abstract) term may correspond to multiple + * concrete terms t1, ..., tn to check, where we make up to n calls to doCheck + * when each of t1, ..., tn fails to satisfy the current refinement lemmas. */ - void doCheck(std::vector<Node>& lems); + bool doCheck(std::vector<Node>& lems); /** do refinement * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. */ @@ -94,7 +104,7 @@ class SynthConjecture /** * Prints the synthesis solution to output stream out. This invokes solution * reconstruction if the conjecture is single invocation. Otherwise, it - * returns the enumer + * returns the solution found by sygus enumeration. */ void printSynthSolution(std::ostream& out); /** get synth solutions @@ -182,6 +192,9 @@ class SynthConjecture /** * Get model values for terms n, store in vector v. This method returns true * if and only if all values added to v are non-null. + * + * It removes terms from n that correspond to "inactive" enumerators, that + * is, enumerators whose values have been exhausted. */ bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v); /** @@ -282,18 +295,6 @@ class SynthConjecture d_cinfo[d_candidates[i]].d_inst.push_back(vs[i]); } } - /** - * This performs the next check of the syntax-guided enumerative check - * (see doCheck above). The method returns true if a new solution was - * considered. - * - * Notice that one call to doCheck may correspond to multiple calls to - * doCheckNext. For example, if we are using an actively-generated enumerator, - * one enumerated (abstract) term may correspond to multiple concrete - * terms t1, ..., tn to check, where we make up to n calls to doCheckNext when - * each of t1, ..., tn fail to satisfy the current refinement lemmas. - */ - bool doCheckNext(std::vector<Node>& lems); /** get synth solutions internal * * This function constructs the body of solutions for all @@ -343,9 +344,15 @@ class SynthConjecture /** * Prints the current synthesis solution to the output stream indicated by * the Options object, send a lemma blocking the current solution to the - * output channel. + * output channel, which we refer to as a "stream exclusion lemma". */ void printAndContinueStream(); + /** + * Whether we have guarded a stream exclusion lemma when using sygusStream. + * This is an optimization that allows us to guard only the first stream + * exclusion lemma. + */ + bool d_guarded_stream_exc; //-------------------------------- end sygus stream /** expression miner managers for each function-to-synthesize * |