sygus input language and benchmark

1 files changed, 83 insertions, 1 deletions

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 82498b624..50edc3311 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -62,6 +62,9 @@ private:
   std::pair<Expr, std::string> d_lastNamedTerm;
   // this is a user-context stack
   std::stack< std::map<Expr, std::string> > d_unsatCoreNames;
+  std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols;
+  std::vector< std::pair<std::string, Expr> > d_sygusFuns;
+  size_t d_nextSygusFun;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
@@ -94,7 +97,7 @@ public:
    *
    * @param name the name of the logic (e.g., QF_UF, AUFLIA)
    */
-  void setLogic(const std::string& name);
+  void setLogic(std::string name);
 
   /**
    * Get the logic.
@@ -107,6 +110,9 @@ public:
   bool v2_5() const {
     return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5;
   }
+  bool sygus() const {
+    return getInput()->getLanguage() == language::input::LANG_SYGUS;
+  }
 
   void setLanguage(InputLanguage lang) {
     ((Smt2Input*) getInput())->setLanguage(lang);
@@ -166,6 +172,82 @@ public:
     return getExprManager()->mkConst(AbstractValue(Integer(name.substr(1))));
   }
 
+  Expr mkSygusVar(const std::string& name, const Type& type) {
+    Expr e = mkBoundVar(name, type);
+    d_sygusVars.push_back(e);
+    return e;
+  }
+
+  void addSygusFun(const std::string& fun, Expr eval) {
+    d_sygusFuns.push_back(std::make_pair(fun, eval));
+  }
+
+  void defineSygusFuns() {
+    // only define each one once
+    while(d_nextSygusFun < d_sygusFuns.size()) {
+      std::pair<std::string, Expr> p = d_sygusFuns[d_nextSygusFun];
+      std::string fun = p.first;
+      Expr eval = p.second;
+      FunctionType evalType = eval.getType();
+      std::vector<Type> argTypes = evalType.getArgTypes();
+      Type rangeType = evalType.getRangeType();
+
+      // first make the function type
+      std::vector<Type> funType;
+      for(size_t j = 1; j < argTypes.size(); ++j) {
+        funType.push_back(argTypes[j]);
+      }
+      Type funt = getExprManager()->mkFunctionType(funType, rangeType);
+
+      // 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);
+      Expr lambda = mkFunction(fun, t, ExprManager::VAR_FLAG_DEFINED);
+      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]);
+      }
+      Expr apply = getExprManager()->mkExpr(kind::APPLY_UF, applyv);
+      Command* cmd = new DefineFunctionCommand(fun, lambda, d_sygusVars, apply);
+      preemptCommand(cmd);
+
+      ++d_nextSygusFun;
+    }
+  }
+
+  void addSygusConstraint(Expr constraint) {
+    d_sygusConstraints.push_back(constraint);
+  }
+
+  Expr getSygusConstraints() {
+    switch(d_sygusConstraints.size()) {
+    case 0: return getExprManager()->mkConst(bool(true));
+    case 1: return d_sygusConstraints[0];
+    default: return getExprManager()->mkExpr(kind::AND, d_sygusConstraints);
+    }
+  }
+
+  const std::vector<Expr>& getSygusVars() {
+    return d_sygusVars;
+  }
+
+  const std::vector<Expr>& getSygusFunSymbols() {
+    return d_sygusFunSymbols;
+  }
+
   /**
    * Smt2 parser provides its own checkDeclaration, which does the
    * same as the base, but with some more helpful errors.