diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-04 12:46:05 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-04 12:46:05 -0600 |
| commit | 5035105b8d3ca8d260581581ca2beccf9ead3354 (patch) | |
| tree | 80f6db8e777ce3665a0b41967d66a5c33c54c673 /src/theory/quantifiers/term_database_sygus.cpp | |
| parent | b72de87fb2804325137352ce79a6044d1b805576 (diff) | |
Sample based on sygus grammar by default (#1558)
Diffstat (limited to 'src/theory/quantifiers/term_database_sygus.cpp')
| -rw-r--r-- | src/theory/quantifiers/term_database_sygus.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp index 87bfa1901..7d7cc624e 100644 --- a/src/theory/quantifiers/term_database_sygus.cpp +++ b/src/theory/quantifiers/term_database_sygus.cpp @@ -147,6 +147,12 @@ Node TermDbSygus::mkGeneric( const Datatype& dt, int c, std::map< TypeNode, int return ret; } +Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre) +{ + std::map<TypeNode, int> var_count; + return mkGeneric(dt, c, var_count, pre); +} + Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { Assert( n.getType()==tn ); Assert( tn.isDatatype() ); |