Support for TPTP's TFF0 (with arithmetic)

This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).

This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made.  These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.

8 files changed, 669 insertions, 202 deletions

diff --git a/src/parser/options b/src/parser/options
index e16f963f4..f277b231d 100644
--- a/src/parser/options
+++ b/src/parser/options
@@ -14,9 +14,6 @@ option memoryMap --mmap bool
 option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
  disable ALL semantic checks, including type checks
 
-option szsCompliant --szs-compliant bool :default false
- temporary support for szs ontolotogy, print if conjecture is found
-
 # this is just to support security in the online version
 # (--no-include-file disables filesystem access in TPTP and SMT2 parsers)
 undocumented-option canIncludeFile /--no-include-file bool :default true
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 684a495b6..cb8c0d4f6 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -90,11 +90,7 @@ Parser* ParserBuilder::build()
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   case language::input::LANG_TPTP:
-  {
-    Tptp * tparser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
-    tparser->d_szsCompliant = d_szsCompliant;
-    parser = tparser;
-  }
+    parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   default:
     parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
@@ -152,7 +148,6 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
 }
 
 ParserBuilder& ParserBuilder::withOptions(const Options& options) {
-  d_szsCompliant = options[options::szsCompliant];
   return
     withInputLanguage(options[options::inputLanguage])
       .withMmap(options[options::memoryMap])
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 9779bf37b..b6e15b2ff 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -80,9 +80,6 @@ class CVC4_PUBLIC ParserBuilder {
   /** Are we parsing only? */
   bool d_parseOnly;
 
-  /** hack for szs compliance */
-  bool d_szsCompliant;
-
   /** Initialize this parser builder */
   void init(ExprManager* exprManager, const std::string& filename);
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 16b5bc4ea..c048feea7 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -786,7 +786,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
                    kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
                  args.size() > 2 ) {
         /* "chainable", but CVC4 internally only supports 2 args */
-        expr = MK_EXPR(CVC4::kind::CHAIN, MK_CONST(kind), args);
+        expr = MK_EXPR(MK_CONST(Chain(kind)), args);
       } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS &&
                  args.size() == 1 && !args[0].getType().isInteger() ) {
         /* first, check that ABS is even defined in this logic */
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 9e814b358..beeca818e 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -27,7 +27,7 @@ options {
   // Only lookahead of <= k requested (disable for LL* parsing)
   // Note that CVC4's BoundedTokenBuffer requires a fixed k !
   // If you change this k, change it also in tptp_input.cpp !
-  k = 1;
+  k = 2;
 }/* options */
 
 @header {
@@ -102,6 +102,8 @@ using namespace CVC4::parser;
 #include "util/output.h"
 #include "util/rational.h"
 #include <vector>
+#include <iterator>
+#include <algorithm>
 
 using namespace CVC4;
 using namespace CVC4::parser;
@@ -114,12 +116,12 @@ using namespace CVC4::parser;
 #define EXPR_MANAGER PARSER_STATE->getExprManager()
 #undef MK_EXPR
 #define MK_EXPR EXPR_MANAGER->mkExpr
+#undef MK_EXPR_ASSOCIATIVE
+#define MK_EXPR_ASSOCIATIVE EXPR_MANAGER->mkAssociative
 #undef MK_CONST
 #define MK_CONST EXPR_MANAGER->mkConst
 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 
-
-
 }/* parser::postinclude */
 
 /**
@@ -139,46 +141,81 @@ parseCommand returns [CVC4::Command* cmd = NULL]
 @declarations {
   Expr expr;
   Tptp::FormulaRole fr;
-  std::string name;
-  std::string incl_args;
+  std::string name, inclSymbol;
 }
 //  : 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->pushScope(); }
+  { PARSER_STATE->cnf = true; PARSER_STATE->fof = false; PARSER_STATE->pushScope(); }
     cnfFormula[expr]
   { PARSER_STATE->popScope();
     std::vector<Expr> bvl = PARSER_STATE->getFreeVar();
-    if(!bvl.empty()){
+    if(!bvl.empty()) {
       expr = MK_EXPR(kind::FORALL,MK_EXPR(kind::BOUND_VAR_LIST,bvl),expr);
     };
   }
     (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
     {
-      cmd = PARSER_STATE->makeCommand(fr,expr);
+      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->cnf = false; PARSER_STATE->fof = true; }
     fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
     {
-      cmd = PARSER_STATE->makeCommand(fr,expr);
+      cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false);
     }
+  | 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; }
+      tffFormula[expr] (COMMA_TOK anything*)?
+      {
+        cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false);
+      }
+    ) RPAREN_TOK DOT_TOK
   | INCLUDE_TOK LPAREN_TOK unquotedFileName[name]
-    ( COMMA_TOK LBRACK_TOK nameN[incl_args] ( COMMA_TOK nameN[incl_args] )* RBRACK_TOK )?
+    ( COMMA_TOK LBRACK_TOK nameN[inclSymbol]
+      ( COMMA_TOK nameN[inclSymbol] )* RBRACK_TOK )?
     RPAREN_TOK DOT_TOK
-    {
-      PARSER_STATE->includeFile(name);
-      // The command of the included file will be produce at the new parseCommand call
+    { /* TODO - implement symbol filtering for file inclusion.
+       * the following removes duplicates and "all", just need to pass it
+       * through to includeFile() and implement it there.
+      std::sort(inclArgs.begin(), inclArgs.end());
+      std::vector<std::string>::iterator it =
+        std::unique(inclArgs.begin(), inclArgs.end());
+      inclArgs.resize(std::distance(inclArgs.begin(), it));
+      it = std::lower_bound(inclArgs.begin(), inclArgs.end(), std::string("all"));
+      if(it != inclArgs.end() && *it == "all") {
+        inclArgs.erase(it);
+      }
+      */
+      PARSER_STATE->includeFile(name /* , inclArgs */ );
+      // The command of the included file will be produced at the new parseCommand call
       cmd = new EmptyCommand("include::" + name);
     }
   | EOF
     {
-      PARSER_STATE->preemptCommand(new CheckSatCommand(MK_CONST(bool(true))));
+      std::string filename = PARSER_STATE->getInput()->getInputStreamName();
+      size_t i = filename.find_last_of('/');
+      if(i != std::string::npos) {
+        filename = filename.substr(i + 1);
+      }
+      if(filename.substr(filename.length() - 2) == ".p") {
+        filename = filename.substr(0, filename.length() - 2);
+      }
+      CommandSequence* seq = new CommandSequence();
+      seq->addCommand(new SetInfoCommand("name", filename));
+      if(PARSER_STATE->hasConjecture()) {
+        seq->addCommand(new QueryCommand(MK_CONST(bool(false))));
+      } else {
+        seq->addCommand(new CheckSatCommand());
+      }
+      PARSER_STATE->preemptCommand(seq);
       cmd = NULL;
     }
   ;
 
 /* Parse a formula Role */
