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

1 files changed, 22 insertions, 8 deletions

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;