src/parser/tptp/Tptp.g

   1 /* *******************                                                        */
   2 /*! \file Tptp.g
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa, Francois Bobot, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Parser for TPTP input language.
  13  **
  14  ** Parser for TPTP input language.
  15  ** cf. http://www.cs.miami.edu/~tptp/cgi-bin/SeeTPTP?Category=Documents&File=SyntaxBNF
  16  **/
  17
  18 grammar Tptp;
  19
  20 options {
  21   // C output for antlr
  22   language = 'C';
  23
  24   // Skip the default error handling, just break with exceptions
  25   // defaultErrorHandler = false;
  26
  27   // Only lookahead of <= k requested (disable for LL* parsing)
  28   // Note that CVC4's BoundedTokenBuffer requires a fixed k !
  29   // If you change this k, change it also in tptp_input.cpp !
  30   k = 2;
  31 }/* options */
  32
  33 @header {
  34 /**
  35  ** This file is part of the CVC4 project.
  36  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
  37  ** in the top-level source directory) and their institutional affiliations.
  38  ** All rights reserved.  See the file COPYING in the top-level source
  39  ** directory for licensing information.
  40  **/
  41 }/* @header */
  42
  43 @lexer::includes {
  44
  45 /** This suppresses warnings about the redefinition of token symbols between
  46   * different parsers. The redefinitions should be harmless as long as no
  47   * client: (a) #include's the lexer headers for two grammars AND (b) uses the
  48   * token symbol definitions.
  49   */
  50 #pragma GCC system_header
  51
  52 /* This improves performance by ~10 percent on big inputs.
  53  * This option is only valid if we know the input is ASCII (or some 8-bit encoding).
  54  * If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
  55  * Otherwise, we have to let the lexer detect the encoding at runtime.
  56  */
  57 #define ANTLR3_INLINE_INPUT_ASCII
  58
  59 #include "parser/antlr_tracing.h"
  60
  61 }/* @lexer::includes */
  62
  63 @lexer::postinclude {
  64
  65 #include "parser/tptp/tptp.h"
  66 #include "parser/antlr_input.h"
  67
  68 using namespace CVC4;
  69 using namespace CVC4::parser;
  70
  71 /* These need to be macros so they can refer to the PARSER macro, which will be defined
  72  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
  73 #undef PARSER_STATE
  74 #define PARSER_STATE ((Tptp*)LEXER->super)
  75 #undef SOLVER
  76 #define SOLVER PARSER_STATE->getSolver()
  77 #undef MK_TERM
  78 #define MK_TERM SOLVER->mkTerm
  79 #undef MK_TERM
  80 #define MK_TERM SOLVER->mkTerm
  81 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
  82
  83 }/* @lexer::postinclude */
  84
  85 @parser::includes {
  86
  87 #include <memory>
  88
  89 #include "smt/command.h"
  90 #include "parser/parse_op.h"
  91 #include "parser/parser.h"
  92 #include "parser/tptp/tptp.h"
  93 #include "parser/antlr_tracing.h"
  94
  95 }/* @parser::includes */
  96
  97 @parser::postinclude {
  98
  99 #include <algorithm>
 100 #include <iterator>
 101 #include <vector>
 102
 103 #include "api/cvc4cpp.h"
 104 #include "base/output.h"
 105 #include "parser/antlr_input.h"
 106 #include "parser/parser.h"
 107 #include "parser/tptp/tptp.h"
 108 #include "util/integer.h"
 109 #include "util/rational.h"
 110
 111 using namespace CVC4;
 112 using namespace CVC4::parser;
 113
 114 /* These need to be macros so they can refer to the PARSER macro, which will be defined
 115  * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */
 116 #undef PARSER_STATE
 117 #define PARSER_STATE ((Tptp*)PARSER->super)
 118 #undef SOLVER
 119 #define SOLVER PARSER_STATE->getSolver()
 120 #undef SYM_MAN
 121 #define SYM_MAN PARSER_STATE->getSymbolManager()
 122 #undef MK_TERM
 123 #define MK_TERM SOLVER->mkTerm
 124 #define UNSUPPORTED PARSER_STATE->unimplementedFeature
 125
 126 }/* parser::postinclude */
 127
 128 /**
 129  * Parses an expression.
 130  * @return the parsed expression, or the Null CVC4::api::Term if we've reached
 131  * the end of the input
 132  */
 133 parseExpr returns [CVC4::parser::tptp::myExpr expr]
 134   : cnfFormula[expr]
 135   | EOF
 136   ;
 137
 138 /**
 139  * Parses a command
 140  * @return the parsed command, or NULL if we've reached the end of the input
 141  */
 142 parseCommand returns [CVC4::Command* cmd = NULL]
 143 @declarations {
 144   CVC4::api::Term expr;
 145   Tptp::FormulaRole fr;
 146   std::string name, inclSymbol;
 147   ParseOp p;
 148 }
 149   : CNF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
 150   { PARSER_STATE->setCnf(true);
 151     PARSER_STATE->setFof(false);
 152     PARSER_STATE->pushScope(); }
 153     cnfFormula[expr]
 154   { PARSER_STATE->popScope();
 155     std::vector<api::Term> bvl = PARSER_STATE->getFreeVar();
 156     if(!bvl.empty()) {
 157       expr = MK_TERM(api::FORALL,MK_TERM(api::BOUND_VAR_LIST,bvl),expr);
 158     };
 159   }
 160     (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
 161     {
 162       CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr);
 163       if( !aexpr.isNull() ){
 164         // set the expression name (e.g. used with unsat core printing)
 165         SYM_MAN->setExpressionName(aexpr, name, true);
 166       }
 167       // make the command to assert the formula
 168       cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ true, true);
 169     }
 170   | FOF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK
 171     { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(true); }
 172     fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
 173     {
 174       CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
 175       if( !aexpr.isNull() ){
 176         // set the expression name (e.g. used with unsat core printing)
 177         SYM_MAN->setExpressionName(aexpr, name, true);
 178       }
 179       // make the command to assert the formula
 180       cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
 181     }
 182   | TFF_TOK LPAREN_TOK nameN[name] COMMA_TOK
 183     ( TYPE_TOK COMMA_TOK tffTypedAtom[cmd]
 184     | formulaRole[fr] COMMA_TOK
 185       { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); }
 186       tffFormula[expr] (COMMA_TOK anything*)?
 187       {
 188         CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr);
 189         if( !aexpr.isNull() ){
 190           // set the expression name (e.g. used with unsat core printing)
 191           SYM_MAN->setExpressionName(aexpr, name, true);
 192         }
 193         // make the command to assert the formula
 194         cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true);
 195       }
 196     ) RPAREN_TOK DOT_TOK
 197   | THF_TOK LPAREN_TOK nameN[name] COMMA_TOK
 198     // Supported THF formulas: either a logic formula or a typing atom (i.e. we
 199     // ignore subtyping and logic sequents). Also, only TH0
 200     ( TYPE_TOK COMMA_TOK thfAtomTyping[cmd]
 201     | formulaRole[fr] COMMA_TOK
 202       { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); }
 203       thfLogicFormula[p] (COMMA_TOK anything*)?
 204       {
 205         if (p.d_expr.isNull())
 206         {
 207           PARSER_STATE->parseError("Top level expression must be a formula");
 208         }
 209         expr = p.d_expr;
 210         CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr);
 211         if (!aexpr.isNull())
 212         {
 213           // set the expression name (e.g. used with unsat core printing)
 214           SYM_MAN->setExpressionName(aexpr, name, true);
 215         }
 216         // make the command to assert the formula
 217         cmd = PARSER_STATE->makeAssertCommand(
 218             fr, aexpr, /* cnf == */ false, true);
 219       }
 220     ) RPAREN_TOK DOT_TOK
 221   | INCLUDE_TOK LPAREN_TOK unquotedFileName[name]
 222     ( COMMA_TOK LBRACK_TOK nameN[inclSymbol]
 223       ( COMMA_TOK nameN[inclSymbol] )* RBRACK_TOK )?
 224     RPAREN_TOK DOT_TOK
 225     { /* TODO - implement symbol filtering for file inclusion.
 226        * the following removes duplicates and "all", just need to pass it
 227        * through to includeFile() and implement it there.
 228       std::sort(inclArgs.begin(), inclArgs.end());
 229       std::vector<std::string>::iterator it =
 230         std::unique(inclArgs.begin(), inclArgs.end());
 231       inclArgs.resize(std::distance(inclArgs.begin(), it));
 232       it = std::lower_bound(inclArgs.begin(), inclArgs.end(), std::string("all"));
 233       if(it != inclArgs.end() && *it == "all") {
 234         inclArgs.erase(it);
 235       }
 236       */
 237       PARSER_STATE->includeFile(name /* , inclArgs */ );
 238       // The command of the included file will be produced at the next parseCommand() call
 239       cmd = new EmptyCommand("include::" + name);
 240     }
 241   | EOF
 242     {
 243       CommandSequence* seq = new CommandSequence();
 244       // assert that all distinct constants are distinct
 245       CVC4::api::Term aexpr = PARSER_STATE->getAssertionDistinctConstants();
 246       if( !aexpr.isNull() )
 247       {
 248         seq->addCommand(new AssertCommand(aexpr, false));
 249       }
 250
 251       std::string filename = PARSER_STATE->getInput()->getInputStreamName();
 252       size_t i = filename.find_last_of('/');
 253       if(i != std::string::npos) {
 254         filename = filename.substr(i + 1);
 255       }
 256       if(filename.substr(filename.length() - 2) == ".p") {
 257         filename = filename.substr(0, filename.length() - 2);
 258       }
 259       seq->addCommand(new SetInfoCommand("filename", filename));
 260       if(PARSER_STATE->hasConjecture()) {
 261         seq->addCommand(new QueryCommand(SOLVER->mkFalse()));
 262       } else {
 263         seq->addCommand(new CheckSatCommand());
 264       }
 265       PARSER_STATE->preemptCommand(seq);
 266       cmd = NULL;
 267     }
 268   ;
 269
 270 /* Parse a formula Role */
 271 formulaRole[CVC4::parser::Tptp::FormulaRole& role]
 272   : LOWER_WORD
 273     {
 274       std::string r = AntlrInput::tokenText($LOWER_WORD);
 275       if      (r == "axiom")              role = Tptp::FR_AXIOM;
 276       else if (r == "hypothesis")         role = Tptp::FR_HYPOTHESIS;
 277       else if (r == "definition")         role = Tptp::FR_DEFINITION;
 278       else if (r == "assumption")         role = Tptp::FR_ASSUMPTION;
 279       else if (r == "lemma")              role = Tptp::FR_LEMMA;
 280       else if (r == "theorem")            role = Tptp::FR_THEOREM;
 281       else if (r == "negated_conjecture") role = Tptp::FR_NEGATED_CONJECTURE;
 282       else if (r == "conjecture")         role = Tptp::FR_CONJECTURE;
 283       else if (r == "unknown")            role = Tptp::FR_UNKNOWN;
 284       else if (r == "plain")              role = Tptp::FR_PLAIN;
 285       else if (r == "fi_domain")          role = Tptp::FR_FI_DOMAIN;
 286       else if (r == "fi_functor")         role = Tptp::FR_FI_FUNCTORS;
 287       else if (r == "fi_predicate")       role = Tptp::FR_FI_PREDICATES;
 288       else if (r == "type")               role = Tptp::FR_TYPE;
 289       else PARSER_STATE->parseError("Invalid formula role: " + r);
 290     }
 291   ;
 292
 293 /*******/
 294 /* CNF */
 295
 296 /* It can parse a little more than the cnf grammar: false and true can appear.
 297  * Normally only false can appear and only at top level. */
 298
 299 cnfFormula[CVC4::api::Term& expr]
 300   : LPAREN_TOK cnfDisjunction[expr] RPAREN_TOK
 301   | cnfDisjunction[expr]
 302 ;
 303
 304 cnfDisjunction[CVC4::api::Term& expr]
 305 @declarations {
 306   std::vector<api::Term> args;
 307 }
 308   : cnfLiteral[expr] { args.push_back(expr); }
 309     ( OR_TOK cnfLiteral[expr] { args.push_back(expr); } )*
 310     { if(args.size() > 1) {
 311         expr = MK_TERM(api::OR, args);
 312       } // else its already in the expr
 313     }
 314 ;
 315
 316 cnfLiteral[CVC4::api::Term& expr]
 317   : atomicFormula[expr]
 318   | NOT_TOK atomicFormula[expr] { expr = MK_TERM(api::NOT, expr); }
 319   ;
 320
 321 atomicFormula[CVC4::api::Term& expr]
 322 @declarations {
 323   CVC4::api::Term expr2;
 324   std::string name;
 325   std::vector<CVC4::api::Term> args;
 326   bool equal;
 327   ParseOp p;
 328 }
 329   : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
 330     ( equalOp[equal] term[expr2]
 331       { // equality/disequality between terms
 332         expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
 333                             : PARSER_STATE->applyParseOp(p, args);
 334         args.clear();
 335         args.push_back(expr);
 336         args.push_back(expr2);
 337         ParseOp p1(api::EQUAL);
 338         expr = PARSER_STATE->applyParseOp(p1, args);
 339         if (!equal)
 340         {
 341           expr = MK_TERM(api::NOT, expr);
 342         }
 343       }
 344     | { // predicate
 345         p.d_type = SOLVER->getBooleanSort();
 346         expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
 347                             : PARSER_STATE->applyParseOp(p, args);
 348       }
 349     )
 350   | definedFun[p]
 351     (
 352      LPAREN_TOK arguments[args] RPAREN_TOK
 353      equalOp[equal] term[expr2]
 354      {
 355        expr = PARSER_STATE->applyParseOp(p, args);
 356        args.clear();
 357        args.push_back(expr);
 358        args.push_back(expr2);
 359        ParseOp p1(api::EQUAL);
 360        expr = PARSER_STATE->applyParseOp(p1, args);
 361        if (!equal)
 362        {
 363          expr = MK_TERM(api::NOT, expr);
 364        }
 365      }
 366     )
 367   | (simpleTerm[expr] | letTerm[expr] | conditionalTerm[expr])
 368     (
 369       equalOp[equal] term[expr2]
 370       { // equality/disequality between terms
 371         args.push_back(expr);
 372         args.push_back(expr2);
 373         p.d_kind = api::EQUAL;
 374         expr = PARSER_STATE->applyParseOp(p, args);
 375         if (!equal)
 376         {
 377           expr = MK_TERM(api::NOT, expr);
 378         }
 379       }
 380     )?
 381   | definedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)
 382     {
 383       p.d_type = SOLVER->getBooleanSort();
 384       expr = PARSER_STATE->applyParseOp(p, args);
 385     }
 386   | definedProp[expr]
 387   ;
 388
 389 thfAtomicFormula[CVC4::ParseOp& p]
 390 @declarations {
 391   CVC4::api::Term expr2;
 392   std::string name;
 393   std::vector<CVC4::api::Term> args;
 394   bool equal;
 395 }
 396   : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
 397     {
 398       p.d_expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
 399                               : PARSER_STATE->applyParseOp(p, args);
 400     }
 401   | definedFun[p]
 402     (
 403       LPAREN_TOK arguments[args] RPAREN_TOK
 404       equalOp[equal] term[expr2]
 405       {
 406         p.d_expr = PARSER_STATE->applyParseOp(p, args);
 407         args.clear();
 408         args.push_back(p.d_expr);
 409         args.push_back(expr2);
 410         ParseOp p1(api::EQUAL);
 411         p.d_expr = PARSER_STATE->applyParseOp(p1, args);
 412         if (!equal)
 413         {
 414           p.d_expr = MK_TERM(api::NOT, p.d_expr);
 415         }
 416       }
 417     )?
 418   | thfSimpleTerm[p.d_expr]
 419   | letTerm[p.d_expr]
 420   | conditionalTerm[p.d_expr]
 421   | thfDefinedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)?
 422     {
 423       p.d_type = SOLVER->getBooleanSort();
 424       if (!args.empty())
 425       {
 426         p.d_expr = PARSER_STATE->applyParseOp(p, args);
 427       }
 428     }
 429   | definedProp[p.d_expr]
 430   ;
 431
 432 //%----Using <plain_term> removes a reduce/reduce ambiguity in lex/yacc.
 433 //%----Note: "defined" means a word starting with one $ and "system" means $$.
 434
 435 definedProp[CVC4::api::Term& expr]
 436   : TRUE_TOK { expr = SOLVER->mkTrue(); }
 437   | FALSE_TOK  { expr = SOLVER->mkFalse(); }
 438   ;
 439
 440 definedPred[CVC4::ParseOp& p]
 441   : '$less'
 442     {
 443       p.d_kind = api::LT;
 444     }
 445   | '$lesseq'
 446     {
 447       p.d_kind = api::LEQ;
 448     }
 449   | '$greater'
 450     {
 451       p.d_kind = api::GT;
 452     }
 453   | '$greatereq'
 454     {
 455       p.d_kind = api::GEQ;
 456     }
 457   | '$is_rat'
 458     // a real n is a rational if there exists q,r integers such that
 459     //   to_real(q) = n*to_real(r),
 460     // where r is non-zero.
 461     {
 462       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
 463       api::Term q = SOLVER->mkVar(SOLVER->getIntegerSort(), "Q");
 464       api::Term qr = MK_TERM(api::TO_REAL, q);
 465       api::Term r = SOLVER->mkVar(SOLVER->getIntegerSort(), "R");
 466       api::Term rr = MK_TERM(api::TO_REAL, r);
 467       api::Term body =
 468           MK_TERM(api::AND,
 469                   MK_TERM(api::NOT,
 470                           MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
 471                   MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
 472       api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
 473       body = MK_TERM(api::EXISTS, bvl, body);
 474       api::Term lbvl = MK_TERM(api::BOUND_VAR_LIST, n);
 475       p.d_kind = api::LAMBDA;
 476       p.d_expr = MK_TERM(api::LAMBDA, lbvl, body);
 477     }
 478   | '$is_int'
 479     {
 480       p.d_kind = api::IS_INTEGER;
 481     }
 482   | '$distinct'
 483     {
 484       p.d_kind = api::DISTINCT;
 485     }
 486   | AND_TOK
 487     {
 488       p.d_kind = api::AND;
 489     }
 490   | IMPLIES_TOK
 491     {
 492       p.d_kind = api::IMPLIES;
 493     }
 494   | OR_TOK
 495     {
 496       p.d_kind = api::OR;
 497     }
 498   ;
 499
 500 thfDefinedPred[CVC4::ParseOp& p]
 501   : '$less'
 502      {
 503        p.d_kind = api::LT;
 504      }
 505   | '$lesseq'
 506     {
 507       p.d_kind = api::LEQ;
 508     }
 509   | '$greater'
 510     {
 511       p.d_kind = api::GT;
 512     }
 513   | '$greatereq'
 514     {
 515       p.d_kind = api::GEQ;
 516     }
 517   | '$is_rat'
 518     // a real n is a rational if there exists q,r integers such that
 519     //   to_real(q) = n*to_real(r),
 520     // where r is non-zero.
 521     {
 522       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
 523       api::Term q = SOLVER->mkVar(SOLVER->getIntegerSort(), "Q");
 524       api::Term qr = MK_TERM(api::TO_REAL, q);
 525       api::Term r = SOLVER->mkVar(SOLVER->getIntegerSort(), "R");
 526       api::Term rr = MK_TERM(api::TO_REAL, r);
 527       api::Term body = MK_TERM(
 528           api::AND,
 529           MK_TERM(api::NOT,
 530                   MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
 531           MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
 532       api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
 533       body = MK_TERM(api::EXISTS, bvl, body);
 534       api::Term lbvl = MK_TERM(api::BOUND_VAR_LIST, n);
 535       p.d_kind = api::LAMBDA;
 536       p.d_expr = MK_TERM(api::LAMBDA, lbvl, body);
 537     }
 538   | '$is_int'
 539     {
 540       p.d_kind = api::IS_INTEGER;
 541     }
 542   | '$distinct'
 543     {
 544       p.d_kind = api::DISTINCT;
 545     }
 546   | LPAREN_TOK
 547     (
 548       AND_TOK
 549       {
 550         p.d_kind = api::AND;
 551       }
 552     | OR_TOK
 553       {
 554         p.d_kind = api::OR;
 555       }
 556     | IMPLIES_TOK
 557       {
 558         p.d_kind = api::IMPLIES;
 559       }
 560     )
 561     RPAREN_TOK
 562   ;
 563
 564 definedFun[CVC4::ParseOp& p]
 565 @declarations {
 566   bool remainder = false;
 567 }
 568   : '$uminus'
 569     {
 570       p.d_kind = api::UMINUS;
 571     }
 572   | '$sum'
 573     {
 574       p.d_kind = api::PLUS;
 575     }
 576   | '$difference'
 577     {
 578       p.d_kind = api::MINUS;
 579     }
 580   | '$product'
 581     {
 582       p.d_kind = api::MULT;
 583     }
 584   | '$quotient'
 585     {
 586       p.d_kind = api::DIVISION;
 587     }
 588   | ( '$quotient_e' { remainder = false; }
 589     | '$remainder_e' { remainder = true; }
 590     )
 591     {
 592       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
 593       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
 594       api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
 595       api::Term expr = MK_TERM(api::DIVISION, n, d);
 596       expr = MK_TERM(api::ITE,
 597                      MK_TERM(api::GEQ, d, SOLVER->mkReal(0)),
 598                      MK_TERM(api::TO_INTEGER, expr),
 599                      MK_TERM(api::UMINUS,
 600                              MK_TERM(api::TO_INTEGER,
 601                                      MK_TERM(api::UMINUS, expr))));
 602       if (remainder)
 603       {
 604         expr = MK_TERM(
 605             api::TO_INTEGER,
 606             MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d)));
 607       }
 608       p.d_kind = api::LAMBDA;
 609       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
 610     }
 611   | ( '$quotient_t' { remainder = false; }
 612     | '$remainder_t' { remainder = true; }
 613     )
 614     {
 615       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
 616       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
 617       api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
 618       api::Term expr = MK_TERM(api::DIVISION, n, d);
 619       expr = MK_TERM(api::ITE,
 620                      MK_TERM(api::GEQ, expr, SOLVER->mkReal(0)),
 621                      MK_TERM(api::TO_INTEGER, expr),
 622                      MK_TERM(api::UMINUS,
 623                              MK_TERM(api::TO_INTEGER,
 624                                      MK_TERM(api::UMINUS, expr))));
 625       if (remainder)
 626       {
 627         expr = MK_TERM(
 628             api::TO_INTEGER,
 629             MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d)));
 630       }
 631       p.d_kind = api::LAMBDA;
 632       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
 633     }
 634   | ( '$quotient_f' { remainder = false; }
 635     | '$remainder_f' { remainder = true; }
 636     )
 637     {
 638       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
 639       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
 640       api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
 641       api::Term expr = MK_TERM(api::DIVISION, n, d);
 642       expr = MK_TERM(api::TO_INTEGER, expr);
 643       if (remainder)
 644       {
 645         expr = MK_TERM(api::TO_INTEGER,
 646                        MK_TERM(api::MINUS, n, MK_TERM(api::MULT, expr, d)));
 647       }
 648       p.d_kind = api::LAMBDA;
 649       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
 650     }
 651   | '$floor'
 652     {
 653       p.d_kind = api::TO_INTEGER;
 654     }
 655   | '$ceiling'
 656     {
 657       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
 658       api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
 659       api::Term expr = MK_TERM(api::UMINUS,
 660                           MK_TERM(api::TO_INTEGER, MK_TERM(api::UMINUS, n)));
 661       p.d_kind = api::LAMBDA;
 662       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
 663     }
 664   | '$truncate'
 665     {
 666       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
 667       api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
 668       api::Term expr =
 669           MK_TERM(api::ITE,
 670                   MK_TERM(api::GEQ, n, SOLVER->mkReal(0)),
 671                   MK_TERM(api::TO_INTEGER, n),
 672                   MK_TERM(api::UMINUS,
 673                           MK_TERM(api::TO_INTEGER, MK_TERM(api::UMINUS, n))));
 674       p.d_kind = api::LAMBDA;
 675       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
 676     }
 677   | '$round'
 678     {
 679       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
 680       api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
 681       api::Term decPart = MK_TERM(api::MINUS, n, MK_TERM(api::TO_INTEGER, n));
 682       api::Term expr = MK_TERM(
 683           api::ITE,
 684           MK_TERM(api::LT, decPart, SOLVER->mkReal(1, 2)),
 685           // if decPart < 0.5, round down
 686           MK_TERM(api::TO_INTEGER, n),
 687           MK_TERM(api::ITE,
 688                   MK_TERM(api::GT, decPart, SOLVER->mkReal(1, 2)),
 689                   // if decPart > 0.5, round up
 690                   MK_TERM(api::TO_INTEGER,
 691                           MK_TERM(api::PLUS, n, SOLVER->mkReal(1))),
 692                   // if decPart == 0.5, round to nearest even integer:
 693                   // result is: to_int(n/2 + .5) * 2
 694                   MK_TERM(api::MULT,
 695                           MK_TERM(api::TO_INTEGER,
 696                                   MK_TERM(api::PLUS,
 697                                           MK_TERM(api::DIVISION,
 698                                                   n,
 699                                                   SOLVER->mkReal(2)),
 700                                           SOLVER->mkReal(1, 2))),
 701                           SOLVER->mkInteger(2))));
 702       p.d_kind = api::LAMBDA;
 703       p.d_expr = MK_TERM(api::LAMBDA, formals, expr);
 704       }
 705   | '$to_int'
 706     {
 707       p.d_kind = api::TO_INTEGER;
 708     }
 709   | '$to_rat'
 710     {
 711       p.d_kind = api::TO_REAL;
 712     }
 713   | '$to_real'
 714     {
 715       p.d_kind = api::TO_REAL;
 716     }
 717   ;
 718
 719 //%----Pure CNF should not use $true or $false in problems, and use $false only
 720 //%----at the roots of a refutation.
 721
 722 equalOp[bool& equal]
 723   : EQUAL_TOK    { equal = true; }
 724   | DISEQUAL_TOK { equal = false; }
 725   ;
 726
 727 term[CVC4::api::Term& expr]
 728   : functionTerm[expr]
 729   | conditionalTerm[expr]
 730   | simpleTerm[expr]
 731   | letTerm[expr]
 732   ;
 733
 734 letTerm[CVC4::api::Term& expr]
 735 @declarations {
 736   CVC4::api::Term lhs, rhs;
 737 }
 738   : '$let_ft' LPAREN_TOK { PARSER_STATE->pushScope(); }
 739     tffLetFormulaDefn[lhs, rhs] COMMA_TOK
 740     term[expr]
 741     { PARSER_STATE->popScope();
 742       expr = expr.substitute(lhs, rhs);
 743     }
 744     RPAREN_TOK
 745   | '$let_tt' LPAREN_TOK { PARSER_STATE->pushScope(); }
 746     tffLetTermDefn[lhs, rhs] COMMA_TOK
 747     term[expr]
 748     { PARSER_STATE->popScope();
 749       expr = expr.substitute(lhs, rhs);
 750     }
 751     RPAREN_TOK
 752   ;
 753
 754 /* Not an application */
 755 simpleTerm[CVC4::api::Term& expr]
 756   : variable[expr]
 757   | NUMBER { expr = PARSER_STATE->d_tmp_expr; }
 758   | DISTINCT_OBJECT { expr = PARSER_STATE->convertStrToUnsorted(AntlrInput::tokenText($DISTINCT_OBJECT)); }
 759   ;
 760
 761 /* Not an application */
 762 thfSimpleTerm[CVC4::api::Term& expr]
 763   : NUMBER { expr = PARSER_STATE->d_tmp_expr; }
 764   | DISTINCT_OBJECT
 765     {
 766       expr = PARSER_STATE->convertStrToUnsorted(
 767           AntlrInput::tokenText($DISTINCT_OBJECT));
 768     }
 769   ;
 770
 771 functionTerm[CVC4::api::Term& expr]
 772 @declarations {
 773   std::vector<CVC4::api::Term> args;
 774   ParseOp p;
 775 }
 776   : plainTerm[expr]
 777   | definedFun[p] LPAREN_TOK arguments[args] RPAREN_TOK
 778     {
 779       expr = PARSER_STATE->applyParseOp(p, args);
 780     }
 781   ;
 782
 783 conditionalTerm[CVC4::api::Term& expr]
 784 @declarations {
 785   CVC4::api::Term expr2, expr3;
 786 }
 787   : '$ite_t' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK term[expr2] COMMA_TOK term[expr3] RPAREN_TOK
 788     { expr = MK_TERM(api::ITE, expr, expr2, expr3); }
 789   ;
 790
 791 plainTerm[CVC4::api::Term& expr]
 792 @declarations {
 793   std::string name;
 794   std::vector<api::Term> args;
 795   ParseOp p;
 796 }
 797   : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
 798     {
 799       expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
 800                           : PARSER_STATE->applyParseOp(p, args);
 801     }
 802   ;
 803
 804 arguments[std::vector<CVC4::api::Term>& args]
 805 @declarations {
 806   CVC4::api::Term expr;
 807 }
 808   :
 809   term[expr] { args.push_back(expr); } ( COMMA_TOK term[expr] { args.push_back(expr); } )*
 810   ;
 811
 812 variable[CVC4::api::Term& expr]
 813   : UPPER_WORD
 814     {
 815       std::string name = AntlrInput::tokenText($UPPER_WORD);
 816       if(!PARSER_STATE->cnf() || PARSER_STATE->isDeclared(name)) {
 817         expr = PARSER_STATE->getVariable(name);
 818       } else {
 819         expr = PARSER_STATE->bindBoundVar(name, PARSER_STATE->d_unsorted);
 820         if(PARSER_STATE->cnf()) PARSER_STATE->addFreeVar(expr);
 821       }
 822     }
 823     ;
 824
 825 /*******/
 826 /* FOF */
 827 fofFormula[CVC4::api::Term& expr] : fofLogicFormula[expr] ;
 828
 829 fofLogicFormula[CVC4::api::Term& expr]
 830 @declarations {
 831   tptp::NonAssoc na;
 832   std::vector< CVC4::api::Term > args;
 833   CVC4::api::Term expr2;
 834 }
 835   : fofUnitaryFormula[expr]
 836     ( // Non-associative: <=> <~> ~& ~|
 837       ( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
 838         { switch(na) {
 839            case tptp::NA_IFF:
 840              expr = MK_TERM(api::EQUAL,expr,expr2);
 841              break;
 842            case tptp::NA_REVIFF:
 843              expr = MK_TERM(api::XOR,expr,expr2);
 844              break;
 845            case tptp::NA_IMPLIES:
 846              expr = MK_TERM(api::IMPLIES,expr,expr2);
 847              break;
 848            case tptp::NA_REVIMPLIES:
 849              expr = MK_TERM(api::IMPLIES,expr2,expr);
 850              break;
 851            case tptp::NA_REVOR:
 852              expr = MK_TERM(api::NOT,MK_TERM(api::OR,expr,expr2));
 853              break;
 854            case tptp::NA_REVAND:
 855              expr = MK_TERM(api::NOT,MK_TERM(api::AND,expr,expr2));
 856              break;
 857           }
 858         }
 859       )
 860     | // N-ary and &
 861       ( { args.push_back(expr); }
 862         ( AND_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
 863         { expr = MK_TERM(api::AND, args); }
 864       )
 865     | // N-ary or |
 866       ( { args.push_back(expr); }
 867         ( OR_TOK fofUnitaryFormula[expr] { args.push_back(expr); } )+
 868         { expr = MK_TERM(api::OR, args); }
 869       )
 870     )?
 871   ;
 872
 873 fofUnitaryFormula[CVC4::api::Term& expr]
 874 @declarations {
 875   api::Kind kind;
 876   std::vector< CVC4::api::Term > bv;
 877 }
 878   : atomicFormula[expr]
 879   | LPAREN_TOK fofLogicFormula[expr] RPAREN_TOK
 880   | NOT_TOK fofUnitaryFormula[expr] { expr = MK_TERM(api::NOT,expr); }
 881   | // Quantified
 882     folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
 883     ( bindvariable[expr] { bv.push_back(expr); }
 884       ( COMMA_TOK bindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
 885     COLON_TOK fofUnitaryFormula[expr]
 886     { PARSER_STATE->popScope();
 887       expr = MK_TERM(kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
 888     }
 889   ;
 890
 891 bindvariable[CVC4::api::Term& expr]
 892   : UPPER_WORD
 893     { std::string name = AntlrInput::tokenText($UPPER_WORD);
 894       expr = PARSER_STATE->bindBoundVar(name, PARSER_STATE->d_unsorted);
 895     }
 896   ;
 897
 898 fofBinaryNonAssoc[CVC4::parser::tptp::NonAssoc& na]
 899   : IFF_TOK      { na = tptp::NA_IFF; }
 900   | REVIFF_TOK   { na = tptp::NA_REVIFF; }
 901   | REVOR_TOK    { na = tptp::NA_REVOR; }
 902   | REVAND_TOK   { na = tptp::NA_REVAND; }
 903   | IMPLIES_TOK    { na = tptp::NA_IMPLIES; }
 904   | REVIMPLIES_TOK { na = tptp::NA_REVIMPLIES; }
 905   ;
 906
 907 folQuantifier[CVC4::api::Kind& kind]
 908   : FORALL_TOK { kind = api::FORALL; }
 909   | EXISTS_TOK { kind = api::EXISTS; }
 910   ;
 911
 912 /*******/
 913 /* THF */
 914
 915 thfQuantifier[CVC4::api::Kind& kind]
 916   : FORALL_TOK { kind = api::FORALL; }
 917   | EXISTS_TOK { kind = api::EXISTS; }
 918   | LAMBDA_TOK { kind = api::LAMBDA; }
 919   | CHOICE_TOK
 920     {
 921       UNSUPPORTED("Choice operator");
 922     }
 923   | DEF_DESC_TOK
 924     {
 925       UNSUPPORTED("Description quantifier");
 926     }
 927   | (TH1_UN_A | TH1_UN_E)
 928     {
 929       UNSUPPORTED("TH1 operator");
 930     }
 931   ;
 932
 933 thfAtomTyping[CVC4::Command*& cmd]
 934 // for now only supports mapping types (i.e. no applied types)
 935 @declarations {
 936   CVC4::api::Term expr;
 937   CVC4::api::Sort type;
 938   std::string name;
 939 }
 940   : LPAREN_TOK thfAtomTyping[cmd] RPAREN_TOK
 941   | nameN[name] COLON_TOK
 942     ( '$tType'
 943       {
 944         if (PARSER_STATE->isDeclared(name, SYM_SORT))
 945         {
 946           // duplicate declaration is fine, they're compatible
 947           cmd = new EmptyCommand("compatible redeclaration of sort " + name);
 948         }
 949         else if (PARSER_STATE->isDeclared(name, SYM_VARIABLE))
 950         {
 951           // error: cannot be both sort and constant
 952           PARSER_STATE->parseError(
 953               "Symbol `" + name
 954               + "' previously declared as a constant; cannot also be a sort");
 955         }
 956         else
 957         {
 958           // as yet, it's undeclared
 959           api::Sort atype = PARSER_STATE->mkSort(name);
 960           cmd = new DeclareSortCommand(name, 0, atype);
 961         }
 962       }
 963     | parseThfType[type]
 964       {
 965         if (PARSER_STATE->isDeclared(name, SYM_SORT))
 966         {
 967           // error: cannot be both sort and constant
 968           PARSER_STATE->parseError("Symbol `" + name
 969                                    + "' previously declared as a sort");
 970           cmd = new EmptyCommand("compatible redeclaration of sort " + name);
 971         }
 972         else if (PARSER_STATE->isDeclared(name, SYM_VARIABLE))
 973         {
 974           if (type == PARSER_STATE->getVariable(name).getSort())
 975           {
 976             // duplicate declaration is fine, they're compatible
 977             cmd = new EmptyCommand("compatible redeclaration of constant "
 978                                    + name);
 979           }
 980           else
 981           {
 982             // error: sorts incompatible
 983             PARSER_STATE->parseError(
 984                 "Symbol `" + name
 985                 + "' declared previously with a different sort");
 986           }
 987         }
 988         else
 989         {
 990           // as of yet, it's undeclared
 991           CVC4::api::Term freshExpr;
 992           if (type.isFunction())
 993           {
 994             freshExpr = PARSER_STATE->bindVar(name, type);
 995           }
 996           else
 997           {
 998             freshExpr = PARSER_STATE->bindVar(name, type);
 999           }
1000           cmd = new DeclareFunctionCommand(name, freshExpr, type);
1001         }
1002       }
1003     )
1004   ;
1005
1006 thfLogicFormula[CVC4::ParseOp& p]
1007 @declarations {
1008   tptp::NonAssoc na;
1009   std::vector<CVC4::api::Term> args;
1010   std::vector<ParseOp> p_args;
1011   CVC4::api::Term expr2;
1012   bool equal;
1013   ParseOp p1;
1014 }
1015   //prefix unary formula case
1016   // ~
1017   : thfUnitaryFormula[p]
1018     ( // Equality: =
1019       equalOp[equal]
1020       thfUnitaryFormula[p1]
1021       {
1022         if (p.d_expr.isNull() && !p1.d_expr.isNull())
1023         {
1024           // make p.d_expr with a lambda of the same type as p1.d_expr
1025           p.d_expr =
1026               PARSER_STATE->mkLambdaWrapper(p.d_kind, p1.d_expr.getSort());
1027         }
1028         else if (p1.d_expr.isNull() && !p.d_expr.isNull())
1029         {
1030           // make p1.d_expr with a lambda of the same type as p.d_expr
1031           p1.d_expr =
1032               PARSER_STATE->mkLambdaWrapper(p1.d_kind, p.d_expr.getSort());
1033         }
1034         else if (p.d_expr.isNull() && p1.d_expr.isNull())
1035         {
1036           // Without a reference type it's not possible in general to know what
1037           // the lambda wrapping should be, so we fail in these cases
1038           UNSUPPORTED("Equality between theory functions");
1039         }
1040         args.push_back(p.d_expr);
1041         args.push_back(p1.d_expr);
1042         p.d_expr = MK_TERM(api::EQUAL, args);
1043         if (!equal)
1044         {
1045           p.d_expr = MK_TERM(api::NOT, p.d_expr);
1046         }
1047       }
1048     | // Non-associative: <=> <~> ~& ~|
1049       fofBinaryNonAssoc[na] thfUnitaryFormula[p1]
1050       {
1051         if (p.d_expr.isNull() || p1.d_expr.isNull())
1052         {
1053           PARSER_STATE->parseError(
1054               "Non-associative operator must be applied to formulas");
1055         }
1056         switch (na)
1057         {
1058           case tptp::NA_IFF:
1059             p.d_expr = MK_TERM(api::EQUAL, p.d_expr, p1.d_expr);
1060             break;
1061           case tptp::NA_REVIFF:
1062             p.d_expr = MK_TERM(api::XOR, p.d_expr, p1.d_expr);
1063             break;
1064           case tptp::NA_IMPLIES:
1065             p.d_expr = MK_TERM(api::IMPLIES, p.d_expr, p1.d_expr);
1066             break;
1067           case tptp::NA_REVIMPLIES:
1068             p.d_expr = MK_TERM(api::IMPLIES, p1.d_expr, p.d_expr);
1069             break;
1070           case tptp::NA_REVOR:
1071             p.d_expr =
1072                 MK_TERM(api::NOT, MK_TERM(api::OR, p.d_expr, p1.d_expr));
1073             break;
1074           case tptp::NA_REVAND:
1075             p.d_expr =
1076                 MK_TERM(api::NOT, MK_TERM(api::AND, p.d_expr, p1.d_expr));
1077             break;
1078         }
1079       }
1080     | // N-ary and &
1081       (
1082         {
1083           if (p.d_expr.isNull())
1084           {
1085             PARSER_STATE->parseError("AND must be applied to a formula");
1086           }
1087           args.push_back(p.d_expr);
1088           p = ParseOp();
1089         }
1090         ( AND_TOK thfUnitaryFormula[p]
1091           {
1092             if (p.d_expr.isNull())
1093             {
1094               PARSER_STATE->parseError("AND must be applied to a formula");
1095             }
1096             args.push_back(p.d_expr);
1097             p = ParseOp();
1098           }
1099         )+
1100         {
1101           p.d_expr = MK_TERM(api::AND, args);
1102         }
1103       )
1104     | // N-ary or |
1105       (
1106         {
1107           if (p.d_expr.isNull())
1108           {
1109             PARSER_STATE->parseError("OR must be applied to a formula");
1110           }
1111           args.push_back(p.d_expr);
1112           p = ParseOp();
1113         }
1114         ( OR_TOK thfUnitaryFormula[p]
1115           {
1116             if (p.d_expr.isNull())
1117             {
1118               PARSER_STATE->parseError("OR must be applied to a formula");
1119             }
1120             args.push_back(p.d_expr);
1121             p = ParseOp();
1122           }
1123         )+
1124         {
1125           p.d_expr = MK_TERM(api::OR, args);
1126         }
1127       )
1128     | // N-ary @ |
1129       //
1130       // @ (denoting apply) is left-associative and lambda is right-associative.
1131       // ^ [X] : ^ [Y] : f @ g (where f is a <thf_apply_formula> and g is a
1132       // <thf_unitary_formula>) should be parsed as: (^ [X] : (^ [Y] : f)) @ g.
1133       // That is, g is not in the scope of either lambda.
1134       {
1135         p_args.push_back(p);
1136         p = ParseOp();
1137       }
1138       ( APP_TOK
1139         (
1140          thfUnitaryFormula[p]
1141          {
1142            p_args.push_back(p);
1143            p = ParseOp();
1144          }
1145          | LBRACK_TOK
1146            { UNSUPPORTED("Tuple terms"); }
1147            thfTupleForm[args]
1148            RBRACK_TOK
1149         )
1150       )+
1151       {
1152         if (p_args[0].d_expr.isNull())
1153         {
1154           for (unsigned i = 1, size = p_args.size(); i < size; ++i)
1155           {
1156             if (p_args[i].d_expr.isNull())
1157             {
1158               PARSER_STATE->parseError(
1159                   "Application chains with defined symbol heads and at least "
1160                   "one defined symbol as argument are unsupported.");
1161             }
1162             args.push_back(p_args[i].d_expr);
1163           }
1164           p.d_expr = PARSER_STATE->applyParseOp(p_args[0], args);
1165         }
1166         else
1167         {
1168           p.d_expr = p_args[0].d_expr;
1169           // check if any argument is a defined function, e.g. "~", and create a
1170           // lambda wrapper then, e.g. (\lambda x. ~ x)
1171           for (unsigned i = 1, size = p_args.size(); i < size; ++i)
1172           {
1173             if (!p_args[i].d_expr.isNull())
1174             {
1175               args.push_back(p_args[i].d_expr);
1176               continue;
1177             }
1178             // create a lambda wrapper, e.g. (\lambda x. ~ x).
1179             //
1180             // The type is determined by the first element of the application
1181             // chain, which must be a function of type t1...tn -> t, so the
1182             // lambda must have type ti
1183             args.push_back(PARSER_STATE->mkLambdaWrapper(
1184                 p_args[i].d_kind,
1185                 p.d_expr.getSort()
1186                     .getFunctionDomainSorts()[i - 1]));
1187           }
1188           for (unsigned i = 0, size = args.size(); i < size; ++i)
1189           {
1190             p.d_expr = MK_TERM(api::HO_APPLY, p.d_expr, args[i]);
1191           }
1192         }
1193       }
1194     )?
1195   ;
1196
1197 thfTupleForm[std::vector<CVC4::api::Term>& args]
1198 @declarations {
1199   ParseOp p;
1200 }
1201   : thfUnitaryFormula[p]
1202    {
1203      if (p.d_expr.isNull())
1204      {
1205        PARSER_STATE->parseError("TUPLE element must be a formula");
1206      }
1207      args.push_back(p.d_expr);
1208    }
1209    ( COMMA_TOK thfUnitaryFormula[p]
1210      {
1211        if (p.d_expr.isNull())
1212        {
1213          PARSER_STATE->parseError("TUPLE element must be a formula");
1214        }
1215        args.push_back(p.d_expr);
1216      }
1217    )+
1218 ;
1219
1220 thfUnitaryFormula[CVC4::ParseOp& p]
1221 @declarations {
1222   api::Kind kind;
1223   std::vector< CVC4::api::Term > bv;
1224   CVC4::api::Term expr;
1225   bool equal;
1226   ParseOp p1;
1227 }
1228   : variable[p.d_expr]
1229   | thfAtomicFormula[p]
1230   | LPAREN_TOK
1231     thfLogicFormula[p]
1232     RPAREN_TOK
1233   | NOT_TOK
1234     {
1235       p.d_kind = api::NOT;
1236     }
1237     (
1238      thfUnitaryFormula[p1]
1239      {
1240        if (p1.d_expr.isNull())
1241        {
1242          PARSER_STATE->parseError("NOT must be applied to a formula");
1243        }
1244        std::vector<api::Term> args{p1.d_expr};
1245        p.d_expr = PARSER_STATE->applyParseOp(p, args);
1246      }
1247     )?
1248   | // Quantified
1249     thfQuantifier[p.d_kind]
1250     LBRACK_TOK {PARSER_STATE->pushScope();}
1251     thfBindVariable[expr]
1252     {
1253       bv.push_back(expr);
1254     }
1255     ( COMMA_TOK thfBindVariable[expr]
1256       {
1257         bv.push_back(expr);
1258       }
1259     )*
1260     RBRACK_TOK COLON_TOK
1261     thfUnitaryFormula[p1]
1262     {
1263       if (p1.d_expr.isNull())
1264       {
1265         PARSER_STATE->parseError("In scope of binder there must be a formula.");
1266       }
1267       expr = p1.d_expr;
1268       PARSER_STATE->popScope();
1269       // handle lambda case, in which case return type must be flattened and the
1270       // auxiliary variables introduced in the proccess must be added no the
1271       // variable list
1272       //
1273       // see documentation of mkFlatFunctionType for how it's done
1274       //
1275       // flatten body via flattening its type
1276       std::vector<api::Sort> sorts;
1277       std::vector<api::Term> flattenVars;
1278       PARSER_STATE->mkFlatFunctionType(sorts, expr.getSort(), flattenVars);
1279       if (!flattenVars.empty())
1280       {
1281         // apply body of lambda to flatten vars
1282         expr = PARSER_STATE->mkHoApply(expr, flattenVars);
1283         // add variables to BOUND_VAR_LIST
1284         bv.insert(bv.end(), flattenVars.begin(), flattenVars.end());
1285       }
1286       p.d_expr = MK_TERM(p.d_kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
1287     }
1288   ;
1289
1290 /*******/
1291 /* TFF */
1292 tffFormula[CVC4::api::Term& expr] : tffLogicFormula[expr];
1293
1294 tffTypedAtom[CVC4::Command*& cmd]
1295 @declarations {
1296   CVC4::api::Term expr;
1297   CVC4::api::Sort type;
1298   std::string name;
1299 }
1300   : LPAREN_TOK tffTypedAtom[cmd] RPAREN_TOK
1301   | nameN[name] COLON_TOK
1302     ( '$tType'
1303       { if(PARSER_STATE->isDeclared(name, SYM_SORT)) {
1304           // duplicate declaration is fine, they're compatible
1305           cmd = new EmptyCommand("compatible redeclaration of sort " + name);
1306         } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
1307           // error: cannot be both sort and constant
1308           PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a constant; cannot also be a sort");
1309         } else {
1310           // as yet, it's undeclared
1311           api::Sort atype = PARSER_STATE->mkSort(name);
1312           cmd = new DeclareSortCommand(name, 0, atype);
1313         }
1314       }
1315     | parseType[type]
1316       { if(PARSER_STATE->isDeclared(name, SYM_SORT)) {
1317           // error: cannot be both sort and constant
1318           PARSER_STATE->parseError("Symbol `" + name + "' previously declared as a sort");
1319           cmd = new EmptyCommand("compatible redeclaration of sort " + name);
1320         } else if(PARSER_STATE->isDeclared(name, SYM_VARIABLE)) {
1321           if(type == PARSER_STATE->getVariable(name).getSort()) {
1322             // duplicate declaration is fine, they're compatible
1323             cmd = new EmptyCommand("compatible redeclaration of constant " + name);
1324           } else {
1325             // error: sorts incompatible
1326             PARSER_STATE->parseError("Symbol `" + name + "' declared previously with a different sort");
1327           }
1328         } else {
1329           // as yet, it's undeclared
1330           CVC4::api::Term aexpr = PARSER_STATE->bindVar(name, type);
1331           cmd = new DeclareFunctionCommand(name, aexpr, type);
1332         }
1333       }
1334     )
1335   ;
1336
1337 tffLogicFormula[CVC4::api::Term& expr]
1338 @declarations {
1339   tptp::NonAssoc na;
1340   std::vector< CVC4::api::Term > args;
1341   CVC4::api::Term expr2;
1342 }
1343   : tffUnitaryFormula[expr]
1344     ( // Non Assoc <=> <~> ~& ~|
1345       ( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
1346         { switch(na) {
1347            case tptp::NA_IFF:
1348              expr = MK_TERM(api::EQUAL,expr,expr2);
1349              break;
1350            case tptp::NA_REVIFF:
1351              expr = MK_TERM(api::XOR,expr,expr2);
1352              break;
1353            case tptp::NA_IMPLIES:
1354              expr = MK_TERM(api::IMPLIES,expr,expr2);
1355              break;
1356            case tptp::NA_REVIMPLIES:
1357              expr = MK_TERM(api::IMPLIES,expr2,expr);
1358              break;
1359            case tptp::NA_REVOR:
1360              expr = MK_TERM(api::NOT,MK_TERM(api::OR,expr,expr2));
1361              break;
1362            case tptp::NA_REVAND:
1363              expr = MK_TERM(api::NOT,MK_TERM(api::AND,expr,expr2));
1364              break;
1365           }
1366         }
1367       )
1368     | // And &
1369       ( { args.push_back(expr); }
1370         ( AND_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
1371         { expr = MK_TERM(api::AND,args); }
1372       )
1373     | // Or |
1374       ( { args.push_back(expr); }
1375         ( OR_TOK tffUnitaryFormula[expr] { args.push_back(expr); } )+
1376         { expr = MK_TERM(api::OR,args); }
1377       )
1378     )?
1379   ;
1380
1381 tffUnitaryFormula[CVC4::api::Term& expr]
1382 @declarations {
1383   api::Kind kind;
1384   std::vector< CVC4::api::Term > bv;
1385   CVC4::api::Term lhs, rhs;
1386 }
1387   : atomicFormula[expr]
1388   | LPAREN_TOK tffLogicFormula[expr] RPAREN_TOK
1389   | NOT_TOK tffUnitaryFormula[expr] { expr = MK_TERM(api::NOT,expr); }
1390   | // Quantified
1391     folQuantifier[kind] LBRACK_TOK {PARSER_STATE->pushScope();}
1392     ( tffbindvariable[expr] { bv.push_back(expr); }
1393       ( COMMA_TOK tffbindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
1394     COLON_TOK tffUnitaryFormula[expr]
1395     { PARSER_STATE->popScope();
1396       expr = MK_TERM(kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
1397     }
1398   | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK
1399     { expr = MK_TERM(api::ITE, expr, lhs, rhs); }
1400   | '$let_tf' LPAREN_TOK { PARSER_STATE->pushScope(); }
1401     tffLetTermDefn[lhs, rhs] COMMA_TOK
1402     tffFormula[expr]
1403     { PARSER_STATE->popScope();
1404       expr = expr.substitute(lhs, rhs);
1405     }
1406     RPAREN_TOK
1407   | '$let_ff' LPAREN_TOK { PARSER_STATE->pushScope(); }
1408     tffLetFormulaDefn[lhs, rhs] COMMA_TOK
1409     tffFormula[expr]
1410     { PARSER_STATE->popScope();
1411       expr = expr.substitute(lhs, rhs);
1412     }
1413     RPAREN_TOK
1414   ;
1415
1416 tffLetTermDefn[CVC4::api::Term& lhs, CVC4::api::Term& rhs]
1417 @declarations {
1418   std::vector<CVC4::api::Term> bvlist;
1419 }
1420   : (FORALL_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
1421     tffLetTermBinding[bvlist, lhs, rhs]
1422   ;
1423
1424 tffLetTermBinding[std::vector<CVC4::api::Term> & bvlist,
1425                   CVC4::api::Term& lhs,
1426                   CVC4::api::Term& rhs]
1427   : term[lhs] EQUAL_TOK term[rhs]
1428   {
1429     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
1430     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
1431     rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
1432     // since lhs is always APPLY_UF (otherwise we'd have had a parser error in
1433     // checkLetBinding) the function to be replaced is always the first
1434     // argument. Note that the way in which lchildren is built above is also
1435     // relying on this.
1436     lhs = lhs[0];
1437   }
1438   | LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
1439   ;
1440
1441 tffLetFormulaDefn[CVC4::api::Term& lhs, CVC4::api::Term& rhs]
1442 @declarations {
1443   std::vector<CVC4::api::Term> bvlist;
1444 }
1445   : (FORALL_TOK LBRACK_TOK tffVariableList[bvlist] RBRACK_TOK COLON_TOK)*
1446     tffLetFormulaBinding[bvlist, lhs, rhs]
1447   ;
1448
1449 tffLetFormulaBinding[std::vector<CVC4::api::Term> & bvlist,
1450                      CVC4::api::Term& lhs,
1451                      CVC4::api::Term& rhs]
1452
1453   : atomicFormula[lhs] IFF_TOK tffUnitaryFormula[rhs]
1454   {
1455     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
1456     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
1457     rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
1458     // since lhs is always APPLY_UF (otherwise we'd have had a parser error in
1459     // checkLetBinding) the function to be replaced is always the first
1460     // argument. Note that the way in which lchildren is built above is also
1461     // relying on this.
1462     lhs = lhs[0];
1463   }
1464   | LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
1465   ;
1466
1467 thfBindVariable[CVC4::api::Term& expr]
1468 @declarations {
1469   std::string name;
1470   CVC4::api::Sort type = PARSER_STATE->d_unsorted;
1471 }
1472   : UPPER_WORD
1473     { name = AntlrInput::tokenText($UPPER_WORD); }
1474     ( COLON_TOK parseThfType[type] )?
1475     {
1476       expr = PARSER_STATE->bindBoundVar(name, type);
1477     }
1478   ;
1479
1480
1481 tffbindvariable[CVC4::api::Term& expr]
1482 @declarations {
1483   CVC4::api::Sort type = PARSER_STATE->d_unsorted;
1484 }
1485   : UPPER_WORD
1486     ( COLON_TOK parseType[type] )?
1487     { std::string name = AntlrInput::tokenText($UPPER_WORD);
1488       expr = PARSER_STATE->bindBoundVar(name, type);
1489     }
1490   ;
1491
1492 // bvlist is accumulative; it can already contain elements
1493 // on the way in, which are left undisturbed
1494 tffVariableList[std::vector<CVC4::api::Term>& bvlist]
1495 @declarations {
1496   CVC4::api::Term e;
1497 }
1498   : tffbindvariable[e] { bvlist.push_back(e); }
1499     ( COMMA_TOK tffbindvariable[e] { bvlist.push_back(e); } )*
1500   ;
1501
1502 parseThfType[CVC4::api::Sort& type]
1503 // assumes only mapping types (arrows), no tuple type
1504 @declarations {
1505   std::vector<CVC4::api::Sort> sorts;
1506 }
1507   : thfType[type] { sorts.push_back(type); }
1508     (
1509      (ARROW_TOK | TIMES_TOK) thfType[type] { sorts.push_back(type); }
1510     )*
1511     {
1512       if (sorts.size() < 1)
1513       {
1514         type = sorts[0];
1515       }
1516       else
1517       {
1518         api::Sort range = sorts.back();
1519         sorts.pop_back();
1520         type = PARSER_STATE->mkFlatFunctionType(sorts, range);
1521       }
1522     }
1523   ;
1524
1525 thfType[CVC4::api::Sort& type]
1526 // assumes only mapping types (arrows), no tuple type
1527   : simpleType[type]
1528     | LPAREN_TOK parseThfType[type] RPAREN_TOK
1529     | LBRACK_TOK { UNSUPPORTED("Tuple types"); } parseThfType[type] RBRACK_TOK
1530   ;
1531
1532 parseType[CVC4::api::Sort & type]
1533 @declarations
1534 {
1535   std::vector<CVC4::api::Sort> v;
1536 }
1537   : simpleType[type]
1538   | ( simpleType[type] { v.push_back(type); }
1539     | LPAREN_TOK simpleType[type] { v.push_back(type); }
1540       ( TIMES_TOK simpleType[type] { v.push_back(type); } )+
1541       RPAREN_TOK
1542     )
1543     ARROW_TOK simpleType[type]
1544     { type = SOLVER->mkFunctionSort(v,type);
1545     }
1546   ;
1547
1548 // non-function types
1549 simpleType[CVC4::api::Sort& type]
1550 @declarations {
1551   std::string name;
1552 }
1553   : DEFINED_SYMBOL
1554     { std::string s = AntlrInput::tokenText($DEFINED_SYMBOL);
1555       if(s == "\$i") type = PARSER_STATE->d_unsorted;
1556       else if(s == "\$o") type = SOLVER->getBooleanSort();
1557       else if(s == "\$int") type = SOLVER->getIntegerSort();
1558       else if(s == "\$rat") type = SOLVER->getRealSort();
1559       else if(s == "\$real") type = SOLVER->getRealSort();
1560       else if(s == "\$tType") PARSER_STATE->parseError("Type of types `\$tType' cannot be used here");
1561       else PARSER_STATE->parseError("unknown defined type `" + s + "'");
1562     }
1563   | atomicWord[name]
1564     { type = PARSER_STATE->getSort(name); }
1565   ;
1566
1567 /***********************************************/
1568 /* Anything well parenthesis */
1569
1570 anything
1571   : LPAREN_TOK anything* RPAREN_TOK
1572   | LBRACK_TOK anything* RBRACK_TOK
1573   | COMMA_TOK
1574   | DOT_TOK
1575   | COLON_TOK
1576   | OR_TOK
1577   | NOT_TOK
1578   | FORALL_TOK
1579   | EXISTS_TOK
1580   | AND_TOK
1581   | IFF_TOK
1582   | IMPLIES_TOK
1583   | REVIMPLIES_TOK
1584   | REVIFF_TOK
1585   | REVOR_TOK
1586   | REVAND_TOK
1587   | TIMES_TOK
1588   | PLUS_TOK
1589   | MINUS_TOK
1590   | TRUE_TOK
1591   | FALSE_TOK
1592   | EQUAL_TOK
1593   | DISEQUAL_TOK
1594   | CNF_TOK
1595   | FOF_TOK
1596   | THF_TOK
1597   | TFF_TOK
1598   | TYPE_TOK
1599   | INCLUDE_TOK
1600   | DISTINCT_OBJECT
1601   | UPPER_WORD
1602   | LOWER_WORD
1603   | LOWER_WORD_SINGLE_QUOTED
1604   | SINGLE_QUOTED
1605   | NUMBER
1606   | DEFINED_SYMBOL
1607   ;
1608 /*********/
1609
1610 //punctuation
1611 COMMA_TOK  : ',';
1612 DOT_TOK    : '.';
1613 LPAREN_TOK : '(';
1614 RPAREN_TOK : ')';
1615 LBRACK_TOK : '[';
1616 RBRACK_TOK : ']';
1617 COLON_TOK  : ':';
1618
1619 // typing
1620 ARROW_TOK   : '>';
1621 SUBTYPE_TOK : '>>';
1622
1623 //operator
1624 OR_TOK         : '|';
1625 NOT_TOK        : '~';
1626 FORALL_TOK     : '!';
1627 EXISTS_TOK     : '?';
1628 LAMBDA_TOK     : '^';
1629 CHOICE_TOK     : '@+';
1630 DEF_DESC_TOK   : '@-';
1631 AND_TOK        : '&';
1632 IFF_TOK        : '<=>';
1633 IMPLIES_TOK    : '=>';
1634 REVIMPLIES_TOK : '<=';
1635 REVIFF_TOK     : '<~>';
1636 REVOR_TOK      : '~|';
1637 REVAND_TOK     : '~&';
1638 TIMES_TOK      : '*';
1639 PLUS_TOK       : '+';
1640 MINUS_TOK      : '-';
1641 APP_TOK        : '@';
1642
1643 TH1_UN_A       : '!!';
1644 TH1_UN_E       : '??';
1645
1646 //predicate
1647 TRUE_TOK     : '$true';
1648 FALSE_TOK    : '$false';
1649 EQUAL_TOK    : '=';
1650 DISEQUAL_TOK : '!=';
1651
1652 //KEYWORD
1653 CNF_TOK     : 'cnf';
1654 FOF_TOK     : 'fof';
1655 THF_TOK     : 'thf';
1656 TFF_TOK     : 'tff';
1657 TYPE_TOK    : 'type';
1658 INCLUDE_TOK : 'include';
1659
1660 //Other defined symbols, must be defined after all the other
1661 DEFINED_SYMBOL : '$' LOWER_WORD;
1662
1663 /*********/
1664 /* Token */
1665
1666 /*
1667  * Matches and skips whitespace in the input.
1668  */
1669
1670 WHITESPACE
1671   : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }
1672   ;
1673
1674
1675 /**
1676  * Matches a double or single quoted string literal. Escaping is supported, and
1677  * escape character '\' has to be escaped.
1678  */
1679 DISTINCT_OBJECT : '"' (DO_CHAR)* '"' ;
1680 fragment DO_CHAR : ' '..'!'| '#'..'[' | ']'..'~' | '\\"' | '\\\\';
1681
1682 //The order of this two rules is important
1683 LOWER_WORD_SINGLE_QUOTED : '\'' LOWER_WORD '\'' ;
1684 SINGLE_QUOTED : '\'' (SQ_CHAR)* '\'' ;
1685
1686 fragment SQ_CHAR : ' '..'&' | '('..'[' | ']'..'~' | '\\\'' | '\\\\';
1687
1688 /* Define upper (variable) and lower (everything else) word */
1689 fragment NUMERIC : '0'..'9';
1690 fragment LOWER_ALPHA : 'a'..'z';
1691 fragment UPPER_ALPHA : 'A'..'Z';
1692 fragment ALPHA_NUMERIC : LOWER_ALPHA | UPPER_ALPHA | NUMERIC | '_';
1693 UPPER_WORD : UPPER_ALPHA ALPHA_NUMERIC*;
1694 LOWER_WORD : LOWER_ALPHA ALPHA_NUMERIC*;
1695
1696 /* filename */
1697 unquotedFileName[std::string& name] /* Beware fileName identifier is used by the backend ... */
1698  : (s=LOWER_WORD_SINGLE_QUOTED | s=SINGLE_QUOTED)
1699     { name = AntlrInput::tokenText($s);
1700       name = name.substr(1, name.size() - 2 );
1701     };
1702
1703 /* axiom name */
1704 nameN[std::string& name]
1705  : atomicWord[name]
1706  | NUMBER { name = AntlrInput::tokenText($NUMBER); }
1707  ;
1708
1709 /* atomic word everything (fof, cnf, thf, tff, include must not be keyword at this position ) */
1710 atomicWord[std::string& name]
1711  : FOF_TOK     { name = "fof"; }
1712  | CNF_TOK     { name = "cnf"; }
1713  | THF_TOK     { name = "thf"; }
1714  | TFF_TOK     { name = "tff"; }
1715  | TYPE_TOK    { name = "type"; }
1716  | INCLUDE_TOK { name = "include"; }
1717  | LOWER_WORD  { name = AntlrInput::tokenText($LOWER_WORD); }
1718  | LOWER_WORD_SINGLE_QUOTED // the lower word single quoted are considered without quote
1719     { /* strip off the quotes */
1720       name = AntlrInput::tokenTextSubstr($LOWER_WORD_SINGLE_QUOTED, 1 ,
1721                                          ($LOWER_WORD_SINGLE_QUOTED->stop - $LOWER_WORD_SINGLE_QUOTED->start) - 1);
1722     }
1723  | SINGLE_QUOTED {name = AntlrInput::tokenText($SINGLE_QUOTED); }; //for the others the quote remains
1724
1725 /** I don't understand how is made the difference between rational and real in SyntaxBNF. So I put all in rational */
1726 /* Rational */
1727
1728 fragment DOT              : '.';
1729 fragment EXPONENT         : 'E' | 'e';
1730 fragment SLASH            : '/';
1731
1732 fragment DECIMAL : NUMERIC+;
1733
1734 /* Currently we put all in the rational type */
1735 fragment SIGN[bool& pos]
1736   : PLUS_TOK { pos = true; }
1737   | MINUS_TOK { pos = false; }
1738   ;
1739
1740 NUMBER
1741 @declarations {
1742   bool pos = true;
1743   bool posE = true;
1744 }
1745   : ( SIGN[pos]? num=DECIMAL
1746       { std::stringstream ss;
1747         ss << ( pos ? "" : "-" ) << AntlrInput::tokenText($num);
1748         std::string str = ss.str();
1749         if (str.find(".") == std::string::npos)
1750         {
1751           PARSER_STATE->d_tmp_expr = SOLVER->mkInteger(str);
1752         }
1753         else
1754         {
1755           PARSER_STATE->d_tmp_expr = SOLVER->mkReal(str);
1756         }
1757       }
1758     | SIGN[pos]? num=DECIMAL DOT den=DECIMAL (EXPONENT SIGN[posE]? e=DECIMAL)?
1759       {
1760         std::string snum = AntlrInput::tokenText($num);
1761         std::string sden = AntlrInput::tokenText($den);
1762         size_t exp = ($e == NULL ? 0 : AntlrInput::tokenToUnsigned($e));
1763         PARSER_STATE->d_tmp_expr = PARSER_STATE->mkDecimal(snum, sden, pos, exp, posE);
1764       }
1765     | SIGN[pos]? num=DECIMAL SLASH den=DECIMAL
1766       { std::stringstream ss;
1767         ss << AntlrInput::tokenText($num) << "/" << AntlrInput::tokenText($den);
1768         PARSER_STATE->d_tmp_expr = SOLVER->mkReal(ss.str());
1769       }
1770     )
1771     { if(PARSER_STATE->cnf() || PARSER_STATE->fof()) {
1772         // We're in an unsorted context, so put a conversion around it
1773         PARSER_STATE->d_tmp_expr = PARSER_STATE->convertRatToUnsorted( PARSER_STATE->d_tmp_expr );
1774       }
1775     }
1776   ;
1777
1778 /**
1779  * Matches the comments and ignores them
1780  */
1781 COMMENT
1782   : '%' (~('\n' | '\r'))*     { SKIP(); }     //comment line
1783   | '/*'  ( options {greedy=false;} : . )*  '*/' { SKIP(); } //comment block
1784   ;