-formulaRole[CVC4::parser::Tptp::FormulaRole & role]
+formulaRole[CVC4::parser::Tptp::FormulaRole& role]
   : LOWER_WORD
     {
       std::string r = AntlrInput::tokenText($LOWER_WORD);
@@ -204,33 +241,30 @@ formulaRole[CVC4::parser::Tptp::FormulaRole & role]
 /* CNF */
 
 /* It can parse a little more than the cnf grammar: false and true can appear.
-   Normally only false can appear and only at top level
-*/
+ * Normally only false can appear and only at top level. */
 
 cnfFormula[CVC4::Expr& expr]
-  :
-  LPAREN_TOK disjunction[expr] RPAREN_TOK
-| disjunction[expr]
+  : LPAREN_TOK cnfDisjunction[expr] RPAREN_TOK
+  | cnfDisjunction[expr]
 //| FALSE_TOK { expr = MK_CONST(bool(false)); }
 ;
 
-disjunction[CVC4::Expr& expr]
+cnfDisjunction[CVC4::Expr& expr]
 @declarations {
   std::vector<Expr> args;
 }
-  :
-    literal[expr] {args.push_back(expr); } ( OR_TOK literal[expr] {args.push_back(expr); } )*
-    {
-      if(args.size() > 1){
-        expr = MK_EXPR(kind::OR,args);
+  : cnfLiteral[expr] { args.push_back(expr); }
+    ( OR_TOK cnfLiteral[expr] { args.push_back(expr); } )*
+    { if(args.size() > 1) {
+        expr = MK_EXPR_ASSOCIATIVE(kind::OR, args);
       } // else its already in the expr
     }
 ;
 
-literal[CVC4::Expr& expr]
+cnfLiteral[CVC4::Expr& expr]
   : atomicFormula[expr]
-  | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT,expr); }
-//  | folInfixUnary[expr]
+  | NOT_TOK atomicFormula[expr] { expr = MK_EXPR(kind::NOT, expr); }
+//| folInfixUnary[expr]
   ;
 
 atomicFormula[CVC4::Expr& expr]
@@ -241,28 +275,32 @@ atomicFormula[CVC4::Expr& expr]
   bool equal;
 }
   : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
-    ( ( equalOp[equal] //equality/disequality between terms
-       {
-         PARSER_STATE->makeApplication(expr,name,args,true);
-       }
-       term[expr2]
-       {
-         expr = MK_EXPR(kind::EQUAL, expr, expr2);
-         if(!equal) expr = MK_EXPR(kind::NOT,expr);
-       }
-      )
-    | //predicate
-      {
-        PARSER_STATE->makeApplication(expr,name,args,false);
+    ( equalOp[equal] term[expr2]
+      { // equality/disequality between terms
+        PARSER_STATE->makeApplication(expr, name, args, true);
+        expr = MK_EXPR(kind::EQUAL, expr, expr2);
+        if(!equal) expr = MK_EXPR(kind::NOT, expr);
       }
-  )
-  | simpleTerm[expr] equalOp[equal] term[expr2]
-    {
+    | { // predicate
+        PARSER_STATE->makeApplication(expr, name, args, false);
+      }
+    )
+  | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+    equalOp[equal] term[expr2]
+    { expr = EXPR_MANAGER->mkExpr(expr, args);
+      expr = MK_EXPR(kind::EQUAL, expr, expr2);
+      if(!equal) expr = MK_EXPR(kind::NOT, expr);
+    }
+  | (simpleTerm[expr] | letTerm[expr] | conditionalTerm[expr])
+    equalOp[equal] term[expr2]
+    { // equality/disequality between terms
       expr = MK_EXPR(kind::EQUAL, expr, expr2);
-      if(!equal) expr = MK_EXPR(kind::NOT,expr);
+      if(!equal) expr = MK_EXPR(kind::NOT, expr);
     }
+  | definedPred[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+    { expr = EXPR_MANAGER->mkExpr(expr, args); }
   | definedProp[expr]
-;
+  ;
 //%----Using <plain_term> removes a reduce/reduce ambiguity in lex/yacc.
 //%----Note: "defined" means a word starting with one $ and "system" means $$.
 
@@ -270,35 +308,170 @@ definedProp[CVC4::Expr& expr]
   : TRUE_TOK { expr = MK_CONST(bool(true)); }
   | FALSE_TOK  { expr = MK_CONST(bool(false)); }
   ;
+
+definedPred[CVC4::Expr& expr]
+  : '$less' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LT); }
+  | '$lesseq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::LEQ); }
+  | '$greater' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GT); }
+  | '$greatereq' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::GEQ); }
+  | '$is_rat' // all "real" are actually "rat" in CVC4
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      n = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      expr = MK_EXPR(CVC4::kind::LAMBDA, n, MK_CONST(bool(true)));
+    }
+  | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); }
+  | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); }
+  ;
+
+definedFun[CVC4::Expr& expr]
+@declarations {
+  bool remainder = false;
+}
+  : '$uminus' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::UMINUS); }
+  | '$sum' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::PLUS); }
+  | '$difference' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MINUS); }
+  | '$product' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::MULT); }
+  | '$quotient' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DIVISION_TOTAL); }
+  | ( '$quotient_e' { remainder = false; }
+    | '$remainder_e' { remainder = true; }
+    )
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+      expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+      expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, d, MK_CONST(Rational(0))),
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, expr),
+                                      MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
+      if(remainder) {
+        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+      }
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | ( '$quotient_t' { remainder = false; }
+    | '$remainder_t' { remainder = true; }
+    )
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+      expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+      expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, expr, MK_CONST(Rational(0))),
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, expr),
+                                      MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, expr))));
+      if(remainder) {
+        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+      }
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | ( '$quotient_f' { remainder = false; }
+    | '$remainder_f' { remainder = true; }
+    )
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr d = EXPR_MANAGER->mkBoundVar("D", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n, d);
+      expr = MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, d);
+      expr = MK_EXPR(CVC4::kind::TO_INTEGER, expr);
+      if(remainder) {
+        expr = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d));
+      }
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | '$floor' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); }
+  | '$ceiling'
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      expr = MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n)));
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | '$truncate'
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GEQ, n, MK_CONST(Rational(0))),
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, n),
+                                      MK_EXPR(CVC4::kind::UMINUS, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::UMINUS, n))));
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | '$round'
+    { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+      Expr formals = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
+      Expr decPart = MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::TO_INTEGER, n));
+      expr = MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::LT, decPart, MK_CONST(Rational(1, 2))),
+                                      // if decPart < 0.5, round down
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, n),
+             MK_EXPR(CVC4::kind::ITE, MK_EXPR(CVC4::kind::GT, decPart, MK_CONST(Rational(1, 2))),
+                                      // if decPart > 0.5, round up
+                                      MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, n, MK_CONST(Rational(1)))),
+                                      // if decPart == 0.5, round to nearest even integer:
+                                      // result is: to_int(n/2 + .5) * 2
+                                      MK_EXPR(CVC4::kind::MULT, MK_EXPR(CVC4::kind::TO_INTEGER, MK_EXPR(CVC4::kind::PLUS, MK_EXPR(CVC4::kind::DIVISION_TOTAL, n, MK_CONST(Rational(2))), MK_CONST(Rational(1, 2)))), MK_CONST(Rational(2)))));
+      expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+    }
+  | '$to_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_INTEGER); }
+  | '$to_rat' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); }
+  | '$to_real' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::TO_REAL); }
+  ;
+
 //%----Pure CNF should not use $true or $false in problems, and use $false only
 //%----at the roots of a refutation.
 
