Modify the smt2 parser to use the Sygus grammar. (#4829)

1 files changed, 79 insertions, 61 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2e36190b4..97a51277b 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -90,7 +90,6 @@ ostream& operator<<(ostream& out, const CommandStatus* s)
   return out;
 }
 
-
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
 {
@@ -137,7 +136,7 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
 
 Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
 
-Command::Command(api::Solver* solver)
+Command::Command(const api::Solver* solver)
     : d_solver(solver), d_commandStatus(nullptr), d_muted(false)
 {
 }
@@ -652,40 +651,49 @@ std::string DeclareSygusFunctionCommand::getCommandName() const
 }
 
 /* -------------------------------------------------------------------------- */
-/* class SynthFunCommand                                                    */
+/* class SynthFunCommand                                                      */
 /* -------------------------------------------------------------------------- */
 
-SynthFunCommand::SynthFunCommand(const std::string& id,
-                                 Expr func,
-                                 Type sygusType,
+SynthFunCommand::SynthFunCommand(const api::Solver* solver,
+                                 const std::string& id,
+                                 api::Term fun,
+                                 const std::vector<api::Term>& vars,
+                                 api::Sort sort,
                                  bool isInv,
-                                 const std::vector<Expr>& vars)
+                                 api::Grammar* g)
     : DeclarationDefinitionCommand(id),
-      d_func(func),
-      d_sygusType(sygusType),
+      d_fun(fun),
+      d_vars(vars),
+      d_sort(sort),
       d_isInv(isInv),
-      d_vars(vars)
+      d_grammar(g)
 {
+  d_solver = solver;
 }
 
-SynthFunCommand::SynthFunCommand(const std::string& id,
-                                 Expr func,
-                                 Type sygusType,
-                                 bool isInv)
-    : SynthFunCommand(id, func, sygusType, isInv, {})
+api::Term SynthFunCommand::getFunction() const { return d_fun; }
+
+const std::vector<api::Term>& SynthFunCommand::getVars() const
 {
+  return d_vars;
 }
 
-Expr SynthFunCommand::getFunction() const { return d_func; }
-const std::vector<Expr>& SynthFunCommand::getVars() const { return d_vars; }
-Type SynthFunCommand::getSygusType() const { return d_sygusType; }
+api::Sort SynthFunCommand::getSort() const { return d_sort; }
 bool SynthFunCommand::isInv() const { return d_isInv; }
 
+const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
+
 void SynthFunCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    smtEngine->declareSynthFun(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+    smtEngine->declareSynthFun(d_symbol,
+                               d_fun.getExpr(),
+                               d_grammar == nullptr
+                                   ? d_sort.getType()
+                                   : d_grammar->resolve().getType(),
+                               d_isInv,
+                               api::termVectorToExprs(d_vars));
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -697,15 +705,13 @@ void SynthFunCommand::invoke(SmtEngine* smtEngine)
 Command* SynthFunCommand::exportTo(ExprManager* exprManager,
                                    ExprManagerMapCollection& variableMap)
 {
-  return new SynthFunCommand(d_symbol,
-                             d_func.exportTo(exprManager, variableMap),
-                             d_sygusType.exportTo(exprManager, variableMap),
-                             d_isInv);
+  Unimplemented();
 }
 
 Command* SynthFunCommand::clone() const
 {
-  return new SynthFunCommand(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+  return new SynthFunCommand(
+      d_solver, d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
 }
 
 std::string SynthFunCommand::getCommandName() const
@@ -1352,7 +1358,7 @@ Command* DefineNamedFunctionCommand::clone() const
 /* -------------------------------------------------------------------------- */
 
 DefineFunctionRecCommand::DefineFunctionRecCommand(
-    api::Solver* solver,
+    const api::Solver* solver,
     api::Term func,
     const std::vector<api::Term>& formals,
     api::Term formula,
@@ -1365,7 +1371,7 @@ DefineFunctionRecCommand::DefineFunctionRecCommand(
 }
 
 DefineFunctionRecCommand::DefineFunctionRecCommand(
-    api::Solver* solver,
+    const api::Solver* solver,
     const std::vector<api::Term>& funcs,
     const std::vector<std::vector<api::Term>>& formals,
     const std::vector<api::Term>& formulas,
@@ -2094,40 +2100,49 @@ std::string GetSynthSolutionCommand::getCommandName() const
   return "get-instantiations";
 }
 
-GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+/* -------------------------------------------------------------------------- */
+/* class GetInterpolCommand                                                   */
+/* -------------------------------------------------------------------------- */
+
+GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
                                        const std::string& name,
                                        api::Term conj)
     : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
 {
 }
-GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
                                        const std::string& name,
                                        api::Term conj,
-                                       const Type& gtype)
+                                       api::Grammar* g)
     : Command(solver),
       d_name(name),
       d_conj(conj),
-      d_sygus_grammar_type(gtype),
+      d_sygus_grammar(g),
       d_resultStatus(false)
 {
 }
 
 api::Term GetInterpolCommand::getConjecture() const { return d_conj; }
-Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; }
+
+const api::Grammar* GetInterpolCommand::getGrammar() const
+{
+  return d_sygus_grammar;
+}
+
 api::Term GetInterpolCommand::getResult() const { return d_result; }
 
 void GetInterpolCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    if (d_sygus_grammar_type.isNull())
