diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-10 15:35:51 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-10 15:35:51 -0500 |
| commit | 44b167728ce08c9f1cc7dd5df6e4503f159daff4 (patch) | |
| tree | b55cecde529c87f865f54afadb1dc3027e65e467 | |
| parent | 31a2135f4650a63fa772f001fcf191f2f7093a8d (diff) | |
Add ITE to default Boolean sygus grammar (#1898)
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index b6a780b6c..f331d8fc6 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -633,17 +633,23 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } } //add operators - for( unsigned i=0; i<3; i++ ){ - CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : kind::OR ); + for (unsigned i = 0; i < 4; i++) + { + CVC4::Kind k = i == 0 + ? kind::NOT + : (i == 1 ? kind::AND : (i == 2 ? kind::OR : kind::ITE)); 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 >() ); - if( k==kind::NOT ){ - cargs.back().push_back(unres_bt); - }else if( k==kind::AND || k==kind::OR ){ - cargs.back().push_back(unres_bt); + 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); + } } } //add predicates for types |