sygus input language and benchmark

13 files changed, 704 insertions, 73 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9035ed8b8..c011671f8 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -34,6 +34,7 @@
 #include "expr/command.h"
 #include "util/configuration.h"
 #include "options/options.h"
+#include "theory/quantifiers/options.h"
 #include "main/command_executor.h"
 
 #ifdef PORTFOLIO_BUILD
@@ -198,6 +199,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
         opts.set(options::inputLanguage, language::input::LANG_CVC4);
+      } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
+                || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
+        opts.set(options::inputLanguage, language::input::LANG_SYGUS);
       }
     }
   }
@@ -206,6 +210,12 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage]));
   }
 
+  // if doing sygus, turn on CEGQI by default
+  if(opts[options::inputLanguage] == language::input::LANG_SYGUS &&
+     !opts.wasSetByUser(options::ceGuidedInst)) {
+    opts.set(options::ceGuidedInst, true);
+  }
+
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(CVC4::null_os);
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 62bff7ec1..a9721ad20 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -265,6 +265,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
     smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   tptp                           TPTP format (cnf and fof)\n\
+  sygus                          SyGuS format\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
   auto                           match output language to input language\n\
@@ -274,8 +275,8 @@ Languages currently supported as arguments to the --output-lang option:\n\
   smt | smtlib | smt2 |\n\
     smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
-  z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
   tptp                           TPTP format\n\
+  z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
   ast                            internal format (simple syntax trees)\n\
 ";
 
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index f8730e372..4c779c46a 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -32,6 +32,7 @@
 #include "parser/cvc/cvc_input.h"
 #include "parser/smt1/smt1_input.h"
 #include "parser/smt2/smt2_input.h"
+#include "parser/smt2/sygus_input.h"
 #include "parser/tptp/tptp_input.h"
 #include "util/output.h"
 
@@ -206,6 +207,10 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new Smt2Input(inputStream, lang);
     break;
 
+  case LANG_SYGUS:
+    input = new SygusInput(inputStream);
+    break;
+
   case LANG_TPTP:
     input = new TptpInput(inputStream);
     break;
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 241c9c815..a2faec704 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -93,6 +93,9 @@ Parser* ParserBuilder::build()
   case language::input::LANG_SMTLIB_V2_5:
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
+  case language::input::LANG_SYGUS:
+    parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
+    break;
   case language::input::LANG_TPTP:
     parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index bf42e9288..38de258cc 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -33,6 +33,8 @@ libparsersmt2_la_SOURCES = \
 	smt2.cpp \
 	smt2_input.h \
 	smt2_input.cpp \
+	sygus_input.h \
+	sygus_input.cpp \
 	$(ANTLR_STUFF)
 
 BUILT_SOURCES = \
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index d7f4489bf..320fead5f 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -215,6 +215,18 @@ parseCommand returns [CVC4::Command* cmd = NULL]
   ;
 
 /**
+ * Parses a SyGuS command
+ * @return the parsed SyGuS command, or NULL if we've reached the end of the input
+ */
+parseSygus returns [CVC4::Command* cmd = NULL]
+@declarations {
+  std::string name;
+}
+  : LPAREN_TOK c=sygusCommand RPAREN_TOK { $cmd = c; }
+  | EOF { $cmd = 0; }
+  ;
+
+/**
  * Parse the internal portion of the command, ignoring the surrounding
  * parentheses.
  */
@@ -468,6 +480,302 @@ command returns [CVC4::Command* cmd = NULL]
     }
   ;
 
