diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-12 15:18:30 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-12 15:18:30 -0500 |
commit | 093d5ffdfa5c1656309da6b9cbdfbbf28574a8a0 (patch) | |
tree | 96c76652c60e286223523cf08f599b4cd84fb687 /src/theory/quantifiers/sygus_sampler.h | |
parent | ec8ea8a9c993435c4c5e671b1beea45ac088de64 (diff) |
Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 29 |
1 files changed, 22 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 98f52992b..526a9e4b1 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -188,14 +188,15 @@ class SygusSampler : public LazyTrieEvaluator }; /** a trie for samples */ PtTrie d_samples_trie; - /** type of nodes we will be registering with this class */ - TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; - /** whether we are registering terms of type d_ftn */ + /** whether we are registering terms of sygus types with this sampler */ bool d_use_sygus_type; - /** map from builtin terms to the sygus term they correspond to */ - std::map<Node, Node> d_builtin_to_sygus; + /** + * For each (sygus) type, a map from builtin terms to the sygus term they + * correspond to. + */ + std::map<TypeNode, std::map<Node, Node> > d_builtin_to_sygus; /** all variables we are sampling values for */ std::vector<Node> d_vars; /** type variables @@ -229,8 +230,22 @@ class SygusSampler : public LazyTrieEvaluator * that type. */ std::map<TypeNode, std::vector<Node> > d_type_consts; - /** the lazy trie */ - LazyTrie d_trie; + /** a lazy trie for each type + * + * This stores the evaluation of all terms registered to this class. + * + * Notice if we are registering sygus terms with this class, then terms + * are grouped into this trie according to their sygus type, and not their + * builtin type. For example, for grammar: + * A -> x | B+1 + * B -> x | 0 | 1 | B+B + * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class, + * then x+0 is registered to d_trie[B] and x is registered to d_trie[A], + * and no rewrite rule is reported. The reason for this is that otherwise + * we would end up reporting many useless rewrites since the same builtin + * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()). + */ + std::map<TypeNode, LazyTrie> d_trie; /** is this sampler valid? * * A sampler can be invalid if sample points cannot be generated for a type |