+    if (!d_sygus_grammar)
     {
       d_resultStatus = d_solver->getInterpolant(d_conj, d_result);
     }
     else
     {
       d_resultStatus =
-          d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result);
+          d_solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
     }
     d_commandStatus = CommandSuccess::instance();
   }
@@ -2167,7 +2182,8 @@ Command* GetInterpolCommand::exportTo(ExprManager* exprManager,
 
 Command* GetInterpolCommand::clone() const
 {
-  GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj);
+  GetInterpolCommand* c =
+      new GetInterpolCommand(d_solver, d_name, d_conj, d_sygus_grammar);
   c->d_result = d_result;
   c->d_resultStatus = d_resultStatus;
   return c;
@@ -2178,42 +2194,50 @@ std::string GetInterpolCommand::getCommandName() const
   return "get-interpol";
 }
 
-GetAbductCommand::GetAbductCommand() {}
-GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
-    : d_name(name), d_conj(conj), d_resultStatus(false)
+/* -------------------------------------------------------------------------- */
+/* class GetAbductCommand                                                     */
+/* -------------------------------------------------------------------------- */
+
+GetAbductCommand::GetAbductCommand(const api::Solver* solver,
+                                   const std::string& name,
+                                   api::Term conj)
+    : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
 {
 }
-GetAbductCommand::GetAbductCommand(const std::string& name,
-                                   Expr conj,
-                                   const Type& gtype)
-    : d_name(name),
+GetAbductCommand::GetAbductCommand(const api::Solver* solver,
+                                   const std::string& name,
+                                   api::Term conj,
+                                   api::Grammar* g)
+    : Command(solver),
+      d_name(name),
       d_conj(conj),
-      d_sygus_grammar_type(gtype),
+      d_sygus_grammar(g),
       d_resultStatus(false)
 {
 }
 
-Expr GetAbductCommand::getConjecture() const { return d_conj; }
-Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; }
+api::Term GetAbductCommand::getConjecture() const { return d_conj; }
+
+const api::Grammar* GetAbductCommand::getGrammar() const
+{
+  return d_sygus_grammar;
+}
+
 std::string GetAbductCommand::getAbductName() const { return d_name; }
-Expr GetAbductCommand::getResult() const { return d_result; }
+api::Term GetAbductCommand::getResult() const { return d_result; }
 
 void GetAbductCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    Node conjNode = Node::fromExpr(d_conj);
-    Node resn;
-    if (d_sygus_grammar_type.isNull())
+    if (!d_sygus_grammar)
     {
-      d_resultStatus = smtEngine->getAbduct(conjNode, resn);
+      d_resultStatus = d_solver->getAbduct(d_conj, d_result);
     }
     else
     {
-      TypeNode gtype = TypeNode::fromType(d_sygus_grammar_type);
-      d_resultStatus = smtEngine->getAbduct(conjNode, gtype, resn);
+      d_resultStatus = d_solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
     }
-    d_result = resn.toExpr();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -2246,19 +2270,13 @@ void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
 Command* GetAbductCommand::exportTo(ExprManager* exprManager,
                                     ExprManagerMapCollection& variableMap)
 {
-  GetAbductCommand* c =
-      new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap));
-  c->d_sygus_grammar_type =
-      d_sygus_grammar_type.exportTo(exprManager, variableMap);
-  c->d_result = d_result.exportTo(exprManager, variableMap);
-  c->d_resultStatus = d_resultStatus;
-  return c;
+  Unimplemented();
 }
 
 Command* GetAbductCommand::clone() const
 {
-  GetAbductCommand* c = new GetAbductCommand(d_name, d_conj);
-  c->d_sygus_grammar_type = d_sygus_grammar_type;
+  GetAbductCommand* c =
+      new GetAbductCommand(d_solver, d_name, d_conj, d_sygus_grammar);
   c->d_result = d_result;
   c->d_resultStatus = d_resultStatus;
   return c;