diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-06 16:36:23 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-06 16:36:23 -0500 |
commit | 4cd9597f8449bf7117cd76615f7b6a609620c0e9 (patch) | |
tree | ea64fddf730075a18d45bd7920fa3a6c7893997d /src/theory/quantifiers | |
parent | aacd3dda388891bf2302555d0754f1e2a19368b7 (diff) |
Fix degenerate case of sygus grammar construction for 0-argument Bools (#2260)
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 67 |
1 files changed, 34 insertions, 33 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index deea1c261..d6a6d0944 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -392,6 +392,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector<CVC4::Datatype>& datatypes, std::set<Type>& unres) { + NodeManager* nm = NodeManager::currentNM(); Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " " << range << std::endl; // collect the variables @@ -584,9 +585,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( }else{ std::stringstream sserr; sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl; - //AlwaysAssert( false, sserr.str() ); - // FIXME - AlwaysAssert( false ); + throw LogicException(sserr.str()); } //add for all selectors to this type if( !sels[types[i]].empty() ){ @@ -628,7 +627,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } } - //make Boolean type + //------ make Boolean type TypeNode btype = NodeManager::currentNM()->booleanType(); datatypes.push_back(Datatype(dbname)); ops.push_back(std::vector<Expr>()); @@ -667,35 +666,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( pcs.push_back(nullptr); weights.push_back(-1); } - //add operators - for (unsigned i = 0; i < 4; i++) - { - CVC4::Kind k = i == 0 - ? kind::NOT - : (i == 1 ? kind::AND : (i == 2 ? kind::OR : kind::ITE)); - // TODO #1935 ITEs are added to Boolean grammars so that we can infer - // unification strategies. We can do away with this if we can infer - // unification strategies from and/or/not - if (k == ITE && !options::sygusUnif()) - { - continue; - } - Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); - cnames.push_back(kind::kindToString(k)); - cargs.push_back( std::vector< CVC4::Type >() ); - cargs.back().push_back(unres_bt); - if (k != kind::NOT) - { - cargs.back().push_back(unres_bt); - if (k == kind::ITE) - { - cargs.back().push_back(unres_bt); - } - } - pcs.push_back(nullptr); - weights.push_back(-1); - } //add predicates for types for( unsigned i=0; i<types.size(); i++ ){ Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl; @@ -738,6 +708,37 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } } } + // add Boolean connectives, if not in a degenerate case of (recursively) + // having only constant constructors + if (ops.back().size() > consts.size()) + { + for (unsigned i = 0; i < 4; i++) + { + Kind k = i == 0 ? NOT : (i == 1 ? AND : (i == 2 ? OR : ITE)); + // TODO #1935 ITEs are added to Boolean grammars so that we can infer + // unification strategies. We can do away with this if we can infer + // unification strategies from and/or/not + if (k == ITE && !options::sygusUnif()) + { + continue; + } + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + ops.back().push_back(nm->operatorOf(k).toExpr()); + cnames.push_back(kindToString(k)); + cargs.push_back(std::vector<CVC4::Type>()); + cargs.back().push_back(unres_bt); + if (k != NOT) + { + cargs.back().push_back(unres_bt); + if (k == ITE) + { + cargs.back().push_back(unres_bt); + } + } + pcs.push_back(nullptr); + weights.push_back(-1); + } + } if( range==btype ){ startIndex = datatypes.size()-1; } |