Extended rewrite builtin solutions.

2 files changed, 26 insertions, 0 deletions

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 1a3574990..8b2acfec5 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -323,6 +323,31 @@ Node ExtendedRewriter::extendedRewriteIte(Kind itek, Node n, bool full)
     }
     return new_ret;
   }
+  // Boolean true/false return
+  TypeNode tn = n.getType();
+  if( tn.isBoolean() )
+  {
+    for( unsigned i=1; i<=2; i++ )
+    {
+      if( n[i].isConst() )
+      {
+        Node cond = i==1 ? n[0] : n[0].negate();
+        Node other = n[i==1 ? 2 : 1];
+        Kind retk = AND;
+        if( n[i].getConst<bool>() )
+        {
+          retk = OR;
+          cond = cond.negate();
+        }
+        Node new_ret = nm->mkNode( retk, cond, other );
+        if (full)
+        {
+          debugExtendedRewrite(n, new_ret, "ITE const return");
+        }
+        return new_ret;
+      }
+    }
+  }
 
   // get entailed equalities in the condition
   std::vector<Node> eq_conds;
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index f279b4ff4..d4547ca7d 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -727,6 +727,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         out << dt.getSygusType() << " ";
         if (status == 0)
         {
+          sol = d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
           out << sol;
         }
         else