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.

1 files changed, 7 insertions, 9 deletions

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index a21cc6785..51b852eac 100644
--- 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.");
         }