+sygusCommand returns [CVC4::Command* cmd = NULL]
+@declarations {
+  std::string name, fun;
+  std::vector<std::string> names;
+  Expr expr, expr2;
+  Type t, range;
+  std::vector<Expr> terms;
+  std::vector<Type> sorts;
+  std::vector<std::pair<std::string, Type> > sortedVarNames;
+  SExpr sexpr;
+  CommandSequence* seq;
+  std::vector<CVC4::Datatype> datatypes;
+  std::vector< std::vector<Expr> > ops;
+}
+  : /* set the logic */
+    SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
+    { PARSER_STATE->setLogic(name);
+      $cmd = new SetBenchmarkLogicCommand("ALL_SUPPORTED"); }
+  | /* set-options */
+    SET_OPTIONS_TOK LPAREN_TOK { seq = new CommandSequence(); }
+    ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] symbolicExpr[sexpr] RPAREN_TOK
+      { PARSER_STATE->setOption(name.c_str(), sexpr);
+        seq->addCommand(new SetOptionCommand(name.c_str() + 1, sexpr));
+      }
+    )+ RPAREN_TOK
+    { $cmd = seq; }
+  | /* sort definition */
+    DEFINE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_SORT]
+    { PARSER_STATE->checkUserSymbol(name); }
+    LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
+    { PARSER_STATE->pushScope(true);
+      for(std::vector<std::string>::const_iterator i = names.begin(),
+            iend = names.end();
+          i != iend;
+          ++i) {
+        sorts.push_back(PARSER_STATE->mkSort(*i));
+      }
+    }
+    sortSymbol[t,CHECK_DECLARED]
+    { PARSER_STATE->popScope();
+      // Do NOT call mkSort, since that creates a new sort!
+      // This name is not its own distinct sort, it's an alias.
+      PARSER_STATE->defineParameterizedType(name, sorts, t);
+      $cmd = new DefineTypeCommand(name, sorts, t);
+    }
+  | /* declare-var */
+    DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    sortSymbol[t,CHECK_DECLARED]
+    { PARSER_STATE->mkSygusVar(name, t);
+      $cmd = new EmptyCommand(); }
+  | /* declare-fun */
+    (DECLARE_FUN_TOK)=>
+    DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { PARSER_STATE->parseError("declare-fun not yet supported in SyGuS input"); }
+  | /* function definition */
+    DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
+    sortSymbol[t,CHECK_DECLARED]
+    { /* add variables to parser state before parsing term */
+      Debug("parser") << "define fun: '" << name << "'" << std::endl;
+      if( sortedVarNames.size() > 0 ) {
+        std::vector<CVC4::Type> sorts;
+        sorts.reserve(sortedVarNames.size());
+        for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+              sortedVarNames.begin(), iend = sortedVarNames.end();
+            i != iend;
+            ++i) {
+          sorts.push_back((*i).second);
+        }
+        t = EXPR_MANAGER->mkFunctionType(sorts, t);
+      }
+      PARSER_STATE->pushScope(true);
+      for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+            sortedVarNames.begin(), iend = sortedVarNames.end();
+          i != iend;
+          ++i) {
+        terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
+      }
+    }
+    term[expr, expr2]
+    { PARSER_STATE->popScope();
+      // declare the name down here (while parsing term, signature
+      // must not be extended with the name itself; no recursion
+      // permitted)
+      Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
+      $cmd = new DefineFunctionCommand(name, func, terms, expr);
+    }
+  | /* synth-fun */
+    SYNTH_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
+    LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
+    { seq = new CommandSequence();
+      PARSER_STATE->pushScope(true);
+      for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+            sortedVarNames.begin(), iend = sortedVarNames.end();
+          i != iend;
+          ++i) {
+        terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second));
+      }
+      Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, terms);
+      terms.clear();
+      terms.push_back(bvl);
+    }
+    sortSymbol[range,CHECK_DECLARED]
+    LPAREN_TOK
+    ( LPAREN_TOK
+      symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->pushScope(true); }
+      sortSymbol[t,CHECK_DECLARED]
+      { sorts.push_back(t);
+        datatypes.push_back(Datatype(name));
+        ops.push_back(std::vector<Expr>());
+        if(!PARSER_STATE->isUnresolvedType(name)) {
+          // if not unresolved, must be undeclared
+          PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
+        }
+      }
+      // Note the official spec for NTDef is missing the ( parens )
+      // but they are necessary to parse SyGuS examples
+      LPAREN_TOK sygusGTerm[datatypes.back(), ops.back()]+ RPAREN_TOK
+      RPAREN_TOK
+      { PARSER_STATE->popScope(); }
+    )+
+    RPAREN_TOK
+    { PARSER_STATE->popScope();
+      seq = new CommandSequence();
+      std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
+      seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
+      std::map<DatatypeType, Expr> evals;
+      // make all the evals first, since they are mutually referential
+      for(size_t i = 0; i < datatypeTypes.size(); ++i) {
+        DatatypeType dtt = datatypeTypes[i];
+        const Datatype& dt = dtt.getDatatype();
+        name = "eval_" + dt.getName();
+        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());
+        }
+        evalType.push_back(sorts[i]);
+        Expr eval = PARSER_STATE->mkVar(name, EXPR_MANAGER->mkFunctionType(evalType));
+        evals.insert(std::make_pair(dtt, eval));
+        if(i == 0) {
+          PARSER_STATE->addSygusFun(fun, eval);
+        }
+      }
+      // now go through and settle everything
+      for(size_t i = 0; i < datatypeTypes.size(); ++i) {
+        DatatypeType dtt = datatypeTypes[i];
+        const Datatype& dt = dtt.getDatatype();
+        Expr eval = evals[dtt];
+        for(size_t j = 0; j < dt.getNumConstructors(); ++j) {
+          const DatatypeConstructor& ctor = dt[j];
+          std::vector<Expr> bvs, extraArgs;
+          for(size_t k = 0; k < ctor.getNumArgs(); ++k) {
+            Expr bv = EXPR_MANAGER->mkBoundVar(ctor[k].getName(), SelectorType(ctor[k].getType()).getRangeType());
+            bvs.push_back(bv);
+            extraArgs.push_back(bv);
+          }
+          bvs.insert(bvs.end(), terms[0].begin(), terms[0].end());
+          Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, bvs);
+          std::vector<Expr> patv;
+          patv.push_back(eval);
+          std::vector<Expr> applyv;
+          applyv.push_back(ctor.getConstructor());
+          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));
+          patv.insert(patv.end(), terms[0].begin(), terms[0].end());
+          Expr evalApply = MK_EXPR(kind::APPLY_UF, patv);
+          std::vector<Expr> builtApply;
+          for(size_t k = 0; k < extraArgs.size(); ++k) {
+            patv.clear();
+            patv.push_back(evals[DatatypeType(extraArgs[k].getType())]);
+            patv.push_back(extraArgs[k]);
+            patv.insert(patv.end(), terms[0].begin(), terms[0].end());
+            builtApply.push_back(MK_EXPR(kind::APPLY_UF, patv));
+          }
+          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 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);
+          seq->addCommand(new AssertCommand(assertion));
+        }
+      }
+      $cmd = seq;
+    }
+  | /* constraint */
+    CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { PARSER_STATE->defineSygusFuns(); }
+    term[expr, expr2]
+    { PARSER_STATE->addSygusConstraint(expr);
+      $cmd = new EmptyCommand();
+    }
+  | /* check-synth */
+    CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    { 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;
+      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);
+      body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr);
+      Command* c = new SetUserAttributeCommand("sygus", sygusVar);
+      c->setMuted(true);
+      PARSER_STATE->preemptCommand(c);
+      c = new AssertCommand(body);
+      PARSER_STATE->preemptCommand(c);
+      $cmd = new CheckSatCommand();
+    }
+
+    /* error handling */
+  | (~(CHECK_SYNTH_TOK))=> token=.
+    { std::string id = AntlrInput::tokenText($token);
+      std::stringstream ss;
+      ss << "Not a recognized SyGuS command: `" << id << "'";
+      PARSER_STATE->parseError(ss.str());
+    }
+  ;
+
+// SyGuS grammar term
+sygusGTerm[CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops]
+@declarations {
+  std::string name;
+  Kind k;
+  Type t;
+  CVC4::DatatypeConstructor* ctor = NULL;
+  unsigned count = 0;
+}
+  : LPAREN_TOK
+    ( builtinOp[k]
+      { ops.push_back(EXPR_MANAGER->operatorOf(k));
+        name = kind::kindToString(k);
+      }
+    | symbol[name,CHECK_UNDECLARED,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);
+      }
+    )
+    { name = dt.getName() + "_" + name;
+      std::string testerId("is-");
+      testerId.append(name);
+      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+      ctor = new CVC4::DatatypeConstructor(name, testerId);
+    }
+    ( sortSymbol[t,CHECK_NONE]
+      { std::stringstream cname;
+        cname << name << "_" << ++count;
+        ctor->addArg(cname.str(), t);
+      } )+ RPAREN_TOK
+    { dt.addConstructor(*ctor);
+      delete ctor; }
+  | INTEGER_LITERAL
+    { ops.push_back(MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL))));
+      name = dt.getName() + "_" + AntlrInput::tokenText($INTEGER_LITERAL);
+      std::string testerId("is-");
+      testerId.append(name);
+      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+      CVC4::DatatypeConstructor c(name, testerId);
+      dt.addConstructor(c);
+    }
+  | HEX_LITERAL
+    { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
+      std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
+      ops.push_back(MK_CONST( BitVector(hexString, 16) ));
+    }
+  | BINARY_LITERAL
+    { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
+      std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
+      ops.push_back(MK_CONST( BitVector(binString, 2) ));
+    }
+  | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
+    { Expr bv = PARSER_STATE->getVariable(name);
+      ops.push_back(bv);
+      name = dt.getName() + "_" + name;
+      std::string testerId("is-");
+      testerId.append(name);
+      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
+      CVC4::DatatypeConstructor c(name, testerId);
+      dt.addConstructor(c);
+    }
+  ;
+
 // Separate this into its own rule (can be invoked by set-info or meta-info)
 metaInfoInternal[CVC4::Command*& cmd]
 @declarations {
@@ -749,7 +1057,7 @@ datatypesDefCommand[bool isCo, CVC4::Command*& cmd]
   std::string name;
   std::vector<Type> sorts;
 }
