diff options
Diffstat (limited to 'src')
104 files changed, 592 insertions, 1832 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index e681b831b..4f4101d7e 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -290,7 +290,7 @@ Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { } Expr Expr::iffExpr(const Expr& right) const { - return getEM()->mkExpr(CVC4::kind::IFF, *this, right); + return getEM()->mkExpr(CVC4::kind::EQUAL, *this, right); } Expr Expr::impExpr(const Expr& right) const { @@ -434,9 +434,11 @@ bool Expr::isAtomicFormula() const { case CVC4::kind::AND: case CVC4::kind::OR: case CVC4::kind::ITE: - case CVC4::kind::IFF: case CVC4::kind::IMPLIES: return false; + case CVC4::kind::EQUAL: + return (*this)[0].getType().isBool(); + break; default: ; /* fall through */ } @@ -469,10 +471,12 @@ bool Expr::isBoolConnective() const { case CVC4::kind::AND: case CVC4::kind::OR: case CVC4::kind::IMPLIES: - case CVC4::kind::IFF: case CVC4::kind::XOR: case CVC4::kind::ITE: return true; + case CVC4::kind::EQUAL: + return (*this)[0].getType().isBool(); + break; default: return false; } @@ -547,7 +551,7 @@ bool Expr::isITE() const { } bool Expr::isIff() const { - return getKind() == CVC4::kind::IFF; + return getKind() == CVC4::kind::EQUAL && (*this)[0].getType().isBool();; } bool Expr::isImpl() const { @@ -1663,7 +1667,7 @@ Expr ValidityChecker::impliesExpr(const Expr& hyp, const Expr& conc) { } Expr ValidityChecker::iffExpr(const Expr& left, const Expr& right) { - return d_em->mkExpr(CVC4::kind::IFF, left, right); + return d_em->mkExpr(CVC4::kind::EQUAL, left, right); } Expr ValidityChecker::eqExpr(const Expr& child0, const Expr& child1) { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index cfa478c7d..c0d65cbe6 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -142,10 +142,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D inline void computeXorIffDesiredValues (Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2) { - Assert(k == kind::IFF || k == kind::XOR); + Assert(k == kind::EQUAL || k == kind::XOR); bool shouldInvert = - (desiredVal == SAT_VALUE_TRUE && k == kind::IFF) || + (desiredVal == SAT_VALUE_TRUE && k == kind::EQUAL) || (desiredVal == SAT_VALUE_FALSE && k == kind::XOR); if(desiredVal1 == SAT_VALUE_UNKNOWN && @@ -449,6 +449,10 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) /* What type of node is this */ Kind k = node.getKind(); theory::TheoryId tId = theory::kindToTheoryId(k); + bool isAtom = + (k == kind::BOOLEAN_TERM_VARIABLE ) || + ( (tId != theory::THEORY_BOOL) && + (k != kind::EQUAL || (!node[0].getType().isBoolean())) ); /* Some debugging stuff */ Debug("decision::jh") << "kind = " << k << std::endl @@ -459,7 +463,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) /** * If not in theory of booleans, check if this is something to split-on. */ - if(tId != theory::THEORY_BOOL) { + if(isAtom) { // if node has embedded ites, resolve that first if(handleEmbeddedITEs(node) == FOUND_SPLITTER) return FOUND_SPLITTER; @@ -516,7 +520,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) break; case kind::XOR: - case kind::IFF: { + case kind::EQUAL: { SatValue desiredVal1 = tryGetSatValue(node[0]); SatValue desiredVal2 = tryGetSatValue(node[1]); computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 43e4a7b76..dad437bc6 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -528,7 +528,7 @@ Expr Expr::iffExpr(const Expr& e) const { "Don't have an expression manager for this expression!"); PrettyCheckArgument(d_exprManager == e.d_exprManager, e, "Different expression managers!"); - return d_exprManager->mkExpr(IFF, *this, e); + return d_exprManager->mkExpr(EQUAL, *this, e); } Expr Expr::impExpr(const Expr& e) const { diff --git a/src/expr/node.h b/src/expr/node.h index c9bfb75a4..6dbb5aa2b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -893,8 +893,6 @@ public: NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart, const NodeTemplate<ref_count3>& elsepart) const; template <bool ref_count2> - NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const; - template <bool ref_count2> NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const; template <bool ref_count2> NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const; @@ -1203,14 +1201,6 @@ NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart, template <bool ref_count> template <bool ref_count2> NodeTemplate<true> -NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const { - assertTNodeNotExpired(); - return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); -} - -template <bool ref_count> -template <bool ref_count2> -NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const { assertTNodeNotExpired(); return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a9be51418..ebf78f541 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -780,6 +780,13 @@ Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } +Node NodeManager::mkBooleanTermVariable() { + Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE); + n.setAttribute(TypeAttr(), booleanType()); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) { std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type ); if( it==d_unique_vars[k].end() ){ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index d85ff23d5..d2b45a636 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -528,6 +528,9 @@ public: /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); + + /** Create a boolean term variable. */ + Node mkBooleanTermVariable(); /** Make a new abstract value with the given type. */ Node mkAbstractValue(const TypeNode& type); diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp index 0673718bb..4fc9b1f8d 100644 --- a/src/options/boolean_term_conversion_mode.cpp +++ b/src/options/boolean_term_conversion_mode.cpp @@ -20,22 +20,5 @@ namespace CVC4 { -std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { - switch(mode) { - case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: - out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS"; - break; - case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: - out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES"; - break; - case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE: - out << "BOOLEAN_TERM_CONVERT_NATIVE"; - break; - default: - out << "BooleanTermConversionMode!UNKNOWN"; - } - - return out; -} }/* CVC4 namespace */ diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h index f2f4a51af..57e2ccaf4 100644 --- a/src/options/boolean_term_conversion_mode.h +++ b/src/options/boolean_term_conversion_mode.h @@ -26,28 +26,9 @@ namespace CVC4 { namespace theory { namespace booleans { -enum BooleanTermConversionMode { - /** - * Convert Boolean terms to bitvectors of size 1. - */ - BOOLEAN_TERM_CONVERT_TO_BITVECTORS, - /** - * Convert Boolean terms to enumerations in the Datatypes theory. - */ - BOOLEAN_TERM_CONVERT_TO_DATATYPES, - /** - * Convert Boolean terms to enumerations in the Datatypes theory IF - * used in a datatypes context, otherwise to a bitvector of size 1. - */ - BOOLEAN_TERM_CONVERT_NATIVE - -}; - }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ -std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC; - }/* CVC4 namespace */ #endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */ diff --git a/src/options/booleans_options b/src/options/booleans_options index a150c1d83..6143f4f67 100644 --- a/src/options/booleans_options +++ b/src/options/booleans_options @@ -5,7 +5,5 @@ module BOOLEANS "options/booleans_options.h" Boolean theory -option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "options/boolean_term_conversion_mode.h" :handler stringToBooleanTermConversionMode - policy for converting Boolean terms endmodule diff --git a/src/options/expr_options b/src/options/expr_options index 75354a010..d6997b2dd 100644 --- a/src/options/expr_options +++ b/src/options/expr_options @@ -26,8 +26,5 @@ option earlyTypeChecking --eager-type-checking/--lazy-type-checking bool :defaul option typeChecking type-checking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking never type check expressions -option biasedITERemoval --biased-ites bool :default false - try the new remove ite pass that is biased against term ites appearing - endmodule diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 0dac42362..c0aa67cd4 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1061,41 +1061,6 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionEx } } - -// theory/booleans/options_handlers.h -const std::string OptionsHandler::s_booleanTermConversionModeHelp = "\ -Boolean term conversion modes currently supported by the\n\ ---boolean-term-conversion-mode option:\n\ -\n\ -bitvectors [default]\n\ -+ Boolean terms are converted to bitvectors of size 1.\n\ -\n\ -datatypes\n\ -+ Boolean terms are converted to enumerations in the Datatype theory.\n\ -\n\ -native\n\ -+ Boolean terms are converted in a \"natural\" way depending on where they\n\ - are used. If in a datatype context, they are converted to an enumeration.\n\ - Elsewhere, they are converted to a bitvector of size 1.\n\ -"; - -theory::booleans::BooleanTermConversionMode OptionsHandler::stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException){ - if(optarg == "bitvectors") { - return theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS; - } else if(optarg == "datatypes") { - return theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES; - } else if(optarg == "native") { - return theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE; - } else if(optarg == "help") { - puts(s_booleanTermConversionModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + - optarg + "'. Try --boolean-term-conversion-mode help."); - } -} - - // theory/uf/options_handlers.h const std::string OptionsHandler::s_ufssModeHelp = "\ UF strong solver options currently supported by the --uf-ss option:\n\ diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 45aea7b79..248f15c98 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -118,10 +118,6 @@ public: theory::bv::SatSolverMode stringToSatSolver(std::string option, std::string optarg) throw(OptionException); - - // theory/booleans/options_handlers.h - theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException); - // theory/uf/options_handlers.h theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException); 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); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index a9eab4a8c..01978b2e5 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -225,7 +225,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo // BUILTIN case kind::EQUAL: - op << '='; + if( n[0].getType().isBoolean() ){ + op << "<=>"; + }else{ + op << '='; + } opType = INFIX; break; case kind::ITE: @@ -294,10 +298,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << "XOR"; opType = INFIX; break; - case kind::IFF: - op << "<=>"; - opType = INFIX; - break; case kind::IMPLIES: op << "=>"; opType = INFIX; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index d75ec2126..a7add27f8 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -355,7 +355,6 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // bool theory case kind::NOT: case kind::AND: - case kind::IFF: case kind::IMPLIES: case kind::OR: case kind::XOR: @@ -719,7 +718,6 @@ static string smtKindString(Kind k) throw() { // bool theory case kind::NOT: return "not"; case kind::AND: return "and"; - case kind::IFF: return "="; case kind::IMPLIES: return "=>"; case kind::OR: return "or"; case kind::XOR: return "xor"; diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index b7ed0b2ec..0f0c14eb2 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -24,7 +24,7 @@ namespace CVC4 { inline static Node eqNode(TNode n1, TNode n2) { - return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); + return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); } // congrence matching term helper @@ -429,7 +429,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, // and use it to determine which option we need. - if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + if(n2.getKind() == kind::EQUAL) { if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { // We are in a sequence of identical equalities @@ -487,8 +487,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq } else { // We have a "next node". Use it to guide us. - Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL || - nodeAfterEqualitySequence.getKind() == kind::IFF); + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { @@ -533,7 +532,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Debug("pf::arith") << "\ndoing trans proof, got n2 " << n2 << "\n"; if(tb == 1) { Debug("pf::arith") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; - Debug("pf::arith") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + Debug("pf::arith") << (n2.getKind() == kind::EQUAL) << "\n"; if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { Debug("pf::arith") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; @@ -549,8 +548,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq } ss << "(trans _ _ _ _ "; - if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) && - (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF)) + if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL)) // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { @@ -580,7 +578,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq Unreachable(); } Debug("pf::arith") << "++ trans proof[" << i << "], now have " << n1 << std::endl; - } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { + } else if(n1.getKind() == kind::EQUAL) { // n1 is an equality/iff, but n2 is a predicate if(n1[0] == n2) { n1 = n1[1]; @@ -591,7 +589,7 @@ Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq } else { Unreachable(); } - } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + } else if(n2.getKind() == kind::EQUAL) { // n2 is an equality/iff, but n1 is a predicate if(n2[0] == n1) { n1 = n2[1]; diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index 32a7c247d..cc60d8c07 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -24,7 +24,7 @@ namespace CVC4 { inline static Node eqNode(TNode n1, TNode n2) { - return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); + return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); } // congrence matching term helper @@ -640,7 +640,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, // and use it to determine which option we need. - if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + if(n2.getKind() == kind::EQUAL) { if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { // We are in a sequence of identical equalities @@ -701,8 +701,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, nodeAfterEqualitySequence = nodeAfterEqualitySequence[0]; } - Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL || - nodeAfterEqualitySequence.getKind() == kind::IFF); + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { @@ -747,7 +746,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Debug("mgd") << "\ndoing trans proof, got n2 " << n2 << "\n"; if(tb == 1) { Debug("mgdx") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; - Debug("mgdx") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + Debug("mgdx") << (n2.getKind() == kind::EQUAL) << "\n"; if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { Debug("mgdx") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; @@ -784,8 +783,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, ss << "(trans _ _ _ _ "; } - if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) && - (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF)) + if((n2.getKind() == kind::EQUAL) && (n1.getKind() == kind::EQUAL)) // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { @@ -824,7 +822,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, Unreachable(); } Debug("mgd") << "++ trans proof[" << i << "], now have " << n1 << std::endl; - } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { + } else if(n1.getKind() == kind::EQUAL) { // n1 is an equality/iff, but n2 is a predicate if(n1[0] == n2) { n1 = n1[1]; @@ -836,7 +834,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out, } else { Unreachable(); } - } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + } else if(n2.getKind() == kind::EQUAL) { // n2 is an equality/iff, but n1 is a predicate if(n2[0] == n1) { n1 = n2[1]; diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index cbe54ff4b..926dae9fd 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -412,7 +412,7 @@ void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) { } void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) { - std::string op = utils::toLFSCKind(term.getKind()); + std::string op = utils::toLFSCKindTerm(term); std::ostringstream paren; std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : ""; unsigned size = term.getKind() == kind::BITVECTOR_CONCAT? utils::getSize(term) : @@ -431,7 +431,7 @@ void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const Pr void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; - os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" "; + os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" "; os << " "; d_proofEngine->printBoundTerm(term[0], os, map); os <<")"; @@ -439,7 +439,7 @@ void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const P void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; - os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term[0]) <<" "; + os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term[0]) <<" "; os << " "; d_proofEngine->printBoundTerm(term[0], os, map); os << " "; @@ -449,7 +449,7 @@ void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const Proof void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) { os <<"("; - os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" "; + os << utils::toLFSCKindTerm(term) << " " << utils::getSize(term) <<" "; os <<" "; if (term.getKind() == kind::BITVECTOR_REPEAT) { unsigned amount = term.getOperator().getConst<BitVectorRepeat>().repeatAmount; @@ -872,7 +872,7 @@ void LFSCBitVectorProof::printAtomBitblasting(Expr atom, std::ostream& os, bool case kind::EQUAL: { Debug("pf::bv") << "Bitblasing kind = " << kind << std::endl; - os << "(bv_bbl_" << utils::toLFSCKind(atom.getKind()); + os << "(bv_bbl_" << utils::toLFSCKindTerm(atom); if (swap) {os << "_swap";} diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index b58ade35e..69b613f28 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -596,16 +596,16 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os << ")"; } } - }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){ + }else if( base_assertion.getKind()==kind::XOR || ( base_assertion.getKind()==kind::EQUAL && base_assertion[0].getType().isBoolean() ) ){ //eliminate negation int num_nots_2 = 0; int num_nots_1 = 0; Kind k; if( !base_pol ){ - if( base_assertion.getKind()==kind::IFF ){ + if( base_assertion.getKind()==kind::EQUAL ){ num_nots_2 = 1; } - k = kind::IFF; + k = kind::EQUAL; }else{ k = base_assertion.getKind(); } @@ -623,7 +623,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, if( i==0 ){ //figure out which way to elim elimNum = child_pol==childPol[child_base] ? 2 : 1; - if( (elimNum==2)==(k==kind::IFF) ){ + if( (elimNum==2)==(k==kind::EQUAL) ){ num_nots_2++; } if( elimNum==1 ){ @@ -651,9 +651,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os_base_n << ProofManager::getLitName(lit1, d_name) << " "; } Assert( elimNum!=0 ); - os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; + os_base_n << "(" << ( k==kind::EQUAL ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ "; if( !base_pol ){ - os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; + os_base_n << "(not_" << ( base_assertion.getKind()==kind::EQUAL ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")"; }else{ os_base_n << os_base.str(); } diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp index fe0d42242..3ace236b5 100644 --- a/src/proof/proof_utils.cpp +++ b/src/proof/proof_utils.cpp @@ -41,7 +41,6 @@ std::string toLFSCKind(Kind kind) { case kind::AND: return "and"; case kind::XOR: return "xor"; case kind::EQUAL: return "="; - case kind::IFF: return "iff"; case kind::IMPLIES: return "impl"; case kind::NOT: return "not"; @@ -123,5 +122,18 @@ std::string toLFSCKind(Kind kind) { } } +std::string toLFSCKindTerm(Expr node) { + Kind k = node.getKind(); + if( k==kind::EQUAL ){ + if( node[0].getType().isBoolean() ){ + return "iff"; + }else{ + return "="; + } + }else{ + return toLFSCKind( k ); + } +} + } /* namespace CVC4::utils */ } /* namespace CVC4 */ diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index b172217d8..a7590451d 100644 --- a/src/proof/proof_utils.h +++ b/src/proof/proof_utils.h @@ -88,6 +88,7 @@ typedef std::vector<LetOrderElement> Bindings; namespace utils { std::string toLFSCKind(Kind kind); +std::string toLFSCKindTerm(Expr node); inline unsigned getExtractHigh(Expr node) { return node.getOperator().getConst<BitVectorExtract>().high; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 1912dbada..156c90e47 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -856,9 +856,13 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro case kind::EQUAL: os << "("; - os << "= "; - printSort(term[0].getType(), os); - os << " "; + if( term[0].getType().isBoolean() ){ + os << "iff "; + }else{ + os << "= "; + printSort(term[0].getType(), os); + os << " "; + } printBoundTerm(term[0], os, map); os << " "; printBoundTerm(term[1], os, map); @@ -912,6 +916,12 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro // LFSC doesn't allow declarations with variable numbers of // arguments, so we have to flatten chained operators, like =. Kind op = term.getOperator().getConst<Chain>().getOperator(); + std::string op_str; + if( op==kind::EQUAL && term[0].getType().isBoolean() ){ + op_str = "iff"; + }else{ + op_str = utils::toLFSCKind(op); + } size_t n = term.getNumChildren(); std::ostringstream paren; for(size_t i = 1; i < n; ++i) { @@ -919,7 +929,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro os << "(" << utils::toLFSCKind(kind::AND) << " "; paren << ")"; } - os << "(" << utils::toLFSCKind(op) << " "; + os << "(" << op_str << " "; printBoundTerm(term[i - 1], os, map); os << " "; printBoundTerm(term[i], os, map); @@ -1096,7 +1106,6 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe // If letification is off or there were 2 children, same treatment as the other cases. // (No break is intentional). case kind::XOR: - case kind::IFF: case kind::IMPLIES: case kind::NOT: // print the Boolean operators diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 27f351102..41262051c 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -24,7 +24,7 @@ namespace CVC4 { inline static Node eqNode(TNode n1, TNode n2) { - return NodeManager::currentNM()->mkNode(n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2); + return NodeManager::currentNM()->mkNode(kind::EQUAL, n1, n2); } // congrence matching term helper @@ -472,7 +472,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E // we look at the node after the equality sequence. If it needs a, we go for a=a; and if it needs // b, we go for b=b. If there is no following node, we look at the goal of the transitivity proof, // and use it to determine which option we need. - if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + if(n2.getKind() == kind::EQUAL) { if (((n1[0] == n2[0]) && (n1[1] == n2[1])) || ((n1[0] == n2[1]) && (n1[1] == n2[0]))) { // We are in a sequence of identical equalities @@ -530,8 +530,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } else { // We have a "next node". Use it to guide us. - Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL || - nodeAfterEqualitySequence.getKind() == kind::IFF); + Assert(nodeAfterEqualitySequence.getKind() == kind::EQUAL); if ((n1[0] == nodeAfterEqualitySequence[0]) || (n1[0] == nodeAfterEqualitySequence[1])) { @@ -576,7 +575,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Debug("pf::uf") << "\ndoing trans proof, got n2 " << n2 << "\n"; if(tb == 1) { Debug("pf::uf") << "\ntrans proof[" << i << "], got n2 " << n2 << "\n"; - Debug("pf::uf") << (n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) << "\n"; + Debug("pf::uf") << (n2.getKind() == kind::EQUAL) << "\n"; if ((n1.getNumChildren() >= 2) && (n2.getNumChildren() >= 2)) { Debug("pf::uf") << n1[0].getId() << " " << n1[1].getId() << " / " << n2[0].getId() << " " << n2[1].getId() << "\n"; @@ -592,8 +591,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E } ss << "(trans _ _ _ _ "; - if((n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) && - (n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF)) + if(n2.getKind() == kind::EQUAL && n1.getKind() == kind::EQUAL) // Both elements of the transitivity rule are equalities/iffs { if(n1[0] == n2[0]) { @@ -623,24 +621,24 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::E Unreachable(); } Debug("pf::uf") << "++ trans proof[" << i << "], now have " << n1 << std::endl; - } else if(n1.getKind() == kind::EQUAL || n1.getKind() == kind::IFF) { + } else if(n1.getKind() == kind::EQUAL) { // n1 is an equality/iff, but n2 is a predicate if(n1[0] == n2) { - n1 = n1[1].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n1[1].eqNode(NodeManager::currentNM()->mkConst(true)); ss << "(symm _ _ _ " << ss1.str() << ") (pred_eq_t _ " << ss2.str() << ")"; } else if(n1[1] == n2) { - n1 = n1[0].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n1[0].eqNode(NodeManager::currentNM()->mkConst(true)); ss << ss1.str() << " (pred_eq_t _ " << ss2.str() << ")"; } else { Unreachable(); } - } else if(n2.getKind() == kind::EQUAL || n2.getKind() == kind::IFF) { + } else if(n2.getKind() == kind::EQUAL) { // n2 is an equality/iff, but n1 is a predicate if(n2[0] == n1) { - n1 = n2[1].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n2[1].eqNode(NodeManager::currentNM()->mkConst(true)); ss << "(symm _ _ _ " << ss2.str() << ") (pred_eq_t _ " << ss1.str() << ")"; } else if(n2[1] == n1) { - n1 = n2[0].iffNode(NodeManager::currentNM()->mkConst(true)); + n1 = n2[0].eqNode(NodeManager::currentNM()->mkConst(true)); ss << ss2.str() << " (pred_eq_t _ " << ss1.str() << ")"; } else { Unreachable(); @@ -707,6 +705,10 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& os << term; return; } + if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) { + os << "(p_app " << term << ")"; + return; + } Assert (term.getKind() == kind::APPLY_UF); d_proofEngine->treatBoolsAsFormulas(false); diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f2401041e..bc819801b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -242,7 +242,7 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { bool preRegister = false; // Is this a variable add it to the list - if (node.isVar()) { + if (node.isVar() && node.getKind()!=BOOLEAN_TERM_VARIABLE) { d_booleanVariables.push_back(node); } else { theoryLiteral = true; @@ -389,7 +389,7 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { Assert(!hasLiteral(iffNode), "Atom already mapped!"); - Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!"); + Assert(iffNode.getKind() == EQUAL, "Expecting an EQUAL expression!"); Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!"); Debug("cnf") << "handleIff(" << iffNode << ")" << endl; @@ -488,9 +488,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { case ITE: nodeLit = handleIte(node); break; - case IFF: - nodeLit = handleIff(node); - break; case IMPLIES: nodeLit = handleImplies(node); break; @@ -502,8 +499,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { break; case EQUAL: if(node[0].getType().isBoolean()) { - // normally this is an IFF, but EQUAL is possible with pseudobooleans - nodeLit = handleIff(node[0].iffNode(node[1])); + nodeLit = handleIff(node); } else { nodeLit = convertAtom(node); } @@ -722,9 +718,6 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { case OR: convertAndAssertOr(node, negated); break; - case IFF: - convertAndAssertIff(node, negated); - break; case XOR: convertAndAssertXor(node, negated); break; @@ -737,6 +730,11 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { case NOT: convertAndAssert(node[0], !negated); break; + case EQUAL: + if( node[0].getType().isBoolean() ){ + convertAndAssertIff(node, negated); + break; + } default: { Node nnode = node; diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index bcacd4bd4..442355580 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -38,824 +38,5 @@ using namespace CVC4::theory::booleans; namespace CVC4 { namespace smt { -BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) : - d_smt(smt), - d_ff(), - d_tt(), - d_ffDt(), - d_ttDt(), - d_varCache(smt.d_userContext), - d_termCache(smt.d_userContext), - d_typeCache(), - d_datatypeCache(), - d_datatypeReverseCache() { - - // set up our "false" and "true" conversions based on command-line option - if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS || - options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE) { - d_ff = NodeManager::currentNM()->mkConst(BitVector(1u, 0u)); - d_tt = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); - } - if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS) { - d_ffDt = d_ff; - d_ttDt = d_tt; - } else { - Datatype spec("BooleanTerm"); - // don't change the order; false is assumed to come first by the model postprocessor - spec.addConstructor(DatatypeConstructor("BT_False")); - spec.addConstructor(DatatypeConstructor("BT_True")); - const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype(); - d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor())); - d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor())); - // mark this datatype type as being special for Boolean term conversion - TypeNode::fromType(dt.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null()); - if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES) { - Assert(d_ff.isNull() && d_tt.isNull()); - d_ff = d_ffDt; - d_tt = d_ttDt; - } - } - - // assert that we set it up correctly - Assert(!d_ff.isNull() && !d_tt.isNull()); - Assert(!d_ffDt.isNull() && !d_ttDt.isNull()); - Assert(d_ff != d_tt); - Assert(d_ff.getType() == d_tt.getType()); - Assert(d_ffDt != d_ttDt); - Assert(d_ffDt.getType() == d_ttDt.getType()); - -}/* BooleanTermConverter::BooleanTermConverter() */ - -static inline bool isBoolean(TNode top, unsigned i) { - switch(top.getKind()) { - case kind::NOT: - case kind::AND: - case kind::IFF: - case kind::IMPLIES: - case kind::OR: - case kind::XOR: - case kind::FORALL: - case kind::EXISTS: - case kind::REWRITE_RULE: - case kind::RR_REWRITE: - case kind::RR_DEDUCTION: - case kind::RR_REDUCTION: - case kind::INST_PATTERN: - return true; - - case kind::ITE: - if(i == 0) { - return true; - } - return top.getType().isBoolean(); - - default: - return false; - } -} - -// This function rewrites "in" as an "as"---this is actually expected -// to be for model-substitution, so the "in" is a Boolean-term-converted -// node, and "as" is the original. See how it's used in function -// handling, below. -// -// Note this isn't the case any longer, and parts of what's below have -// been repurposed for *forward* conversion, meaning this works in either -// direction. -Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw() { - Debug("boolean-terms2") << "Rewrite as " << in << " " << as << std::endl; - if(in.getType() == as) { - return in; - } - if(in.getType().isBoolean()) { - Assert(d_tt.getType() == as); - return NodeManager::currentNM()->mkNode(kind::ITE, in, d_tt, d_ff); - } - if(as.isBoolean() && in.getType().isBitVector() && in.getType().getBitVectorSize() == 1) { - return NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in); - } - TypeNode in_t = in.getType(); - if( processing.find( in_t )==processing.end() ){ - processing[in_t] = true; - if(in.getType().isParametricDatatype() && - in.getType().isInstantiatedDatatype()) { - // We have something here like (Pair Bool Bool)---need to dig inside - // and make it (Pair BV1 BV1) - Assert(as.isParametricDatatype() && as.isInstantiatedDatatype()); - const Datatype* dt2 = &as[0].getDatatype(); - std::vector<TypeNode> fromParams, toParams; - for(unsigned i = 0; i < dt2->getNumParameters(); ++i) { - fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); - toParams.push_back(as[i + 1]); - } - const Datatype* dt1; - if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { - dt1 = d_datatypeCache[dt2]; - } else { - dt1 = d_datatypeReverseCache[dt2]; - } - Assert(dt1 != NULL, "expected datatype in cache"); - Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes"); - Node out; - for(size_t i = 0; i < dt1->getNumConstructors(); ++i) { - DatatypeConstructor ctor = (*dt1)[i]; - NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); - appctorb << (*dt2)[i].getConstructor(); - for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()); - asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType, processing); - } - Node appctor = appctorb; - if(i == 0) { - out = appctor; - } else { - Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); - out = newOut; - } - } - processing.erase( in_t ); - return out; - } - if(in.getType().isDatatype()) { - if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) { - processing.erase( in_t ); - return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in); - } - Assert(as.isDatatype()); - const Datatype* dt2 = &as.getDatatype(); - const Datatype* dt1; - if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) { - dt1 = d_datatypeCache[dt2]; - } else { - dt1 = d_datatypeReverseCache[dt2]; - } - Assert(dt1 != NULL, "expected datatype in cache"); - Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes"); - Node out; - for(size_t i = 0; i < dt1->getNumConstructors(); ++i) { - DatatypeConstructor ctor = (*dt1)[i]; - NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); - appctorb << (*dt2)[i].getConstructor(); - for(size_t j = 0; j < ctor.getNumArgs(); ++j) { - appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing); - } - Node appctor = appctorb; - if(i == 0) { - out = appctor; - } else { - Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out); - out = newOut; - } - } - processing.erase( in_t ); - return out; - } - if(in.getType().isArray()) { - // convert in to in' - // e.g. in : (Array Int Bool) - // for in' : (Array Int (_ BitVec 1)) - // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x] - Assert(as.isArray()); - Assert(as.getArrayIndexType() == in.getType().getArrayIndexType()); - Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType()); - Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType()); - Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x); - Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x); - Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing); - Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime); - Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam); - Assert(out.getType() == as); - processing.erase( in_t ); - return out; - } - Unhandled(in); - }else{ - Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl; - exit( 0 ); - } -} - -const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() { - const Datatype*& out = d_datatypeCache[&dt]; - if(out != NULL) { - return *out; - } - - Debug("boolean-terms") << "convertDatatype: considering " << dt.getName() << endl; - for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) { - TypeNode t = TypeNode::fromType((*c).getConstructor().getType()); - for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) { - TypeNode converted = convertType(*a, true); - Debug("boolean-terms") << "GOT: " << converted << ":" << converted.getId() << endl; - if(*a != converted) { - SortConstructorType mySelfType; - set<Type> unresolvedTypes; - if(dt.isParametric()) { - mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters()); - unresolvedTypes.insert(mySelfType); - } - vector<Datatype> newDtVector; - if(dt.isParametric()) { - newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters(), false)); - } else { - newDtVector.push_back(Datatype(dt.getName() + "'", false)); - } - Datatype& newDt = newDtVector.front(); - Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl; - for(c = dt.begin(); c != dt.end(); ++c) { - DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'"); - t = TypeNode::fromType((*c).getConstructor().getType()); - for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) { - Type argType = (*a).getType().getRangeType(); - if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) { - Debug("boolean-terms") << "argtype " << argType << " is self" << endl; - if(dt.isParametric()) { - Debug("boolean-terms") << "is-parametric self is " << mySelfType << endl; - ctor.addArg((*a).getName() + "'", mySelfType.instantiate(DatatypeType(argType).getDatatype().getParameters())); - } else { - ctor.addArg((*a).getName() + "'", DatatypeSelfType()); - } - } else { - Debug("boolean-terms") << "argtype " << argType << " is NOT self" << endl; - converted = convertType(TypeNode::fromType(argType), true); - if(TypeNode::fromType(argType) != converted) { - ctor.addArg((*a).getName() + "'", converted.toType()); - } else { - ctor.addArg((*a).getName() + "'", argType); - } - } - } - newDt.addConstructor(ctor); - } - vector<DatatypeType> newDttVector = - NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes); - DatatypeType& newDtt = newDttVector.front(); - const Datatype& newD = newDtt.getDatatype(); - for(c = dt.begin(); c != dt.end(); ++c) { - Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl; - const DatatypeConstructor *newC; - Node::fromExpr((*(newC = &newD[(*c).getName() + "'"])).getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr? - Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl; - d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor()); - d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester()); - for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) { - Node::fromExpr((*newC)[(*a).getName() + "'"].getSelector()).setAttribute(BooleanTermAttr(), Node::fromExpr((*a).getSelector()));// other attr? - d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'")); - } - } - out = &newD; - d_datatypeReverseCache[&newD] = &dt; - return newD; - } - } - } - - // this is identity; don't need the reverse cache - out = &dt; - return dt; - -}/* BooleanTermConverter::convertDatatype() */ - -TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) { - Debug("boolean-terms") << "CONVERT-TYPE[" << type << ":" << type.getId() << ", " << datatypesContext << "]" << endl; - // This function recursively converts the type. - if(type.isBoolean()) { - return datatypesContext ? d_ttDt.getType() : d_tt.getType(); - } - const pair<TypeNode, bool> cacheKey(type, datatypesContext); - if(d_typeCache.find(cacheKey) != d_typeCache.end()) { - TypeNode out = d_typeCache[cacheKey]; - return out.isNull() ? type : out; - } - TypeNode& outNode = d_typeCache[cacheKey]; - if(type.getKind() == kind::DATATYPE_TYPE || - type.getKind() == kind::PARAMETRIC_DATATYPE) { - bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE); - const Datatype& dt = parametric ? type[0].getDatatype() : type.getDatatype(); - TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType()); - Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl; - if(parametric) { - // re-parameterize the translation - vector<TypeNode> params = type.getParamTypes(); - for(size_t i = 0; i < params.size(); ++i) { - Debug("boolean-terms") << "in loop, got "<< params[i] << endl; - params[i] = convertType(params[i], true); - Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl; - } - params.insert(params.begin(), out[0]); - out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params); - Debug("boolean-terms") << "got OUT: " << out << endl; - } - if(out != type) { - outNode = out;// cache it - Debug("boolean-terms") << "OUT is same as TYPE" << endl; - } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl; - return out; - } - if(!type.isSort() && type.getNumChildren() > 0) { - Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl; - // This should handle tuples and arrays ok. - // Might handle function types too, but they can't go - // in other types, so it doesn't matter. - NodeBuilder<> b(type.getKind()); - if(type.getMetaKind() == kind::metakind::PARAMETERIZED) { - b << type.getOperator(); - } - for(TypeNode::iterator i = type.begin(); i != type.end(); ++i) { - b << convertType(*i, false); - } - TypeNode out = b; - if(out != type) { - outNode = out;// cache it - } - Debug("boolean-terms") << "here at B, returning " << out << ":" << out.getId() << endl; - return out; - } - // leave the cache at Null - return type; -}/* BooleanTermConverter::convertType() */ - -// look for vars from "vars" that occur in a term-context in n; transfer them to output. -static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TNode>& output, bool boolParent, std::hash_set< std::pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> >& alreadySeen) { - if(vars.empty()) { - return; - } - const pair<TNode, bool> cacheKey(n, boolParent); - if(alreadySeen.find(cacheKey) != alreadySeen.end()) { - return; - } - alreadySeen.insert(cacheKey); - - if(n.isVar() && vars.find(n) != vars.end() && !boolParent) { - vars.erase(n); - output.insert(n); - if(vars.empty()) { - return; - } - } - for(size_t i = 0; i < n.getNumChildren(); ++i) { - collectVarsInTermContext(n[i], vars, output, isBoolean(n, i), alreadySeen); - if(vars.empty()) { - return; - } - } -} - -Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() { - - stack< triple<TNode, theory::TheoryId, bool> > worklist; - worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false)); - stack< NodeBuilder<> > result; - //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder. Since TUPLE is no longer a kind, replacing this with "AND". - //result.push(NodeBuilder<>(kind::TUPLE)); - result.push(NodeBuilder<>(kind::AND)); - - NodeManager* nm = NodeManager::currentNM(); - - while(!worklist.empty()) { - top = worklist.top().first; - parentTheory = worklist.top().second; - bool& childrenPushed = worklist.top().third; - - Kind k = top.getKind(); - kind::MetaKind mk = top.getMetaKind(); - - // we only distinguish between datatypes, booleans, and "other", and we - // don't even distinguish datatypes except when in "native" conversion - // mode - if(parentTheory != theory::THEORY_BOOL) { - if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE || - parentTheory != theory::THEORY_DATATYPES) { - parentTheory = theory::THEORY_BUILTIN; - } - } - - if(!childrenPushed) { - Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl; - - BooleanTermVarCache::iterator i = d_varCache.find(top); - if(i != d_varCache.end()) { - result.top() << ((*i).second.isNull() ? Node(top) : (*i).second); - worklist.pop(); - goto next_worklist; - } - BooleanTermCache::iterator j = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory)); - if(j != d_termCache.end()) { - result.top() << ((*j).second.isNull() ? Node(top) : (*j).second); - worklist.pop(); - goto next_worklist; - } - - if(quantBoolVars.find(top) != quantBoolVars.end()) { - // this Bool variable is quantified over and we're changing it to a BitVector var - if(parentTheory == theory::THEORY_BOOL) { - result.top() << quantBoolVars[top].eqNode(d_tt); - } else { - result.top() << quantBoolVars[top]; - } - worklist.pop(); - goto next_worklist; - } - - if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean() && top.getKind()!=kind::SEP_STAR && top.getKind()!=kind::SEP_WAND) { - // still need to rewrite e.g. function applications over boolean - Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars); - Node n; - if(parentTheory == theory::THEORY_DATATYPES) { - n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt); - } else { - n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff); - } - Debug("boolean-terms") << "constructed ITE: " << n << endl; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - - if(mk == kind::metakind::CONSTANT) { - if(k == kind::STORE_ALL) { - const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>(); - ArrayType arrType = asa.getType(); - TypeNode indexType = TypeNode::fromType(arrType.getIndexType()); - Type constituentType = arrType.getConstituentType(); - if(constituentType.isBoolean()) { - // we have store_all(true) or store_all(false) - // just turn it into store_all(1) or store_all(0) - if(indexType.isBoolean()) { - // change index type to BV(1) also - indexType = d_tt.getType(); - } - ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(), - (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr()); - Node n = nm->mkConst(asaRepl); - Debug("boolean-terms") << " returning new store_all: " << n << endl; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - if(indexType.isBoolean()) { - // must change index type to BV(1) - indexType = d_tt.getType(); - ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr()); - Node n = nm->mkConst(asaRepl); - Debug("boolean-terms") << " returning new store_all: " << n << endl; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - } - result.top() << top; - worklist.pop(); - goto next_worklist; - } else if(mk == kind::metakind::VARIABLE) { - TypeNode t = top.getType(); - if(t.isFunction()) { - for(unsigned i = 0; i < t.getNumChildren(); ++i) { - TypeNode newType = convertType(t[i], false); - // is this the return type? (allowed to be Bool) - bool returnType = (i == t.getNumChildren() - 1); - if(newType != t[i] && (!t[i].isBoolean() || !returnType)) { - vector<TypeNode> argTypes = t.getArgTypes(); - for(unsigned j = 0; j < argTypes.size(); ++j) { - argTypes[j] = convertType(argTypes[j], false); - } - TypeNode rangeType = t.getRangeType(); - if(!rangeType.isBoolean()) { - rangeType = convertType(rangeType, false); - } - TypeNode newType = nm->mkFunctionType(argTypes, rangeType); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__", - newType, "a function introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl; - top.setAttribute(BooleanTermAttr(), n); - NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST); - NodeBuilder<> bodyBuilder(kind::APPLY_UF); - bodyBuilder << n; - for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) { - Node var = nm->mkBoundVar(t[j]); - boundVarsBuilder << var; - if(t[j] != argTypes[j]) { - std::map< TypeNode, bool > processing; - bodyBuilder << rewriteAs(var, argTypes[j], processing); - } else { - bodyBuilder << var; - } - } - Node boundVars = boundVarsBuilder; - Node body = bodyBuilder; - if(t.getRangeType() != rangeType) { - std::map< TypeNode, bool > processing; - Node convbody = rewriteAs(body, t.getRangeType(), processing); - body = convbody; - } - Node lam = nm->mkNode(kind::LAMBDA, boundVars, body); - Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl; - d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam); - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - } - } else if(t.isArray()) { - TypeNode indexType = convertType(t.getArrayIndexType(), false); - TypeNode constituentType = convertType(t.getArrayConstituentType(), false); - if(indexType != t.getArrayIndexType() && constituentType == t.getArrayConstituentType()) { - TypeNode newType = nm->mkArrayType(indexType, constituentType); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", - newType, "an array variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - top.setAttribute(BooleanTermAttr(), n); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - Node n_ff = nm->mkNode(kind::SELECT, n, d_ff); - Node n_tt = nm->mkNode(kind::SELECT, n, d_tt); - Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), (*TypeEnumerator(n_ff.getType())).toExpr())); - Node repl = nm->mkNode(kind::STORE, - nm->mkNode(kind::STORE, base, nm->mkConst(true), - n_tt), - nm->mkConst(false), n_ff); - Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl; - d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl); - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } else if(indexType == t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) { - TypeNode newType = nm->mkArrayType(indexType, constituentType); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", - newType, "an array variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - top.setAttribute(BooleanTermAttr(), n); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } else if(indexType != t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) { - TypeNode newType = nm->mkArrayType(indexType, constituentType); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", - newType, "an array variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - top.setAttribute(BooleanTermAttr(), n); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - Node n_ff = nm->mkNode(kind::SELECT, n, d_ff); - Node n_tt = nm->mkNode(kind::SELECT, n, d_tt); - Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr())); - Node repl = nm->mkNode(kind::STORE, - nm->mkNode(kind::STORE, base, nm->mkConst(false), - nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true), - nm->mkNode(kind::EQUAL, n_tt, d_tt)); - Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl; - d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl); - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - d_varCache[top] = Node::null(); - result.top() << top; - worklist.pop(); - goto next_worklist; - } else if(t.isDatatype() || t.isParametricDatatype()) { - Debug("boolean-terms") << "found a var of datatype type" << endl; - TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES); - if(t != newT) { - Assert(d_varCache.find(top) == d_varCache.end(), - "Node `%s' already in cache ?!", top.toString().c_str()); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'", - newT, "a datatype variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl; - top.setAttribute(BooleanTermAttr(), n); - d_smt.d_theoryEngine->getModel()->addSubstitution(top, n); - Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl; - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } else { - d_varCache[top] = Node::null(); - result.top() << top; - worklist.pop(); - goto next_worklist; - } - } else if(t.isConstructor()) { - Assert(parentTheory != theory::THEORY_BOOL); - Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE || - t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE); - const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ? - t[t.getNumChildren() - 1].getDatatype() : - t[t.getNumChildren() - 1][0].getDatatype(); - TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); - const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype(); - if(dt != dt2) { - Assert(d_varCache.find(top) != d_varCache.end(), - "constructor `%s' not in cache", top.toString().c_str()); - result.top() << d_varCache[top].get(); - worklist.pop(); - goto next_worklist; - } - d_varCache[top] = Node::null(); - result.top() << top; - worklist.pop(); - goto next_worklist; - } else if(t.isTester() || t.isSelector()) { - Assert(parentTheory != theory::THEORY_BOOL); - const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ? - t[0].getDatatype() : - t[0][0].getDatatype(); - TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES); - const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getDatatype(); - if(dt != dt2) { - Assert(d_varCache.find(top) != d_varCache.end(), - "tester or selector `%s' not in cache", top.toString().c_str()); - result.top() << d_varCache[top].get(); - worklist.pop(); - goto next_worklist; - } else { - d_varCache[top] = Node::null(); - result.top() << top; - worklist.pop(); - goto next_worklist; - } - } else if(!t.isSort() && t.getNumChildren() > 0) { - if( t.getKind()!=kind::SEP_STAR && t.getKind()!=kind::SEP_WAND ){ - for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) { - if((*i).isBoolean()) { - vector<TypeNode> argTypes(t.begin(), t.end()); - replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType()); - TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes); - Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()), - newType, "a variable introduced by Boolean-term conversion", - NodeManager::SKOLEM_EXACT_NAME); - Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl; - top.setAttribute(BooleanTermAttr(), n); - d_varCache[top] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - } - } - } - result.top() << top; - worklist.pop(); - goto next_worklist; - } - switch(k) { - //case kind::INST_ATTRIBUTE: - case kind::BOUND_VAR_LIST: - result.top() << top; - worklist.pop(); - goto next_worklist; - - case kind::REWRITE_RULE: - case kind::RR_REWRITE: - case kind::RR_DEDUCTION: - case kind::RR_REDUCTION: - case kind::SEP_STAR: - case kind::SEP_WAND: - // not yet supported - result.top() << top; - worklist.pop(); - goto next_worklist; - - case kind::FORALL: - case kind::EXISTS: { - Debug("bt") << "looking at quantifier -> " << top << endl; - set<TNode> ourVars; - set<TNode> output; - for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) { - if((*i).getType().isBoolean()) { - ourVars.insert(*i); - } else if(convertType((*i).getType(), false) != (*i).getType()) { - output.insert(*i); - } - } - if(ourVars.empty() && output.empty()) { - // Simple case, quantifier doesn't quantify over Boolean vars, - // no special handling needed for quantifier. Fall through. - Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl; - } else { - hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen; - collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen); - if(output.empty()) { - // Simple case, quantifier quantifies over Boolean vars, but they - // don't occur in term context. Fall through. - Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl; - } else { - Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl; - // We have Boolean vars appearing in term context. Convert their - // types in the quantifier. - for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) { - Node newVar = nm->mkBoundVar((*i).toString(), convertType((*i).getType(), false)); - Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)"); - quantBoolVars[*i] = newVar; - } - vector<TNode> boundVars; - for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) { - map<TNode, Node>::const_iterator j = quantBoolVars.find(*i); - if(j == quantBoolVars.end()) { - boundVars.push_back(*i); - } else { - boundVars.push_back((*j).second); - } - } - Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars); - Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars); - Node quant; - if( top.getNumChildren()==3 ){ - Node ipl = rewriteBooleanTermsRec(top[2], theory::THEORY_BOOL, quantBoolVars); - quant = nm->mkNode(top.getKind(), boundVarList, body, ipl ); - }else{ - quant = nm->mkNode(top.getKind(), boundVarList, body); - } - Debug("bt") << "rewrote quantifier to -> " << quant << endl; - d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant; - d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff); - d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff); - result.top() << quant; - worklist.pop(); - goto next_worklist; - } - } - /* intentional fall-through for some cases above */ - } - - default: - result.push(NodeBuilder<>(k)); - Debug("bt") << "looking at: " << top << endl; - // rewrite the operator, as necessary - if(mk == kind::metakind::PARAMETERIZED) { - if(k == kind::APPLY_TYPE_ASCRIPTION) { - Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType())); - result.top() << asc; - Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl; - asc.setAttribute(BooleanTermAttr(), top.getOperator()); - } else if(kindToTheoryId(k) != THEORY_BV && - k != kind::TUPLE_UPDATE && - k != kind::RECORD_UPDATE && - k != kind::DIVISIBLE && - // Theory parametric functions go here - k != kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR && - k != kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT && - k != kind::FLOATINGPOINT_TO_FP_REAL && - k != kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR && - k != kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR && - k != kind::FLOATINGPOINT_TO_UBV && - k != kind::FLOATINGPOINT_TO_SBV && - k != kind::FLOATINGPOINT_TO_REAL - ) { - Debug("bt") << "rewriting: " << top.getOperator() << endl; - result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars); - Debug("bt") << "got: " << result.top().getOperator() << endl; - } else { - result.top() << top.getOperator(); - } - } - // push children - for(int i = top.getNumChildren() - 1; i >= 0; --i) { - Debug("bt") << "rewriting: " << top[i] << endl; - worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], top.getKind() == kind::CHAIN ? parentTheory : ((isBoolean(top, i) || top.getKind()==kind::INST_ATTRIBUTE) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false)); - //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars); - //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl; - } - childrenPushed = true; - } - } else { - Node n = result.top(); - result.pop(); - Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << endl; - if(parentTheory == theory::THEORY_BOOL) { - if(n.getType().isBitVector() && - n.getType().getBitVectorSize() == 1) { - n = nm->mkNode(kind::EQUAL, n, d_tt); - } else if(n.getType().isDatatype() && - n.getType().hasAttribute(BooleanTermAttr())) { - n = nm->mkNode(kind::EQUAL, n, d_ttDt); - } - } - d_termCache[make_pair(top, parentTheory)] = n; - result.top() << n; - worklist.pop(); - goto next_worklist; - } - - next_worklist: - ; - } - - Assert(worklist.size() == 0); - Assert(result.size() == 1); - Node retval = result.top()[0]; - result.top().clear(); - result.pop(); - return retval; - -}/* BooleanTermConverter::rewriteBooleanTermsRec() */ - }/* CVC4::smt namespace */ }/* CVC4 namespace */ diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index 0a63f7fd8..0fb82aafe 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -28,84 +28,5 @@ namespace CVC4 { namespace smt { -namespace attr { - struct BooleanTermAttrTag { }; -}/* CVC4::smt::attr namespace */ - -typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr; - -class BooleanTermConverter { - /** The type of the Boolean term conversion variable cache */ - typedef context::CDHashMap<Node, Node, NodeHashFunction> BooleanTermVarCache; - - /** The type of the Boolean term conversion cache */ - typedef context::CDHashMap< std::pair<Node, theory::TheoryId>, Node, - PairHashFunction< Node, bool, - NodeHashFunction, std::hash<size_t> > > BooleanTermCache; - /** The type of the Boolean term conversion type cache */ - typedef std::hash_map< std::pair<TypeNode, bool>, TypeNode, - PairHashFunction< TypeNode, bool, - TypeNodeHashFunction, std::hash<int> > > BooleanTermTypeCache; - /** The type of the Boolean term conversion datatype cache */ - typedef std::hash_map<const Datatype*, const Datatype*, DatatypeHashFunction> BooleanTermDatatypeCache; - - /** The SmtEngine to which we're associated */ - SmtEngine& d_smt; - - /** The conversion for "false." */ - Node d_ff; - /** The conversion for "true." */ - Node d_tt; - /** The conversion for "false" when in datatypes contexts. */ - Node d_ffDt; - /** The conversion for "true" when in datatypes contexts. */ - Node d_ttDt; - - /** The cache used during Boolean term variable conversion */ - BooleanTermVarCache d_varCache; - /** The cache used during Boolean term conversion */ - BooleanTermCache d_termCache; - /** The cache used during Boolean term type conversion */ - BooleanTermTypeCache d_typeCache; - /** The cache used during Boolean term datatype conversion */ - BooleanTermDatatypeCache d_datatypeCache; - /** A (reverse) cache for Boolean term datatype conversion */ - BooleanTermDatatypeCache d_datatypeReverseCache; - - Node rewriteAs(TNode in, TypeNode as, std::map< TypeNode, bool >& processing) throw(); - - /** - * Scan a datatype for and convert as necessary. - */ - const Datatype& convertDatatype(const Datatype& dt) throw(); - - /** - * Convert a type. - */ - TypeNode convertType(TypeNode type, bool datatypesContext); - - Node rewriteBooleanTermsRec(TNode n, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw(); - -public: - - /** - * Construct a Boolean-term converter associated to the given - * SmtEngine. - */ - BooleanTermConverter(SmtEngine& smt); - - /** - * Rewrite Boolean terms under a node. The node itself is not converted - * if boolParent is true, but its Boolean subterms appearing in a - * non-Boolean context will be rewritten. - */ - Node rewriteBooleanTerms(TNode n, bool boolParent = true, bool dtParent = false) throw() { - std::map<TNode, Node> quantBoolVars; - Assert(!(boolParent && dtParent)); - return rewriteBooleanTermsRec(n, boolParent ? theory::THEORY_BOOL : (dtParent ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN), quantBoolVars); - } - -};/* class BooleanTermConverter */ - }/* CVC4::smt namespace */ }/* CVC4 namespace */ diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp index d31d54121..0202a5a2d 100644 --- a/src/smt/ite_removal.cpp +++ b/src/smt/ite_removal.cpp @@ -25,36 +25,36 @@ using namespace std; namespace CVC4 { -RemoveITE::RemoveITE(context::UserContext* u) +RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u) : d_iteCache(u) { d_containsVisitor = new theory::ContainsTermITEVisitor(); } -RemoveITE::~RemoveITE(){ +RemoveTermFormulas::~RemoveTermFormulas(){ delete d_containsVisitor; } -void RemoveITE::garbageCollect(){ +void RemoveTermFormulas::garbageCollect(){ d_containsVisitor->garbageCollect(); } -theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() { +theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() { return d_containsVisitor; } -size_t RemoveITE::collectedCacheSizes() const{ +size_t RemoveTermFormulas::collectedCacheSizes() const{ return d_containsVisitor->cache_size() + d_iteCache.size(); } -void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps) +void RemoveTermFormulas::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps) { size_t n = output.size(); for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { // Do this in two steps to avoid Node problems(?) // Appears related to bug 512, splitting this into two lines // fixes the bug on clang on Mac OS - Node itesRemoved = run(output[i], output, iteSkolemMap, false); + Node itesRemoved = run(output[i], output, iteSkolemMap, false, false); // In some calling contexts, not necessary to report dependence information. if (reportDeps && (options::unsatCores() || options::fewerPreprocessingHoles())) { @@ -69,22 +69,27 @@ void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool } } -bool RemoveITE::containsTermITE(TNode e) const { +bool RemoveTermFormulas::containsTermITE(TNode e) const { return d_containsVisitor->containsTermITE(e); } -Node RemoveITE::run(TNode node, std::vector<Node>& output, - IteSkolemMap& iteSkolemMap, bool inQuant) { +Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output, + IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) { // Current node - Debug("ite") << "removeITEs(" << node << ")" << endl; - - if(node.isVar() || node.isConst() || - (options::biasedITERemoval() && !containsTermITE(node))){ + Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl; + + //if(node.isVar() || node.isConst()){ + // (options::biasedITERemoval() && !containsTermITE(node))){ + //if(node.isVar()){ + // return Node(node); + //} + if( node.getKind()==kind::INST_PATTERN_LIST ){ return Node(node); } // The result may be cached already - std::pair<Node, bool> cacheKey(node, inQuant); + int cv = cacheVal( inQuant, inTerm ); + std::pair<Node, int> cacheKey(node, cv); NodeManager *nodeManager = NodeManager::currentNM(); ITECache::const_iterator i = d_iteCache.find(cacheKey); if(i != d_iteCache.end()) { @@ -93,14 +98,10 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, return cached.isNull() ? Node(node) : cached; } - // Remember that we're inside a quantifier - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { - inQuant = true; - } - // If an ITE replace it + // If an ITE, replace it + TypeNode nodeType = node.getType(); if(node.getKind() == kind::ITE) { - TypeNode nodeType = node.getType(); if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { Node skolem; // Make the skolem to represent the ITE @@ -116,7 +117,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, d_iteCache.insert(cacheKey, skolem); // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap, inQuant); + newAssertion = run(newAssertion, output, iteSkolemMap, false, false); iteSkolemMap[skolem] = output.size(); output.push_back(newAssertion); @@ -125,6 +126,40 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, return skolem; } } + //if a non-variable Boolean term, replace it + if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ + Node skolem; + // Make the skolem to represent the Boolean term + //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal"); + skolem = nodeManager->mkBooleanTermVariable(); + + // The new assertion + Node newAssertion = skolem.eqNode( node ); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the skolem + d_iteCache.insert(cacheKey, skolem); + + // Remove ITEs from the new assertion, rewrite it and push it to the output + newAssertion = run(newAssertion, output, iteSkolemMap, false, false); + + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + + // The representation is now the skolem + return skolem; + } + + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + // Remember if we're inside a quantifier + inQuant = true; + }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && + node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && + node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){ + // Remember if we're inside a term + Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl; + inTerm = true; + } // If not an ITE, go deep vector<Node> newChildren; @@ -134,7 +169,7 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, } // Remove the ITEs from the children for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, iteSkolemMap, inQuant); + Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); } @@ -150,24 +185,32 @@ Node RemoveITE::run(TNode node, std::vector<Node>& output, } } -Node RemoveITE::replace(TNode node, bool inQuant) const { - if(node.isVar() || node.isConst() || - (options::biasedITERemoval() && !containsTermITE(node))){ +Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { + //if(node.isVar() || node.isConst()){ + // (options::biasedITERemoval() && !containsTermITE(node))){ + //if(node.isVar()){ + // return Node(node); + //} + if( node.getKind()==kind::INST_PATTERN_LIST ){ return Node(node); } // Check the cache NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant)); + int cv = cacheVal( inQuant, inTerm ); + ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv)); if(i != d_iteCache.end()) { Node cached = (*i).second; return cached.isNull() ? Node(node) : cached; } - // Remember that we're inside a quantifier if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + // Remember if we're inside a quantifier inQuant = true; - } + }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){ + // Remember if we're inside a term + inTerm = true; + } vector<Node> newChildren; bool somethingChanged = false; @@ -176,7 +219,7 @@ Node RemoveITE::replace(TNode node, bool inQuant) const { } // Replace in children for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = replace(*it, inQuant); + Node newChild = replace(*it, inQuant, inTerm); somethingChanged |= (newChild != *it); newChildren.push_back(newChild); } diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h index c0a46c316..e629c93d7 100644 --- a/src/smt/ite_removal.h +++ b/src/smt/ite_removal.h @@ -35,15 +35,15 @@ namespace theory { typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap; -class RemoveITE { - typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache; +class RemoveTermFormulas { + typedef context::CDInsertHashMap< std::pair<Node, int>, Node, PairHashFunction<Node, int, NodeHashFunction, BoolHashFunction> > ITECache; ITECache d_iteCache; - + static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); } public: - RemoveITE(context::UserContext* u); - ~RemoveITE(); + RemoveTermFormulas(context::UserContext* u); + ~RemoveTermFormulas(); /** * Removes the ITE nodes by introducing skolem variables. All @@ -65,13 +65,13 @@ public: * ite created in conjunction with that skolem variable. */ Node run(TNode node, std::vector<Node>& additionalAssertions, - IteSkolemMap& iteSkolemMap, bool inQuant); + IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm); /** * Substitute under node using pre-existing cache. Do not remove * any ITEs not seen during previous runs. */ - Node replace(TNode node, bool inQuant = false) const; + Node replace(TNode node, bool inQuant = false, bool inTerm = false) const; /** Returns true if e contains a term ite. */ bool containsTermITE(TNode e) const; @@ -82,7 +82,7 @@ public: /** Garbage collects non-context dependent data-structures. */ void garbageCollect(); - /** Return the RemoveITE's containsVisitor. */ + /** Return the RemoveTermFormulas's containsVisitor. */ theory::ContainsTermITEVisitor* getContainsVisitor(); private: diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index 5988d81f9..0076b9de9 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -25,209 +25,6 @@ using namespace std; namespace CVC4 { namespace smt { -Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { - if(n.getType().isSubtypeOf(asType)) { - // good to go, we have the right type - return n; - } - if(n.getKind() == kind::LAMBDA) { - Assert(asType.isFunction()); - Node rhs = rewriteAs(n[1], asType[1]); - Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs); - Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl; - Debug("boolean-terms") << "need type " << asType << endl; - // Assert(out.getType() == asType); - return out; - } - if(!n.isConst()) { - // we don't handle non-const right now - return n; - } - if(asType.isBoolean()) { - if(n.getType().isBitVector(1u)) { - // type mismatch: should only happen for Boolean-term conversion under - // datatype constructor applications; rewrite from BV(1) back to Boolean - bool tf = (n.getConst<BitVector>().getValue() == 1); - return NodeManager::currentNM()->mkConst(tf); - } - if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) { - // type mismatch: should only happen for Boolean-term conversion under - // datatype constructor applications; rewrite from datatype back to Boolean - Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); - Assert(n.getNumChildren() == 0); - // we assume (by construction) false is first; see boolean_terms.cpp - bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1); - Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl; - return NodeManager::currentNM()->mkConst(tf); - } - } - if(n.getType().isBoolean()) { - bool tf = n.getConst<bool>(); - if(asType.isBitVector(1u)) { - return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u)); - } - if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) { - const Datatype& asDatatype = asType.getDatatype(); - return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor()); - } - } - Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl; - if(n.getType().isArray()) { - Assert(asType.isArray()); - if(n.getKind() == kind::STORE) { - return NodeManager::currentNM()->mkNode(kind::STORE, - rewriteAs(n[0], asType), - rewriteAs(n[1], asType[0]), - rewriteAs(n[2], asType[1])); - } - Assert(n.getKind() == kind::STORE_ALL); - const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>(); - Node val = rewriteAs(asa.getExpr(), asType[1]); - return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr())); - } - if( n.getType().isSet() ){ - if( n.getKind()==kind::UNION ){ - std::vector< Node > children; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - children.push_back( rewriteAs( n[i], asType ) ); - } - return NodeManager::currentNM()->mkNode(kind::UNION,children); - } - } - if(n.getType().isParametricDatatype() && - n.getType().isInstantiatedDatatype() && - asType.isParametricDatatype() && - asType.isInstantiatedDatatype() && - n.getType()[0] == asType[0]) { - // Here, we're doing something like rewriting a (Pair BV1 BV1) as a - // (Pair Bool Bool). - const Datatype* dt2 = &asType[0].getDatatype(); - std::vector<TypeNode> fromParams, toParams; - for(unsigned i = 0; i < dt2->getNumParameters(); ++i) { - fromParams.push_back(TypeNode::fromType(dt2->getParameter(i))); - toParams.push_back(asType[i + 1]); - } - Assert(dt2 == &Datatype::datatypeOf(n.getOperator().toExpr())); - size_t ctor_ix = Datatype::indexOf(n.getOperator().toExpr()); - NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR); - appctorb << (*dt2)[ctor_ix].getConstructor(); - for(size_t j = 0; j < n.getNumChildren(); ++j) { - TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[ctor_ix][j].getSelector().getType()).getRangeType()); - asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end()); - appctorb << rewriteAs(n[j], asType); - } - Node out = appctorb; - return out; - } - if(asType.getNumChildren() != n.getNumChildren() || - n.getMetaKind() == kind::metakind::CONSTANT) { - return n; - } - NodeBuilder<> b(n.getKind()); - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { - b << n.getOperator(); - } - TypeNode::iterator t = asType.begin(); - for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) { - Assert(t != asType.end()); - b << rewriteAs(*i, *t); - } - Assert(t == asType.end()); - Debug("boolean-terms") << "+++ constructing " << b << endl; - Node out = b; - return out; -} - -void ModelPostprocessor::visit(TNode current, TNode parent) { - Debug("tuprec") << "visiting " << current << endl; - Assert(!alreadyVisited(current, TNode::null())); - bool rewriteChildren = false; - if(current.getKind() == kind::APPLY_CONSTRUCTOR && - ( current.getOperator().hasAttribute(BooleanTermAttr()) || - ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION && - current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) { - NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); - Node realOp; - if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) { - TNode oldAsc = current.getOperator().getOperator(); - Debug("boolean-terms") << "old asc: " << oldAsc << endl; - Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr()); - Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType())); - Debug("boolean-terms") << "new asc: " << newAsc << endl; - if(newCons.getType().getRangeType().isParametricDatatype()) { - vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes(); - vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes(); - Assert(oldParams.size() == newParams.size() && oldParams.size() > 0); - newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType())); - } - realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons); - } else { - realOp = current.getOperator().getAttribute(BooleanTermAttr()); - } - b << realOp; - Debug("boolean-terms") << "+ op " << b.getOperator() << endl; - TypeNode::iterator j = realOp.getType().begin(); - for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) { - Assert(j != realOp.getType().end()); - Assert(alreadyVisited(*i, TNode::null())); - TNode repl = d_nodes[*i]; - repl = repl.isNull() ? *i : repl; - Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl; - b << rewriteAs(repl, *j); - } - Node n = b; - Debug("boolean-terms") << "model-post: " << current << endl - << "- returning " << n << endl; - d_nodes[current] = n; - return; - //all kinds with children that can occur in nodes in a model go here - } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION || - current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) { - rewriteChildren = true; - } - if( rewriteChildren ){ - // rewrite based on children - bool self = true; - for(size_t i = 0; i < current.getNumChildren(); ++i) { - Assert(d_nodes.find(current[i]) != d_nodes.end()); - if(!d_nodes[current[i]].isNull()) { - self = false; - break; - } - } - if(self) { - Debug("tuprec") << "returning self for kind " << current.getKind() << endl; - // rewrite to self - d_nodes[current] = Node::null(); - } else { - // rewrite based on children - NodeBuilder<> nb(current.getKind()); - if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { - TNode op = current.getOperator(); - Node realOp; - if(op.getAttribute(BooleanTermAttr(), realOp)) { - nb << realOp; - } else { - nb << op; - } - } - for(size_t i = 0; i < current.getNumChildren(); ++i) { - Assert(d_nodes.find(current[i]) != d_nodes.end()); - TNode rw = d_nodes[current[i]]; - if(rw.isNull()) { - rw = current[i]; - } - nb << rw; - } - d_nodes[current] = nb; - Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl; - } - } else { - Debug("tuprec") << "returning self for kind " << current.getKind() << endl; - // rewrite to self - d_nodes[current] = Node::null(); - } -}/* ModelPostprocessor::visit() */ } /* namespace smt */ } /* namespace CVC4 */ diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h index d9e749677..a354315ef 100644 --- a/src/smt/model_postprocessor.h +++ b/src/smt/model_postprocessor.h @@ -24,28 +24,6 @@ namespace CVC4 { namespace smt { -class ModelPostprocessor { - std::hash_map<TNode, Node, TNodeHashFunction> d_nodes; - -public: - typedef Node return_type; - - Node rewriteAs(TNode n, TypeNode asType); - - bool alreadyVisited(TNode current, TNode parent) { - return d_nodes.find(current) != d_nodes.end(); - } - - void visit(TNode current, TNode parent); - - void start(TNode n) { } - - Node done(TNode n) { - Assert(alreadyVisited(n, TNode::null())); - TNode retval = d_nodes[n]; - return retval.isNull() ? n : retval; - } -};/* class ModelPostprocessor */ }/* CVC4::smt namespace */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e647c45d1..cefef9345 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -185,8 +185,6 @@ public: struct SmtEngineStatistics { /** time spent in definition-expansion */ TimerStat d_definitionExpansionTime; - /** time spent in Boolean term rewriting */ - TimerStat d_rewriteBooleanTermsTime; /** time spent in non-clausal simplification */ TimerStat d_nonclausalSimplificationTime; /** time spent in miplib pass */ @@ -233,7 +231,6 @@ struct SmtEngineStatistics { SmtEngineStatistics() : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), - d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_miplibPassTime("smt::SmtEngine::miplibPassTime"), d_numMiplibAssertionsRemoved("smt::SmtEngine::numMiplibAssertionsRemoved", 0), @@ -258,7 +255,6 @@ struct SmtEngineStatistics { { smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime); - smtStatisticsRegistry()->registerStat(&d_rewriteBooleanTermsTime); smtStatisticsRegistry()->registerStat(&d_nonclausalSimplificationTime); smtStatisticsRegistry()->registerStat(&d_miplibPassTime); smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved); @@ -284,7 +280,6 @@ struct SmtEngineStatistics { ~SmtEngineStatistics() { smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime); - smtStatisticsRegistry()->unregisterStat(&d_rewriteBooleanTermsTime); smtStatisticsRegistry()->unregisterStat(&d_nonclausalSimplificationTime); smtStatisticsRegistry()->unregisterStat(&d_miplibPassTime); smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved); @@ -510,9 +505,6 @@ class SmtEnginePrivate : public NodeManagerListener { /** Size of assertions array when preprocessing starts */ unsigned d_realAssertionsEnd; - /** The converter for Boolean terms -> BITVECTOR(1). */ - BooleanTermConverter* d_booleanTermConverter; - /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; bool d_propagatorNeedsFinish; @@ -567,7 +559,7 @@ public: IteSkolemMap d_iteSkolemMap; /** Instance of the ITE remover */ - RemoveITE d_iteRemover; + RemoveTermFormulas d_iteRemover; private: @@ -676,7 +668,6 @@ public: d_listenerRegistrations(new ListenerRegistrationList()), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), - d_booleanTermConverter(NULL), d_propagator(d_nonClausalLearnedLiterals, true, true), d_propagatorNeedsFinish(false), d_assertions(), @@ -756,10 +747,6 @@ public: d_propagator.finish(); d_propagatorNeedsFinish = false; } - if(d_booleanTermConverter != NULL) { - delete d_booleanTermConverter; - d_booleanTermConverter = NULL; - } d_smt.d_nodeManager->unsubscribeEvents(this); } @@ -859,11 +846,6 @@ public: throw(TypeCheckingException, LogicException, UnsafeInterruptException); /** - * Rewrite Boolean terms in a Node. - */ - Node rewriteBooleanTerms(TNode n); - - /** * Simplify node "in" by expanding definitions and applying any * substitutions learned from preprocessing. */ @@ -1447,6 +1429,15 @@ void SmtEngine::setDefaults() { d_logic = log; d_logic.lock(); } + if(d_logic.isTheoryEnabled(THEORY_ARRAY) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) { + if(!d_logic.isTheoryEnabled(THEORY_UF)) { + LogicInfo log(d_logic.getUnlockedCopy()); + Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl; + log.enableTheory(THEORY_UF); + d_logic = log; + d_logic.lock(); + } + } // by default, symmetry breaker is on only for QF_UF if(! options::ufSymmetryBreaker.wasSetByUser()) { @@ -2918,7 +2909,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { for (; pos != newSubstitutions.end(); ++pos) { // Add back this substitution as an assertion TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second); - Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs); + Node n = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs); substitutionsBuilder << n; Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl; } @@ -3775,42 +3766,6 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, return false; } -Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) { - TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime); - - spendResource(options::preprocessStep()); - - if(d_booleanTermConverter == NULL) { - // This needs to be initialized _after_ the whole SMT framework is in place, subscribed - // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype - // definition, and not dump it properly. - d_booleanTermConverter = new BooleanTermConverter(d_smt); - } - Node retval = d_booleanTermConverter->rewriteBooleanTerms(n); - if(retval != n) { - switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { - case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: - case booleans::BOOLEAN_TERM_CONVERT_NATIVE: - if(!d_smt.d_logic.isTheoryEnabled(THEORY_BV)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_BV); - d_smt.d_logic.lock(); - } - break; - case booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: - if(!d_smt.d_logic.isTheoryEnabled(THEORY_DATATYPES)) { - d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); - d_smt.d_logic.enableTheory(THEORY_DATATYPES); - d_smt.d_logic.lock(); - } - break; - default: - Unhandled(mode); - } - } - return retval; -} - void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); spendResource(options::preprocessStep()); @@ -3904,15 +3859,6 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-abstraction", d_assertions); } - dumpAssertions("pre-boolean-terms", d_assertions); - { - Chat() << "rewriting Boolean terms..." << endl; - for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) { - d_assertions.replace(i, rewriteBooleanTerms(d_assertions[i])); - } - } - dumpAssertions("post-boolean-terms", d_assertions); - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; dumpAssertions("pre-constrain-subtypes", d_assertions); @@ -4523,6 +4469,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec }/* SmtEngine::assertFormula() */ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { +/* ModelPostprocessor mpost; NodeVisitor<ModelPostprocessor> visitor; Node value = visitor.run(mpost, node); @@ -4534,6 +4481,8 @@ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl; } return realValue; + */ + return node; } Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { @@ -4627,8 +4576,9 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin // used by the Model classes. It's not clear to me exactly how these // two are different, but they need to be unified. This ugly hack here // is to fix bug 554 until we can revamp boolean-terms and models [MGD] + + //AJR : necessary? if(!n.getType().isFunction()) { - n = d_private->rewriteBooleanTerms(n); n = Rewriter::rewrite(n); } @@ -4732,7 +4682,6 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptExce // Expand, then normalize hash_map<Node, Node, NodeHashFunction> cache; Node n = d_private->expandDefinitions(*i, cache); - n = d_private->rewriteBooleanTerms(n); n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index cb8cd8dca..da69436f1 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -109,11 +109,7 @@ bool ArithCongruenceManager::ArithCongruenceNotify::eqNotifyTriggerTermEquality( } void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyConstantTermMerge(TNode t1, TNode t2) { Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; - if (t1.getKind() == kind::CONST_BOOLEAN) { - d_acm.propagate(t1.iffNode(t2)); - } else { - d_acm.propagate(t1.eqNode(t2)); - } + d_acm.propagate(t1.eqNode(t2)); } void ArithCongruenceManager::ArithCongruenceNotify::eqNotifyNewClass(TNode t) { d_acm.eqNotifyNewClass(t); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 7946fea59..f9b97d524 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -247,16 +247,14 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck for (j = leftWrites - 1; j > i; --j) { index_j = write_j[1]; if (!ppCheck || !ppDisequal(index_i, index_j)) { - Node hyp2(index_i.getType() == nm->booleanType()? - index_i.iffNode(index_j) : index_i.eqNode(index_j)); + Node hyp2(index_i.eqNode(index_j)); hyp << hyp2.notNode(); } write_j = write_j[0]; } Node r1 = nm->mkNode(kind::SELECT, e1, index_i); - conc = (r1.getType() == nm->booleanType())? - r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]); + conc = r1.eqNode(write_i[2]); if (hyp.getNumChildren() != 0) { if (hyp.getNumChildren() == 1) { conc = hyp.getChild(0).impNode(conc); @@ -356,8 +354,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs case kind::NOT: { d_ppFacts.push_back(in); - Assert(in[0].getKind() == kind::EQUAL || - in[0].getKind() == kind::IFF ); + Assert(in[0].getKind() == kind::EQUAL ); Node a = in[0][0]; Node b = in[0][1]; d_ppEqualityEngine.assertEquality(in[0], false, in); @@ -403,7 +400,7 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::E TNode atom = polarity ? literal : literal[0]; //eq::EqProof * eqp = new eq::EqProof; // eq::EqProof * eqp = NULL; - if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if (atom.getKind() == kind::EQUAL) { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, proof); } else { d_equalityEngine.explainPredicate(atom, polarity, assumptions, proof); @@ -2235,11 +2232,7 @@ void TheoryArrays::conflict(TNode a, TNode b) { Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl; eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL; - if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b), proof); - } else { - d_conflictNode = explain(a.eqNode(b), proof); - } + d_conflictNode = explain(a.eqNode(b), proof); if (!d_inCheckModel) { ProofArray* proof_array = NULL; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 77c5928f0..a1d275364 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -296,7 +296,13 @@ class TheoryArrays : public Theory { } bool eqNotifyTriggerPredicate(TNode predicate, bool value) { - Unreachable(); + Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; + // Just forward to arrays + if (value) { + return d_arrays.propagate(predicate); + } else { + return d_arrays.propagate(predicate.notNode()); + } } bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 2726f386b..e63c224a0 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -33,7 +33,7 @@ void setMostFrequentValue(TNode store, TNode value); void setMostFrequentValueCount(TNode store, uint64_t count); static inline Node mkEqNode(Node a, Node b) { - return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b); + return a.eqNode(b); } class TheoryArraysRewriter { @@ -377,8 +377,7 @@ public: } break; } - case kind::EQUAL: - case kind::IFF: { + case kind::EQUAL:{ if(node[0] == node[1]) { Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl; return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); @@ -483,8 +482,7 @@ public: } break; } - case kind::EQUAL: - case kind::IFF: { + case kind::EQUAL:{ if(node[0] == node[1]) { Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl; return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 297ff6d9f..8e9116543 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -135,7 +135,8 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) { } } break; - case kind::IFF: + case kind::EQUAL: + Assert( parent[0].getType().isBoolean() ); if (parentAssignment) { // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment]) if (isAssigned(parent[0])) { @@ -285,7 +286,8 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) { } } break; - case kind::IFF: + case kind::EQUAL: + Assert( parent[0].getType().isBoolean() ); if (isAssigned(parent[0]) && isAssigned(parent[1])) { // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment)) assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1])); diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index ad45e3cbb..9d7b3fbd6 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -30,7 +30,6 @@ enumerator BOOLEAN_TYPE \ operator NOT 1 "logical not" operator AND 2: "logical and (N-ary)" -operator IFF 2 "logical equivalence (exactly two parameters)" operator IMPLIES 2 "logical implication (exactly two parameters)" operator OR 2: "logical or (N-ary)" operator XOR 2 "exclusive or (exactly two parameters)" @@ -40,7 +39,6 @@ typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule typerule NOT ::CVC4::theory::boolean::BooleanTypeRule typerule AND ::CVC4::theory::boolean::BooleanTypeRule -typerule IFF ::CVC4::theory::boolean::BooleanTypeRule typerule IMPLIES ::CVC4::theory::boolean::BooleanTypeRule typerule OR ::CVC4::theory::boolean::BooleanTypeRule typerule XOR ::CVC4::theory::boolean::BooleanTypeRule diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index d483ba105..b0f2efcda 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -56,6 +56,22 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti return PP_ASSERT_STATUS_SOLVED; } +/* +void TheoryBool::check(Effort level) { + if (done() && !fullEffort(level)) { + return; + } + while (!done()) + { + // Get all the assertions + Assertion assertion = get(); + TNode fact = assertion.assertion; + Trace("ajr-bool") << "Assert : " << fact << std::endl; + } + if( Theory::fullEffort(level) ){ + } +} +*/ }/* CVC4::theory::booleans namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index eef379bf9..353143c43 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -35,6 +35,8 @@ public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); + //void check(Effort); + std::string identify() const { return std::string("TheoryBool"); } };/* class TheoryBool */ diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index dc5f655aa..32f69e037 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -173,7 +173,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0])); break; } - case kind::IFF: case kind::EQUAL: { // rewrite simple cases of IFF if(n[0] == tt) { @@ -318,7 +317,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { int parityTmp; if ((parityTmp = equalityParity(n[1], n[2])) != 0) { - Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].iffNode(n[1]); + Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]); Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp << " " << n << ": " << resp << std::endl; return RewriteResponse(REWRITE_AGAIN, resp); diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 300a2b0d4..a2fb3f3f6 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -32,7 +32,7 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) { if(in.getNumChildren() == 2) { // if this is the case exactly 1 != pair will be generated so the // AND is not required - Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ? kind::IFF : kind::EQUAL, in[0], in[1]); + Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, in[0], in[1]); Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); return neq; } @@ -42,7 +42,7 @@ Node TheoryBuiltinRewriter::blastDistinct(TNode in) { for(TNode::iterator i = in.begin(); i != in.end(); ++i) { TNode::iterator j = i; while(++j != in.end()) { - Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ? kind::IFF : kind::EQUAL, *i, *j); + Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, *i, *j); Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); diseqs.push_back(neq); } diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index af25feaa5..85adfb41c 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -86,10 +86,6 @@ class EqualityTypeRule { throw TypeCheckingExceptionPrivate(n, ss.str()); } - - if ( lhsType == booleanType && rhsType == booleanType ) { - throw TypeCheckingExceptionPrivate(n, "equality between two boolean terms (use IFF instead)"); - } } return booleanType; } diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index bb2c403aa..934e2fffd 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -194,15 +194,6 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { } break; } - case kind::IFF: - { - Assert (node.getNumChildren() == 2); - Abc_Obj_t* child1 = bbFormula(node[0]); - Abc_Obj_t* child2 = bbFormula(node[1]); - - result = mkIff(child1, child2); - break; - } case kind::XOR: { result = bbFormula(node[0]); @@ -247,6 +238,18 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) { result = mkInput(node); break; } + case kind::EQUAL: + { + if( node[0].getType().isBoolean() ){ + Assert (node.getNumChildren() == 2); + Abc_Obj_t* child1 = bbFormula(node[0]); + Abc_Obj_t* child2 = bbFormula(node[1]); + + result = mkIff(child1, child2); + break; + } + //else, continue... + } default: bbAtom(node); result = getBBAtom(node); diff --git a/src/theory/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h index a63c548a2..baa85f64b 100644 --- a/src/theory/bv/bitblast_utils.h +++ b/src/theory/bv/bitblast_utils.h @@ -119,7 +119,7 @@ Node mkXor<Node>(Node a, Node b) { template <> inline Node mkIff<Node>(Node a, Node b) { - return NodeManager::currentNM()->mkNode(kind::IFF, a, b); + return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b); } template <> inline diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index b7e973928..60515b2d1 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -507,7 +507,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) { bool changed = subst.addSubstitution(var, new_right, reason); if (Dump.isOn("bv-algebraic")) { - Node query = utils::mkNot(utils::mkNode(kind::IFF, fact, utils::mkNode(kind::EQUAL, var, new_right))); + Node query = utils::mkNot(utils::mkNode(kind::EQUAL, fact, utils::mkNode(kind::EQUAL, var, new_right))); Dump("bv-algebraic") << EchoCommand("ThoeryBV::AlgebraicSolver::substitution explanation"); Dump("bv-algebraic") << PushCommand(); Dump("bv-algebraic") << AssertCommand(query.toExpr()); diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 36772406d..b38352b77 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -101,7 +101,7 @@ Node BvToBoolPreprocessor::convertBvAtom(TNode node) { Assert (utils::getSize(node[1]) == 1); Node a = convertBvTerm(node[0]); Node b = convertBvTerm(node[1]); - Node result = utils::mkNode(kind::IFF, a, b); + Node result = utils::mkNode(kind::EQUAL, a, b); Debug("bv-to-bool") << "BvToBoolPreprocessor::convertBvAtom " << node <<" => " << result << "\n"; ++(d_statistics.d_numAtomsLifted); diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 2ceca7423..053986b8c 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -109,7 +109,7 @@ void EagerBitblaster::bbAtom(TNode node) { } // asserting that the atom is true iff the definition holds - Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); + Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb); AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); storeBBAtom(node, atom_bb); diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index fd21456ee..1477f183e 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -125,7 +125,7 @@ void TLazyBitblaster::bbAtom(TNode node) { atom_bb = utils::mkAnd(atoms); } Assert (!atom_bb.isNull()); - Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); + Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb); storeBBAtom(node, atom_bb); d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); return; @@ -141,7 +141,7 @@ void TLazyBitblaster::bbAtom(TNode node) { } // asserting that the atom is true iff the definition holds - Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); + Node atom_definition = utils::mkNode(kind::EQUAL, node, atom_bb); storeBBAtom(node, atom_bb); d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); } diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 7200d1dec..aaa3c561d 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -383,12 +383,7 @@ public: std::ostringstream os; os << "RewriteRule <"<<rule<<">; expect unsat"; - Node condition; - if (result.getType().isBoolean()) { - condition = node.iffNode(result).notNode(); - } else { - condition = node.eqNode(result).notNode(); - } + Node condition = node.eqNode(result).notNode(); Dump("bv-rewrites") << CommentCommand(os.str()) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index e58289568..0d58233c9 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -251,7 +251,7 @@ public: Trace("datatypes-rewrite-debug") << "Clash constants : " << n1 << " " << n2 << std::endl; return true; }else{ - Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n1, n2 ); rew.push_back( eq ); } } diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index fe07e44da..f5ae05bc3 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -492,10 +492,11 @@ bool SygusSplit::considerSygusSplitKind( const Datatype& dt, const Datatype& pdt rt.d_req_kind = OR;reqk = NOT; }else if( k==OR ){ rt.d_req_kind = AND;reqk = NOT; - }else if( k==IFF ) { + //AJR : eliminate this if we eliminate xor + }else if( k==EQUAL ) { rt.d_req_kind = XOR; }else if( k==XOR ) { - rt.d_req_kind = IFF; + rt.d_req_kind = EQUAL; }else if( k==ITE ){ rt.d_req_kind = ITE;reqkc[1] = NOT;reqkc[2] = NOT; rt.d_children[0].d_req_type = d_tds->getArgType( dt[c], 0 ); @@ -1331,7 +1332,7 @@ Node SygusSymBreak::getSeparationTemplate( TypeNode tn, Node rep_prog, Node anc bool SygusSymBreak::processConstantArg( TypeNode tnp, const Datatype & pdt, int pc, Kind k, int i, Node arg, std::map< unsigned, bool >& rlv ) { Assert( d_tds->hasKind( tnp, k ) ); - if( k==AND || k==OR || k==IFF || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){ + if( k==AND || k==OR || ( k==EQUAL && arg.getType().isBoolean() ) || k==XOR || k==IMPLIES || ( k==ITE && i==0 ) ){ return false; }else if( d_tds->isIdempotentArg( arg, k, i ) ){ if( pdt[pc].getNumArgs()==2 ){ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 3d114f9f1..8d2e5618f 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -422,7 +422,7 @@ void TheoryDatatypes::doPendingMerges(){ //do all pending merges int i=0; while( i<(int)d_pending_merge.size() ){ - Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF ); + Assert( d_pending_merge[i].getKind()==EQUAL ); merge( d_pending_merge[i][0], d_pending_merge[i][1] ); i++; } @@ -507,15 +507,9 @@ void TheoryDatatypes::preRegisterTerm(TNode n) { d_equalityEngine.addTriggerPredicate(n); break; default: - // Maybe it's a predicate - if (n.getType().isBoolean()) { - // Get triggered for both equal and dis-equal - d_equalityEngine.addTriggerPredicate(n); - } else { - // Function applications/predicates - d_equalityEngine.addTerm(n); - //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES); - } + // Function applications/predicates + d_equalityEngine.addTerm(n); + //d_equalityEngine.addTriggerTerm(n, THEORY_DATATYPES); break; } flushPendingFacts(); @@ -634,11 +628,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) { void TheoryDatatypes::addSharedTerm(TNode t) { Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): " << t << " " << t.getType().isBoolean() << endl; - //if( t.getType().isBoolean() ){ - //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES); - //}else{ d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES); - //} Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl; } @@ -703,7 +693,7 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){ Debug("datatypes-explain") << "Explain " << literal << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if (atom.getKind() == kind::EQUAL) { explainEquality( atom[0], atom[1], polarity, assumptions ); } else if( atom.getKind() == kind::AND && polarity ){ for( unsigned i=0; i<atom.getNumChildren(); i++ ){ @@ -731,11 +721,7 @@ Node TheoryDatatypes::explain( std::vector< Node >& lits ) { /** Conflict when merging two constants */ void TheoryDatatypes::conflict(TNode a, TNode b){ - if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain( a.iffNode(b) ); - } else { - d_conflictNode = explain( a.eqNode(b) ); - } + d_conflictNode = explain( a.eqNode(b) ); Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; @@ -812,8 +798,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ for( unsigned i=0; i<deq_cand.size(); i++ ){ if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){ conf = true; - Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL, - deq_cand[i].first, deq_cand[i].second ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, deq_cand[i].first, deq_cand[i].second ); exp.push_back( eq.negate() ); } } @@ -835,7 +820,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //do unification for( int i=0; i<(int)cons1.getNumChildren(); i++ ) { if( !areEqual( cons1[i], cons2[i] ) ){ - Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] ); + Node eq = cons1[i].eqNode( cons2[i] ); d_pending.push_back( eq ); d_pending_exp[ eq ] = unifEq; Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl; @@ -1284,7 +1269,7 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) { if( !r.isNull() ){ Node rr = Rewriter::rewrite( r ); if( use_s!=rr ){ - Node eq = rr.getType().isBoolean() ? use_s.iffNode( rr ) : use_s.eqNode( rr ); + Node eq = use_s.eqNode( rr ); Node eq_exp; if( options::dtRefIntro() ){ eq_exp = d_true; @@ -1697,7 +1682,7 @@ void TheoryDatatypes::collectTerms( Node n ) { if( children.empty() ){ lem = n.negate(); }else{ - lem = NodeManager::currentNM()->mkNode( IFF, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) ); + lem = NodeManager::currentNM()->mkNode( EQUAL, n, children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children ) ); } Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; //d_pending.push_back( lem ); @@ -1716,7 +1701,7 @@ void TheoryDatatypes::processNewTerm( Node n ){ //see if it is rewritten to be something different Node rn = Rewriter::rewrite( n ); if( rn!=n && !areEqual( rn, n ) ){ - Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n ); + Node eq = rn.eqNode( n ); d_pending.push_back( eq ); d_pending_exp[ eq ] = d_true; Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl; @@ -2053,7 +2038,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); addLemma = dt.involvesExternalType(); } - }else if( n.getKind()==LEQ || n.getKind()==IFF || n.getKind()==OR ){ + }else if( n.getKind()==LEQ || n.getKind()==OR ){ addLemma = true; } if( addLemma ){ @@ -2110,7 +2095,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - if( !eqc.getType().isBoolean() ){ + //if( !eqc.getType().isBoolean() ){ if( eqc.getType().isDatatype() ){ Trace( c ) << "DATATYPE : "; } @@ -2155,7 +2140,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){ Trace( c ) << std::endl; } } - } + //} ++eqcs_i; } } diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index 126f3bfb8..419e5b4dd 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -313,7 +313,7 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed){ d_compressed[original] = skolem; d_compressed[compressed] = skolem; - Node iff = skolem.iffNode(rewritten); + Node iff = skolem.eqNode(rewritten); d_assertions->push_back(iff); ++(d_statistics.d_skolemsAdded); return skolem; diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index a00d6d8a1..a5fd34c64 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -72,7 +72,7 @@ Node AlphaEquivalenceNode::registerNode( AlphaEquivalenceNode* aen, QuantifiersE Trace("alpha-eq") << "Alpha equivalent : " << std::endl; Trace("alpha-eq") << " " << q << std::endl; Trace("alpha-eq") << " " << aen->d_quant << std::endl; - lem = q.iffNode( aen->d_quant ); + lem = q.eqNode( aen->d_quant ); }else{ //do not reduce annotated quantified formulas based on alpha equivalence } diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index c488e8c23..37fbff03a 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -138,7 +138,7 @@ bool BoundedIntegers::IntRangeModel::proxyCurrentRange() { if( d_ranges_proxied.find( curr )==d_ranges_proxied.end() ){ d_ranges_proxied[curr] = true; Assert( d_range_literal.find( curr )!=d_range_literal.end() ); - Node lem = NodeManager::currentNM()->mkNode( IFF, d_range_literal[curr].negate(), + Node lem = NodeManager::currentNM()->mkNode( EQUAL, d_range_literal[curr].negate(), NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(curr) ) ) ); Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << lem << std::endl; d_bi->getQuantifiersEngine()->addLemma( lem ); diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 8e8f34cac..7c9a6196f 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -227,7 +227,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){ CandidateGeneratorQELitDeq::CandidateGeneratorQELitDeq( QuantifiersEngine* qe, Node mpat ) : CandidateGenerator( qe ), d_match_pattern( mpat ){ - Assert( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ); + Assert( d_match_pattern.getKind()==EQUAL ); d_match_pattern_type = d_match_pattern[0].getType(); } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index f4b63f929..9903f14aa 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -710,13 +710,13 @@ Node CegInstantiation::getEagerUnfold( Node n, std::map< Node, Node >& visited ) } for( unsigned j=1; j<n.getNumChildren(); j++ ){ Node nc = getEagerUnfold( n[j], visited ); - if( var_list[j-1].getType().isBoolean() ){ - //TODO: remove this case when boolean term conversion is eliminated - Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); - subs.push_back( nc.eqNode( c ) ); - }else{ - subs.push_back( nc ); - } + //if( var_list[j-1].getType().isBoolean() ){ + // //TODO: remove this case when boolean term conversion is eliminated + // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + // subs.push_back( nc.eqNode( c ) ); + //}else{ + subs.push_back( nc ); + //} Assert( subs[j-1].getType()==var_list[j-1].getType() ); } Assert( vars.size()==subs.size() ); diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 44ac135a7..92d62a177 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -758,13 +758,13 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int& Assert( d_single_inv_arg_sk.size()==varList.getNumChildren() ); for( unsigned i=0; i<d_single_inv_arg_sk.size(); i++ ){ Trace("csi-sol") << d_single_inv_arg_sk[i] << " "; - if( varList[i].getType().isBoolean() ){ - //TODO force boolean term conversion mode - Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); - vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) ); - }else{ - vars.push_back( d_single_inv_arg_sk[i] ); - } + //if( varList[i].getType().isBoolean() ){ + // //TODO force boolean term conversion mode + // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + // vars.push_back( d_single_inv_arg_sk[i].eqNode( c ) ); + //}else{ + vars.push_back( d_single_inv_arg_sk[i] ); + //} d_sol->d_varList.push_back( varList[i] ); } Trace("csi-sol") << std::endl; diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 5cc46d163..d93898a1e 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -215,7 +215,7 @@ Node CegConjectureSingleInvSol::flattenITEs( Node n, bool rec ) { if( n0.getKind()==ITE ){ n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), NodeManager::currentNM()->mkNode( AND, n0.negate(), n2 ) ); - }else if( n0.getKind()==IFF ){ + }else if( n0.getKind()==EQUAL ){ n0 = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, n0, n1 ), NodeManager::currentNM()->mkNode( AND, n0.negate(), n1.negate() ) ); }else{ @@ -271,7 +271,7 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo } }else if( n.getKind()==NOT ){ return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs ); - }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){ + }else if( pol && n.getKind()==EQUAL ){ getAssignEquality( n, vars, new_vars, new_subs ); } } @@ -279,7 +279,7 @@ bool CegConjectureSingleInvSol::getAssign( bool pol, Node n, std::map< Node, boo } bool CegConjectureSingleInvSol::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs ) { - Assert( eq.getKind()==IFF || eq.getKind()==EQUAL ); + Assert( eq.getKind()==EQUAL ); //try to find valid argument for( unsigned r=0; r<2; r++ ){ if( std::find( d_varList.begin(), d_varList.end(), eq[r] )!=d_varList.end() ){ @@ -492,7 +492,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st std::map< Node, bool >::iterator it = atoms.find( atom ); if( it==atoms.end() ){ atoms[atom] = pol; - if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){ + if( status==0 && atom.getKind()==EQUAL ){ if( pol==( sol.getKind()==AND ) ){ Trace("csi-simp") << " ...equality." << std::endl; if( getAssignEquality( atom, vars, new_vars, new_subs ) ){ @@ -567,7 +567,7 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st bool red = false; Node atom = children[i].getKind()==NOT ? children[i][0] : children[i]; bool pol = children[i].getKind()!=NOT; - if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){ + if( status==0 && atom.getKind()==EQUAL ){ if( pol!=( sol.getKind()==AND ) ){ std::vector< Node > tmp_vars; std::vector< Node > tmp_subs; @@ -848,15 +848,19 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in Node new_t; do{ new_t = Node::null(); - if( curr.getKind()==EQUAL && ( curr[0].getType().isInteger() || curr[0].getType().isReal() ) ){ - new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ), - NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) ); + if( curr.getKind()==EQUAL ){ + if( curr[0].getType().isInteger() || curr[0].getType().isReal() ){ + new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, curr[0], curr[1] ), + NodeManager::currentNM()->mkNode( LEQ, curr[1], curr[0] ) ); + }else if( curr[0].getType().isBoolean() ){ + new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), + NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) ); + }else{ + new_t = NodeManager::currentNM()->mkNode( NOT, NodeManager::currentNM()->mkNode( NOT, curr ) ); + } }else if( curr.getKind()==ITE ){ new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[2] ) ); - }else if( curr.getKind()==IFF ){ - new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, curr[0], curr[1] ), - NodeManager::currentNM()->mkNode( AND, curr[0].negate(), curr[1].negate() ) ); }else if( curr.getKind()==OR || curr.getKind()==AND ){ new_t = TermDb::simpleNegate( curr ).negate(); }else if( curr.getKind()==NOT ){ diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 61a20ad42..3dacfca3a 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -753,6 +753,12 @@ void CegInstantiator::processAssertions() { Trace("cbqi-proc") << "......add substitution : " << itae2->first << " -> " << itae2->second << std::endl; } } + }else if( atom.getKind()==BOOLEAN_TERM_VARIABLE ){ + if( std::find( d_aux_vars.begin(), d_aux_vars.end(), atom )!=d_aux_vars.end() ){ + Node val = NodeManager::currentNM()->mkConst( lit.getKind()!=NOT ); + aux_subs[ atom ] = val; + Trace("cbqi-proc") << "......add substitution : " << atom << " -> " << val << std::endl; + } } } } @@ -884,7 +890,7 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) d_is_nested_quant = true; }else if( visited.find( n )==visited.end() ){ visited[n] = true; - if( TermDb::isBoolConnective( n.getKind() ) ){ + if( TermDb::isBoolConnectiveTerm( n ) ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ collectCeAtoms( n[i], visited ); } @@ -940,7 +946,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st //remove ITEs IteSkolemMap iteSkolemMap; - d_qe->getTheoryEngine()->getIteRemover()->run(lems, iteSkolemMap); + d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap); //Assert( d_aux_vars.empty() ); d_aux_vars.clear(); d_aux_eq.clear(); @@ -965,6 +971,14 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } } } + /*else if( lems[i].getKind()==EQUAL && lems[i][0].getType().isBoolean() ){ + //Boolean terms + if( std::find( d_aux_vars.begin(), d_aux_vars.end(), lems[i][0] )!=d_aux_vars.end() ){ + Node v = lems[i][0]; + d_aux_eq[rlem][v] = lems[i][1]; + Trace("cbqi-debug") << " " << rlem << " implies " << v << " = " << lems[i][1] << std::endl; + } + }*/ lems[i] = rlem; } //collect atoms from all lemmas: we will only do bounds coming from original body diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index b6743724b..88b5f5fb1 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -327,7 +327,7 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ }else{ return 0; } - }else if( n.getKind()==IFF ){ + }else if( n.getKind()==EQUAL && n[0].getType().isBoolean() ){ int depIndex1; int eVal = evaluate( n[0], depIndex1, ri ); if( eVal!=0 ){ diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 9109aab8a..1172fb92c 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -49,7 +49,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { Trace("fmf-fun-def-debug") << "Process function " << n << ", body = " << bd << std::endl; if( !bd.isNull() ){ d_funcs.push_back( f ); - bd = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, n, bd ); + bd = NodeManager::currentNM()->mkNode( EQUAL, n, bd ); //create a sort S that represents the inputs of the function std::stringstream ss; @@ -97,7 +97,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions, bool doRewrite ) { for( unsigned i=0; i<assertions.size(); i++ ){ int is_fd = std::find( fd_assertions.begin(), fd_assertions.end(), i )!=fd_assertions.end() ? 1 : 0; //constant boolean function definitions do not add domain constraints - if( is_fd==0 || ( is_fd==1 && ( assertions[i][1].getKind()==EQUAL || assertions[i][1].getKind()==IFF ) ) ){ + if( is_fd==0 || ( is_fd==1 && assertions[i][1].getKind()==EQUAL ) ){ std::vector< Node > constraints; Trace("fmf-fun-def-rewrite") << "Rewriting " << assertions[i] << ", is_fd = " << is_fd << std::endl; Node n = simplifyFormula( assertions[i], true, true, constraints, is_fd==1 ? subs_head[i] : Node::null(), is_fd ); @@ -201,11 +201,7 @@ void FunDefFmf::simplifyTerm( Node n, std::vector< Node >& constraints ) { std::vector< Node > children; for( unsigned j=0; j<n.getNumChildren(); j++ ){ Node uz = NodeManager::currentNM()->mkNode( APPLY_UF, d_input_arg_inj[f][j], z ); - if( !n[j].getType().isBoolean() ){ - children.push_back( uz.eqNode( n[j] ) ); - }else{ - children.push_back( uz.iffNode( n[j] ) ); - } + children.push_back( uz.eqNode( n[j] ) ); } Node bd = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ); bd = bd.negate(); diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index 2a940f1fd..7cf9868bd 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -76,7 +76,7 @@ int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) { unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn ); Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl; return ngtt; -// }else if( d_match_pattern_getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ +// }else if( d_match_pattern_getKind()==EQUAL ){ }else{ return -1; @@ -90,7 +90,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< //we want to add the children of the NOT d_match_pattern = d_pattern[0]; } - if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ + if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){ //make sure the matching portion of the equality is on the LHS of d_pattern // and record what d_match_pattern is for( unsigned i=0; i<2; i++ ){ @@ -150,7 +150,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< //we will be scanning lists trying to find d_match_pattern.getOperator() d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern ); //if matching on disequality, inform the candidate generator not to match on eqc - if( d_pattern.getKind()==NOT && ( d_pattern[0].getKind()==IFF || d_pattern[0].getKind()==EQUAL ) ){ + if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){ ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel ); d_eq_class_rel = Node::null(); } @@ -166,7 +166,7 @@ void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< }else{ d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern ); } - }else if( ( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ) && + }else if( d_match_pattern.getKind()==EQUAL && d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){ //we will be producing candidates via literal matching heuristics if( d_pattern.getKind()!=NOT ){ @@ -253,10 +253,12 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi } }else{ if( pat.getKind()==EQUAL ){ - Assert( t.getType().isReal() ); - t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); - }else if( pat.getKind()==IFF ){ - t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) ); + if( t.getType().isBoolean() ){ + t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermDatabase()->d_true, t ) ); + }else{ + Assert( t.getType().isReal() ); + t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); + } }else if( pat.getKind()==GEQ ){ t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermDatabase()->d_one); }else if( pat.getKind()==GT ){ @@ -706,7 +708,7 @@ InstMatchGeneratorSimple::InstMatchGeneratorSimple( Node q, Node pat, Quantifier }else{ d_pol = true; } - if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){ + if( d_match_pattern.getKind()==EQUAL ){ d_eqc = d_match_pattern[1]; d_match_pattern = d_match_pattern[0]; Assert( !quantifiers::TermDb::hasInstConstAttr( d_eqc ) ); diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 1f68fb787..41099552d 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -366,8 +366,13 @@ bool EqualityQueryInstProp::isPropagateLiteral( Node n ) { return false; }else{ Kind ak = n.getKind()==NOT ? n[0].getKind() : n.getKind(); - Assert( ak!=NOT ); - return ak!=AND && ak!=OR && ak!=IFF && ak!=ITE; + if( ak==EQUAL ){ + Node atom = n.getKind() ? n[0] : n; + return !atom[0].getType().isBoolean(); + }else{ + Assert( ak!=NOT ); + return ak!=AND && ak!=OR && ak!=ITE; + } } } @@ -466,7 +471,7 @@ Node EqualityQueryInstProp::evaluateTermExp( Node n, std::vector< Node >& exp, s addArgument( c, args, watch, is_watch ); abort_i = i; break; - }else if( k==kind::AND || k==kind::OR || k==kind::ITE || k==IFF ){ + }else if( k==kind::AND || k==kind::OR || k==kind::ITE || ( k==EQUAL && n[0].getType().isBoolean() ) ){ Trace("qip-eval-debug") << "Adding argument " << c << " to " << k << ", isProp = " << newHasPol << std::endl; if( ( k==kind::AND || k==kind::OR ) && c.getKind()==k ){ //flatten diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 895a0c93c..0023f7d0f 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -193,7 +193,7 @@ void InstStrategyCbqi::reset_round( Theory::Effort effort ) { Assert( index<(int)d_nested_qe_waitlist[q].size() ); Node nq = d_nested_qe_waitlist[q][index]; Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts ); - Node dqelem = nq.iffNode( nqeqn ); + Node dqelem = nq.eqNode( nqeqn ); Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl; d_quantEngine->getOutputChannel().lemma( dqelem ); d_nested_qe_waitlist_proc[q] = index + 1; diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index c4bf61b28..f2ed81d8c 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -361,9 +361,9 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Assert( Trigger::isAtomicTrigger( pat ) ); if( pat.getType().isBoolean() && rpoleq.isNull() ){ if( options::literalMatchMode()==LITERAL_MATCH_USE ){ - pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); + pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate(); }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){ - pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==1 ) ); + pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) ); } }else{ Assert( !rpoleq.isNull() ); diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 976b81e60..96d682a77 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -147,7 +147,7 @@ bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, } bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ - return pol && ( n.getKind()==EQUAL || n.getKind()==IFF ); + return pol && n.getKind()==EQUAL; } bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { @@ -211,7 +211,7 @@ void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidat } Node QuantifierMacros::solveInEquality( Node n, Node lit ){ - if( lit.getKind()==IFF || lit.getKind()==EQUAL ){ + if( lit.getKind()==EQUAL ){ //return the opposite side of the equality if defined that way for( int i=0; i<2; i++ ){ if( lit[i]==n ){ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index a5ec16e3a..090f2735a 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -674,7 +674,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ std::vector< Node > tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); + Node eq = NodeManager::currentNM()->mkNode( EQUAL, lit, !phase ? fm->d_true : fm->d_false ); tr_terms.push_back( eq ); }else if( lit.getKind()==EQUAL ){ //collect trigger terms diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 1e484311c..420a3d2f7 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -622,7 +622,8 @@ bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) { if( n.getKind()==FORALL ){ //TODO? return true; - }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || n.getKind()==IFF ){ + }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || + ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) ){ for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !isPropagatingInstance( p, n[i] ) ){ return false; @@ -1098,7 +1099,7 @@ void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbva void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) { Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl; - bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==IFF ); + bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL ); if( isComm ){ std::map< int, std::vector< int > > c_to_vars; std::map< int, std::vector< int > > vars_to_c; @@ -1563,7 +1564,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { success = true; } } - }else if( d_n.getKind()==IFF ){ + }else if( d_n.getKind()==EQUAL ){ //construct match based on both children if( d_child_counter%2==0 ){ if( getChild( 0 )->getNextMatch( p, qi ) ){ @@ -1660,7 +1661,7 @@ bool MatchGen::getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vecto }else{ return getChild( d_child_counter )->getExplanation( p, qi, exp ); } - }else if( d_n.getKind()==IFF ){ + }else if( d_n.getKind()==EQUAL ){ for( unsigned i=0; i<2; i++ ){ if( !getChild( i )->getExplanation( p, qi, exp ) ){ return false; @@ -1861,7 +1862,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return TermDb::isBoolConnective( n.getKind() ) && ( n.getKind()!=ITE || n.getType().isBoolean() ) && n.getKind()!=SEP_STAR; + return TermDb::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR; } bool MatchGen::isHandledUfTerm( TNode n ) { @@ -1904,11 +1905,7 @@ d_conflict( c, false ) { } Node QuantConflictFind::mkEqNode( Node a, Node b ) { - if( a.getType().isBoolean() ){ - return a.iffNode( b ); - }else{ - return a.eqNode( b ); - } + return a.eqNode( b ); } //-------------------------------------------------- registration diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp index 3f89a799c..46a8b7ce2 100644 --- a/src/theory/quantifiers/quant_equality_engine.cpp +++ b/src/theory/quantifiers/quant_equality_engine.cpp @@ -93,7 +93,7 @@ void QuantEqualityEngine::assertNode( Node n ) { bool success = true; Node t1; Node t2; - if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL || lit.getKind()==IFF ){ + if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){ lit = getTermDatabase()->getCanonicalTerm( lit ); Trace("qee-debug") << "Canonical : " << lit << ", pol = " << pol << std::endl; if( lit.getKind()==APPLY_UF ){ @@ -102,28 +102,30 @@ void QuantEqualityEngine::assertNode( Node n ) { pol = true; lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 ); }else if( lit.getKind()==EQUAL ){ - t1 = lit[0]; - t2 = lit[1]; - }else if( lit.getKind()==IFF ){ - if( lit[0].getKind()==NOT ){ - t1 = lit[0][0]; - pol = !pol; + if( lit[0].getType().isBoolean() ){ + if( lit[0].getKind()==NOT ){ + t1 = lit[0][0]; + pol = !pol; + }else{ + t1 = lit[0]; + } + if( lit[1].getKind()==NOT ){ + t2 = lit[1][0]; + pol = !pol; + }else{ + t2 = lit[1]; + } + if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){ + t1 = getFunctionAppForPredicateApp( t1 ); + t2 = getFunctionAppForPredicateApp( t2 ); + lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 ); + }else{ + success = false; + } }else{ t1 = lit[0]; - } - if( lit[1].getKind()==NOT ){ - t2 = lit[1][0]; - pol = !pol; - }else{ t2 = lit[1]; } - if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){ - t1 = getFunctionAppForPredicateApp( t1 ); - t2 = getFunctionAppForPredicateApp( t2 ); - lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 ); - }else{ - success = false; - } } }else{ success = false; diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index c0595d3d9..163c576f7 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -201,7 +201,7 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind } Node QuantArith::solveEqualityFor( Node lit, Node v ) { - Assert( lit.getKind()==EQUAL || lit.getKind()==IFF ); + Assert( lit.getKind()==EQUAL ); //first look directly at sides TypeNode tn = lit[0].getType(); for( unsigned r=0; r<2; r++ ){ @@ -513,7 +513,7 @@ Node QuantEPR::mkEPRAxiom( TypeNode tn ) { std::vector< Node > disj; Node x = NodeManager::currentNM()->mkBoundVar( tn ); for( unsigned i=0; i<d_consts[tn].size(); i++ ){ - disj.push_back( NodeManager::currentNM()->mkNode( tn.isBoolean() ? IFF : EQUAL, x, d_consts[tn][i] ) ); + disj.push_back( NodeManager::currentNM()->mkNode( EQUAL, x, d_consts[tn][i] ) ); } Assert( !disj.empty() ); d_epr_axiom[tn] = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ), disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( OR, disj ) ); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index fcd8d1829..2b7e19c48 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -55,7 +55,6 @@ bool QuantifiersRewriter::isLiteral( Node n ){ case IMPLIES: case XOR: case ITE: - case IFF: return false; break; case EQUAL: @@ -251,7 +250,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { k = OR; negCh1 = true; }else if( ok==XOR ){ - k = IFF; + k = EQUAL; negCh1 = true; }else if( ok==NOT ){ if( body[0].getKind()==NOT ){ @@ -265,9 +264,9 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { k = OR; negAllCh = true; body = body[0]; - }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){ - k = IFF; - negCh1 = ( body[0].getKind()==IFF ); + }else if( body[0].getKind()==XOR || ( body[0].getKind()==EQUAL && body[0][0].getType().isBoolean() ) ){ + k = EQUAL; + negCh1 = ( body[0].getKind()==EQUAL ); body = body[0]; }else if( body[0].getKind()==ITE ){ k = body[0].getKind(); @@ -277,7 +276,7 @@ Node QuantifiersRewriter::computeElimSymbols( Node body ) { }else{ return body; } - }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){ + }else if( ( ok!=EQUAL || !body[0].getType().isBoolean() ) && ok!=ITE && ok!=AND && ok!=OR ){ //a literal return body; } @@ -410,8 +409,8 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ }else if( res==-1 ){ return getEntailedCond( n[2], currCond ); } - }else if( n.getKind()==IFF || n.getKind()==ITE ){ - unsigned start = n.getKind()==IFF ? 0 : 1; + }else if( ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) || n.getKind()==ITE ){ + unsigned start = n.getKind()==EQUAL ? 0 : 1; int res1 = 0; for( unsigned j=start; j<=(start+1); j++ ){ int res = getEntailedCond( n[j], currCond ); @@ -423,7 +422,7 @@ int getEntailedCond( Node n, std::map< Node, bool >& currCond ){ Assert( res!=0 ); if( n.getKind()==ITE ){ return res1==res ? res : 0; - }else if( n.getKind()==IFF ){ + }else if( n.getKind()==EQUAL ){ return res1==res ? 1 : -1; } } @@ -512,7 +511,7 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n Assert( !body.isNull() ); Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl; Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds ); - return Rewriter::rewrite( NodeManager::currentNM()->mkNode( h.getType().isBoolean() ? IFF : EQUAL, h, r ) ); + return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) ); }else{ return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds ); } @@ -773,7 +772,7 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){ } } if( options::condVarSplitQuant() ){ - if( body.getKind()==ITE || ( body.getKind()==IFF && options::condVarSplitQuantAgg() ) ){ + if( body.getKind()==ITE || ( body.getKind()==EQUAL && body[0].getType().isBoolean() && options::condVarSplitQuantAgg() ) ){ Assert( !qa.isFunDef() ); Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl; bool do_split = false; @@ -1100,7 +1099,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, s NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) ); return computePrenex( nn, args, nargs, pol, prenexAgg ); - }else if( prenexAgg && body.getKind()==kind::IFF ){ + }else if( prenexAgg && body.getKind()==kind::EQUAL && body[0].getType().isBoolean() ){ Node nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ), NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) ); @@ -1631,11 +1630,7 @@ Node QuantifiersRewriter::rewriteRewriteRule( Node r ) { case kind::RR_REWRITE: // Equality pattern.push_back( head ); - if( head.getType().isBoolean() ){ - body = head.iffNode(body); - }else{ - body = head.eqNode(body); - } + body = head.eqNode(body); break; case kind::RR_REDUCTION: case kind::RR_DEDUCTION: @@ -1780,7 +1775,7 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v //check if it contains a quantifier as a subterm //if so, we will write this node if( containsQuantifiers( n ) ){ - if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || n.getKind()==kind::IFF ){ + if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){ if( options::preSkolemQuantAgg() ){ Node nn; //must remove structure @@ -1788,12 +1783,10 @@ Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::v nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ), NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) ); - }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){ + }else if( n.getKind()==kind::EQUAL ){ nn = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ), NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) ); - }else if( n.getKind()==kind::IMPLIES ){ - nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ); } return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs ); } diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index ec1b41a98..3e6b0ffa9 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -230,27 +230,14 @@ void RewriteEngine::registerQuantifier( Node f ) { } std::vector< Node > cc; - //Node head = rr[2][0]; - //if( head!=d_true ){ - //Node head_eq = head.getType().isBoolean() ? head.iffNode( head ) : head.eqNode( head ); - //head_eq = head_eq.negate(); - //cc.push_back( head_eq ); - //Trace("rr-register-debug") << " head eq is " << head_eq << std::endl; - //} //add patterns for( unsigned i=1; i<f[2].getNumChildren(); i++ ){ std::vector< Node > nc; for( unsigned j=0; j<f[2][i].getNumChildren(); j++ ){ Node nn; Node nbv = NodeManager::currentNM()->mkBoundVar( f[2][i][j].getType() ); - if( f[2][i][j].getType().isBoolean() ){ - if( f[2][i][j].getKind()!=APPLY_UF ){ - nn = f[2][i][j].negate(); - }else{ - nn = f[2][i][j].iffNode( nbv ).negate(); - bvl.push_back( nbv ); - } - //nn = f[2][i][j].negate(); + if( f[2][i][j].getType().isBoolean() && f[2][i][j].getKind()!=APPLY_UF ){ + nn = f[2][i][j].negate(); }else{ nn = f[2][i][j].eqNode( nbv ).negate(); bvl.push_back( nbv ); diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 0bdfa2d24..d394c8fef 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -267,10 +267,10 @@ void TermDb::computeUfTerms( TNode f ) { }else{ if( at!=n && ee->areDisequal( at, n, false ) ){ std::vector< Node > lits; - lits.push_back( NodeManager::currentNM()->mkNode( at.getType().isBoolean() ? IFF : EQUAL, at, n ) ); + lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at, n ) ); for( unsigned i=0; i<at.getNumChildren(); i++ ){ if( at[i]!=n[i] ){ - lits.push_back( NodeManager::currentNM()->mkNode( at[i].getType().isBoolean() ? IFF : EQUAL, at[i], n[i] ).negate() ); + lits.push_back( NodeManager::currentNM()->mkNode( EQUAL, at[i], n[i] ).negate() ); } } Node lem = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode( OR, lits ); @@ -484,7 +484,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, Assert( !qy->extendsEngine() ); Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; Assert( n.getType().isBoolean() ); - if( n.getKind()==EQUAL ){ + if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy ); if( !n1.isNull() ){ TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy ); @@ -518,10 +518,11 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, } } return !simPol; - }else if( n.getKind()==IFF || n.getKind()==ITE ){ + //Boolean equality here + }else if( n.getKind()==EQUAL || n.getKind()==ITE ){ for( unsigned i=0; i<2; i++ ){ if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){ - unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2; + unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2; bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol; return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy ); } @@ -1956,18 +1957,24 @@ Node TermDb::simpleNegate( Node n ){ } bool TermDb::isAssoc( Kind k ) { - return k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + return k==PLUS || k==MULT || k==AND || k==OR || k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR || k==BITVECTOR_CONCAT || k==STRING_CONCAT; } bool TermDb::isComm( Kind k ) { - return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==IFF || + return k==EQUAL || k==PLUS || k==MULT || k==AND || k==OR || k==XOR || k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; } bool TermDb::isBoolConnective( Kind k ) { - return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT || k==SEP_STAR; + return k==OR || k==AND || k==EQUAL || k==ITE || k==FORALL || k==NOT || k==SEP_STAR; +} + +bool TermDb::isBoolConnectiveTerm( TNode n ) { + return isBoolConnective( n.getKind() ) && + ( n.getKind()!=EQUAL || n[0].getType().isBoolean() ) && + ( n.getKind()!=ITE || n.getType().isBoolean() ); } void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ @@ -2018,7 +2025,7 @@ bool TermDb::isFunDefAnnotation( Node ipl ) { } Node TermDb::getFunDefHead( Node q ) { - //&& ( q[1].getKind()==EQUAL || q[1].getKind()==IFF ) && q[1][0].getKind()==APPLY_UF && + //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF && if( q.getKind()==FORALL && q.getNumChildren()==3 ){ for( unsigned i=0; i<q[2].getNumChildren(); i++ ){ @@ -2034,7 +2041,7 @@ Node TermDb::getFunDefHead( Node q ) { Node TermDb::getFunDefBody( Node q ) { Node h = getFunDefHead( q ); if( !h.isNull() ){ - if( q[1].getKind()==EQUAL || q[1].getKind()==IFF ){ + if( q[1].getKind()==EQUAL ){ if( q[1][0]==h ){ return q[1][1]; }else if( q[1][1]==h ){ @@ -2718,7 +2725,7 @@ bool TermDbSygus::isIdempotentArg( Node n, Kind ik, int arg ) { return arg==1; } }else if( n==getTypeMaxValue( tn ) ){ - if( ik==IFF || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){ + if( ik==EQUAL || ik==BITVECTOR_AND || ik==BITVECTOR_XNOR ){ return true; } } @@ -3063,15 +3070,17 @@ Node TermDbSygus::minimizeBuiltinTerm( Node n ) { } Node TermDbSygus::expandBuiltinTerm( Node t ){ - if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){ - return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ), - NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) ); + if( t.getKind()==EQUAL ){ + if( t[0].getType().isReal() ){ + return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ), + NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) ); + }else if( t[0].getType().isBoolean() ){ + return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), + NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); + } }else if( t.getKind()==ITE && t.getType().isBoolean() ){ return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) ); - }else if( t.getKind()==IFF ){ - return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ), - NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) ); } return Node::null(); } @@ -3248,13 +3257,13 @@ void TermDbSygus::registerEvalTerm( Node n ) { Assert( dt.isSygus() ); d_eval_args[n[0]].push_back( std::vector< Node >() ); for( unsigned j=1; j<n.getNumChildren(); j++ ){ - if( var_list[j-1].getType().isBoolean() ){ - //TODO: remove this case when boolean term conversion is eliminated - Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); - d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) ); - }else{ + //if( var_list[j-1].getType().isBoolean() ){ + // //TODO: remove this case when boolean term conversion is eliminated + // Node c = NodeManager::currentNM()->mkConst(BitVector(1u, 1u)); + // d_eval_args[n[0]].back().push_back( n[j].eqNode( c ) ); + //}else{ d_eval_args[n[0]].back().push_back( n[j] ); - } + //} } Node a = getAnchor( n[0] ); d_subterms[a][n[0]] = true; @@ -3297,7 +3306,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems for( unsigned i=start; i<it->second.size(); i++ ){ Assert( vars.size()==it->second[i].size() ); Node sBTerm = bTerm.substitute( vars.begin(), vars.end(), it->second[i].begin(), it->second[i].end() ); - Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? IFF : EQUAL, d_evals[n][i], sBTerm ); + Node lem = NodeManager::currentNM()->mkNode(EQUAL, d_evals[n][i], sBTerm ); lem = NodeManager::currentNM()->mkNode( OR, antec, lem ); Trace("sygus-eager") << "Lemma : " << lem << std::endl; lems.push_back( lem ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index d4fdaa5e5..9f43c1d35 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -499,6 +499,8 @@ public: static bool isComm( Kind k ); /** is bool connective */ static bool isBoolConnective( Kind k ); + /** is bool connective term */ + static bool isBoolConnectiveTerm( TNode n ); //for sygus private: diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 7ab9f7065..cca6543b6 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -255,7 +255,7 @@ Node Trigger::getIsUsableEq( Node q, Node n ) { Assert( isRelationalTrigger( n ) ); for( unsigned i=0; i<2; i++) { if( isUsableEqTerms( q, n[i], n[1-i] ) ){ - if( i==1 && ( n.getKind()==EQUAL || n.getKind()==IFF ) && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ + if( i==1 && n.getKind()==EQUAL && !quantifiers::TermDb::hasInstConstAttr(n[0]) ){ return NodeManager::currentNM()->mkNode( n.getKind(), n[1], n[0] ); }else{ return n; @@ -292,7 +292,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { n = n[0]; } if( n.getKind()==INST_CONSTANT ){ - return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); + return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); }else if( isRelationalTrigger( n ) ){ Node rtr = getIsUsableEq( q, n ); if( rtr.isNull() && n[0].getType().isReal() ){ @@ -331,7 +331,7 @@ Node Trigger::getIsUsableTrigger( Node n, Node q ) { }else{ Trace("trigger-debug") << n << " usable : " << ( quantifiers::TermDb::getInstConstAttr(n)==q ) << " " << isAtomicTrigger( n ) << " " << isUsable( n, q ) << std::endl; if( isUsableAtomicTrigger( n, q ) ){ - return pol ? n : NodeManager::currentNM()->mkNode( IFF, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); + return pol ? n : NodeManager::currentNM()->mkNode( EQUAL, n, NodeManager::currentNM()->mkConst( true ) ).notNode(); } } return Node::null(); @@ -362,7 +362,7 @@ bool Trigger::isRelationalTrigger( Node n ) { } bool Trigger::isRelationalTriggerKind( Kind k ) { - return k==EQUAL || k==IFF || k==GEQ; + return k==EQUAL || k==GEQ; } bool Trigger::isCbqiKind( Kind k ) { @@ -377,7 +377,7 @@ bool Trigger::isCbqiKind( Kind k ) { bool Trigger::isSimpleTrigger( Node n ){ Node t = n.getKind()==NOT ? n[0] : n; - if( t.getKind()==IFF || t.getKind()==EQUAL ){ + if( t.getKind()==EQUAL ){ if( !quantifiers::TermDb::hasInstConstAttr( t[1] ) ){ t = t[0]; } @@ -416,7 +416,7 @@ bool Trigger::collectPatTerms2( Node q, Node n, std::map< Node, Node >& visited, Assert( nu.getKind()!=NOT ); Trace("auto-gen-trigger-debug2") << "...found usable trigger : " << nu << std::endl; Node reqEq; - if( nu.getKind()==IFF || nu.getKind()==EQUAL ){ + if( nu.getKind()==EQUAL ){ if( isAtomicTrigger( nu[0] ) && !quantifiers::TermDb::hasInstConstAttr(nu[1]) ){ if( hasPol ){ reqEq = nu[1]; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 573c97f00..ba50f9ead 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -1275,8 +1275,7 @@ bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){ //Assert( !areEqual( n1, n2 ) ); //Assert( !areDisequal( n1, n2 ) ); - Kind knd = n1.getType()==NodeManager::currentNM()->booleanType() ? IFF : EQUAL; - Node fm = NodeManager::currentNM()->mkNode( knd, n1, n2 ); + Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 ); return addSplit( fm ); } diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 87080ec18..0df122571 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -91,7 +91,7 @@ Node Rewriter::rewrite(TNode node) { Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { #ifdef CVC4_ASSERTIONS - bool isEquality = node.getKind() == kind::EQUAL; + bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean()); if(s_rewriteStack == NULL) { s_rewriteStack = new std::hash_set<Node, NodeHashFunction>(); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 55279e485..81afc0da2 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -121,7 +121,7 @@ void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) { // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if (atom.getKind() == kind::EQUAL) { d_equalityEngine.explainEquality( atom[0], atom[1], polarity, assumptions, NULL ); } else { d_equalityEngine.explainPredicate( atom, polarity, assumptions ); @@ -260,7 +260,7 @@ void TheorySep::postProcessModel( TheoryModel* m ){ } Node nil = getNilRef( it->first ); Node vnil = d_valuation.getModel()->getRepresentative( nil ); - m_neq = NodeManager::currentNM()->mkNode( nil.getType().isBoolean() ? kind::IFF : kind::EQUAL, nil, vnil ); + m_neq = NodeManager::currentNM()->mkNode( kind::EQUAL, nil, vnil ); Trace("sep-model") << "sep.nil = " << vnil << std::endl; Trace("sep-model") << std::endl; if( sep_children.empty() ){ @@ -451,7 +451,7 @@ void TheorySep::check(Effort e) { d_out->requirePhase( lit, true ); d_neg_guards.push_back( lit ); d_guard_to_assertion[lit] = s_atom; - //Node lem = NodeManager::currentNM()->mkNode( kind::IFF, lit, conc ); + //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit.negate(), conc ); Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl; d_out->lemma( lem ); @@ -840,12 +840,7 @@ Node TheorySep::getNextDecisionRequest( unsigned& priority ) { void TheorySep::conflict(TNode a, TNode b) { Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl; - Node conflictNode; - if (a.getKind() == kind::CONST_BOOLEAN) { - conflictNode = explain(a.iffNode(b)); - } else { - conflictNode = explain(a.eqNode(b)); - } + Node conflictNode = explain(a.eqNode(b)); d_conflict = true; d_out->conflict( conflictNode ); } @@ -1164,7 +1159,7 @@ Node TheorySep::getBaseLabel( TypeNode tn ) { Node e = d_type_references_card[tn][r]; //ensure that it is distinct from all other references so far for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){ - Node eq = NodeManager::currentNM()->mkNode( e.getType().isBoolean() ? kind::IFF : kind::EQUAL, e, d_type_references_all[tn][j] ); + Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, e, d_type_references_all[tn][j] ); d_out->lemma( eq.negate() ); } d_type_references_all[tn].push_back( e ); @@ -1429,7 +1424,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std: std::map< Node, Node >::iterator it = pto_model.find( vr ); if( it!=pto_model.end() ){ if( n[1]!=it->second ){ - children.push_back( NodeManager::currentNM()->mkNode( n[1].getType().isBoolean() ? kind::IFF : kind::EQUAL, n[1], it->second ) ); + children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[1], it->second ) ); } }else{ Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl; diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp index 48523cd06..8e9939f61 100644 --- a/src/theory/sep/theory_sep_rewriter.cpp +++ b/src/theory/sep/theory_sep_rewriter.cpp @@ -139,8 +139,7 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) { } break; } - case kind::EQUAL: - case kind::IFF: { + case kind::EQUAL: { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index edd63bddc..c14ef02b2 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -778,7 +778,7 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) { } if( x!=itnm2->second[xr][0] ){ Assert( d_equalityEngine.areEqual( x, itnm2->second[xr][0] ) ); - exp.push_back( NodeManager::currentNM()->mkNode( x.getType().isBoolean() ? kind::IFF : kind::EQUAL, x, itnm2->second[xr][0] ) ); + exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, x, itnm2->second[xr][0] ) ); } valid = true; } @@ -866,7 +866,7 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) { Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType); Node mem1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[0] ); Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] ); - Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::IFF, mem1, mem2 ).negate() ); + Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() ); lem = Rewriter::rewrite( lem ); assertInference( lem, d_emp_exp, lemmas, "diseq", 1 ); flushLemmas( lemmas ); @@ -1901,11 +1901,7 @@ void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { void TheorySetsPrivate::conflict(TNode a, TNode b) { - if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b)); - } else { - d_conflictNode = explain(a.eqNode(b)); - } + d_conflictNode = explain(a.eqNode(b)); d_external.d_out->conflict(d_conflictNode); Debug("sets") << "[sets] conflict: " << a << " iff " << b << ", explaination " << d_conflictNode << std::endl; @@ -1922,7 +1918,7 @@ Node TheorySetsPrivate::explain(TNode literal) TNode atom = polarity ? literal : literal[0]; std::vector<TNode> assumptions; - if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if(atom.getKind() == kind::EQUAL) { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); } else if(atom.getKind() == kind::MEMBER) { if( !d_equalityEngine.hasTerm(atom)) { diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index db29843d8..09865647e 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -992,7 +992,7 @@ int TheorySetsRels::EqcInfo::counter = 0; } Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements); tuple_reduct = NodeManager::currentNM()->mkNode(kind::MEMBER,tuple_reduct, n[1]); - Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::IFF, n, tuple_reduct); + Node tuple_reduction_lemma = NodeManager::currentNM()->mkNode(kind::EQUAL, n, tuple_reduct); sendLemma(tuple_reduction_lemma, d_trueNode, "tuple-reduction"); d_symbolic_tuples.insert(n); } @@ -1097,7 +1097,7 @@ int TheorySetsRels::EqcInfo::counter = 0; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if(atom.getKind() == kind::EQUAL) { d_eqEngine->explainEquality(atom[0], atom[1], polarity, assumptions); } else if(atom.getKind() == kind::MEMBER) { if( !d_eqEngine->hasTerm(atom)) { diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index d21e3fd67..aaf71e8fc 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -191,8 +191,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { B) ); }//kind::SUBSET - case kind::EQUAL: - case kind::IFF: { + case kind::EQUAL: { //rewrite: t = t with true (t term) //rewrite: c = c' with c different from c' false (c, c' constants) //otherwise: sort them @@ -210,7 +209,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, newNode); } break; - }//kind::IFF + } case kind::SETMINUS: { if(node[0] == node[1]) { diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 1f8ec7ee4..6dabf9a13 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -371,7 +371,7 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map< Trace("sort-inference-debug") << "...Process " << n << std::endl; int retType; - if( n.getKind()==kind::EQUAL ){ + if( n.getKind()==kind::EQUAL && !n[0].getType().isBoolean() ){ Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl; //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction if( n[0].getType()!=n[1].getType() ){ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2bce8beea..09cc3cb3b 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -257,7 +257,7 @@ void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions) { TNode atom = polarity ? literal : literal[0]; unsigned ps = assumptions.size(); std::vector< TNode > tassumptions; - if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if (atom.getKind() == kind::EQUAL) { if( atom[0]!=atom[1] ){ Assert( hasTerm( atom[0] ) ); Assert( hasTerm( atom[1] ) ); @@ -402,7 +402,7 @@ int TheoryStrings::getReduction( int effort, Node n, Node& nr ) { std::vector< Node > new_nodes; Node res = d_preproc.simplify( n, new_nodes ); Assert( res!=n ); - new_nodes.push_back( NodeManager::currentNM()->mkNode( res.getType().isBoolean() ? kind::IFF : kind::EQUAL, res, n ) ); + new_nodes.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, res, n ) ); Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); nnlem = Rewriter::rewrite( nnlem ); Trace("strings-red-lemma") << "Reduction_" << effort << " lemma : " << nnlem << std::endl; @@ -820,11 +820,7 @@ void TheoryStrings::conflict(TNode a, TNode b){ Debug("strings-conflict") << "Making conflict..." << std::endl; d_conflict = true; Node conflictNode; - if (a.getKind() == kind::CONST_BOOLEAN) { - conflictNode = explain( a.iffNode(b) ); - } else { - conflictNode = explain( a.eqNode(b) ); - } + conflictNode = explain( a.eqNode(b) ); Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl; d_out->conflict( conflictNode ); } diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index c8fe1fb00..d8d8e393c 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -176,7 +176,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { new_nodes.push_back(lencond); } - Node lem = NodeManager::currentNM()->mkNode(kind::IFF, nonneg.negate(), + Node lem = NodeManager::currentNM()->mkNode(kind::EQUAL, nonneg.negate(), pret.eqNode(NodeManager::currentNM()->mkConst( ::CVC4::String("") ))//lenp.eqNode(d_zero) ); new_nodes.push_back(lem); @@ -300,7 +300,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { str.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(""))), pret.eqNode(negone)); new_nodes.push_back(lem); - /*lem = NodeManager::currentNM()->mkNode(kind::IFF, + /*lem = NodeManager::currentNM()->mkNode(kind::EQUAL, t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("0"))), t.eqNode(d_zero)); new_nodes.push_back(lem);*/ @@ -351,7 +351,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { for(unsigned i=0; i<=9; i++) { chtmp[0] = i + '0'; std::string stmp(chtmp); - c3cc = NodeManager::currentNM()->mkNode(kind::IFF, + c3cc = NodeManager::currentNM()->mkNode(kind::EQUAL, ufMx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::Rational(i))), sx.eqNode(NodeManager::currentNM()->mkConst(::CVC4::String(stmp)))); vec_c3b.push_back(c3cc); diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 2d8ea9fa8..340ab2373 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -88,7 +88,13 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { switch(mode) { case THEORY_OF_TYPE_BASED: // Constants, variables, 0-ary constructors - if (node.isVar() || node.isConst()) { + if (node.isVar()) { + if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){ + tid = THEORY_UF; + }else{ + tid = Theory::theoryOf(node.getType()); + } + }else if (node.isConst()) { tid = Theory::theoryOf(node.getType()); } else if (node.getKind() == kind::EQUAL) { // Equality is owned by the theory that owns the domain @@ -105,8 +111,13 @@ TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) { // We treat the variables as uninterpreted tid = s_uninterpretedSortOwner; } else { - // Except for the Boolean ones, which we just ignore anyhow - tid = theory::THEORY_BOOL; + if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){ + //Boolean vars go to UF + tid = THEORY_UF; + }else{ + // Except for the Boolean ones + tid = THEORY_BOOL; + } } } else if (node.isConst()) { // Constants go to the theory of the type @@ -408,7 +419,7 @@ bool ExtTheory::doInferencesInternal( int effort, std::vector< Node >& terms, st nred.push_back( n ); }else{ if( !nr.isNull() && n!=nr ){ - Node lem = NodeManager::currentNM()->mkNode( n.getType().isBoolean() ? kind::IFF : kind::EQUAL, n, nr ); + Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, n, nr ); if( sendLemma( lem, true ) ){ Trace("extt-lemma") << "ExtTheory : Reduction lemma : " << lem << std::endl; addedLemma = true; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8da1dfc1b..7c1b02f47 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -121,13 +121,15 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori } break; - case kind::IFF: - if (!negated) { - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); - } else { - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); + case kind::EQUAL: + if( nnLemma[0].getType().isBoolean() ){ + if (!negated) { + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); + } else { + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); + } } break; @@ -266,7 +268,7 @@ void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){ TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, - RemoveITE& iteRemover, + RemoveTermFormulas& iteRemover, const LogicInfo& logicInfo, LemmaChannels* channels) : d_propEngine(NULL), @@ -292,7 +294,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_atomRequests(context), - d_iteRemover(iteRemover), + d_tform_remover(iteRemover), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_true(), d_false(), @@ -327,7 +329,7 @@ TheoryEngine::TheoryEngine(context::Context* context, ProofManager::currentPM()->initTheoryProofEngine(); #endif - d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); + d_iteUtilities = new ITEUtilities(d_tform_remover.getContainsVisitor()); smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded); } @@ -1754,8 +1756,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, Node ppNode = preprocess ? this->preprocess(node) : Node(node); // Remove the ITEs + Debug("ite") << "Remove ITE from " << ppNode << std::endl; additionalLemmas.push_back(ppNode); - d_iteRemover.run(additionalLemmas, iteSkolemMap); + d_tform_remover.run(additionalLemmas, iteSkolemMap); + Debug("ite") << "..done " << additionalLemmas[0] << std::endl; additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); if(Debug.isOn("lemma-ites")) { @@ -1923,7 +1927,7 @@ void TheoryEngine::mkAckermanizationAsssertions(std::vector<Node>& assertions) { Node TheoryEngine::ppSimpITE(TNode assertion) { - if (!d_iteRemover.containsTermITE(assertion)) { + if (!d_tform_remover.containsTermITE(assertion)) { return assertion; } else { Node result = d_iteUtilities->simpITE(assertion); @@ -1964,7 +1968,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){ Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl; d_iteUtilities->clear(); Rewriter::clearCaches(); - d_iteRemover.garbageCollect(); + d_tform_remover.garbageCollect(); nm->reclaimZombiesUntil(options::zombieHuntThreshold()); Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl; } @@ -1975,7 +1979,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){ if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH) && !options::incrementalSolving() ){ if(!simpDidALotOfWork){ - ContainsTermITEVisitor& contains = *d_iteRemover.getContainsVisitor(); + ContainsTermITEVisitor& contains = *d_tform_remover.getContainsVisitor(); arith::ArithIteUtils aiteu(contains, d_userContext, getModel()); bool anyItes = false; for(size_t i = 0; i < assertions.size(); ++i){ @@ -2109,7 +2113,7 @@ void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector } Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << endl; - Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially"); + Assert( explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially"); // Mark the explanation NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp); explanationVector.push_back(newExplain); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 3273b3d19..7ce8345f7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -97,7 +97,7 @@ namespace theory { }/* CVC4::theory namespace */ class DecisionEngine; -class RemoveITE; +class RemoveTermFormulas; class UnconstrainedSimplifier; /** @@ -439,7 +439,7 @@ class TheoryEngine { /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); - RemoveITE& d_iteRemover; + RemoveTermFormulas& d_tform_remover; /** sort inference module */ SortInference d_sortInfer; @@ -461,7 +461,7 @@ public: /** Constructs a theory engine */ TheoryEngine(context::Context* context, context::UserContext* userContext, - RemoveITE& iteRemover, const LogicInfo& logic, + RemoveTermFormulas& iteRemover, const LogicInfo& logic, LemmaChannels* channels); /** Destroys a theory engine */ @@ -850,7 +850,7 @@ public: theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } - RemoveITE* getIteRemover() { return &d_iteRemover; } + RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; } SortInference* getSortInference() { return &d_sortInfer; } diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 5d929a708..f7084bec3 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -230,8 +230,8 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { d_isConstant.push_back(false); // No terms to evaluate by defaul d_subtermsToEvaluate.push_back(0); - // Mark Boolean nodes - d_isBoolean.push_back(false); + // Mark equality nodes + d_isEquality.push_back(false); // Mark the node as internal by default d_isInternal.push_back(true); // Add the equality node to the nodes @@ -329,10 +329,10 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { d_isConstant[result] = !isOperator && t.isConst(); } - if (t.getType().isBoolean()) { + if (t.getKind() == kind::EQUAL) { // We set this here as this only applies to actual terms, not the // intermediate application terms - d_isBoolean[result] = true; + d_isEquality[result] = true; } else if (d_constantsAreTriggers && d_isConstant[result]) { // Non-Boolean constants are trigger terms for all tags EqualityNodeId tId = getNodeId(t); @@ -613,7 +613,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect // Update class2 table lookup and information if not a boolean // since booleans can't be in an application - if (!d_isBoolean[class2Id]) { + if (!d_isEquality[class2Id]) { Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl; do { // Get the current node @@ -869,7 +869,7 @@ void EqualityEngine::backtrack() { d_nodeIndividualTrigger.resize(d_nodesCount); d_isConstant.resize(d_nodesCount); d_subtermsToEvaluate.resize(d_nodesCount); - d_isBoolean.resize(d_nodesCount); + d_isEquality.resize(d_nodesCount); d_isInternal.resize(d_nodesCount); d_equalityGraph.resize(d_nodesCount); d_equalityNodes.resize(d_nodesCount); @@ -1268,7 +1268,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st } else { eqp->d_id = MERGED_THROUGH_TRANS; eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() ); - eqp->d_node = NodeManager::currentNM()->mkNode(d_nodes[t1Id].getType().isBoolean() ? kind::IFF : kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); + eqp->d_node = NodeManager::currentNM()->mkNode(kind::EQUAL, d_nodes[t1Id], d_nodes[t2Id]); } eqp->debug_print("pf::ee", 1); diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 18e83bd1a..46ec7403b 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -464,7 +464,7 @@ private: /** * Map from ids to whether they are Boolean. */ - std::vector<bool> d_isBoolean; + std::vector<bool> d_isEquality; /** * Map from ids to whether the nods is internal. An internal node is a node diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 888fa140f..e2d740e20 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -15,6 +15,8 @@ parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; fi typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule +variable BOOLEAN_TERM_VARIABLE "Boolean term variable" + operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S" typerule CARDINALITY_CONSTRAINT ::CVC4::theory::uf::CardinalityConstraintTypeRule diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index ed5d99bdf..ca7284689 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -246,8 +246,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) { } else { if( (*i).getKind() == kind::OR ) { kids.push_back(normInternal(*i, level)); - } else if((*i).getKind() == kind::IFF || - (*i).getKind() == kind::EQUAL) { + } else if((*i).getKind() == kind::EQUAL) { kids.push_back(normInternal(*i, level)); if((*i)[0].isVar() || (*i)[1].isVar()) { @@ -291,8 +290,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) { first = false; matchingTerm = TNode::null(); kids.push_back(normInternal(*i, level + 1)); - } else if((*i).getKind() == kind::IFF || - (*i).getKind() == kind::EQUAL) { + } else if((*i).getKind() == kind::EQUAL) { kids.push_back(normInternal(*i, level + 1)); if((*i)[0].isVar() || (*i)[1].isVar()) { @@ -361,8 +359,7 @@ Node SymmetryBreaker::normInternal(TNode n, size_t level) { sort(kids.begin(), kids.end()); return result = NodeManager::currentNM()->mkNode(k, kids); } - - case kind::IFF: + case kind::EQUAL: if(n[0].isVar() || n[1].isVar()) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 4cdc5e240..e4a3ac78c 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -139,14 +139,14 @@ void TheoryUF::check(Effort level) { } } - - if (d_thss != NULL && ! d_conflict) { - d_thss->check(level); - if( d_thss->isConflict() ){ - d_conflict = true; + if(! d_conflict ){ + if (d_thss != NULL) { + d_thss->check(level); + if( d_thss->isConflict() ){ + d_conflict = true; + } } } - }/* TheoryUF::check() */ void TheoryUF::preRegisterTerm(TNode node) { @@ -217,7 +217,7 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro // Do the work bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; - if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { + if (atom.getKind() == kind::EQUAL) { d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf); } else { d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf); @@ -336,10 +336,10 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { if(n.getKind() == kind::OR && n.getNumChildren() == 2 && n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && - (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && - (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && - (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && - (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) { + (n[0][0].getKind() == kind::EQUAL) && + (n[0][1].getKind() == kind::EQUAL) && + (n[1][0].getKind() == kind::EQUAL) && + (n[1][1].getKind() == kind::EQUAL)) { // now we have (a = b && c = d) || (e = f && g = h) Debug("diamonds") << "has form of a diamond!" << endl; @@ -396,7 +396,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) { (a == h && d == e) ) { // learn: n implies a == d Debug("diamonds") << "+ C holds" << endl; - Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d); + Node newEquality = a.eqNode(d); Debug("diamonds") << " ==> " << newEquality << endl; learned << n.impNode(newEquality); } else { @@ -533,12 +533,7 @@ void TheoryUF::computeCareGraph() { void TheoryUF::conflict(TNode a, TNode b) { eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL; - - if (a.getKind() == kind::CONST_BOOLEAN) { - d_conflictNode = explain(a.iffNode(b),pf); - } else { - d_conflictNode = explain(a.eqNode(b),pf); - } + d_conflictNode = explain(a.eqNode(b),pf); ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL; d_out->conflict(d_conflictNode, puf); d_conflict = true; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 0900b4c90..ce9c70ca2 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -82,27 +82,27 @@ public: } void eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.conflict(t1, t2); } void eqNotifyNewClass(TNode t) { - Debug("uf") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl; d_uf.eqNotifyNewClass(t); } void eqNotifyPreMerge(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.eqNotifyPreMerge(t1, t2); } void eqNotifyPostMerge(TNode t1, TNode t2) { - Debug("uf") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl; d_uf.eqNotifyPostMerge(t1, t2); } void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { - Debug("uf") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; + Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl; d_uf.eqNotifyDisequal(t1, t2, reason); } diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index 166d11451..bce6003eb 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -32,7 +32,7 @@ class TheoryUfRewriter { public: static RewriteResponse postRewrite(TNode node) { - if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { + if(node.getKind() == kind::EQUAL) { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } else if(node[0].isConst() && node[1].isConst()) { @@ -76,7 +76,7 @@ public: } static RewriteResponse preRewrite(TNode node) { - if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) { + if(node.getKind() == kind::EQUAL) { if(node[0] == node[1]) { return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } else if(node[0].isConst() && node[1].isConst()) { diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 6b89c3524..51648fb26 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -639,7 +639,7 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ int bi = d_regions_map[b]; if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){ Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl; - //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) || + //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL || // a!=reason[0][0] || b!=reason[0][1] ){ // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl; //} @@ -1861,8 +1861,9 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ //otherwise, make equal via lemma if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){ Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] ); - Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << lit.iffNode( eqv_lit ) << std::endl; - getOutputChannel().lemma( lit.iffNode( eqv_lit ) ); + eqv_lit = lit.eqNode( eqv_lit ); + Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl; + getOutputChannel().lemma( eqv_lit ); d_card_assertions_eqv_lemma[lit] = true; } } diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 8284f6ff4..57d95d801 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -121,6 +121,7 @@ void UnconstrainedSimplifier::processUnconstrained() parent = d_visitedOnce[current]; if (!parent.isNull()) { swap = isSigned = strict = false; + bool checkParent = false; switch (parent.getKind()) { // If-then-else operator - any two unconstrained children makes the parent unconstrained @@ -170,13 +171,7 @@ void UnconstrainedSimplifier::processUnconstrained() if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) { // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result // is unconstrained - Node test; - if (parent.getType().isBoolean()) { - test = Rewriter::rewrite(parent[1].iffNode(parent[2])); - } - else { - test = Rewriter::rewrite(parent[1].eqNode(parent[2])); - } + Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); if (test == NodeManager::currentNM()->mkConst<bool>(false)) { ++d_numUnconstrainedElim; if (currentSub.isNull()) { @@ -207,6 +202,10 @@ void UnconstrainedSimplifier::processUnconstrained() break; } } + if( parent[0].getType().isBoolean() ){ + checkParent = true; + break; + } case kind::BITVECTOR_COMP: case kind::LT: case kind::LEQ: @@ -271,17 +270,7 @@ void UnconstrainedSimplifier::processUnconstrained() } } if (allUnconstrained) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } + checkParent = true; } } break; @@ -310,17 +299,7 @@ void UnconstrainedSimplifier::processUnconstrained() } } if (allUnconstrained && allDifferent) { - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } + checkParent = true; } break; } @@ -366,23 +345,12 @@ void UnconstrainedSimplifier::processUnconstrained() !parent.getType().isInteger()) { break; } - case kind::IFF: case kind::XOR: case kind::BITVECTOR_XOR: case kind::BITVECTOR_XNOR: case kind::BITVECTOR_PLUS: case kind::BITVECTOR_SUB: - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } + checkParent = true; break; // Multiplication/division: must be non-integer and other operand must be non-zero @@ -486,17 +454,7 @@ void UnconstrainedSimplifier::processUnconstrained() if (done) { break; } - if (d_unconstrained.find(parent) == d_unconstrained.end() && - !d_substitutions.hasSubstitution(parent)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; - } - current = parent; - } - else { - currentSub = Node(); - } + checkParent = true; break; } @@ -671,6 +629,20 @@ void UnconstrainedSimplifier::processUnconstrained() default: break; } + if( checkParent ){ + //run for various cases from above + if (d_unconstrained.find(parent) == d_unconstrained.end() && + !d_substitutions.hasSubstitution(parent)) { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) { + currentSub = current; + } + current = parent; + } + else { + currentSub = Node(); + } + } if (current == parent && d_visited[parent] == 1) { d_unconstrained.insert(parent); continue; |