Fixing Cid 1172009 (#1141)

3 files changed, 167 insertions, 154 deletions

diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index fbd3d8cfb..8163eb239 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -158,7 +158,9 @@ parseCommand returns [CVC4::Command* cmd = NULL]
 }
 //  : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
   : CNF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
-  { PARSER_STATE->cnf = true; PARSER_STATE->fof = false; PARSER_STATE->pushScope(); }
+  { PARSER_STATE->setCnf(true);
+    PARSER_STATE->setFof(false);
+    PARSER_STATE->pushScope(); }
     cnfFormula[expr]
   { PARSER_STATE->popScope();
     std::vector<Expr> bvl = PARSER_STATE->getFreeVar();
@@ -171,7 +173,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ true);
     }
   | FOF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
-    { PARSER_STATE->cnf = false; PARSER_STATE->fof = true; }
+    { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(true); }
     fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
     {
       cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false);
@@ -179,7 +181,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
   | TFF_TOK LPAREN_TOK nameN[name] COMMA_TOK
     ( TYPE_TOK COMMA_TOK tffTypedAtom[cmd]
     | formulaRole[fr] COMMA_TOK
-      { PARSER_STATE->cnf = false; PARSER_STATE->fof = false; }
+      { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); }
       tffFormula[expr] (COMMA_TOK anything*)?
       {
         cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false);
@@ -506,11 +508,11 @@ variable[CVC4::Expr& expr]
   : UPPER_WORD
     {
       std::string name = AntlrInput::tokenText($UPPER_WORD);
-      if(!PARSER_STATE->cnf || PARSER_STATE->isDeclared(name)) {
+      if(!PARSER_STATE->cnf() || PARSER_STATE->isDeclared(name)) {
         expr = PARSER_STATE->getVariable(name);
       } else {
         expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
-        if(PARSER_STATE->cnf) PARSER_STATE->addFreeVar(expr);
+        if(PARSER_STATE->cnf()) PARSER_STATE->addFreeVar(expr);
       }
     }
     ;
@@ -1023,7 +1025,7 @@ NUMBER
         PARSER_STATE->d_tmp_expr = MK_CONST(Rational(pos ? inum : -inum, iden));
       }
     )
-    { if(PARSER_STATE->cnf || PARSER_STATE->fof) {
+    { if(PARSER_STATE->cnf() || PARSER_STATE->fof()) {
         // We're in an unsorted context, so put a conversion around it
         PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr );
       }
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 719f2f38e..a01de9df4 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -231,5 +231,118 @@ void Tptp::checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool f
   }
 }
 