-  : { PARSER_STATE->checkThatLogicIsSet(); 
+  : { PARSER_STATE->checkThatLogicIsSet();
     /* open a scope to keep the UnresolvedTypes contained */
     PARSER_STATE->pushScope(true); }
   LPAREN_TOK /* parametric sorts */
@@ -759,7 +1067,7 @@ datatypesDefCommand[bool isCo, CVC4::Command*& cmd]
   RPAREN_TOK
   LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK
   { PARSER_STATE->popScope();
-  cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
+    cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); }
   ;
 
 rewriterulesCommand[CVC4::Command*& cmd]
@@ -1785,6 +2093,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
   std::string name;
   std::vector<CVC4::Type> args;
   std::vector<uint64_t> numerals;
+  bool indexed;
 }
   : sortName[name,CHECK_NONE]
     {
@@ -1794,65 +2103,77 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
         t = PARSER_STATE->mkUnresolvedType(name);
       }
     }
-  | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
-    {
-      if( name == "BitVec" ) {
-        if( numerals.size() != 1 ) {
-          PARSER_STATE->parseError("Illegal bitvector type.");
-        }
-        if(numerals.front() == 0) {
-          PARSER_STATE->parseError("Illegal bitvector size: 0");
-        }
-        t = EXPR_MANAGER->mkBitVectorType(numerals.front());
-      } else if ( name == "FloatingPoint" ) {
-        if( numerals.size() != 2 ) {
-          PARSER_STATE->parseError("Illegal floating-point type.");
-        }
-        if(!validExponentSize(numerals[0])) {
-          PARSER_STATE->parseError("Illegal floating-point exponent size");
+  | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;})
+    symbol[name,CHECK_NONE,SYM_SORT]
+    ( nonemptyNumeralList[numerals]
+      { // allow sygus inputs to elide the `_'
+        if( !indexed && !PARSER_STATE->sygus() ) {
+          std::stringstream ss;
+          ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name << " ...)";
+          PARSER_STATE->parseError(ss.str());
         }
-        if(!validSignificandSize(numerals[1])) {
-          PARSER_STATE->parseError("Illegal floating-point significand size");
+        if( name == "BitVec" ) {
+          if( numerals.size() != 1 ) {
+            PARSER_STATE->parseError("Illegal bitvector type.");
+          }
+          if(numerals.front() == 0) {
+            PARSER_STATE->parseError("Illegal bitvector size: 0");
+          }
+          t = EXPR_MANAGER->mkBitVectorType(numerals.front());
+        } else if ( name == "FloatingPoint" ) {
+          if( numerals.size() != 2 ) {
+            PARSER_STATE->parseError("Illegal floating-point type.");
+          }
+          if(!validExponentSize(numerals[0])) {
+            PARSER_STATE->parseError("Illegal floating-point exponent size");
+          }
+          if(!validSignificandSize(numerals[1])) {
+            PARSER_STATE->parseError("Illegal floating-point significand size");
+          }
+          t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]);
+        } else {
+          std::stringstream ss;
+          ss << "unknown indexed sort symbol `" << name << "'";
+          PARSER_STATE->parseError(ss.str());
         }
-        t = EXPR_MANAGER->mkFloatingPointType(numerals[0],numerals[1]);
-      } else {
-        std::stringstream ss;
-        ss << "unknown indexed symbol `" << name << "'";
-        PARSER_STATE->parseError(ss.str());
       }
-    }
-  | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
-    {
-      if(args.empty()) {
-        PARSER_STATE->parseError("Extra parentheses around sort name not permitted in SMT-LIB");
-      } else if(name == "Array" &&
-         PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
-        if(args.size() != 2) {
-          PARSER_STATE->parseError("Illegal array type.");
-        }
-        t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
-      } else if(name == "Set" &&
-                PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
-        if(args.size() != 1) {
-          PARSER_STATE->parseError("Illegal set type.");
+    | sortList[args]
+      { if( indexed ) {
+          std::stringstream ss;
+          ss << "Unexpected use of indexing operator `_' before `" << name << "', try leaving it out";
+          PARSER_STATE->parseError(ss.str());
         }
-        t = EXPR_MANAGER->mkSetType( args[0] );
-      } else if(check == CHECK_DECLARED ||
-                PARSER_STATE->isDeclared(name, SYM_SORT)) {
-        t = PARSER_STATE->getSort(name, args);
-      } else {
-        // make unresolved type
         if(args.empty()) {
-          t = PARSER_STATE->mkUnresolvedType(name);
-          Debug("parser-param") << "param: make unres type " << name << std::endl;
+          PARSER_STATE->parseError("Extra parentheses around sort name not permitted in SMT-LIB");
+        } else if(name == "Array" &&
+           PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
+          if(args.size() != 2) {
+            PARSER_STATE->parseError("Illegal array type.");
+          }
+          t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
+        } else if(name == "Set" &&
+                  PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
+          if(args.size() != 1) {
+            PARSER_STATE->parseError("Illegal set type.");
+          }
+          t = EXPR_MANAGER->mkSetType( args[0] );
+        } else if(check == CHECK_DECLARED ||
+                  PARSER_STATE->isDeclared(name, SYM_SORT)) {
+          t = PARSER_STATE->getSort(name, args);
         } else {
-          t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
-          t = SortConstructorType(t).instantiate( args );
-          Debug("parser-param") << "param: make unres param type " << name << " " << args.size() << " "
-                                << PARSER_STATE->getArity( name ) << std::endl;
+          // make unresolved type
+          if(args.empty()) {
+            t = PARSER_STATE->mkUnresolvedType(name);
+            Debug("parser-param") << "param: make unres type " << name << std::endl;
+          } else {
+            t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args);
+            t = SortConstructorType(t).instantiate( args );
+            Debug("parser-param") << "param: make unres param type " << name << " " << args.size() << " "
+                                  << PARSER_STATE->getArity( name ) << std::endl;
+          }
         }
       }
-    }
+    ) RPAREN_TOK
   ;
 
 /**
@@ -1884,10 +2205,16 @@ symbol[std::string& id,
         PARSER_STATE->checkDeclaration(id, check, type);
       }
     }
-  | 'repeat'
-    { id = "repeat";
-      PARSER_STATE->checkDeclaration(id, check, type);
-    }
+  | ( 'repeat' { id = "repeat"; }
+    /* these are keywords in SyGuS but we don't want to inhibit their
+     * use as symbols in SMT-LIB */
+    | SET_OPTIONS_TOK { id = "set-options"; }
+    | DECLARE_VAR_TOK { id = "declare-var"; }
+    | SYNTH_FUN_TOK { id = "synth-fun"; }
+    | CONSTRAINT_TOK { id = "constraint"; }
+    | CHECK_SYNTH_TOK { id = "check-synth"; }
+    )
+    { PARSER_STATE->checkDeclaration(id, check, type); }
   | QUOTED_SYMBOL
     { id = AntlrInput::tokenText($QUOTED_SYMBOL);
       /* strip off the quotes */
@@ -1954,11 +2281,11 @@ constructorDef[CVC4::Datatype& type]
   std::string id;
   CVC4::DatatypeConstructor* ctor = NULL;
 }
