diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 12 | ||||
-rw-r--r-- | src/parser/smt1/Smt1.g | 2 | ||||
-rw-r--r-- | src/parser/smt1/smt1.cpp | 1 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 31 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 7 | ||||
-rw-r--r-- | src/parser/tptp/Tptp.g | 4 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 1 |
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); |