From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 10 May 2018 20:35:51 +0000 (-0500)
Subject: Add ITE to default Boolean sygus grammar (#1898)
X-Git-Tag: cvc5-1.0.0~5067
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44b167728ce08c9f1cc7dd5df6e4503f159daff4;p=cvc5.git

Add ITE to default Boolean sygus grammar (#1898)
---

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