-equalOp[bool & equal]
- :  EQUAL_TOK    {equal = true;}
-  | DISEQUAL_TOK {equal = false;}
+equalOp[bool& equal]
+  : EQUAL_TOK    { equal = true; }
+  | DISEQUAL_TOK { equal = false; }
   ;
 
 term[CVC4::Expr& expr]
- : functionTerm[expr]
+  : functionTerm[expr]
+  | conditionalTerm[expr]
   | simpleTerm[expr]
-//  | conditionalTerm
-//  | let_term
+  | letTerm[expr]
+  ;
+
+letTerm[CVC4::Expr& expr]
+@declarations {
+  CVC4::Expr lhs, rhs;
+}
+  : '$let_ft' LPAREN_TOK { PARSER_STATE->pushScope(); }
+    tffLetFormulaDefn[lhs, rhs] COMMA_TOK
+    term[expr]
+    { PARSER_STATE->popScope();
+      expr = expr.substitute(lhs, rhs);
+    }
+    RPAREN_TOK
+  | '$let_tt' LPAREN_TOK { PARSER_STATE->pushScope(); }
+    tffLetTermDefn[lhs, rhs] COMMA_TOK
+    term[expr]
+    { PARSER_STATE->popScope();
+      expr = expr.substitute(lhs, rhs);
+    }
+    RPAREN_TOK
   ;
 
 /* Not an application */
 simpleTerm[CVC4::Expr& expr]
   : variable[expr]
   | NUMBER { expr = PARSER_STATE->d_tmp_expr; }
-  | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(
-        AntlrInput::tokenText($DISTINCT_OBJECT)); }
-;
+  | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(AntlrInput::tokenText($DISTINCT_OBJECT)); }
+  ;
 
 functionTerm[CVC4::Expr& expr]
-  : plainTerm[expr] // | <defined_term> | <system_term>
+@declarations {
+  std::vector<CVC4::Expr> args;
+}
+  : plainTerm[expr]
+  | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK
+    { expr = EXPR_MANAGER->mkExpr(expr, args); }
+// | <system_term>
+  ;
+
+conditionalTerm[CVC4::Expr& expr]
+@declarations {
+  CVC4::Expr expr2, expr3;
+}
+  : '$ite_t' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK term[expr2] COMMA_TOK term[expr3] RPAREN_TOK
+    { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, expr2, expr3); }
   ;
 
 plainTerm[CVC4::Expr& expr]
-@declarations{
+@declarations {
   std::string name;
   std::vector<Expr> args;
 }
@@ -308,19 +481,19 @@ plainTerm[CVC4::Expr& expr]
     }
   ;
 
-arguments[std::vector<CVC4::Expr> & args]
-@declarations{
+arguments[std::vector<CVC4::Expr>& args]
+@declarations {
   Expr expr;
 }
   :
   term[expr] { args.push_back(expr); } ( COMMA_TOK term[expr] { args.push_back(expr); } )*
   ;
 
-variable[CVC4::Expr & expr]
+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);
@@ -331,18 +504,18 @@ variable[CVC4::Expr & expr]
 
 /*******/
 /* FOF */
-fofFormula[CVC4::Expr & expr] : fofLogicFormula[expr] ;
+fofFormula[CVC4::Expr& expr] : fofLogicFormula[expr] ;
 
