diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 81 |
1 files changed, 71 insertions, 10 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 694e4a0cb..4c18205af 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -35,6 +35,24 @@ namespace CVC4 { namespace theory { namespace quantifiers { +/** + * 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 + * values" a1, ..., an, ..., and generate a (possibly larger) stream of + * "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, .... + */ +class EnumValGenerator +{ + public: + virtual ~EnumValGenerator() {} + /** initialize this class with enumerator e */ + virtual void initialize(Node e) = 0; + /** Inform this generator that abstract value v was enumerated. */ + virtual void addValue(Node v) = 0; + /** Get the next concrete value generated by this class. */ + virtual Node getNext() = 0; +}; + /** a synthesis conjecture * This class implements approaches for a synthesis conecjture, given by data * member d_quant. @@ -113,16 +131,6 @@ class SynthConjecture /** has a conjecture been assigned to this class */ bool isAssigned() { return !d_embed_quant.isNull(); } /** - * 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. - */ - bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v); - /** - * Get model value for term n. If n has a value that was excluded by - * datatypes sygus symmetry breaking, this method returns null. - */ - Node getEnumeratedValue(Node n); - /** * Get model value for term n. */ Node getModelValue(Node n); @@ -174,6 +182,47 @@ class SynthConjecture SygusModule* d_master; //------------------------end modules + //------------------------enumerators + /** + * 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. + */ + bool getEnumeratedValues(std::vector<Node>& n, std::vector<Node>& v); + /** + * Get model value for term n. If n has a value that was excluded by + * datatypes sygus symmetry breaking, this method returns null. + */ + Node getEnumeratedValue(Node n); + /** enumerator generators for each actively-generated enumerator */ + std::map<Node, std::unique_ptr<EnumValGenerator> > d_evg; + /** + * Map from enumerators to whether they are currently being + * "actively-generated". That is, we are in a state where we have called + * d_evg[e].addValue(v) for some v, and d_evg[e].getNext() has not yet + * returned null. The range of this map stores the abstract value that + * we are currently generating values from. + */ + std::map<Node, Node> d_ev_curr_active_gen; + /** the current waiting value of each actively-generated enumerator, if any + * + * This caches values that are actively generated and that we have not yet + * passed to a call to SygusModule::constructCandidates. An example of when + * this may occur is when there are two actively-generated enumerators e1 and + * e2. Say on some iteration we actively-generate v1 for e1, the value + * of e2 was excluded by symmetry breaking, and say the current master sygus + * module does not handle partial models. Hence, we abort the current check. + * We remember that the value of e1 was v1 by storing it here, so that on + * a future check when v2 has a proper value, it is returned. + */ + std::map<Node, Node> d_ev_active_gen_waiting; + /** the first value enumerated for each actively-generated enumerator + * + * This is to implement an optimization that only guards the blocking lemma + * for the first value of an actively-generated enumerator. + */ + std::map<Node, Node> d_ev_active_gen_first_val; + //------------------------end enumerators + /** list of constants for quantified formula * The outer Skolems for the negation of d_embed_quant. */ @@ -237,6 +286,18 @@ 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 |