Handle (degenerate) case of synthesis conjectures for constants. Disable delta lemmas.

4 files changed, 56 insertions, 29 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8b7c0bda2..8dac9915e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -586,7 +586,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           ++i) {
         terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
       }
-      Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms);
+      Expr bvl;
+      if( !terms.empty() ){
+        bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms);
+      }
       terms.clear();
       terms.push_back(bvl);
     }
@@ -633,8 +636,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
         std::vector<Type> evalType;
         evalType.push_back(dtt);
-        for(size_t j = 0; j < terms[0].getNumChildren(); ++j) {
-          evalType.push_back(terms[0][j].getType());
+        if( !terms[0].isNull() ){
+          for(size_t j = 0; j < terms[0].getNumChildren(); ++j) {
+            evalType.push_back(terms[0][j].getType());
+          }
         }
         evalType.push_back(sorts[i]);
         Expr eval = PARSER_STATE->mkVar(name, EXPR_MANAGER->mkFunctionType(evalType));
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 20f3c364b..0c1b36655 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -489,26 +489,30 @@ void Smt2::includeFile(const std::string& filename) {
       ss << fun << "_v_" << j;
       sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), argTypes[j]));
     }
-    Type funt = getExprManager()->mkFunctionType(funType, rangeType);
-    Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
+    Type funt;
+    if( !funType.empty() ){
+      funt = getExprManager()->mkFunctionType(funType, rangeType);
+      Debug("parser-sygus") << "...eval function type : " << funt << std::endl;
+
+      // copy the bound vars
+      /*
+      std::vector<Expr> sygusVars;
+      //std::vector<Type> types;
+      for(size_t i = 0; i < d_sygusVars.size(); ++i) {
+        std::stringstream ss;
+        ss << d_sygusVars[i];
+        Type type = d_sygusVars[i].getType();
+        sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
+        //types.push_back(type);
+      }
+      Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
+      */
 
-    // copy the bound vars
-    /*
-    std::vector<Expr> sygusVars;
-    //std::vector<Type> types;
-    for(size_t i = 0; i < d_sygusVars.size(); ++i) {
-      std::stringstream ss;
-      ss << d_sygusVars[i];
-      Type type = d_sygusVars[i].getType();
-      sygusVars.push_back(getExprManager()->mkBoundVar(ss.str(), type));
-      //types.push_back(type);
+      //Type t = getExprManager()->mkFunctionType(types, rangeType);
+      //Debug("parser-sygus") << "...function type : " << t << std::endl;
+    }else{
+      funt = rangeType;
     }
-    Debug("parser-sygus") << "...made vars, #vars=" << sygusVars.size() << std::endl;
-    */
-
-    //Type t = getExprManager()->mkFunctionType(types, rangeType);
-    //Debug("parser-sygus") << "...function type : " << t << std::endl;
-
     Expr lambda = mkFunction(fun, funt, ExprManager::VAR_FLAG_DEFINED);
     Debug("parser-sygus") << "...made function : " << lambda << std::endl;
     std::vector<Expr> applyv;
@@ -560,8 +564,13 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
     bvs.push_back(bv);
     extraArgs.push_back(bv);
   }
-  bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
-  Expr bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs);
+  if( !terms[0].isNull() ){
+    bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
+  }
+  Expr bvl;
+  if( !bvs.empty() ){
+    bvl = getExprManager()->mkExpr(kind::BOUND_VAR_LIST, bvs);
+  }
   Debug("parser-sygus") << "...made bv list " << bvl << std::endl;
   std::vector<Expr> patv;
   patv.push_back(eval);
@@ -573,7 +582,9 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
   Expr cpatv = getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, applyv);
   Debug("parser-sygus") << "...made eval ctor apply " << cpatv << std::endl;
   patv.push_back(cpatv);
-  patv.insert(patv.end(), terms[0].begin(), terms[0].end());
+  if( !terms[0].isNull() ){  
+    patv.insert(patv.end(), terms[0].begin(), terms[0].end());
+  }
   Expr evalApply = getExprManager()->mkExpr(kind::APPLY_UF, patv);
   Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
   std::vector<Expr> builtApply;
@@ -581,7 +592,9 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
     std::vector<Expr> patvb;
     patvb.push_back(evals[DatatypeType(extraArgs[k].getType())]);
     patvb.push_back(extraArgs[k]);
-    patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
+    if( !terms[0].isNull() ){
+      patvb.insert(patvb.end(), terms[0].begin(), terms[0].end());
+    }
     builtApply.push_back(getExprManager()->mkExpr(kind::APPLY_UF, patvb));
   }
   for(size_t k = 0; k < builtApply.size(); ++k) {
@@ -599,9 +612,11 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
   }
   Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
   Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
-  Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
-  pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
-  assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
+  if( !bvl.isNull() ){
+    Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
+    pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
+    assertion = getExprManager()->mkExpr(kind::FORALL, bvl, assertion, pattern);
+  }
   Debug("parser-sygus") << "...made assertion " << assertion << std::endl;
 
   //linearize multiplication if possible
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 7553eb736..ea97513b8 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -505,7 +505,11 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       }
       if( !(Trace.isOn("cegqi-stats")) ){
         out << "(define-fun " << f << " ";
-        out << dt.getSygusVarList() << " ";
+        if( dt.getSygusVarList().isNull() ){
+          out << "() ";
+        }else{
+          out << dt.getSygusVarList() << " ";
+        }
         out << dt.getSygusType() << " ";
         if( status==0 ){
           out << sol;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index b3c1e1eaa..a612db872 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -637,6 +637,8 @@ Node CegInstantiator::applySubstitution( Node n, std::vector< Node >& subs, std:
 //check if delta has a lower bound L
 // if so, add lemma L>0 => L>d
 void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
+  return;
+  /*  disable for now
   if( !d_n_delta.isNull() ){
     Theory* theory = d_qe->getTheoryEngine()->theoryOf( THEORY_ARITH );
     if( theory && d_qe->getTheoryEngine()->isTheoryEnabled( THEORY_ARITH ) ){
@@ -701,6 +703,7 @@ void CegInstantiator::getDeltaLemmas( std::vector< Node >& lems ) {
       }
     }
   }
+  */
 }
 
 void CegInstantiator::check() {