#include <memory>
#include "smt/command.h"
+#include "parser/parse_op.h"
#include "parser/parser.h"
#include "parser/tptp/tptp.h"
#include "parser/antlr_tracing.h"
std::string name;
std::vector<CVC4::Expr> args;
bool equal;
+ ParseOp p;
}
- : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
+ : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
( 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);
+ expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
+ : PARSER_STATE->applyParseOp(p, args);
+ args.clear();
+ args.push_back(expr);
+ args.push_back(expr2);
+ ParseOp p1(kind::EQUAL);
+ expr = PARSER_STATE->applyParseOp(p1, args);
+ if (!equal)
+ {
+ expr = MK_EXPR(kind::NOT, expr);
+ }
}
| { // predicate
- PARSER_STATE->makeApplication(expr, name, args, false);
+ p.d_type = EXPR_MANAGER->booleanType();
+ expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
+ : PARSER_STATE->applyParseOp(p, args);
}
)
- | definedFun[expr]
+ | definedFun[p]
(
LPAREN_TOK arguments[args] RPAREN_TOK
equalOp[equal] term[expr2]
{
- expr = EXPR_MANAGER->mkExpr(expr, args);
- expr = MK_EXPR(kind::EQUAL, expr, expr2);
+ expr = PARSER_STATE->applyParseOp(p, args);
+ args.clear();
+ args.push_back(expr);
+ args.push_back(expr2);
+ ParseOp p1(kind::EQUAL);
+ expr = PARSER_STATE->applyParseOp(p1, args);
if (!equal)
{
expr = MK_EXPR(kind::NOT, expr);
(
equalOp[equal] term[expr2]
{ // equality/disequality between terms
- expr = MK_EXPR(kind::EQUAL, expr, expr2);
+ args.push_back(expr);
+ args.push_back(expr2);
+ p.d_kind = kind::EQUAL;
+ expr = PARSER_STATE->applyParseOp(p, args);
if (!equal)
{
expr = MK_EXPR(kind::NOT, expr);
}
}
)?
- | definedPred[expr] (LPAREN_TOK arguments[args] RPAREN_TOK)?
+ | definedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)?
{
- if (!args.empty())
- {
- expr = EXPR_MANAGER->mkExpr(expr, args);
- }
+ p.d_type = EXPR_MANAGER->booleanType();
+ expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
+ : PARSER_STATE->applyParseOp(p, args);
}
| definedProp[expr]
;
std::string name;
std::vector<CVC4::Expr> args;
bool equal;
+ ParseOp p;
}
- : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
+ : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
{
- PARSER_STATE->makeApplication(expr, name, args, true);
+ expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
+ : PARSER_STATE->applyParseOp(p, args);
}
- | definedFun[expr]
+ | definedFun[p]
(
LPAREN_TOK arguments[args] RPAREN_TOK
equalOp[equal] term[expr2]
{
- expr = EXPR_MANAGER->mkExpr(expr, args);
- expr = MK_EXPR(kind::EQUAL, expr, expr2);
+ expr = PARSER_STATE->applyParseOp(p, args);
+ args.clear();
+ args.push_back(expr);
+ args.push_back(expr2);
+ ParseOp p1(kind::EQUAL);
+ expr = PARSER_STATE->applyParseOp(p1, args);
if (!equal)
{
expr = MK_EXPR(kind::NOT, expr);
| thfSimpleTerm[expr]
| letTerm[expr]
| conditionalTerm[expr]
- | thfDefinedPred[expr] (LPAREN_TOK arguments[args] RPAREN_TOK)?
+ | thfDefinedPred[p] (LPAREN_TOK arguments[args] RPAREN_TOK)?
{
- if (!args.empty())
- {
- expr = EXPR_MANAGER->mkExpr(expr, args);
- }
+ p.d_type = EXPR_MANAGER->booleanType();
+ expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
+ : PARSER_STATE->applyParseOp(p, args);
}
| definedProp[expr]
;
| 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); }
+definedPred[CVC4::ParseOp& p]
+ : '$less'
+ {
+ p.d_kind = kind::LT;
+ }
+ | '$lesseq'
+ {
+ p.d_kind = kind::LEQ;
+ }
+ | '$greater'
+ {
+ p.d_kind = kind::GT;
+ }
+ | '$greatereq'
+ {
+ p.d_kind = kind::GEQ;
+ }
| '$is_rat'
// a real n is a rational if there exists q,r integers such that
// to_real(q) = n*to_real(r),
// where r is non-zero.
{ Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType());
- Expr qr = MK_EXPR(CVC4::kind::TO_REAL, q);
+ Expr qr = MK_EXPR(kind::TO_REAL, q);
Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType());
- Expr rr = MK_EXPR(CVC4::kind::TO_REAL, r);
+ Expr rr = MK_EXPR(kind::TO_REAL, r);
Expr body =
- MK_EXPR(CVC4::kind::AND,
- MK_EXPR(CVC4::kind::NOT,
- MK_EXPR(CVC4::kind::EQUAL, r, MK_CONST(Rational(0)))),
- MK_EXPR(CVC4::kind::EQUAL, qr, MK_EXPR(CVC4::kind::MULT, n, rr)));
- Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r);
- body = MK_EXPR(CVC4::kind::EXISTS, bvl, body);
- Expr lbvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
- expr = MK_EXPR(CVC4::kind::LAMBDA, lbvl, body);
- }
- | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); }
- | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); }
- | AND_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::AND); }
- | IMPLIES_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IMPLIES); }
- | OR_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::OR); }
+ MK_EXPR(kind::AND,
+ MK_EXPR(kind::NOT,
+ MK_EXPR(kind::EQUAL, r, MK_CONST(Rational(0)))),
+ MK_EXPR(kind::EQUAL, qr, MK_EXPR(kind::MULT, n, rr)));
+ Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, q, r);
+ body = MK_EXPR(kind::EXISTS, bvl, body);
+ Expr lbvl = MK_EXPR(kind::BOUND_VAR_LIST, n);
+ p.d_kind = kind::LAMBDA;
+ p.d_expr = MK_EXPR(kind::LAMBDA, lbvl, body);
+ }
+ | '$is_int'
+ {
+ p.d_kind = kind::IS_INTEGER;
+ }
+ | '$distinct'
+ {
+ p.d_kind = kind::DISTINCT;
+ }
+ | AND_TOK
+ {
+ p.d_kind = kind::AND;
+ }
+ | IMPLIES_TOK
+ {
+ p.d_kind = kind::IMPLIES;
+ }
+ | OR_TOK
+ {
+ p.d_kind = kind::OR;
+ }
;
-thfDefinedPred[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); }
+thfDefinedPred[CVC4::ParseOp& p]
+ : '$less'
+ {
+ p.d_kind = kind::LT;
+ }
+ | '$lesseq'
+ {
+ p.d_kind = kind::LEQ;
+ }
+ | '$greater'
+ {
+ p.d_kind = kind::GT;
+ }
+ | '$greatereq'
+ {
+ p.d_kind = kind::GEQ;
+ }
| '$is_rat'
// a real n is a rational if there exists q,r integers such that
// to_real(q) = n*to_real(r),
{
Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
Expr q = EXPR_MANAGER->mkBoundVar("Q", EXPR_MANAGER->integerType());
- Expr qr = MK_EXPR(CVC4::kind::TO_REAL, q);
+ Expr qr = MK_EXPR(kind::TO_REAL, q);
Expr r = EXPR_MANAGER->mkBoundVar("R", EXPR_MANAGER->integerType());
- Expr rr = MK_EXPR(CVC4::kind::TO_REAL, r);
+ Expr rr = MK_EXPR(kind::TO_REAL, r);
Expr body = MK_EXPR(
- CVC4::kind::AND,
- MK_EXPR(CVC4::kind::NOT,
- MK_EXPR(CVC4::kind::EQUAL, r, MK_CONST(Rational(0)))),
- MK_EXPR(CVC4::kind::EQUAL, qr, MK_EXPR(CVC4::kind::MULT, n, rr)));
- Expr bvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, q, r);
- body = MK_EXPR(CVC4::kind::EXISTS, bvl, body);
- Expr lbvl = MK_EXPR(CVC4::kind::BOUND_VAR_LIST, n);
- expr = MK_EXPR(CVC4::kind::LAMBDA, lbvl, body);
- }
- | '$is_int' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IS_INTEGER); }
- | '$distinct' { expr = EXPR_MANAGER->operatorOf(CVC4::kind::DISTINCT); }
+ kind::AND,
+ MK_EXPR(kind::NOT,
+ MK_EXPR(kind::EQUAL, r, MK_CONST(Rational(0)))),
+ MK_EXPR(kind::EQUAL, qr, MK_EXPR(kind::MULT, n, rr)));
+ Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, q, r);
+ body = MK_EXPR(kind::EXISTS, bvl, body);
+ Expr lbvl = MK_EXPR(kind::BOUND_VAR_LIST, n);
+ p.d_kind = kind::LAMBDA;
+ p.d_expr = MK_EXPR(kind::LAMBDA, lbvl, body);
+ }
+ | '$is_int'
+ {
+ p.d_kind = kind::IS_INTEGER;
+ }
+ | '$distinct'
+ {
+ p.d_kind = kind::DISTINCT;
+ }
| LPAREN_TOK
(
- AND_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::AND); }
- | OR_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::OR); }
- | IMPLIES_TOK { expr = EXPR_MANAGER->operatorOf(CVC4::kind::IMPLIES); }
+ AND_TOK
+ {
+ p.d_kind = kind::AND;
+ }
+ | OR_TOK
+ {
+ p.d_kind = kind::OR;
+ }
+ | IMPLIES_TOK
+ {
+ p.d_kind = kind::IMPLIES;
+ }
)
RPAREN_TOK
;
-definedFun[CVC4::Expr& expr]
+definedFun[CVC4::ParseOp& p]
@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); }
+ : '$uminus'
+ {
+ p.d_kind = kind::UMINUS;
+ }
+ | '$sum'
+ {
+ p.d_kind = kind::PLUS;
+ }
+ | '$difference'
+ {
+ p.d_kind = kind::MINUS;
+ }
+ | '$product'
+ {
+ p.d_kind = kind::MULT;
+ }
+ | '$quotient'
+ {
+ p.d_kind = kind::DIVISION_TOTAL;
+ }
| ( '$quotient_e' { remainder = false; }
| '$remainder_e' { remainder = true; }
)
- { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ {
+ 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::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
+ Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d);
+ Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d);
+ expr = MK_EXPR(kind::ITE,
+ MK_EXPR(kind::GEQ, d, MK_CONST(Rational(0))),
+ MK_EXPR(kind::TO_INTEGER, expr),
+ MK_EXPR(kind::UMINUS,
+ MK_EXPR(kind::TO_INTEGER,
+ MK_EXPR(kind::UMINUS, expr))));
+ if (remainder)
+ {
+ expr = MK_EXPR(
+ kind::TO_INTEGER,
+ MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d)));
}
- expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ p.d_kind = kind::LAMBDA;
+ p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
}
| ( '$quotient_t' { remainder = false; }
| '$remainder_t' { remainder = true; }
)
- { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ {
+ 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::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
+ Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d);
+ Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d);
+ expr = MK_EXPR(kind::ITE,
+ MK_EXPR(kind::GEQ, expr, MK_CONST(Rational(0))),
+ MK_EXPR(kind::TO_INTEGER, expr),
+ MK_EXPR(kind::UMINUS,
+ MK_EXPR(kind::TO_INTEGER,
+ MK_EXPR(kind::UMINUS, expr))));
+ if (remainder)
+ {
+ expr = MK_EXPR(
+ kind::TO_INTEGER,
+ MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d)));
}
- expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ p.d_kind = kind::LAMBDA;
+ p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
}
| ( '$quotient_f' { remainder = false; }
| '$remainder_f' { remainder = true; }
)
- { Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ {
+ 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::TO_INTEGER, MK_EXPR(CVC4::kind::MINUS, n, MK_EXPR(CVC4::kind::MULT, expr, d)));
+ Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n, d);
+ Expr expr = MK_EXPR(kind::DIVISION_TOTAL, n, d);
+ expr = MK_EXPR(kind::TO_INTEGER, expr);
+ if (remainder)
+ {
+ expr = MK_EXPR(kind::TO_INTEGER,
+ MK_EXPR(kind::MINUS, n, MK_EXPR(kind::MULT, expr, d)));
}
- expr = MK_EXPR(CVC4::kind::LAMBDA, formals, expr);
+ p.d_kind = kind::LAMBDA;
+ p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
+ }
+ | '$floor'
+ {
+ p.d_kind = kind::TO_INTEGER;
}
- | '$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);
+ {
+ Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n);
+ Expr expr = MK_EXPR(kind::UMINUS,
+ MK_EXPR(kind::TO_INTEGER, MK_EXPR(kind::UMINUS, n)));
+ p.d_kind = kind::LAMBDA;
+ p.d_expr = MK_EXPR(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);
+ {
+ Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n);
+ Expr expr =
+ MK_EXPR(kind::ITE,
+ MK_EXPR(kind::GEQ, n, MK_CONST(Rational(0))),
+ MK_EXPR(kind::TO_INTEGER, n),
+ MK_EXPR(kind::UMINUS,
+ MK_EXPR(kind::TO_INTEGER, MK_EXPR(kind::UMINUS, n))));
+ p.d_kind = kind::LAMBDA;
+ p.d_expr = MK_EXPR(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); }
+ {
+ Expr n = EXPR_MANAGER->mkBoundVar("N", EXPR_MANAGER->realType());
+ Expr formals = MK_EXPR(kind::BOUND_VAR_LIST, n);
+ Expr decPart = MK_EXPR(kind::MINUS, n, MK_EXPR(kind::TO_INTEGER, n));
+ Expr expr = MK_EXPR(
+ kind::ITE,
+ MK_EXPR(kind::LT, decPart, MK_CONST(Rational(1, 2))),
+ // if decPart < 0.5, round down
+ MK_EXPR(kind::TO_INTEGER, n),
+ MK_EXPR(kind::ITE,
+ MK_EXPR(kind::GT, decPart, MK_CONST(Rational(1, 2))),
+ // if decPart > 0.5, round up
+ MK_EXPR(kind::TO_INTEGER,
+ MK_EXPR(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(kind::MULT,
+ MK_EXPR(kind::TO_INTEGER,
+ MK_EXPR(kind::PLUS,
+ MK_EXPR(kind::DIVISION_TOTAL,
+ n,
+ MK_CONST(Rational(2))),
+ MK_CONST(Rational(1, 2)))),
+ MK_CONST(Rational(2)))));
+ p.d_kind = kind::LAMBDA;
+ p.d_expr = MK_EXPR(kind::LAMBDA, formals, expr);
+ }
+ | '$to_int'
+ {
+ p.d_kind = kind::TO_INTEGER;
+ }
+ | '$to_rat'
+ {
+ p.d_kind = kind::TO_REAL;
+ }
+ | '$to_real'
+ {
+ p.d_kind = kind::TO_REAL;
+ }
;
//%----Pure CNF should not use $true or $false in problems, and use $false only
functionTerm[CVC4::Expr& expr]
@declarations {
std::vector<CVC4::Expr> args;
+ ParseOp p;
}
: plainTerm[expr]
- | definedFun[expr] LPAREN_TOK arguments[args] RPAREN_TOK
- { expr = EXPR_MANAGER->mkExpr(expr, args); }
-// | <system_term>
+ | definedFun[p] LPAREN_TOK arguments[args] RPAREN_TOK
+ {
+ expr = PARSER_STATE->applyParseOp(p, args);
+ }
;
conditionalTerm[CVC4::Expr& expr]
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); }
+ { expr = EXPR_MANAGER->mkExpr(kind::ITE, expr, expr2, expr3); }
;
plainTerm[CVC4::Expr& expr]
@declarations {
std::string name;
std::vector<Expr> args;
+ ParseOp p;
}
- : atomicWord[name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
+ : atomicWord[p.d_name] (LPAREN_TOK arguments[args] RPAREN_TOK)?
{
- PARSER_STATE->makeApplication(expr,name,args,true);
+ expr = args.empty() ? PARSER_STATE->parseOpToExpr(p)
+ : PARSER_STATE->applyParseOp(p, args);
}
;
}
else
{
- // as yet, it's undeclared
+ // as of yet, it's undeclared
CVC4::Expr freshExpr;
if (type.isFunction())
{
{
// TODO create whatever lambda
}
- expr = MK_EXPR(kind::EQUAL, expr, expr2);
+ args.push_back(expr);
+ args.push_back(expr2);
+ ParseOp p(kind::EQUAL);
+ expr = PARSER_STATE->applyParseOp(p, args);
if (!equal)
{
expr = MK_EXPR(kind::NOT, expr);
| // Non-associative: <=> <~> ~& ~|
fofBinaryNonAssoc[na] thfUnitaryFormula[expr2]
{
- switch(na) {
- case tptp::NA_IFF:
- expr = MK_EXPR(kind::EQUAL,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;
+ switch (na)
+ {
+ case tptp::NA_IFF: expr = MK_EXPR(kind::EQUAL, 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;
}
}
| // N-ary and &
thfLogicFormula[expr]
RPAREN_TOK
| NOT_TOK
- { expr = EXPR_MANAGER->operatorOf(CVC4::kind::NOT); }
+ {
+ ParseOp p(kind::NOT);
+ expr = PARSER_STATE->parseOpToExpr(p);
+ }
(thfUnitaryFormula[expr2] { expr = MK_EXPR(expr,expr2); })?
| // Quantified
thfQuantifier[kind]
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); }
+ { expr = EXPR_MANAGER->mkExpr(kind::ITE, expr, lhs, rhs); }
| '$let_tf' LPAREN_TOK { PARSER_STATE->pushScope(); }
tffLetTermDefn[lhs, rhs] COMMA_TOK
tffFormula[expr]
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);
+ rhs = MK_EXPR(kind::LAMBDA, MK_EXPR(kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
lhs = lhs.getOperator();
}
| LPAREN_TOK tffLetTermBinding[bvlist, lhs, rhs] RPAREN_TOK
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);
+ rhs = MK_EXPR(kind::LAMBDA, MK_EXPR(kind::BOUND_VAR_LIST, lhs.getChildren()), rhs);
lhs = lhs.getOperator();
}
| LPAREN_TOK tffLetFormulaBinding[bvlist, lhs, rhs] RPAREN_TOK
#include "api/cvc4cpp.h"
#include "expr/type.h"
+#include "options/options.h"
#include "parser/parser.h"
// ANTLR defines these, which is really bad!
}
}
+Expr Tptp::parseOpToExpr(ParseOp& p)
+{
+ Expr expr;
+ if (!p.d_expr.isNull())
+ {
+ return p.d_expr;
+ }
+ // if it has a kind, it's a builtin one
+ if (p.d_kind != kind::NULL_EXPR)
+ {
+ return getExprManager()->operatorOf(p.d_kind);
+ }
+ if (isDeclared(p.d_name))
+ { // already appeared
+ expr = getVariable(p.d_name);
+ }
+ else
+ {
+ Type t =
+ p.d_type == getExprManager()->booleanType() ? p.d_type : d_unsorted;
+ expr = mkVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
+ preemptCommand(new DeclareFunctionCommand(p.d_name, expr, t));
+ }
+ return expr;
+}
+
+Expr Tptp::applyParseOp(ParseOp& p, std::vector<Expr>& args)
+{
+ assert(!args.empty());
+ bool isBuiltinOperator = false;
+ // the builtin kind of the overall return expression
+ Kind kind = kind::NULL_EXPR;
+ // First phase: process the operator
+ ExprManager* em = getExprManager();
+ // If operator already defined, just build application
+ if (!p.d_expr.isNull())
+ {
+ return em->mkExpr(p.d_expr, args);
+ }
+ // Otherwise piece operator together
+ if (p.d_kind == kind::NULL_EXPR)
+ {
+ // A non-built-in function application, get the expression
+ Expr v;
+ if (isDeclared(p.d_name))
+ { // already appeared
+ v = getVariable(p.d_name);
+ }
+ else
+ {
+ std::vector<Type> sorts(args.size(), d_unsorted);
+ Type t = p.d_type == em->booleanType() ? p.d_type : d_unsorted;
+ t = getExprManager()->mkFunctionType(sorts, t);
+ v = mkVar(p.d_name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
+ preemptCommand(new DeclareFunctionCommand(p.d_name, v, 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(v.getType()).getArgTypes()[i] == d_unsorted)
+ {
+ args[i] = convertRatToUnsorted(args[i]);
+ }
+ }
+ assert(!v.isNull());
+ checkFunctionLike(v);
+ kind = getKindForFunction(v);
+ args.insert(args.begin(), v);
+ }
+ else
+ {
+ kind = p.d_kind;
+ isBuiltinOperator = true;
+ }
+ assert(kind != kind::NULL_EXPR);
+ // Second phase: apply the arguments to the parse op
+ if (isBuiltinOperator)
+ {
+ if (!em->getOptions().getUfHo()
+ && (kind == kind::EQUAL || kind == kind::DISTINCT))
+ {
+ // need --uf-ho if these operators are applied over function args
+ for (std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+ {
+ if ((*i).getType().isFunction())
+ {
+ parseError(
+ "Cannot apply equalty to functions unless --uf-ho is set.");
+ }
+ }
+ }
+ if (args.size() > 2)
+ {
+ if (kind == kind::INTS_DIVISION || kind == kind::XOR
+ || kind == kind::MINUS || kind == kind::DIVISION)
+ {
+ // Builtin operators that are not tokenized, are left associative,
+ // but not internally variadic must set this.
+ return em->mkLeftAssociative(kind, args);
+ }
+ if (kind == kind::IMPLIES)
+ {
+ /* right-associative, but CVC4 internally only supports 2 args */
+ return em->mkRightAssociative(kind, args);
+ }
+ if (kind == kind::EQUAL || kind == kind::LT || kind == kind::GT
+ || kind == kind::LEQ || kind == kind::GEQ)
+ {
+ /* "chainable", but CVC4 internally only supports 2 args */
+ return em->mkExpr(em->mkConst(Chain(kind)), args);
+ }
+ }
+
+ if (kind::isAssociative(kind) && args.size() > em->maxArity(kind))
+ {
+ /* Special treatment for associative operators with lots of children
+ */
+ return em->mkAssociative(kind, args);
+ }
+ if (!strictModeEnabled() && (kind == kind::AND || kind == kind::OR)
+ && args.size() == 1)
+ {
+ // Unary AND/OR can be replaced with the argument.
+ return args[0];
+ }
+ if (kind == kind::MINUS && args.size() == 1)
+ {
+ return em->mkExpr(kind::UMINUS, args[0]);
+ }
+ checkOperator(kind, args.size());
+ return em->mkExpr(kind, args);
+ }
+
+ // check if partially applied function, in this case we use HO_APPLY
+ if (args.size() >= 2)
+ {
+ Type argt = args[0].getType();
+ if (argt.isFunction())
+ {
+ unsigned arity = static_cast<FunctionType>(argt).getArity();
+ if (args.size() - 1 < arity)
+ {
+ if (!em->getOptions().getUfHo())
+ {
+ parseError("Cannot partially apply functions unless --uf-ho is set.");
+ }
+ Debug("parser") << "Partial application of " << args[0];
+ Debug("parser") << " : #argTypes = " << arity;
+ Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
+ // must curry the partial application
+ return em->mkLeftAssociative(kind::HO_APPLY, args);
+ }
+ }
+ }
+ return em->mkExpr(kind, args);
+}
+
void Tptp::forceLogic(const std::string& logic)
{
Parser::forceLogic(logic);
return e;
}
-void Tptp::makeApplication(Expr& expr, std::string& name,
- std::vector<Expr>& args, bool term) {
- if (args.empty()) { // Its a constant
- if (isDeclared(name)) { // already appeared
- expr = getVariable(name);
- } else {
- Type t = term ? d_unsorted : getExprManager()->booleanType();
- expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
- preemptCommand(new DeclareFunctionCommand(name, expr, t));
- }
- } else { // Its an application
- if (isDeclared(name)) { // already appeared
- expr = getVariable(name);
- } else {
- std::vector<Type> sorts(args.size(), d_unsorted);
- Type t = term ? d_unsorted : getExprManager()->booleanType();
- t = getExprManager()->mkFunctionType(sorts, t);
- expr = mkVar(name, t, ExprManager::VAR_FLAG_GLOBAL); // levelZero
- preemptCommand(new DeclareFunctionCommand(name, expr, t));
- }
- // args might be rationals, in which case we need to create
- // distinct constants of the "unsorted" sort to represent them
- for (size_t i = 0; i < args.size(); ++i) {
- if (args[i].getType().isReal() &&
- FunctionType(expr.getType()).getArgTypes()[i] == d_unsorted) {
- args[i] = convertRatToUnsorted(args[i]);
- }
- }
- expr = getExprManager()->mkExpr(kind::APPLY_UF, expr, args);
- }
-}
-
void Tptp::mkLambdaWrapper(Expr& expr, Type argType)
{
std::vector<Expr> lvars;
projects / cvc5.git / commitdiff