summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g12
-rw-r--r--src/parser/smt1/Smt1.g2
-rw-r--r--src/parser/smt1/smt1.cpp1
-rw-r--r--src/parser/smt2/Smt2.g31
-rw-r--r--src/parser/smt2/smt2.cpp7
-rw-r--r--src/parser/tptp/Tptp.g4
-rw-r--r--src/parser/tptp/tptp.cpp1
7 files changed, 19 insertions, 39 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 8d76a5122..3a8f3a794 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -356,7 +356,7 @@ Kind getOperatorKind(int type, bool& negate) {
switch(type) {
// booleanBinop
- case IFF_TOK: return kind::IFF;
+ case IFF_TOK: return kind::EQUAL;
case IMPLIES_TOK: return kind::IMPLIES;
case OR_TOK: return kind::OR;
case XOR_TOK: return kind::XOR;
@@ -440,16 +440,6 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex);
switch(k) {
- case kind::EQUAL: {
- if(lhs.getType().isBoolean()) {
- if(parser->strictModeEnabled()) {
- WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl;
- } else {
- k = kind::IFF;
- }
- }
- break;
- }
case kind::LEQ : if(lhs.getType().isSet()) { k = kind::SUBSET; } break;
case kind::MINUS : if(lhs.getType().isSet()) { k = kind::SETMINUS; } break;
case kind::BITVECTOR_AND: if(lhs.getType().isSet()) { k = kind::INTERSECTION; } break;
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 3e63fb3ab..28c54fc80 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -379,7 +379,7 @@ builtinOp[CVC4::Kind& kind]
| AND_TOK { $kind = CVC4::kind::AND; }
| OR_TOK { $kind = CVC4::kind::OR; }
| XOR_TOK { $kind = CVC4::kind::XOR; }
- | IFF_TOK { $kind = CVC4::kind::IFF; }
+ | IFF_TOK { $kind = CVC4::kind::EQUAL; }
| EQUAL_TOK { $kind = CVC4::kind::EQUAL; }
| DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
// Arithmetic
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index 015129f10..c8d1b774c 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -79,7 +79,6 @@ Smt1::Smt1(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn
// Boolean symbols are always defined
addOperator(kind::AND);
addOperator(kind::EQUAL);
- addOperator(kind::IFF);
addOperator(kind::IMPLIES);
addOperator(kind::ITE);
addOperator(kind::NOT);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ff34fd9a3..735c2b2f1 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1221,8 +1221,7 @@ smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd]
//set the attribute to denote this is a function definition
seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) );
//assert it
- Expr equality = MK_EXPR( func_app.getType().isBoolean() ?
- kind::IFF : kind::EQUAL, func_app, expr);
+ Expr equality = MK_EXPR( kind::EQUAL, func_app, expr);
Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs);
Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, equality, aexpr);
seq->addCommand( new AssertCommand(as, false) );
@@ -1290,8 +1289,7 @@ smt25Command[CVC4::PtrCloser<CVC4::Command>* cmd]
Expr as = EXPR_MANAGER->mkExpr(
kind::FORALL,
EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs),
- MK_EXPR( func_app.getType().isBoolean() ?
- kind::IFF : kind::EQUAL, func_app, expr ),
+ MK_EXPR( kind::EQUAL, func_app, expr ),
aexpr);
seq->addCommand( new AssertCommand(as, false) );
//set up the next scope
@@ -1720,13 +1718,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
{
- if( kind == CVC4::kind::EQUAL &&
- args.size() > 0 &&
- args[0].getType() == EXPR_MANAGER->booleanType() ) {
- /* Use IFF for boolean equalities. */
- kind = CVC4::kind::IFF;
- }
-
if( !PARSER_STATE->strictModeEnabled() &&
(kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
args.size() == 1) {
@@ -1752,7 +1743,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
for(size_t i = args.size() - 1; i > 0;) {
expr = MK_EXPR(kind, args[--i], expr);
}
- } else if( ( kind == CVC4::kind::IFF || kind == CVC4::kind::EQUAL ||
+ } else if( ( kind == CVC4::kind::EQUAL ||
kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
args.size() > 2 ) {
@@ -1993,7 +1984,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
Expr guard;
Expr body;
if(expr[1].getKind() == kind::IMPLIES ||
- expr[1].getKind() == kind::IFF ||
expr[1].getKind() == kind::EQUAL) {
guard = expr[0];
body = expr[1];
@@ -2008,11 +1998,13 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
args.push_back(f2);
}
- if ( body.getKind()==kind::IMPLIES ) kind = kind::RR_DEDUCTION;
- else if( body.getKind()==kind::IFF ) kind = kind::RR_REDUCTION;
- else if( body.getKind()==kind::EQUAL ) kind = kind::RR_REWRITE;
- else PARSER_STATE->parseError("Error parsing rewrite rule.");
-
+ if( body.getKind()==kind::IMPLIES ){
+ kind = kind::RR_DEDUCTION;
+ }else if( body.getKind()==kind::EQUAL ){
+ kind = body[0].getType().isBoolean() ? kind::RR_REDUCTION : kind::RR_REWRITE;
+ }else{
+ PARSER_STATE->parseError("Error parsing rewrite rule.");
+ }
expr = MK_EXPR( kind, args );
} else if(! patexprs.empty()) {
if( !f2.isNull() && f2.getKind()==kind::INST_PATTERN_LIST ){
@@ -2144,8 +2136,7 @@ attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr]
std::string attr_name = attr;
attr_name.erase( attr_name.begin() );
if( attr==":fun-def" ){
- if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) ||
- expr[0].getKind()!=kind::APPLY_UF ){
+ if( expr.getKind()!=kind::EQUAL || expr[0].getKind()!=kind::APPLY_UF ){
success = false;
}else{
FunctionType t = (FunctionType)expr[0].getOperator().getType();
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2e2481a6e..e1b824ba3 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -195,7 +195,6 @@ void Smt2::addTheory(Theory theory) {
Parser::addOperator(kind::AND);
Parser::addOperator(kind::DISTINCT);
Parser::addOperator(kind::EQUAL);
- Parser::addOperator(kind::IFF);
Parser::addOperator(kind::IMPLIES);
Parser::addOperator(kind::ITE);
Parser::addOperator(kind::NOT);
@@ -823,6 +822,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
oldKind = kind::MINUS;
newKind = kind::UMINUS;
}
+ /*
//convert to IFF if boolean EQUAL
if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){
Type ctn = sgt.d_children[0].d_type;
@@ -832,6 +832,7 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
newKind = kind::IFF;
}
}
+ */
if( newKind!=kind::UNDEFINED_KIND ){
Expr newExpr = getExprManager()->operatorOf(newKind);
Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
@@ -1450,7 +1451,7 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
}
}
Debug("parser-sygus") << "...made built term " << builtTerm << std::endl;
- Expr assertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
+ Expr assertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm);
if( !bvl.isNull() ){
Expr pattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
pattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, pattern);
@@ -1502,7 +1503,7 @@ Expr Smt2::getSygusAssertion( std::vector<DatatypeType>& datatypeTypes, std::vec
Debug("parser-sygus") << "builtApply " << builtApply[k] << std::endl;
builtTerm = getExprManager()->mkExpr(ops[i][j], builtApply);
Debug("parser-sygus") << "builtTerm " << builtTerm << std::endl;
- Expr eassertion = getExprManager()->mkExpr(evalApply.getType().isBoolean() ? kind::IFF : kind::EQUAL, evalApply, builtTerm);
+ Expr eassertion = getExprManager()->mkExpr(kind::EQUAL, evalApply, builtTerm);
Expr epattern = getExprManager()->mkExpr(kind::INST_PATTERN, evalApply);
epattern = getExprManager()->mkExpr(kind::INST_PATTERN_LIST, epattern);
eassertion = getExprManager()->mkExpr(kind::FORALL, nbvl, eassertion, epattern);
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 414c2f6b0..4e73fa6cf 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -527,7 +527,7 @@ fofLogicFormula[CVC4::Expr& expr]
( fofBinaryNonAssoc[na] fofUnitaryFormula[expr2]
{ switch(na) {
case tptp::NA_IFF:
- expr = MK_EXPR(kind::IFF,expr,expr2);
+ expr = MK_EXPR(kind::EQUAL,expr,expr2);
break;
case tptp::NA_REVIFF:
expr = MK_EXPR(kind::XOR,expr,expr2);
@@ -662,7 +662,7 @@ tffLogicFormula[CVC4::Expr& expr]
( fofBinaryNonAssoc[na] tffUnitaryFormula[expr2]
{ switch(na) {
case tptp::NA_IFF:
- expr = MK_EXPR(kind::IFF,expr,expr2);
+ expr = MK_EXPR(kind::EQUAL,expr,expr2);
break;
case tptp::NA_REVIFF:
expr = MK_EXPR(kind::XOR,expr,expr2);
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index ba8eb7012..dcb23d3f2 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -78,7 +78,6 @@ void Tptp::addTheory(Theory theory) {
defineVar("$false", em->mkConst(false));
addOperator(kind::AND);
addOperator(kind::EQUAL);
- addOperator(kind::IFF);
addOperator(kind::IMPLIES);
//addOperator(kind::ITE); //only for tff thf
addOperator(kind::NOT);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback