diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-04 16:01:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-04 21:01:41 +0000 |
| commit | be6f9c2ee9201cc5181ce7ba27b6fe992ab3fff6 (patch) | |
| tree | 83e22969a075e584c0b922db1808fb24a4672484 /src | |
| parent | e680a299ac1da58b8fee27e3733d5e5eea255d94 (diff) | |
Improve defaults for sygus default grammars (#7553)
We now add constants from the conjecture to default grammars by default. We also ensure that integer constants are used as real constants when applicable.
Diffstat (limited to 'src')
| -rw-r--r-- | src/options/quantifiers_options.toml | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 11 |
2 files changed, 8 insertions, 5 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index b15ed49a6..e53d3f5ba 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1112,7 +1112,7 @@ name = "Quantifiers" category = "regular" long = "sygus-add-const-grammar" type = "bool" - default = "false" + default = "true" help = "statically add constants appearing in conjecture to grammars" [[option]] diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 9b4cfb9e1..fce0b9f38 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -64,6 +64,7 @@ bool CegGrammarConstructor::hasSyntaxRestrictions(Node q) void CegGrammarConstructor::collectTerms( Node n, std::map<TypeNode, std::unordered_set<Node>>& consts) { + NodeManager * nm = NodeManager::currentNM(); std::unordered_map<TNode, bool> visited; std::unordered_map<TNode, bool>::iterator it; std::stack<TNode> visit; @@ -80,11 +81,13 @@ void CegGrammarConstructor::collectTerms( TypeNode tn = cur.getType(); Node c = cur; if( tn.isReal() ){ - c = NodeManager::currentNM()->mkConst( c.getConst<Rational>().abs() ); + c = nm->mkConst( c.getConst<Rational>().abs() ); } - if( std::find( consts[tn].begin(), consts[tn].end(), c )==consts[tn].end() ){ - Trace("cegqi-debug") << "...consider const : " << c << std::endl; - consts[tn].insert(c); + consts[tn].insert(c); + if (tn.isInteger()) + { + TypeNode rtype = nm->realType(); + consts[rtype].insert(c); } } // recurse |