+void Tptp::addFreeVar(Expr var) {
+  assert(cnf());
+  d_freeVar.push_back(var);
+}
+
+std::vector<Expr> Tptp::getFreeVar() {
+  assert(cnf());
+  std::vector<Expr> r;
+  r.swap(d_freeVar);
+  return r;
+}
+
+Expr Tptp::convertRatToUnsorted(Expr expr) {
+  ExprManager* em = getExprManager();
+
+  // Create the conversion function If they doesn't exists
+  if (d_rtu_op.isNull()) {
+    Type t;
+    // Conversion from rational to unsorted
+    t = em->mkFunctionType(em->realType(), d_unsorted);
+    d_rtu_op = em->mkVar("$$rtu", t);
+    preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
+    // Conversion from unsorted to rational
+    t = em->mkFunctionType(d_unsorted, em->realType());
+    d_utr_op = em->mkVar("$$utr", t);
+    preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
+  }
+  // Add the inverse in order to show that over the elements that
+  // appear in the problem there is a bijection between unsorted and
+  // rational
+  Expr ret = em->mkExpr(kind::APPLY_UF, d_rtu_op, expr);
+  if (d_r_converted.find(expr) == d_r_converted.end()) {
+    d_r_converted.insert(expr);
+    Expr eq = em->mkExpr(kind::EQUAL, expr,
+                         em->mkExpr(kind::APPLY_UF, d_utr_op, ret));
+    preemptCommand(new AssertCommand(eq));
+  }
+  return ret;
+}
+
+Expr Tptp::convertStrToUnsorted(std::string str) {
+  Expr& e = d_distinct_objects[str];
+  if (e.isNull()) {
+    e = getExprManager()->mkConst(
+        UninterpretedConstant(d_unsorted, d_distinct_objects.size() - 1));
+  }
+  return e;
+}
+
+void Tptp::makeApplication(Expr& expr, std::string& name,
+                           std::vector<Expr>& args, bool term) {
+  if (args.empty()) {        // Its a constant
+    if (isDeclared(name)) {  // already appeared
+      expr = getVariable(name);
+    } else {
+      Type t = term ? d_unsorted : getExprManager()->booleanType();
+      expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL);  // levelZero
+      preemptCommand(new DeclareFunctionCommand(name, expr, t));
+    }
+  } else {                   // Its an application
+    if (isDeclared(name)) {  // already appeared
+      expr = getVariable(name);
+    } else {
+      std::vector<Type> sorts(args.size(), d_unsorted);
+      Type t = term ? d_unsorted : getExprManager()->booleanType();
+      t = getExprManager()->mkFunctionType(sorts, t);
+      expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL);  // levelZero
+      preemptCommand(new DeclareFunctionCommand(name, expr, t));
+    }
+    // args might be rationals, in which case we need to create
+    // distinct constants of the "unsorted" sort to represent them
+    for (size_t i = 0; i < args.size(); ++i) {
+      if (args[i].getType().isReal() &&
+          FunctionType(expr.getType()).getArgTypes()[i] == d_unsorted) {
+        args[i] = convertRatToUnsorted(args[i]);
+      }
+    }
+    expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args);
+  }
+}
+
+Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) {
+  // For SZS ontology compliance.
+  // if we're in cnf() though, conjectures don't result in "Theorem" or
+  // "CounterSatisfiable".
+  if (!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
+    d_hasConjecture = true;
+  }
+  switch (fr) {
+    case FR_AXIOM:
+    case FR_HYPOTHESIS:
+    case FR_DEFINITION:
+    case FR_ASSUMPTION:
+    case FR_LEMMA:
+    case FR_THEOREM:
+    case FR_NEGATED_CONJECTURE:
+    case FR_PLAIN:
+      // it's a usual assert
+      return new AssertCommand(expr);
+    case FR_CONJECTURE:
+      // something to prove
+      return new AssertCommand(getExprManager()->mkExpr(kind::NOT, expr));
+    case FR_UNKNOWN:
+    case FR_FI_DOMAIN:
+    case FR_FI_FUNCTORS:
+    case FR_FI_PREDICATES:
+    case FR_TYPE:
+      return new EmptyCommand("Untreated role");
+  }
+  assert(false);  // unreachable
+  return nullptr;
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 3afd29415..e6d7bbb47 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -30,90 +30,23 @@
 #include "util/hash.h"
 
 namespace CVC4 {
-
-class SExpr;
-
 namespace parser {
 
 class Tptp : public Parser {
+ private:
   friend class ParserBuilder;
+ public:
+  bool cnf() const { return d_cnf; }
+  void setCnf(bool cnf) { d_cnf = cnf; }
 
-  // In CNF variable are implicitly binded
-  // d_freevar collect them
-  std::vector< Expr > d_freeVar;
-  Expr d_rtu_op;
-  Expr d_stu_op;
-  Expr d_utr_op;
-  Expr d_uts_op;
-  // The set of expression that already have a bridge
-  std::unordered_set<Expr, ExprHashFunction> d_r_converted;
-  std::unordered_map<std::string, Expr> d_distinct_objects;
-  
-  std::vector< pANTLR3_INPUT_STREAM > d_in_created;
-
-  // TPTP directory where to find includes;
-  // empty if none could be determined
-  std::string d_tptpDir;
-
-  // hack to make output SZS ontology-compliant
-  bool d_hasConjecture;
+  bool fof() const { return d_fof; }
+  void setFof(bool fof) { d_fof = fof; }
 
-  static void myPopCharStream(pANTLR3_LEXER lexer);
-  void (*d_oldPopCharStream)(pANTLR3_LEXER);
+  void addFreeVar(Expr var);
+  std::vector< Expr > getFreeVar();
 
-public:
-
-  bool cnf; // in a cnf formula
-  bool fof; // in an fof formula
-
-  void addFreeVar(Expr var) {
-    assert(cnf);
-    d_freeVar.push_back(var);
-  }
-  std::vector< Expr > getFreeVar() {
-    assert(cnf);
-    std::vector< Expr > r;
-    r.swap(d_freeVar);
-    return r;
-  }
-
-  inline Expr convertRatToUnsorted(Expr expr) {
-    ExprManager * em = getExprManager();
-
-    // Create the conversion function If they doesn't exists
-    if(d_rtu_op.isNull()) {
-      Type t;
-      // Conversion from rational to unsorted
-      t = em->mkFunctionType(em->realType(), d_unsorted);
-      d_rtu_op = em->mkVar("$$rtu",t);
-      preemptCommand(new DeclareFunctionCommand("$$rtu", d_rtu_op, t));
-      // Conversion from unsorted to rational
-      t = em->mkFunctionType(d_unsorted, em->realType());
-      d_utr_op = em->mkVar("$$utr",t);
-      preemptCommand(new DeclareFunctionCommand("$$utr", d_utr_op, t));
-    }
-    // Add the inverse in order to show that over the elements that
-    // appear in the problem there is a bijection between unsorted and
-    // rational
-    Expr ret = em->mkExpr(kind::APPLY_UF,d_rtu_op,expr);
-    if(d_r_converted.find(expr) == d_r_converted.end()) {
-      d_r_converted.insert(expr);
-      Expr eq = em->mkExpr(kind::EQUAL, expr,
-                           em->mkExpr(kind::APPLY_UF, d_utr_op, ret));
-      preemptCommand(new AssertCommand(eq));
-    }
-    return ret;
-  }
-
-  inline Expr convertStrToUnsorted(std::string str) {
-    Expr& e = d_distinct_objects[str];
-    if(e.isNull()) {
-      e = getExprManager()->mkConst(UninterpretedConstant(d_unsorted, d_distinct_objects.size() - 1));
-    }
-    return e;
-  }
-
-public:
+  Expr convertRatToUnsorted(Expr expr);
+  Expr convertStrToUnsorted(std::string str);
 
   // CNF and FOF are unsorted so we define this common type.
   // This is also the Type of $i in TFF.
@@ -142,10 +75,11 @@ public:
 
   bool hasConjecture() const { return d_hasConjecture; }
 
-protected:
-  Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
+ protected:
+  Tptp(ExprManager* exprManager, Input* input, bool strictMode = false,
+       bool parseOnly = false);
 
-public:
+ public:
   ~Tptp();
   /**
    * Add theory symbols to the parser state.
@@ -154,10 +88,10 @@ public:
    */
   void addTheory(Theory theory);
 
-  inline void makeApplication(Expr& expr, std::string& name,
-                              std::vector<Expr>& args, bool term);
+  void makeApplication(Expr& expr, std::string& name, std::vector<Expr>& args,
+                       bool term);
 
-  inline Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf);
+  Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf);
 
   /** Ugly hack because I don't know how to return an expression from a
       token */
@@ -168,75 +102,39 @@ public:
   void includeFile(std::string fileName);
 
   /** Check a TPTP let binding for well-formedness. */
-  void checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula);
-
-private:
+  void checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs,
+                       bool formula);
 
