From 44b167728ce08c9f1cc7dd5df6e4503f159daff4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 May 2018 15:35:51 -0500 Subject: [PATCH] Add ITE to default Boolean sygus grammar (#1898) --- .../quantifiers/sygus/sygus_grammar_cons.cpp | 18 ++++++++++++------ 1 file 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 -- 2.30.2