diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-21 07:01:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-21 07:01:59 -0500 |
| commit | 28e9077fad9d5c61c61a1762e7cf021c226cb9c2 (patch) | |
| tree | 80781281cd4d00c0b234cbd16ee5e39be67bff96 /src/theory/quantifiers/sygus_sampler.h | |
| parent | 583277b93d581e1de40b9df8468fe412ba293438 (diff) | |
Improve sygus sampling for strings (#1802)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.h')
| -rw-r--r-- | src/theory/quantifiers/sygus_sampler.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index a66e7ee21..b741b60d4 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -335,8 +335,12 @@ class SygusSampler : public LazyTrieEvaluator std::map<TypeNode, std::vector<unsigned> > d_rvalue_cindices; /** map from sygus types to non-variable nullary constructors */ std::map<TypeNode, std::vector<unsigned> > d_rvalue_null_cindices; + /** the random string alphabet */ + std::vector<unsigned> d_rstring_alphabet; /** map from variables to sygus types that include them */ std::map<Node, std::vector<TypeNode> > d_var_sygus_types; + /** map from constants to sygus types that include them */ + std::map<Node, std::vector<TypeNode> > d_const_sygus_types; /** register sygus type, intializes the above two data structures */ void registerSygusType(TypeNode tn); }; |