-  : symbol[id,CHECK_UNDECLARED,SYM_SORT]
+  : symbol[id,CHECK_UNDECLARED,SYM_VARIABLE]
     { // make the tester
       std::string testerId("is-");
       testerId.append(id);
-      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT);
+      PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE);
       ctor = new CVC4::DatatypeConstructor(id, testerId);
     }
     ( LPAREN_TOK selector[*ctor] RPAREN_TOK )*
@@ -2031,6 +2358,13 @@ DEFINE_CONST_TOK : 'define-const';
 SIMPLIFY_TOK : 'simplify';
 INCLUDE_TOK : 'include';
 
+// SyGuS commands
+SYNTH_FUN_TOK : 'synth-fun';
+CHECK_SYNTH_TOK : 'check-synth';
+DECLARE_VAR_TOK : 'declare-var';
+CONSTRAINT_TOK : 'constraint';
+SET_OPTIONS_TOK : 'set-options';
+
 // attributes
 ATTRIBUTE_PATTERN_TOK : ':pattern';
 ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern';
@@ -2058,7 +2392,7 @@ NOT_TOK           : 'not';
 OR_TOK            : 'or';
 // PERCENT_TOK       : '%';
 PLUS_TOK          : '+';
-POUND_TOK         : '#';
+//POUND_TOK         : '#';
 SELECT_TOK        : 'select';
 STAR_TOK          : '*';
 STORE_TOK         : 'store';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 7740d0b94..27ba07008 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -30,7 +30,8 @@ namespace parser {
 
 Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
   Parser(exprManager,input,strictMode,parseOnly),
-  d_logicSet(false) {
+  d_logicSet(false),
+  d_nextSygusFun(0) {
   d_unsatCoreNames.push(std::map<Expr, std::string>());
   if( !strictModeEnabled() ) {
     addTheory(Smt2::THEORY_CORE);
@@ -116,7 +117,7 @@ void Smt2::addFloatingPointOperators() {
   Parser::addOperator(kind::FLOATINGPOINT_GT);
   Parser::addOperator(kind::FLOATINGPOINT_ISN);
   Parser::addOperator(kind::FLOATINGPOINT_ISSN);
-  Parser::addOperator(kind::FLOATINGPOINT_ISZ);  
+  Parser::addOperator(kind::FLOATINGPOINT_ISZ);
   Parser::addOperator(kind::FLOATINGPOINT_ISINF);
   Parser::addOperator(kind::FLOATINGPOINT_ISNAN);
   Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
@@ -297,7 +298,23 @@ void Smt2::resetAssertions() {
   this->Parser::reset();
 }
 
-void Smt2::setLogic(const std::string& name) {
+void Smt2::setLogic(std::string name) {
+  if(sygus()) {
+    if(name == "Arrays") {
+      name = "AUF";
+    } else if(name == "Reals") {
+      name = "UFLRA";
+    } else if(name == "LIA") {
+      name = "UFLIA";
+    } else if(name == "BV") {
+      name = "UFBV";
+    } else {
+      std::stringstream ss;
+      ss << "Unknown SyGuS background logic `" << name << "'";
+      parseError(ss.str());
+    }
+  }
+
   d_logicSet = true;
   if(logicIsForced()) {
     d_logic = getForcedLogic();
@@ -364,15 +381,19 @@ void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
 
 void Smt2::checkThatLogicIsSet() {
   if( ! logicIsSet() ) {
-    if( strictModeEnabled() ) {
+    if(strictModeEnabled()) {
       parseError("set-logic must appear before this point.");
     } else {
-      warning("No set-logic command was given before this point.");
-      warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
-      warning("Consider setting a stricter logic for (likely) better performance.");
-      warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
+      if(sygus()) {
+        setLogic("LIA");
+      } else {
+        warning("No set-logic command was given before this point.");
+        warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
+        warning("Consider setting a stricter logic for (likely) better performance.");
+        warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
 
-      setLogic("ALL_SUPPORTED");
+        setLogic("ALL_SUPPORTED");
+      }
 
       Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
       c->setMuted(true);
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.
diff --git a/src/parser/smt2/sygus_input.cpp b/src/parser/smt2/sygus_input.cpp
new file mode 100644
index 000000000..8bd02485b
--- /dev/null
+++ b/src/parser/smt2/sygus_input.cpp
@@ -0,0 +1,70 @@
+/*********************                                                        */
+/*! \file sygus_input.cpp
+ ** \verbatim
+ ** Original author: Christopher L. Conway
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
+#include <antlr3.h>
+
+#include "parser/smt2/sygus_input.h"
+#include "expr/expr_manager.h"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "parser/parser_exception.h"
+#include "parser/smt2/sygus_input.h"
+#include "parser/smt2/generated/Smt2Lexer.h"
+#include "parser/smt2/generated/Smt2Parser.h"
+
+namespace CVC4 {
+namespace parser {
+
+/* Use lookahead=2 */
+SygusInput::SygusInput(AntlrInputStream& inputStream) :
+  AntlrInput(inputStream, 2) {
+
+  pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
+  assert( input != NULL );
+
+  d_pSmt2Lexer = Smt2LexerNew(input);
+  if( d_pSmt2Lexer == NULL ) {
+    throw ParserException("Failed to create SMT2 lexer.");
+  }
+
+  setAntlr3Lexer( d_pSmt2Lexer->pLexer );
+
+  pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream();
+  assert( tokenStream != NULL );
+
+  d_pSmt2Parser = Smt2ParserNew(tokenStream);
+  if( d_pSmt2Parser == NULL ) {
+    throw ParserException("Failed to create SMT2 parser.");
+  }
+
+  setAntlr3Parser(d_pSmt2Parser->pParser);
+}
+
+SygusInput::~SygusInput() {
+  d_pSmt2Lexer->free(d_pSmt2Lexer);
+  d_pSmt2Parser->free(d_pSmt2Parser);
+}
+
+Command* SygusInput::parseCommand() {
+  return d_pSmt2Parser->parseSygus(d_pSmt2Parser);
+}
+
+Expr SygusInput::parseExpr() {
+  return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/smt2/sygus_input.h b/src/parser/smt2/sygus_input.h
new file mode 100644
index 000000000..d5e6b8b87
--- /dev/null
+++ b/src/parser/smt2/sygus_input.h
@@ -0,0 +1,96 @@
+/*********************                                                        */
+/*! \file sygus_input.h
+ ** \verbatim
+ ** Original author: Christopher L. Conway
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
+#include "cvc4parser_private.h"
+
+#ifndef __CVC4__PARSER__SYGUS_INPUT_H
+#define __CVC4__PARSER__SYGUS_INPUT_H
+
+#include "parser/antlr_input.h"
+#include "parser/smt2/generated/Smt2Lexer.h"
+#include "parser/smt2/generated/Smt2Parser.h"
+
+// extern void Smt2ParserSetAntlrParser(CVC4::parser::AntlrParser* newAntlrParser);
+
+namespace CVC4 {
+
+class Command;
+class Expr;
+class ExprManager;
+
+namespace parser {
+
+class Smt2;
+
+class SygusInput : public AntlrInput {
+  typedef AntlrInput super;
+
+  /** The ANTLR3 SMT2 lexer for the input. */
+  pSmt2Lexer d_pSmt2Lexer;
+
+  /** The ANTLR3 SMT2 parser for the input. */
+  pSmt2Parser d_pSmt2Parser;
+
+  /** Which (variant of the) input language we're using */
+  InputLanguage d_lang;
+
+  /**
+   * Initialize the class. Called from the constructors once the input
+   * stream is initialized.
+   */
+  void init();
+
+public:
+
+  /**
+   * Create an input.
+   *
+   * @param inputStream the input stream to use
+   */
+  SygusInput(AntlrInputStream& inputStream);
+
+  /** Destructor. Frees the lexer and the parser. */
+  virtual ~SygusInput();
+
+  /** Get the language that this Input is reading. */
+  InputLanguage getLanguage() const throw() {
+    return language::input::LANG_SYGUS;
+  }
+
+protected:
+
+  /**
+   * Parse a command from the input. Returns <code>NULL</code> if
+   * there is no command there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
+  Command* parseCommand();
+
+  /**
+   * Parse an expression from the input. Returns a null
+   * <code>Expr</code> if there is no expression there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
+  Expr parseExpr();
+
+};/* class SygusInput */
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__SYGUS_INPUT_H */
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 8c43453d7..e04e76835 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -192,8 +192,8 @@ option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0
 option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
  more aggressive merging for universal equality engine, introduces terms
  
-option ceGuidedInst --cegqi bool :default false
-  counterexample guided quantifier instantiation
+option ceGuidedInst --cegqi bool :default false :read-write
+  counterexample-guided quantifier instantiation
 option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h"
   if and how to apply fairness for cegqi
  
diff --git a/src/util/language.cpp b/src/util/language.cpp
index ca611f729..4b213422c 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -113,6 +113,8 @@ InputLanguage toInputLanguage(std::string language) {
   } else if(language == "smtlib2.5" || language == "smt2.5" ||
             language == "LANG_SMTLIB_V2_5") {
     return input::LANG_SMTLIB_V2_5;
+  } else if(language == "sygus" || language == "LANG_SYGUS") {
+    return input::LANG_SYGUS;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
diff --git a/src/util/language.h b/src/util/language.h
index abde0b509..c865c2615 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -60,6 +60,8 @@ enum CVC4_PUBLIC Language {
 
   // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
+  /** The SyGuS input language */
+  LANG_SYGUS,
 
   /** LANG_MAX is > any valid InputLanguage id */
   LANG_MAX
@@ -89,6 +91,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_Z3STR:
     out << "LANG_Z3STR";
     break;
+  case LANG_SYGUS:
+    out << "LANG_SYGUS";
+    break;
   default:
     out << "undefined_input_language";
   }