+ private:
   void addArithmeticOperators();
+
+  // In CNF variable are implicitly binded
+  // d_freevar collect them
+  std::vector< Expr > d_freeVar;
+  Expr d_rtu_op;
+  Expr d_stu_op;
+  Expr d_utr_op;
+  Expr d_uts_op;
+  // The set of expression that already have a bridge
+  std::unordered_set<Expr, ExprHashFunction> d_r_converted;
+  std::unordered_map<std::string, Expr> d_distinct_objects;
+
+  std::vector< pANTLR3_INPUT_STREAM > d_in_created;
+
+  // TPTP directory where to find includes;
+  // empty if none could be determined
+  std::string d_tptpDir;
+
+  // hack to make output SZS ontology-compliant
+  bool d_hasConjecture;
+
+  bool d_cnf; // in a cnf formula
+  bool d_fof; // in an fof formula
+
+  static void myPopCharStream(pANTLR3_LEXER lexer);
+  void (*d_oldPopCharStream)(pANTLR3_LEXER);
 };/* class Tptp */
 
-inline void Tptp::makeApplication(Expr& expr, std::string& name,
-                                  std::vector<Expr>& args, bool term) {
-  if(args.empty()) { // Its a constant
-    if(isDeclared(name)) { // already appeared
-      expr = getVariable(name);
-    } else {
-      Type t = term ? d_unsorted : getExprManager()->booleanType();
-      expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
-      preemptCommand(new DeclareFunctionCommand(name, expr, t));
-    }
-  } else { // Its an application
-    if(isDeclared(name)) { // already appeared
-      expr = getVariable(name);
-    } else {
-      std::vector<Type> sorts(args.size(), d_unsorted);
-      Type t = term ? d_unsorted : getExprManager()->booleanType();
-      t = getExprManager()->mkFunctionType(sorts, t);
-      expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
-      preemptCommand(new DeclareFunctionCommand(name, expr, t));
-    }
-    // args might be rationals, in which case we need to create
-    // distinct constants of the "unsorted" sort to represent them
-    for(size_t i = 0; i < args.size(); ++i) {
-      if(args[i].getType().isReal() && FunctionType(expr.getType()).getArgTypes()[i] == d_unsorted) {
-        args[i] = convertRatToUnsorted(args[i]);
-      }
-    }
-    expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args);
-  }
-}
-
-inline Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) {
-  // For SZS ontology compliance.
-  // if we're in cnf() though, conjectures don't result in "Theorem" or
-  // "CounterSatisfiable".
-  if(!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
-    d_hasConjecture = true;
-  }
-  switch(fr) {
-  case FR_AXIOM:
-  case FR_HYPOTHESIS:
-  case FR_DEFINITION:
-  case FR_ASSUMPTION:
-  case FR_LEMMA:
-  case FR_THEOREM:
-  case FR_NEGATED_CONJECTURE:
-  case FR_PLAIN:
-    // it's a usual assert
-    return new AssertCommand(expr);
-  case FR_CONJECTURE:
-    // something to prove
-    return new AssertCommand(getExprManager()->mkExpr(kind::NOT,expr));
-  case FR_UNKNOWN:
-  case FR_FI_DOMAIN:
-  case FR_FI_FUNCTORS:
-  case FR_FI_PREDICATES:
-  case FR_TYPE:
-    return new EmptyCommand("Untreated role");
-  }
-  assert(false);// unreachable
-  return NULL;
-}
 
 namespace tptp {
 /**