-fofLogicFormula[CVC4::Expr & expr]
-@declarations{
+fofLogicFormula[CVC4::Expr& expr]
+@declarations {
   tptp::NonAssoc na;
   std::vector< Expr > args;
   Expr expr2;
 }
   : fofUnitaryFormula[expr]
-    ( //Non Assoc <=> <~> ~& ~|
+    ( // Non-associative: <=> <~> ~& ~|
       ( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
-        { switch(na){
+        { switch(na) {
            case tptp::NA_IFF:
              expr = MK_EXPR(kind::IFF,expr,expr2);
              break;
@@ -364,21 +537,21 @@ fofLogicFormula[CVC4::Expr & expr]
           }
         }
       )
-    | //And &
+    | // N-ary and &
       ( { args.push_back(expr); }
         ( AND_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
-        { expr = MK_EXPR(kind::AND,args); }
+        { expr = MK_EXPR_ASSOCIATIVE(kind::AND, args); }
       )
-    | //Or |
+    | // N-ary or |
       ( { args.push_back(expr); }
         ( OR_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
-        { expr = MK_EXPR(kind::OR,args); }
+        { expr = MK_EXPR_ASSOCIATIVE(kind::OR, args); }
       )
-   )?
+    )?
   ;
 
-fofUnitaryFormula[CVC4::Expr & expr]
-@declarations{
+fofUnitaryFormula[CVC4::Expr& expr]
+@declarations {
   Kind kind;
   std::vector< Expr > bv;
 }
@@ -389,20 +562,20 @@ fofUnitaryFormula[CVC4::Expr & expr]
     folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
     ( bindvariable[expr] { bv.push_back(expr); }
       ( COMMA_TOK bindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
-  COLON_TOK fofUnitaryFormula[expr]
-  { PARSER_STATE->popScope();
-    expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
-  } ;
+    COLON_TOK fofUnitaryFormula[expr]
+    { PARSER_STATE->popScope();
+      expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+    }
+  ;
 
-bindvariable[CVC4::Expr & expr]
+bindvariable[CVC4::Expr& expr]
   : UPPER_WORD
-    {
-      std::string name = AntlrInput::tokenText($UPPER_WORD);
+    { std::string name = AntlrInput::tokenText($UPPER_WORD);
       expr = PARSER_STATE->mkBoundVar(name, PARSER_STATE->d_unsorted);
     }
-    ;
+  ;
 
-fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc & na]
+fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc& na]
   : IFF_TOK      { na = tptp::NA_IFF; }
   | REVIFF_TOK   { na = tptp::NA_REVIFF; }
   | REVOR_TOK    { na = tptp::NA_REVOR; }
@@ -411,11 +584,229 @@ fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc & na]
   | REVIMPLIES_TOK { na = tptp::NA_REVIMPLIES; }
   ;
 
-folQuantifier[CVC4::Kind & kind]
+folQuantifier[CVC4::Kind& kind]
   : BANG_TOK { kind = kind::FORALL; }
   | MARK_TOK { kind = kind::EXISTS; }
   ;
 
+/*******/
+/* TFF */
+tffFormula[CVC4::Expr& expr] : tffLogicFormula[expr];
+
+tffTypedAtom[CVC4::Command*& cmd]
+@declarations {
+  CVC4::Expr expr;
+  CVC4::Type type;
+  std::string name;
+}
+  : LPAREN_TOK tffTypedAtom[cmd] RPAREN_TOK
+  | nameN[name] COLON_TOK
+    ( '$tType'
+      { if(PARSER_STATE->isDeclared(name, SYM_SORT)) {
+          // duplicate declaration is fine, they're compatible
+          cmd = new EmptyCommand("compatible redeclaration of sort " + name);
+        } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
+          // error: cannot be both sort and constant
+          PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a constant; cannot also be a sort");
+        } else {
+          // as yet, it's undeclared
+          Type type = PARSER_STATE->mkSort(name);
+          cmd = new DeclareTypeCommand(name, 0, type);
+        }
+      }
+    | parseType[type]
+      { if(PARSER_STATE->isDeclared(name, SYM_SORT)) {
+          // error: cannot be both sort and constant
+          PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a sort");
+          cmd = new EmptyCommand("compatible redeclaration of sort " + name);
+        } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
+          if(type == PARSER_STATE->getVariable(name).getType()) {
+            // duplicate declaration is fine, they're compatible
+            cmd = new EmptyCommand("compatible redeclaration of constant " + name);
+          } else {
+            // error: sorts incompatible
+            PARSER_STATE->parseError("Symbol `" + name + "' declared previously with a different sort");
+          }
+        } else {
+          // as yet, it's undeclared
+          CVC4::Expr expr;
+          if(type.isFunction()) {
+            expr = PARSER_STATE->mkTffFunction(name, type);
+          } else {
+            expr = PARSER_STATE->mkTffVar(name, type);
+          }
+          cmd = new DeclareFunctionCommand(name, expr, type);
+        }
+      }
+    )
+  ;
+
+tffLogicFormula[CVC4::Expr& expr]
+@declarations {
+  tptp::NonAssoc na;
+  std::vector< Expr > args;
+  Expr expr2;
+}
+  : tffUnitaryFormula[expr]
+    ( // Non Assoc <=> <~> ~& ~|
+      ( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
+        { switch(na) {
+           case tptp::NA_IFF:
+             expr = MK_EXPR(kind::IFF,expr,expr2);
+             break;
+           case tptp::NA_REVIFF:
+             expr = MK_EXPR(kind::XOR,expr,expr2);
+             break;
+           case tptp::NA_IMPLIES:
+             expr = MK_EXPR(kind::IMPLIES,expr,expr2);
+             break;
+           case tptp::NA_REVIMPLIES:
+             expr = MK_EXPR(kind::IMPLIES,expr2,expr);
+             break;
+           case tptp::NA_REVOR:
+             expr = MK_EXPR(kind::NOT,MK_EXPR(kind::OR,expr,expr2));
+             break;
+           case tptp::NA_REVAND:
+             expr = MK_EXPR(kind::NOT,MK_EXPR(kind::AND,expr,expr2));
+             break;
+          }
+        }
+      )
+    | // And &
+      ( { args.push_back(expr); }
+        ( AND_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
+        { expr = MK_EXPR(kind::AND,args); }
+      )
+    | // Or |
+      ( { args.push_back(expr); }
+        ( OR_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
+        { expr = MK_EXPR(kind::OR,args); }
+      )
+    )?
+  ;
+
+tffUnitaryFormula[CVC4::Expr& expr]
+@declarations {
+  Kind kind;
+  std::vector< Expr > bv;
+  Expr lhs, rhs;
+}
+  : atomicFormula[expr]
+  | LPAREN_TOK tffLogicFormula[expr] RPAREN_TOK
+  | NOT_TOK tffUnitaryFormula[expr] { expr = MK_EXPR(kind::NOT,expr); }
+  | // Quantified
+    folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
+    ( tffbindvariable[expr] { bv.push_back(expr); }
+      ( COMMA_TOK tffbindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
+    COLON_TOK tffUnitaryFormula[expr]
+    { PARSER_STATE->popScope();
+      expr = MK_EXPR(kind, MK_EXPR(kind::BOUND_VAR_LIST, bv), expr);
+    }
+  | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK
+    { expr = EXPR_MANAGER->mkExpr(CVC4::kind::ITE, expr, lhs, rhs); }
+  | '$let_tf' LPAREN_TOK { PARSER_STATE->pushScope(); }
+    tffLetTermDefn[lhs, rhs] COMMA_TOK
+    tffFormula[expr]
+    { PARSER_STATE->popScope();
+      expr = expr.substitute(lhs, rhs);
+    }
+    RPAREN_TOK
+  | '$let_ff' LPAREN_TOK { PARSER_STATE->pushScope(); }
+    tffLetFormulaDefn[lhs, rhs] COMMA_TOK
+    tffFormula[expr]
+    { PARSER_STATE->popScope();
+      expr = expr.substitute(lhs, rhs);
+    }
+    RPAREN_TOK
+  ;
+
+tffLetTermDefn[CVC4::Expr& lhs, CVC4::Expr& rhs]
+@declarations {
+  std::vector<CVC4::Expr> bvlist;
+}
+  : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
+    tffLetTermBinding[bvlist, lhs, rhs]
+  ;
+
+tffLetTermBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs]
+  : term[lhs] EQUAL_TOK term[rhs]
+    { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
+      rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
+      lhs = lhs.getOperator();
+    }
+  | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
+  ;
+
+tffLetFormulaDefn[CVC4::Expr& lhs, CVC4::Expr& rhs]
+@declarations {
+  std::vector<CVC4::Expr> bvlist;
+}
+  : (BANG_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
+    tffLetFormulaBinding[bvlist, lhs, rhs]
+  ;
+
+tffLetFormulaBinding[std::vector<CVC4::Expr>& bvlist, CVC4::Expr& lhs, CVC4::Expr& rhs]
+  : atomicFormula[lhs] IFF_TOK tffUnitaryFormula[rhs]
+    { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
+      rhs = MK_EXPR(CVC4::kind::LAMBDA, MK_EXPR(CVC4::kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
+      lhs = lhs.getOperator();
+    }
+  | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
+  ;
+
+tffbindvariable[CVC4::Expr& expr]
+@declarations {
+  CVC4::Type type = PARSER_STATE->d_unsorted;
+}
+  : UPPER_WORD
+    ( COLON_TOK parseType[type] )?
+    { std::string name = AntlrInput::tokenText($UPPER_WORD);
+      expr = PARSER_STATE->mkBoundVar(name, type);
+    }
+  ;
+
+// bvlist is accumulative; it can already contain elements
+// on the way in, which are left undisturbed
+tffVariableList[std::vector<CVC4::Expr>& bvlist]
+@declarations {
+  CVC4::Expr e;
+}
+  : tffbindvariable[e] { bvlist.push_back(e); }
+    ( COMMA_TOK tffbindvariable[e] { bvlist.push_back(e); } )*
+  ;
+
+parseType[CVC4::Type& type]
+@declarations {
+  std::vector<CVC4::Type> v;
+}
+  : simpleType[type]
+  | ( simpleType[type] { v.push_back(type); }
+    | LPAREN_TOK simpleType[type] { v.push_back(type); }
+      ( TIMES_TOK simpleType[type] { v.push_back(type); } )+
+      RPAREN_TOK
+    )
+    GREATER_TOK simpleType[type]
+    { v.push_back(type);
+      type = EXPR_MANAGER->mkFunctionType(v);
+    }
+  ;
+
+// non-function types
+simpleType[CVC4::Type& type]
+  : DEFINED_SYMBOL
+    { std::string s = AntlrInput::tokenText($DEFINED_SYMBOL);
+      if(s == "\$i") type = PARSER_STATE->d_unsorted;
+      else if(s == "\$o") type = EXPR_MANAGER->booleanType();
+      else if(s == "\$int") type = EXPR_MANAGER->integerType();
+      else if(s == "\$rat") type = EXPR_MANAGER->realType();
+      else if(s == "\$real") type = EXPR_MANAGER->realType();
+      else if(s == "\$tType") PARSER_STATE->parseError("Type of types `\$tType' cannot be used here");
+      else PARSER_STATE->parseError("unknown defined type `" + s + "'");
+    }
+  | LOWER_WORD
+    { type = PARSER_STATE->getSort(AntlrInput::tokenText($LOWER_WORD)); }
+  ;
+
 /***********************************************/
 /* Anything well parenthesis */
 
@@ -447,6 +838,7 @@ anything
   | FOF_TOK
   | THF_TOK
   | TFF_TOK
+  | TYPE_TOK
   | INCLUDE_TOK
   | DISTINCT_OBJECT
   | UPPER_WORD
@@ -467,6 +859,8 @@ LBRACK_TOK : '[';
 RBRACK_TOK : ']';
 COLON_TOK  : ':';
 
+GREATER_TOK  : '>';
+
 //operator
 OR_TOK       : '|';
 NOT_TOK      : '~';
@@ -494,6 +888,7 @@ CNF_TOK     : 'cnf';
 FOF_TOK     : 'fof';
 THF_TOK     : 'thf';
 TFF_TOK     : 'tff';
+TYPE_TOK    : 'type';
 INCLUDE_TOK : 'include';
 
 //Other defined symbols, must be defined after all the other
@@ -533,30 +928,30 @@ UPPER_WORD : UPPER_ALPHA ALPHA_NUMERIC*;
 LOWER_WORD : LOWER_ALPHA ALPHA_NUMERIC*;
 
 /* filename */
-unquotedFileName[std::string & name] /* Beware fileName identifier is used by the backend ... */
+unquotedFileName[std::string& name] /* Beware fileName identifier is used by the backend ... */
  : (s=LOWER_WORD_SINGLE_QUOTED | s=SINGLE_QUOTED)
     { name = AntlrInput::tokenText($s);
       name = name.substr(1, name.size() - 2 );
     };
 
 /* axiom name */
-nameN[std::string & name]
+nameN[std::string& name]
  : atomicWord[name]
  | NUMBER { name = AntlrInput::tokenText($NUMBER); }
  ;
 
 /* atomic word everything (fof, cnf, thf, tff, include must not be keyword at this position ) */
-atomicWord[std::string & name]
+atomicWord[std::string& name]
  : FOF_TOK     { name = "fof"; }
  | CNF_TOK     { name = "cnf"; }
  | THF_TOK     { name = "thf"; }
  | TFF_TOK     { name = "tff"; }
+ | TYPE_TOK    { name = "type"; }
  | INCLUDE_TOK { name = "include"; }
  | LOWER_WORD  { name = AntlrInput::tokenText($LOWER_WORD); }
- | LOWER_WORD_SINGLE_QUOTED //the lower word single quoted are considered without quote
-    {
-      /* strip off the quotes */
-      name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED,1,
+ | LOWER_WORD_SINGLE_QUOTED // the lower word single quoted are considered without quote
+    { /* strip off the quotes */
+      name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED, 1 ,
                                          ($LOWER_WORD_SINGLE_QUOTED->stop - $LOWER_WORD_SINGLE_QUOTED->start) - 1);
     }
  | SINGLE_QUOTED {name = AntlrInput::tokenText($SINGLE_QUOTED); }; //for the others the quote remains
@@ -565,35 +960,34 @@ atomicWord[std::string & name]
 /* Rational */
 
 fragment DOT              : '.';
-fragment EXPONENT         : 'E'|'e';
+fragment EXPONENT         : 'E' | 'e';
 fragment SLASH            : '/';
 
 fragment DECIMAL : NUMERIC+;
 
-/* Currently we put all in the rationnal type */
-fragment SIGN[bool & pos] : PLUS_TOK | MINUS_TOK { pos = false; } ;
-
+/* Currently we put all in the rational type */
+fragment SIGN[bool& pos]
+  : PLUS_TOK { pos = true; }
+  | MINUS_TOK { pos = false; }
+  ;
 
 NUMBER
-@declarations{
+@declarations {
   bool pos = true;
   bool posE = true;
 }
-  :
-  ( SIGN[pos]? num=DECIMAL
-    {
-      Integer i (AntlrInput::tokenText($num));
-      Rational r = ( pos ? i : -i );
-      PARSER_STATE->d_tmp_expr = MK_CONST(r);
-    }
-  | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
-    {
-        std::string snum = AntlrInput::tokenText($num);
+  : ( SIGN[pos]? num=DECIMAL
+      { Integer i(AntlrInput::tokenText($num));
+        Rational r = pos ? i : -i;
+        PARSER_STATE->d_tmp_expr = MK_CONST(r);
+      }
+    | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
+      { std::string snum = AntlrInput::tokenText($num);
         std::string sden = AntlrInput::tokenText($den);
         /* compute the numerator */
-        Integer inum( snum + sden );
+        Integer inum(snum + sden);
         // The sign
-        inum = pos ? inum : - inum;
+        inum = pos ? inum : -inum;
         // The exponent
         size_t exp = ($e == NULL ? 0 : AntlrInput::tokenToUnsigned($e));
         // Decimal part
@@ -601,26 +995,25 @@ NUMBER
         /* multiply it by 10 raised to the exponent reduced by the
          * number of decimal place in den (dec) */
         Rational r;
-        if( !posE ) r = Rational(inum, Integer(10).pow(exp + dec));
-        else if( exp == dec ) r = Rational(inum);
-        else if( exp > dec ) r = Rational(inum * Integer(10).pow(exp - dec));
+        if(!posE) r = Rational(inum, Integer(10).pow(exp + dec));
+        else if(exp == dec) r = Rational(inum);
+        else if(exp > dec) r = Rational(inum * Integer(10).pow(exp - dec));
         else r = Rational(inum, Integer(10).pow(dec - exp));
-        PARSER_STATE->d_tmp_expr = MK_CONST( r );
+        PARSER_STATE->d_tmp_expr = MK_CONST(r);
+      }
+    | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
+      { Integer inum(AntlrInput::tokenText($num));
+        Integer iden(AntlrInput::tokenText($den));
+        PARSER_STATE->d_tmp_expr = MK_CONST(Rational(pos ? inum : -inum, iden));
+      }
+    )
+    { 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 );
       }
-  | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
-    {
-      Integer inum(AntlrInput::tokenText($num));
-      Integer iden(AntlrInput::tokenText($den));
-      PARSER_STATE->d_tmp_expr = MK_CONST(
-        Rational(pos ? inum : -inum, iden));
-    }
-  ) {
-      //Put a convertion around it
-      PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr );
     }
   ;
 
-
 /**
  * Matches the comments and ignores them
  */
@@ -629,5 +1022,3 @@ COMMENT
   | '/*'  ( options {greedy=false;} : . )*  '*/' { SKIP(); } //comment block
   ;
 
-
-
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 93c2168b1..3e6aa82b7 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -33,26 +33,26 @@ Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn
   /* Try to find TPTP dir */
   // From tptp4x FileUtilities
   //----Try the TPTP directory, and TPTP variations
-    char* home = getenv("TPTP");
-    if (home == NULL) {
-        home = getenv("TPTP_HOME");
+  char* home = getenv("TPTP");
+  if(home == NULL) {
+     home = getenv("TPTP_HOME");
 // //----If no TPTP_HOME, try the tptp user (aaargh)
-//         if (home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) {
-//             home = PasswdEntry->pw_dir;
+//         if(home == NULL && (PasswdEntry = getpwnam("tptp")) != NULL) {
+//            home = PasswdEntry->pw_dir;
 //         }
 //----Now look in the TPTP directory from there
-        if (home != NULL) {
-          d_tptpDir = home;
-          d_tptpDir.append("/TPTP/");
-        }
-    } else {
+    if(home != NULL) {
       d_tptpDir = home;
-      //add trailing "/"
-      if( d_tptpDir[d_tptpDir.size() - 1] != '/'){
-        d_tptpDir.append("/");
-      }
+      d_tptpDir.append("/TPTP/");
     }
-    d_hasConjecture = false;
+  } else {
+    d_tptpDir = home;
+    //add trailing "/"
+    if(d_tptpDir[d_tptpDir.size() - 1] != '/') {
+      d_tptpDir.append("/");
+    }
+  }
+  d_hasConjecture = false;
 }
 
 void Tptp::addTheory(Theory theory) {
@@ -92,7 +92,7 @@ void Tptp::addTheory(Theory theory) {
 /* The include are managed in the lexer but called in the parser */
 // Inspired by http://www.antlr3.org/api/C/interop.html
 
-bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){
+bool newInputStream(std::string fileName, pANTLR3_LEXER lexer) {
   Debug("parser") << "Including " << fileName << std::endl;
   // Create a new input stream and take advantage of built in stream stacking
   // in C target runtime.
@@ -103,7 +103,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){
 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
   in = antlr3FileStreamNew((pANTLR3_UINT8) fileName.c_str(), ANTLR3_ENC_8BIT);
 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
-  if( in == NULL ) {
+  if(in == NULL) {
     Debug("parser") << "Can't open " << fileName << std::endl;
     return false;
   }
@@ -126,8 +126,15 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer){
   return true;
 }
 
+/* overridden popCharStream for the lexer - necessary if we had symbol
+ * filtering in file inclusion.
+void Tptp::myPopCharStream(pANTLR3_LEXER lexer) {
+  ((Tptp*)lexer->super)->d_oldPopCharStream(lexer);
+  ((Tptp*)lexer->super)->popScope();
+}
+*/
 
-void Tptp::includeFile(std::string fileName){
+void Tptp::includeFile(std::string fileName) {
   // security for online version
   if(!canIncludeFile()) {
     parseError("include-file feature was disabled for this run.");
@@ -136,36 +143,78 @@ void Tptp::includeFile(std::string fileName){
   // Get the lexer
   AntlrInput * ai = static_cast<AntlrInput *>(getInput());
   pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
+
+  // set up popCharStream - would be necessary for handling symbol
+  // filtering in inclusions
+  /*
+  if(d_oldPopCharStream == NULL) {
+    d_oldPopCharStream = lexer->popCharStream;
+    lexer->popCharStream = myPopCharStream;
+  }
+  */
+
+  // push the inclusion scope; will be popped by our special popCharStream
+  // would be necessary for handling symbol filtering in inclusions
+  //pushScope();
+
   // get the name of the current stream "Does it work inside an include?"
   const std::string inputName = ai->getInputStreamName();
 
   // Test in the directory of the actual parsed file
   std::string currentDirFileName;
-  if( inputName != "<stdin>"){
+  if(inputName != "<stdin>") {
     // TODO: Use dirname ot Boost::filesystem?
     size_t pos = inputName.rfind('/');
-    if( pos != std::string::npos){
+    if(pos != std::string::npos) {
       currentDirFileName = std::string(inputName, 0, pos + 1);
     }
     currentDirFileName.append(fileName);
-    if( newInputStream(currentDirFileName,lexer) ){
+    if(newInputStream(currentDirFileName,lexer)) {
       return;
     }
   } else {
     currentDirFileName = "<unknown current directory for stdin>";
   }
 
-  if( d_tptpDir.empty() ){
+  if(d_tptpDir.empty()) {
     parseError("Couldn't open included file: " + fileName
                + " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)");
   };
 
   std::string tptpDirFileName = d_tptpDir + fileName;
-  if( !newInputStream(tptpDirFileName,lexer) ){
+  if(! newInputStream(tptpDirFileName,lexer)) {
     parseError("Couldn't open included file: " + fileName
                + " at " + currentDirFileName + " or " + tptpDirFileName);
   }
 }
 
+void Tptp::checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula) {
+  if(lhs.getKind() != CVC4::kind::APPLY_UF) {
+    parseError("malformed let: LHS must be a flat function application");
+  }
+  std::vector<CVC4::Expr> v = lhs.getChildren();
+  if(formula && !lhs.getType().isBoolean()) {
+    parseError("malformed let: LHS must be formula");
+  }
+  for(size_t i = 0; i < v.size(); ++i) {
+    if(v[i].hasOperator()) {
+      parseError("malformed let: LHS must be flat, illegal child: " + v[i].toString());
+    }
+  }
+  std::sort(v.begin(), v.end());
+  std::sort(bvlist.begin(), bvlist.end());
+  // ensure all let-bound variables appear on the LHS, and appear only once
+  for(size_t i = 0; i < bvlist.size(); ++i) {
+    std::vector<CVC4::Expr>::const_iterator found = std::lower_bound(v.begin(), v.end(), bvlist[i]);
+    if(found == v.end() || *found != bvlist[i]) {
+      parseError("malformed let: LHS must make use of all quantified variables, missing `" + bvlist[i].toString() + "'");
+    }
+    std::vector<CVC4::Expr>::const_iterator found2 = found + 1;
+    if(found2 != v.end() && *found2 == *found) {
+      parseError("malformed let: LHS cannot use same bound variable twice: " + (*found).toString());
+    }
+  }
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index cea246282..79092e98f 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -25,6 +25,7 @@
 #include <ext/hash_set>
 #include <cassert>
 #include "parser/options.h"
+#include "parser/antlr_input.h"
 
 namespace CVC4 {
 
@@ -46,51 +47,57 @@ class Tptp : public Parser {
   std::hash_set<Expr, ExprHashFunction> d_r_converted;
   std::hash_map<std::string, Expr, StringHashFunction> d_distinct_objects;
 
-  //TPTP directory where to find includes
+  // TPTP directory where to find includes;
   // empty if none could be determined
   std::string d_tptpDir;
 
-  //hack to make output SZS ontology-compliant
+  // hack to make output SZS ontology-compliant
   bool d_hasConjecture;
-  // hack for szs compliance
-  bool d_szsCompliant;
+
+  static void myPopCharStream(pANTLR3_LEXER lexer);
+  void (*d_oldPopCharStream)(pANTLR3_LEXER);
 
 public:
-  bool cnf; //in a cnf formula
 
-  void addFreeVar(Expr var){assert(cnf); d_freeVar.push_back(var); };
-  std::vector< Expr > getFreeVar(){
+  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){
+  inline Expr convertRatToUnsorted(Expr expr) {
     ExprManager * em = getExprManager();
 
     // Create the conversion function If they doesn't exists
-    if(d_rtu_op.isNull()){
+    if(d_rtu_op.isNull()) {
       Type t;
-      //Conversion from rational to unsorted
+      // 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
+      // Conversion from unsorted to rational
       t = em->mkFunctionType(d_unsorted, em->realType());
       d_utr_op = em->mkVar("$$utr",t);
-      preemptCommand(new DeclareFunctionCommand("$$utur", d_utr_op, 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() ){
+    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));
+      Expr eq = em->mkExpr(kind::EQUAL, expr,
+                           em->mkExpr(kind::APPLY_UF, d_utr_op, ret));
       preemptCommand(new AssertCommand(eq));
-    };
+    }
     return ret;
   }
 
@@ -104,12 +111,13 @@ public:
 
 public:
 
-  //TPTP (CNF and FOF) is unsorted so we define this common type
+  // CNF and FOF are unsorted so we define this common type.
+  // This is also the Type of $i in TFF.
   Type d_unsorted;
 
   enum Theory {
     THEORY_CORE,
-  };
+  };/* enum Theory */
 
   enum FormulaRole {
     FR_AXIOM,
@@ -126,8 +134,9 @@ public:
     FR_FI_FUNCTORS,
     FR_FI_PREDICATES,
     FR_TYPE,
-  };
+  };/* enum FormulaRole */
 
+  bool hasConjecture() const { return d_hasConjecture; }
 
 protected:
   Tptp(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
@@ -140,10 +149,30 @@ public:
    */
   void addTheory(Theory theory);
 
-  inline void makeApplication(Expr & expr, std::string & name,
-                              std::vector<Expr> & args, bool term);
+  inline void makeApplication(Expr& expr, std::string& name,
+                              std::vector<Expr>& args, bool term);
+
+  inline Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf);
+
+  inline Expr mkTffVar(std::string& name, const Type& type) {
+    std::string orig = name;
+    std::stringstream ss;
+    ss << name << "_0";
+    name = ss.str();
+    Expr var = mkVar(name, type);
+    defineFunction(orig, var);
+    return var;
+  }
 
-  inline Command* makeCommand(FormulaRole fr, Expr & expr);
+  inline Expr mkTffFunction(std::string& name, const FunctionType& type) {
+    std::string orig = name;
+    std::stringstream ss;
+    ss << name << "_" << type.getArity();
+    name = ss.str();
+    Expr fun = mkFunction(name, type);
+    defineFunction(orig, fun);
+    return fun;
+  }
 
   /** Ugly hack because I don't know how to return an expression from a
       token */
@@ -153,48 +182,57 @@ public:
       is reused */
   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 addArithmeticOperators();
 };/* class Tptp */
 
-inline void Tptp::makeApplication(Expr & expr, std::string & name,
-                           std::vector<Expr> & args, bool term){
+inline void Tptp::makeApplication(Expr& expr, std::string& name,
+                                  std::vector<Expr>& args, bool term) {
   // We distinguish the symbols according to their arities
   std::stringstream ss;
   ss << name << "_" << args.size();
   name = ss.str();
-  if(args.empty()){ // Its a constant
-    if(isDeclared(name)){ //already appeared
+  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,true); //levelZero
+      expr = mkVar(name, t, true); // levelZero
       preemptCommand(new DeclareFunctionCommand(name, expr, t));
     }
   } else { // Its an application
-    if(isDeclared(name)){ //already appeared
+    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,true); //levelZero
+      expr = mkVar(name, t, true); // 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){
-  //hack for SZS ontology compliance
-  if(d_szsCompliant && (fr==FR_NEGATED_CONJECTURE || fr==FR_CONJECTURE)){
-    if( !d_hasConjecture ){
-      d_hasConjecture = true;
-      std::cout << "conjecture-";
-    }
+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){
+  switch(fr) {
   case FR_AXIOM:
   case FR_HYPOTHESIS:
   case FR_DEFINITION:
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index 34a620187..bfaeb07c9 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -28,9 +28,9 @@
 namespace CVC4 {
 namespace parser {
 
-/* Use lookahead=1 */
+/* Use lookahead=2 */
 TptpInput::TptpInput(AntlrInputStream& inputStream) :
-  AntlrInput(inputStream, 1) {
+  AntlrInput(inputStream, 2) {
   pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   assert( input != NULL );