Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare-var vs synth-fun arguments. Handle ground properties in sythesis conjectures.

2 files changed, 54 insertions, 14 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 67f26533e..3f999366d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -636,8 +636,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         DatatypeType dtt = datatypeTypes[i];
         const Datatype& dt = dtt.getDatatype();
         Expr eval = evals[dtt];
+        Debug("parser-sygus") << "Sygus : process grammar : " << dt << std::endl;
         for(size_t j = 0; j < dt.getNumConstructors(); ++j) {
           const DatatypeConstructor& ctor = dt[j];
+          Debug("parser-sygus") << "Sygus : process constructor " << j << " : " << dt[j] << std::endl;
           std::vector<Expr> bvs, extraArgs;
           for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
             std::string vname = "v_" + ctor[k].getName();
@@ -647,6 +649,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           }
           bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
           Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, bvs);
+          Debug("parser-sygus") << "...made bv list." << std::endl;
           std::vector<Expr> patv;
           patv.push_back(eval);
           std::vector<Expr> applyv;
@@ -654,9 +657,12 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           applyv.insert(applyv.end(), extraArgs.begin(), extraArgs.end());
           for(size_t k = 0; k < applyv.size(); ++k) {
           }
-          patv.push_back(MK_EXPR(kind::APPLY_CONSTRUCTOR, applyv));
+          Expr cpatv = MK_EXPR(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());
           Expr evalApply = MK_EXPR(kind::APPLY_UF, patv);
+          Debug("parser-sygus") << "...made eval apply " << evalApply << std::endl;
           std::vector<Expr> builtApply;
           for(size_t k = 0; k < extraArgs.size(); ++k) {
             patv.clear();
@@ -667,11 +673,19 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           }
           for(size_t k = 0; k < builtApply.size(); ++k) {
           }
-          Expr builtTerm = ops[i][j].getKind() == kind::BUILTIN ? MK_EXPR(ops[i][j], builtApply) : ops[i][j];
+          Expr builtTerm;
+          //if( ops[i][j].getKind() == kind::BUILTIN ){
+          if( !builtApply.empty() ){
+            builtTerm = MK_EXPR(ops[i][j], builtApply);
+          }else{
+            builtTerm = ops[i][j];
+          }
+          Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
           Expr assertion = MK_EXPR(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
           Expr pattern = MK_EXPR(kind::INST_PATTERN, evalApply);
           pattern = MK_EXPR(kind::INST_PATTERN_LIST, pattern);
           assertion = MK_EXPR(kind::FORALL, bvl, assertion, pattern);
+          Debug("parser-sygus") << "Add assertion " << assertion << std::endl;
           seq->addCommand(new AssertCommand(assertion));
         }
       }
@@ -679,9 +693,13 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
     }
   | /* constraint */
     CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { PARSER_STATE->defineSygusFuns(); }
+    { Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
+      PARSER_STATE->defineSygusFuns(); 
+      Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
+    }
     term[expr, expr2]
-    { PARSER_STATE->addSygusConstraint(expr);
+    { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
+      PARSER_STATE->addSygusConstraint(expr);
       $cmd = new EmptyCommand();
     }
   | /* check-synth */
@@ -689,9 +707,15 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
     { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType());
       Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar));
       std::vector<Expr> bodyv;
+      Debug("parser-sygus") << "Sygus : Constructing sygus constraint..." << std::endl;
       Expr body = EXPR_MANAGER->mkExpr(kind::NOT, PARSER_STATE->getSygusConstraints());
-      body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body);
+      Debug("parser-sygus") << "...constructed sygus constraint " << body << std::endl;      
+      if( !PARSER_STATE->getSygusVars().empty() ){
+        body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body);
+        Debug("parser-sygus") << "...constructed exists " << body << std::endl;   
+      }
       body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+      Debug("parser-sygus") << "...constructed forall " << body << std::endl;   
       Command* c = new SetUserAttributeCommand("sygus", sygusVar);
       c->setMuted(true);
       PARSER_STATE->preemptCommand(c);
@@ -722,13 +746,15 @@ sygusGTerm[CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops]
     ( builtinOp[k]
       { ops.push_back(EXPR_MANAGER->operatorOf(k));
         name = kind::kindToString(k);
+        Debug("parser-sygus") << "Sygus : grammar builtin symbol : " << name << std::endl;
       }
-    | symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    | symbol[name,CHECK_NONE,SYM_VARIABLE]
       { // what is this sygus term trying to accomplish here, if the
         // symbol isn't yet declared?!  probably the following line will
         // fail, but we need an operator to continue here..
         Expr bv = PARSER_STATE->getVariable(name);
         ops.push_back(bv);
+        Debug("parser-sygus") << "Sygus : grammar symbol : " << name << std::endl;
       }
     )
     { name = dt.getName() + "_" + name;
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 50edc3311..35842f308 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -187,41 +187,55 @@ public:
     while(d_nextSygusFun < d_sygusFuns.size()) {
       std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
       std::string fun = p.first;
+      Debug("parser-sygus") << "Sygus : define fun " << fun << std::endl;
       Expr eval = p.second;
       FunctionType evalType = eval.getType();
       std::vector<Type> argTypes = evalType.getArgTypes();
       Type rangeType = evalType.getRangeType();
+      Debug("parser-sygus") << "...eval type : " << evalType << ", #args=" << argTypes.size() << std::endl;
 
       // first make the function type
+      std::vector<Expr> sygusVars;
       std::vector<Type> funType;
       for(size_t j = 1; j < argTypes.size(); ++j) {
         funType.push_back(argTypes[j]);
+        std::stringstream ss;
+        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;
 
       // copy the bound vars
+      /*
       std::vector<Expr> sygusVars;
-      std::vector<Type> types;
+      //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);
+        //types.push_back(type);
       }
-
-      Type t = getExprManager()->mkFunctionType(types, rangeType);
-      Expr lambda = mkFunction(fun, t, ExprManager::VAR_FLAG_DEFINED);
+      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;
       Expr funbv = getExprManager()->mkBoundVar(std::string("f") + fun, argTypes[0]);
       d_sygusFunSymbols.push_back(funbv);
       applyv.push_back(eval);
       applyv.push_back(funbv);
-      for(size_t i = 0; i < d_sygusVars.size(); ++i) {
-        applyv.push_back(d_sygusVars[i]);
+      for(size_t i = 0; i < sygusVars.size(); ++i) {
+        applyv.push_back(sygusVars[i]);
       }
       Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
-      Command* cmd = new DefineFunctionCommand(fun, lambda, d_sygusVars, apply);
+      Debug("parser-sygus") << "...made apply " << apply << std::endl;
+      Command* cmd = new DefineFunctionCommand(fun, lambda, sygusVars, apply);
       preemptCommand(cmd);
 
       ++d_nextSygusFun;