Clean up more uses of ExprManager in parsers (#3932)

Towards parser migration.

Beyond Datatypes, there are still a handful of calls to the ExprManager in the parsers.
This eliminates a few missing cases from TPTP and also inlines the access of ExprManager in the places its used.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 64eb56c74db67a8727a22478f8940bcbb1307445..abfd363f822ec48042d3935ab24d182c3296413c 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2331,7 +2331,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
       )* RBRACKET
     )?
     {
-      datatypes.push_back(Datatype(PARSER_STATE->getExprManager(),
+      datatypes.push_back(Datatype(SOLVER->getExprManager(),
                                    id,
                                    api::sortVectorToTypes(params),
                                    false));

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 87fa93dcc4758c72daf9caeaa9107a867233284f..e9a037d6e30e1c329c6865cdc4e6f24984a202ba 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -76,11 +76,6 @@ Parser::~Parser() {
   delete d_input;
 }
 
-ExprManager* Parser::getExprManager() const
-{
-  return d_solver->getExprManager();
-}
-
 api::Solver* Parser::getSolver() const { return d_solver; }
 
 api::Term Parser::getSymbol(const std::string& name, SymbolType type)
@@ -339,7 +334,7 @@ void Parser::defineParameterizedType(const std::string& name,
 api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
 {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
-  api::Sort type = getExprManager()->mkSort(name, flags);
+  api::Sort type = d_solver->getExprManager()->mkSort(name, flags);
   defineType(
       name,
       type,
@@ -353,7 +348,8 @@ api::Sort Parser::mkSortConstructor(const std::string& name,
 {
   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
-  api::Sort type = getExprManager()->mkSortConstructor(name, arity, flags);
+  api::Sort type =
+      d_solver->getExprManager()->mkSortConstructor(name, arity, flags);
   defineType(
       name,
       vector<api::Sort>(arity),
@@ -383,7 +379,7 @@ api::Sort Parser::mkUnresolvedTypeConstructor(
 {
   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
                   << ")" << std::endl;
-  api::Sort unresolved = getExprManager()->mkSortConstructor(
+  api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor(
       name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
   defineType(name, params, unresolved);
   api::Sort t = getSort(name, params);
@@ -404,7 +400,8 @@ std::vector<api::Sort> Parser::mkMutualDatatypeTypes(
   try {
     std::set<Type> tset = api::sortSetToTypes(d_unresolved);
     std::vector<DatatypeType> dtypes =
-        getExprManager()->mkMutualDatatypeTypes(datatypes, tset, flags);
+        d_solver->getExprManager()->mkMutualDatatypeTypes(
+            datatypes, tset, flags);
     std::vector<api::Sort> types;
     for (unsigned i = 0, dtsize = dtypes.size(); i < dtsize; i++)
     {
@@ -593,7 +590,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
     // parametric datatype.
     if (s.isParametricDatatype())
     {
-      ExprManager* em = getExprManager();
+      ExprManager* em = d_solver->getExprManager();
       // apply type ascription to the operator
       Expr e = t.getExpr();
       const DatatypeConstructor& dtc =
@@ -633,7 +630,8 @@ api::Term Parser::mkVar(const std::string& name,
                         const api::Sort& type,
                         uint32_t flags)
 {
-  return api::Term(getExprManager()->mkVar(name, type.getType(), flags));
+  return api::Term(
+      d_solver->getExprManager()->mkVar(name, type.getType(), flags));
 }
 //!!!!!!!!!!! temporary
 

diff --git a/src/parser/parser.h b/src/parser/parser.h
index c7efcbacb94b46544a2e486b1c8e922fdcb5e5d5..1197c1ff6004377646c6ec6820a13610346a8003 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -265,9 +265,6 @@ public:
 
   virtual ~Parser();
 
-  /** Get the associated <code>ExprManager</code>. */
-  ExprManager* getExprManager() const;
-
   /** Get the associated solver. */
   api::Solver* getSolver() const;
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index aa62eab5db6608e1b45c14ffb4f04e08fe80036e..d87c44a683fc04a741cbac40d3973e191bd93e69 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -959,7 +959,7 @@ sygusGrammar[CVC4::api::Sort & ret,
       Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
       // make the datatype, which encodes terms generated by this non-terminal
       std::string dname = i.first;
-      datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), dname));
+      datatypes.push_back(Datatype(SOLVER->getExprManager(), dname));
       // make its unresolved type, used for referencing the final version of
       // the datatype
       PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
@@ -1537,7 +1537,7 @@ datatypesDef[bool isCo,
           PARSER_STATE->parseError("Wrong number of parameters for datatype.");
         }
         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
-        dts.push_back(Datatype(PARSER_STATE->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo));
+        dts.push_back(Datatype(SOLVER->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo));
       }
       LPAREN_TOK
       ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
@@ -1547,7 +1547,7 @@ datatypesDef[bool isCo,
           PARSER_STATE->parseError("No parameters given for datatype.");
         }
         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
-        dts.push_back(Datatype(PARSER_STATE->getExprManager(),
+        dts.push_back(Datatype(SOLVER->getExprManager(),
                                dnames[dts.size()],
                                api::sortVectorToTypes(params),
                                isCo));
@@ -2532,7 +2532,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
      * below. */
   : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
     {
-      datatypes.push_back(Datatype(PARSER_STATE->getExprManager(),
+      datatypes.push_back(Datatype(SOLVER->getExprManager(),
                                    id,
                                    api::sortVectorToTypes(params),
                                    isCo));

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2df73d9e48769b6f8dd536f582f605aef25ae60a..c0484e52b0a2b41cade002d828ae81cae2444fa9 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1112,7 +1112,7 @@ bool Smt2::pushSygusDatatypeDef(
     std::vector<std::vector<std::string>>& unresolved_gterm_sym)
 {
   sorts.push_back(t);
-  datatypes.push_back(Datatype(getExprManager(), dname));
+  datatypes.push_back(Datatype(d_solver->getExprManager(), dname));
   ops.push_back(std::vector<ParseOp>());
   cnames.push_back(std::vector<std::string>());
   cargs.push_back(std::vector<std::vector<api::Sort>>());
@@ -1573,7 +1573,7 @@ void Smt2::addSygusConstructorVariables(Datatype& dt,
 
 InputLanguage Smt2::getLanguage() const
 {
-  return getExprManager()->getOptions().getInputLanguage();
+  return d_solver->getExprManager()->getOptions().getInputLanguage();
 }
 
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
@@ -1746,7 +1746,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     }
   }
   // Second phase: apply the arguments to the parse op
-  ExprManager* em = getExprManager();
+  const Options& opts = d_solver->getExprManager()->getOptions();
   // handle special cases
   if (p.d_kind == api::STORE_ALL && !p.d_type.isNull())
   {
@@ -1842,8 +1842,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   else if (isBuiltinOperator)
   {
     Trace("ajr-temp") << "mkTerm builtin operator" << std::endl;
-    if (!em->getOptions().getUfHo()
-        && (kind == api::EQUAL || kind == api::DISTINCT))
+    if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
     {
       // need --uf-ho if these operators are applied over function args
       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
@@ -1884,7 +1883,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       unsigned arity = argt.getFunctionArity();
       if (args.size() - 1 < arity)
       {
-        if (!em->getOptions().getUfHo())
+        if (!opts.getUfHo())
         {
           parseError("Cannot partially apply functions unless --uf-ho is set.");
         }

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index a21cc678509d8d4773863785b236ae2f3b37628a..51b852eac2feef320e652f09a705a8d336d8a70e 100644 (file)
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -69,20 +69,19 @@ Tptp::~Tptp() {
 }
 
 void Tptp::addTheory(Theory theory) {
-  ExprManager * em = getExprManager();
   switch(theory) {
   case THEORY_CORE:
     //TPTP (CNF and FOF) is unsorted so we define this common type
     {
       std::string d_unsorted_name = "$$unsorted";
-      d_unsorted = api::Sort(em->mkSort(d_unsorted_name));
+      d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name);
       preemptCommand(
           new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted.getType()));
     }
     // propositionnal
-    defineType("Bool", em->booleanType());
-    defineVar("$true", em->mkConst(true));
-    defineVar("$false", em->mkConst(false));
+    defineType("Bool", d_solver->getBooleanSort());
+    defineVar("$true", d_solver->mkTrue());
+    defineVar("$false", d_solver->mkFalse());
     addOperator(api::AND);
     addOperator(api::EQUAL);
     addOperator(api::IMPLIES);
@@ -312,12 +311,11 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     isBuiltinKind = true;
   }
   assert(kind != api::NULL_EXPR);
-  ExprManager* em = getExprManager();
+  const Options& opts = d_solver->getExprManager()->getOptions();
   // Second phase: apply parse op to the arguments
   if (isBuiltinKind)
   {
-    if (!em->getOptions().getUfHo()
-        && (kind == api::EQUAL || kind == api::DISTINCT))
+    if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
     {
       // need --uf-ho if these operators are applied over function args
       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
@@ -352,7 +350,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       unsigned arity = argt.getFunctionArity();
       if (args.size() - 1 < arity)
       {
-        if (!em->getOptions().getUfHo())
+        if (!opts.getUfHo())
         {
           parseError("Cannot partially apply functions unless --uf-ho is set.");
         }