From ff0f2571025cf590658fa136e71e9442e0a74cc1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 16 May 2018 18:35:38 -0700 Subject: [PATCH] remove iff Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 3 +- src/ast/ast.cpp | 24 +-- src/ast/ast.h | 19 +- src/ast/ast_smt2_pp.cpp | 4 - src/ast/ast_smt_pp.cpp | 3 - src/ast/macro_substitution.cpp | 4 +- src/ast/macros/macro_manager.cpp | 5 +- src/ast/macros/macro_util.cpp | 9 +- src/ast/macros/quasi_macros.cpp | 2 +- src/ast/normal_forms/nnf.cpp | 5 +- src/ast/proofs/proof_checker.cpp | 6 +- src/ast/proofs/proof_utils.h | 4 +- src/ast/rewriter/bool_rewriter.cpp | 5 +- src/ast/rewriter/bool_rewriter.h | 2 +- src/ast/rewriter/der.cpp | 11 +- src/ast/rewriter/quant_hoist.cpp | 2 +- src/ast/rewriter/th_rewriter.cpp | 2 +- src/ast/static_features.cpp | 8 +- src/model/model_implicant.cpp | 5 - src/muz/base/rule_properties.cpp | 6 +- src/muz/pdr/pdr_context.cpp | 2 +- src/muz/rel/udoc_relation.cpp | 2 +- src/muz/spacer/spacer_legacy_mev.cpp | 5 - src/muz/spacer/spacer_util.cpp | 192 ++++++++---------- src/muz/transforms/dl_mk_array_blast.cpp | 2 +- .../dl_mk_quantifier_instantiation.cpp | 2 +- src/nlsat/tactic/goal2nlsat.cpp | 1 - src/parsers/util/cost_parser.cpp | 2 +- src/qe/qe.cpp | 2 +- src/qe/qe_lite.cpp | 2 +- src/sat/tactic/atom2bool_var.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 2 - src/smt/asserted_formulas.cpp | 7 +- src/smt/cost_evaluator.cpp | 3 +- src/smt/expr_context_simplifier.cpp | 18 +- src/smt/smt_checker.cpp | 28 +-- src/smt/smt_conflict_resolution.cpp | 4 +- src/smt/smt_internalizer.cpp | 16 +- src/smt/smt_model_finder.cpp | 3 - src/smt/smt_quantifier_stat.cpp | 12 +- src/smt/smt_quick_checker.cpp | 12 +- src/tactic/aig/aig.cpp | 4 - src/tactic/core/cofactor_elim_term_ite.cpp | 1 - src/tactic/core/dom_simplify_tactic.cpp | 2 +- src/tactic/core/elim_uncnstr_tactic.cpp | 1 - src/tactic/core/solve_eqs_tactic.cpp | 5 +- src/tactic/core/tseitin_cnf_tactic.cpp | 2 - 47 files changed, 199 insertions(+), 264 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 536b94fb2..34168f1f4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -190,7 +190,7 @@ extern "C" { MK_UNARY(Z3_mk_not, mk_c(c)->get_basic_fid(), OP_NOT, SKIP); MK_BINARY(Z3_mk_eq, mk_c(c)->get_basic_fid(), OP_EQ, SKIP); MK_NARY(Z3_mk_distinct, mk_c(c)->get_basic_fid(), OP_DISTINCT, SKIP); - MK_BINARY(Z3_mk_iff, mk_c(c)->get_basic_fid(), OP_IFF, SKIP); + MK_BINARY(Z3_mk_iff, mk_c(c)->get_basic_fid(), OP_EQ, SKIP); MK_BINARY(Z3_mk_implies, mk_c(c)->get_basic_fid(), OP_IMPLIES, SKIP); MK_BINARY(Z3_mk_xor, mk_c(c)->get_basic_fid(), OP_XOR, SKIP); MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP); @@ -894,7 +894,6 @@ extern "C" { case OP_ITE: return Z3_OP_ITE; case OP_AND: return Z3_OP_AND; case OP_OR: return Z3_OP_OR; - case OP_IFF: return Z3_OP_IFF; case OP_XOR: return Z3_OP_XOR; case OP_NOT: return Z3_OP_NOT; case OP_IMPLIES: return Z3_OP_IMPLIES; diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index cae1618c0..681f64a25 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -643,7 +643,6 @@ basic_decl_plugin::basic_decl_plugin(): m_false_decl(nullptr), m_and_decl(nullptr), m_or_decl(nullptr), - m_iff_decl(nullptr), m_xor_decl(nullptr), m_not_decl(nullptr), m_implies_decl(nullptr), @@ -861,7 +860,6 @@ void basic_decl_plugin::set_manager(ast_manager * m, family_id id) { m_false_decl = mk_bool_op_decl("false", OP_FALSE); m_and_decl = mk_bool_op_decl("and", OP_AND, 2, true, true, true, true); m_or_decl = mk_bool_op_decl("or", OP_OR, 2, true, true, true, true); - m_iff_decl = mk_bool_op_decl("iff", OP_IFF, 2, false, true, false, false, true); m_xor_decl = mk_bool_op_decl("xor", OP_XOR, 2, true, true); m_not_decl = mk_bool_op_decl("not", OP_NOT, 1); m_implies_decl = mk_implies_decl(); @@ -892,13 +890,13 @@ void basic_decl_plugin::get_op_names(svector & op_names, symbol co if (logic == symbol::null) { // user friendly aliases op_names.push_back(builtin_name("implies", OP_IMPLIES)); - op_names.push_back(builtin_name("iff", OP_IFF)); + op_names.push_back(builtin_name("iff", OP_EQ)); op_names.push_back(builtin_name("if_then_else", OP_ITE)); op_names.push_back(builtin_name("if", OP_ITE)); op_names.push_back(builtin_name("&&", OP_AND)); op_names.push_back(builtin_name("||", OP_OR)); op_names.push_back(builtin_name("equals", OP_EQ)); - op_names.push_back(builtin_name("equiv", OP_IFF)); + op_names.push_back(builtin_name("equiv", OP_EQ)); } } @@ -919,7 +917,6 @@ void basic_decl_plugin::finalize() { DEC_REF(m_and_decl); DEC_REF(m_or_decl); DEC_REF(m_not_decl); - DEC_REF(m_iff_decl); DEC_REF(m_xor_decl); DEC_REF(m_implies_decl); DEC_ARRAY_REF(m_eq_decls); @@ -1051,7 +1048,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_AND: return m_and_decl; case OP_OR: return m_or_decl; case OP_NOT: return m_not_decl; - case OP_IFF: return m_iff_decl; case OP_IMPLIES: return m_implies_decl; case OP_XOR: return m_xor_decl; case OP_ITE: return arity == 3 ? mk_ite_decl(join(domain[1], domain[2])) : nullptr; @@ -1093,7 +1089,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_AND: return m_and_decl; case OP_OR: return m_or_decl; case OP_NOT: return m_not_decl; - case OP_IFF: return m_iff_decl; case OP_IMPLIES: return m_implies_decl; case OP_XOR: return m_xor_decl; case OP_ITE: return num_args == 3 ? mk_ite_decl(join(m_manager->get_sort(args[1]), m_manager->get_sort(args[2]))): nullptr; @@ -2636,10 +2631,10 @@ proof * ast_manager::mk_modus_ponens(proof * p1, proof * p2) { if (!p1 || !p2) return nullptr; SASSERT(has_fact(p1)); SASSERT(has_fact(p2)); - CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_iff(get_fact(p2)) || is_oeq(get_fact(p2))), + CTRACE("mk_modus_ponens", !(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2))), tout << mk_ll_pp(p1, *this) << "\n"; tout << mk_ll_pp(p2, *this) << "\n";); - SASSERT(is_implies(get_fact(p2)) || is_iff(get_fact(p2)) || is_oeq(get_fact(p2))); + SASSERT(is_implies(get_fact(p2)) || is_eq(get_fact(p2)) || is_oeq(get_fact(p2))); CTRACE("mk_modus_ponens", to_app(get_fact(p2))->get_arg(0) != get_fact(p1), tout << mk_pp(get_fact(p1), *this) << "\n" << mk_pp(get_fact(p2), *this) << "\n";); SASSERT(to_app(get_fact(p2))->get_arg(0) == get_fact(p1)); @@ -2717,8 +2712,6 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) { tout << mk_pp(to_app(get_fact(p1))->get_decl(), *this) << "\n"; tout << mk_pp(to_app(get_fact(p2))->get_decl(), *this) << "\n";); SASSERT(to_app(get_fact(p1))->get_decl() == to_app(get_fact(p2))->get_decl() || - ((is_iff(get_fact(p1)) || is_eq(get_fact(p1))) && - (is_iff(get_fact(p2)) || is_eq(get_fact(p2)))) || ( (is_eq(get_fact(p1)) || is_oeq(get_fact(p1))) && (is_eq(get_fact(p2)) || is_oeq(get_fact(p2))))); CTRACE("mk_transitivity", to_app(get_fact(p1))->get_arg(1) != to_app(get_fact(p2))->get_arg(0), @@ -2797,7 +2790,7 @@ proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) if (!p) return nullptr; SASSERT(q1->get_num_decls() == q2->get_num_decls()); SASSERT(has_fact(p)); - SASSERT(is_iff(get_fact(p))); + SASSERT(is_eq(get_fact(p))); return mk_app(m_basic_family_id, PR_QUANT_INTRO, p, mk_iff(q1, q2)); } @@ -2884,8 +2877,7 @@ bool ast_manager::is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vectorget_arg(0), r1, r2) || - is_iff(to_app(e)->get_arg(0), r1, r2)); + VERIFY (is_eq(to_app(e)->get_arg(0), r1, r2)); return true; } else { @@ -2913,7 +2905,7 @@ proof * ast_manager::mk_unit_resolution(unsigned num_proofs, proof * const * pro fact = mk_false(); } else { - CTRACE("mk_unit_resolution_bug", !is_or(f1), tout << mk_pp(f1, *this) << " " << mk_pp(f2, *this) << "\n";); + CTRACE("mk_unit_resolution_bug", !is_or(f1), tout << mk_ll_pp(f1, *this) << "\n" << mk_ll_pp(f2, *this) << "\n";); SASSERT(is_or(f1)); ptr_buffer new_lits; app const * cls = to_app(f1); @@ -3044,7 +3036,7 @@ proof * ast_manager::mk_iff_oeq(proof * p) { if (!p) return p; SASSERT(has_fact(p)); - SASSERT(is_iff(get_fact(p)) || is_oeq(get_fact(p))); + SASSERT(is_eq(get_fact(p)) || is_oeq(get_fact(p))); if (is_oeq(get_fact(p))) return p; diff --git a/src/ast/ast.h b/src/ast/ast.h index e85f164e1..ce193e8b1 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1041,7 +1041,7 @@ enum basic_sort_kind { }; enum basic_op_kind { - OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, LAST_BASIC_OP, + OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, LAST_BASIC_OP, PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO, PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT, @@ -1060,7 +1060,6 @@ protected: func_decl * m_false_decl; func_decl * m_and_decl; func_decl * m_or_decl; - func_decl * m_iff_decl; func_decl * m_xor_decl; func_decl * m_not_decl; func_decl * m_implies_decl; @@ -1344,9 +1343,9 @@ public: bool is_and(expr const * n) const { return is_app_of(n, m_fid, OP_AND); } bool is_not(expr const * n) const { return is_app_of(n, m_fid, OP_NOT); } bool is_eq(expr const * n) const { return is_app_of(n, m_fid, OP_EQ); } + bool is_iff(expr const* n) const { return is_eq(n) && is_bool(to_app(n)->get_arg(0)); } bool is_oeq(expr const * n) const { return is_app_of(n, m_fid, OP_OEQ); } bool is_distinct(expr const * n) const { return is_app_of(n, m_fid, OP_DISTINCT); } - bool is_iff(expr const * n) const { return is_app_of(n, m_fid, OP_IFF); } bool is_xor(expr const * n) const { return is_app_of(n, m_fid, OP_XOR); } bool is_ite(expr const * n) const { return is_app_of(n, m_fid, OP_ITE); } bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); } @@ -1361,7 +1360,6 @@ public: bool is_and(func_decl const * d) const { return is_decl_of(d, m_fid, OP_AND); } bool is_not(func_decl const * d) const { return is_decl_of(d, m_fid, OP_NOT); } bool is_eq(func_decl const * d) const { return is_decl_of(d, m_fid, OP_EQ); } - bool is_iff(func_decl const * d) const { return is_decl_of(d, m_fid, OP_IFF); } bool is_xor(func_decl const * d) const { return is_decl_of(d, m_fid, OP_XOR); } bool is_ite(func_decl const * d) const { return is_decl_of(d, m_fid, OP_ITE); } bool is_term_ite(func_decl const * d) const { return is_ite(d) && !is_bool(d->get_range()); } @@ -1369,13 +1367,13 @@ public: MATCH_UNARY(is_not); MATCH_BINARY(is_eq); - MATCH_BINARY(is_iff); MATCH_BINARY(is_implies); MATCH_BINARY(is_and); MATCH_BINARY(is_or); MATCH_BINARY(is_xor); MATCH_TERNARY(is_and); MATCH_TERNARY(is_or); + bool is_iff(expr const* n, expr*& lhs, expr*& rhs) const { return is_eq(n, lhs, rhs) && is_bool(lhs); } bool is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const; }; @@ -1663,7 +1661,7 @@ public: bool is_bool(expr const * n) const; bool is_bool(sort const * s) const { return s == m_bool_sort; } - decl_kind get_eq_op(expr const * n) const { return is_bool(n) ? OP_IFF : OP_EQ; } + decl_kind get_eq_op(expr const * n) const { return OP_EQ; } private: sort * mk_sort(symbol const & name, sort_info * info); @@ -1987,9 +1985,9 @@ public: bool is_and(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_AND); } bool is_not(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_NOT); } bool is_eq(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_EQ); } + bool is_iff(expr const * n) const { return is_eq(n) && is_bool(to_app(n)->get_arg(0)); } bool is_oeq(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_OEQ); } bool is_distinct(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_DISTINCT); } - bool is_iff(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_IFF); } bool is_xor(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_XOR); } bool is_ite(expr const * n) const { return is_app_of(n, m_basic_family_id, OP_ITE); } bool is_term_ite(expr const * n) const { return is_ite(n) && !is_bool(n); } @@ -2005,7 +2003,7 @@ public: bool is_and(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_AND); } bool is_not(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_NOT); } bool is_eq(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_EQ); } - bool is_iff(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_IFF); } + bool is_iff(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_EQ) && is_bool(d->get_range()); } bool is_xor(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_XOR); } bool is_ite(func_decl const * d) const { return is_decl_of(d, m_basic_family_id, OP_ITE); } bool is_term_ite(func_decl const * d) const { return is_ite(d) && !is_bool(d->get_range()); } @@ -2015,7 +2013,6 @@ public: MATCH_UNARY(is_not); MATCH_BINARY(is_eq); - MATCH_BINARY(is_iff); MATCH_BINARY(is_implies); MATCH_BINARY(is_and); MATCH_BINARY(is_or); @@ -2023,6 +2020,8 @@ public: MATCH_TERNARY(is_and); MATCH_TERNARY(is_or); + bool is_iff(expr const* n, expr*& lhs, expr*& rhs) const { return is_eq(n, lhs, rhs) && is_bool(lhs); } + bool is_ite(expr const* n, expr*& t1, expr*& t2, expr*& t3) const { if (is_ite(n)) { t1 = to_app(n)->get_arg(0); @@ -2035,7 +2034,7 @@ public: public: app * mk_eq(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, get_eq_op(lhs), lhs, rhs); } - app * mk_iff(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_IFF, lhs, rhs); } + app * mk_iff(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_EQ, lhs, rhs); } app * mk_oeq(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_OEQ, lhs, rhs); } app * mk_xor(expr * lhs, expr * rhs) { return mk_app(m_basic_family_id, OP_XOR, lhs, rhs); } app * mk_ite(expr * c, expr * t, expr * e) { return mk_app(m_basic_family_id, OP_ITE, c, t, e); } diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index a2958e3c9..9d27ffb24 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -63,10 +63,6 @@ format * smt2_pp_environment::pp_fdecl_name(func_decl * f, unsigned & len) const len = 3; return mk_string(m, "ite"); } - else if (m.is_iff(f)) { - len = 1; - return mk_string(m, "="); - } else { symbol s = f->get_name(); return pp_fdecl_name(s, len, f->is_skolem()); diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 635899d23..22adf42d9 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -225,9 +225,6 @@ class smt_printer { else if (m_manager.is_ite(d)) { m_out << "ite"; } - else if (m_manager.is_iff(d)) { - m_out << "="; - } else if (m_manager.is_implies(d)) { m_out << "=>"; } diff --git a/src/ast/macro_substitution.cpp b/src/ast/macro_substitution.cpp index a51e1a066..2868a1876 100644 --- a/src/ast/macro_substitution.cpp +++ b/src/ast/macro_substitution.cpp @@ -77,7 +77,7 @@ void macro_substitution::cleanup() { void macro_substitution::insert(func_decl * f, quantifier * q, proof * pr, expr_dependency * dep) { DEBUG_CODE({ app * body = to_app(q->get_expr()); - SASSERT(m_manager.is_eq(body) || m_manager.is_iff(body)); + SASSERT(m_manager.is_eq(body)); expr * lhs = body->get_arg(0); expr * rhs = body->get_arg(1); SASSERT(is_app_of(lhs, f) || is_app_of(rhs, f)); @@ -146,7 +146,7 @@ void macro_substitution::erase(func_decl * f) { void macro_substitution::get_head_def(quantifier * q, func_decl * f, app * & head, expr * & def) { app * body = to_app(q->get_expr()); - SASSERT(m_manager.is_eq(body) || m_manager.is_iff(body)); + SASSERT(m_manager.is_eq(body)); expr * lhs = to_app(body)->get_arg(0); expr * rhs = to_app(body)->get_arg(1); SASSERT(is_app_of(lhs, f) || is_app_of(rhs, f)); diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index 71bdac0a4..2f429ccf7 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -169,9 +169,8 @@ void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) { void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const { app * body = to_app(q->get_expr()); - SASSERT(m.is_eq(body) || m.is_iff(body)); - expr * lhs = to_app(body)->get_arg(0); - expr * rhs = to_app(body)->get_arg(1); + expr * lhs = nullptr, *rhs = nullptr; + VERIFY(m.is_eq(body, lhs, rhs)); SASSERT(is_app_of(lhs, d) || is_app_of(rhs, d)); SASSERT(!is_app_of(lhs, d) || !is_app_of(rhs, d)); if (is_app_of(lhs, d)) { diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 77290c95f..b2f31e374 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -175,7 +175,7 @@ bool macro_util::is_macro_head(expr * n, unsigned num_decls) const { */ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const { - if (m_manager.is_eq(n) || m_manager.is_iff(n)) { + if (m_manager.is_eq(n)) { expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); if (is_macro_head(lhs, num_decls) && !is_forbidden(to_app(lhs)->get_decl()) && @@ -207,7 +207,7 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he */ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const { - if (m_manager.is_eq(n) || m_manager.is_iff(n)) { + if (m_manager.is_eq(n)) { expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); if (is_macro_head(rhs, num_decls) && !is_forbidden(to_app(rhs)->get_decl()) && @@ -339,10 +339,9 @@ bool macro_util::is_pseudo_predicate_macro(expr * n, app_ref & head, app_ref & t TRACE("macro_util", tout << "processing: " << mk_pp(n, m_manager) << "\n";); expr * body = to_quantifier(n)->get_expr(); unsigned num_decls = to_quantifier(n)->get_num_decls(); - if (!m_manager.is_iff(body)) + expr * lhs, *rhs; + if (!m_manager.is_iff(body, lhs, rhs)) return false; - expr * lhs = to_app(body)->get_arg(0); - expr * rhs = to_app(body)->get_arg(1); if (is_pseudo_head(lhs, num_decls, head, t) && !is_forbidden(head->get_decl()) && !occurs(head->get_decl(), rhs)) { diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp index a308b5b17..3a0735e25 100644 --- a/src/ast/macros/quasi_macros.cpp +++ b/src/ast/macros/quasi_macros.cpp @@ -158,7 +158,7 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const { if (is_quantifier(e) && to_quantifier(e)->is_forall()) { quantifier * q = to_quantifier(e); expr * qe = q->get_expr(); - if ((m_manager.is_eq(qe) || m_manager.is_iff(qe))) { + if ((m_manager.is_eq(qe))) { expr * lhs = to_app(qe)->get_arg(0); expr * rhs = to_app(qe)->get_arg(1); diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 11461680d..c7f20ced6 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/src/ast/normal_forms/nnf.cpp @@ -582,7 +582,7 @@ struct nnf::imp { return true; } - bool is_eq(app * t) const { return m().is_eq(t) || m().is_iff(t); } + bool is_eq(app * t) const { return m().is_eq(t); } bool process_iff_xor(app * t, frame & fr) { SASSERT(t->get_num_args() == 2); @@ -630,7 +630,7 @@ struct nnf::imp { } bool process_eq(app * t, frame & fr) { - if (m().is_bool(t->get_arg(0))) + if (m().is_iff(t)) return process_iff_xor(t, fr); else return process_default(t, fr); @@ -725,7 +725,6 @@ struct nnf::imp { return process_implies(t, fr); case OP_ITE: return process_ite(t, fr); - case OP_IFF: case OP_XOR: return process_iff_xor(t, fr); case OP_EQ: diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index 0e16abd11..24841016c 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -12,7 +12,7 @@ Copyright (c) 2015 Microsoft Corporation #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/var_subst.h" -#define IS_EQUIV(_e_) (m.is_eq(_e_) || m.is_iff(_e_)) +#define IS_EQUIV(_e_) m.is_eq(_e_) #define SAME_OP(_d1_, _d2_) ((_d1_ == _d2_) || (IS_EQUIV(_d1_) && IS_EQUIV(_d2_))) @@ -1032,7 +1032,7 @@ bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const { } bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const { - return match_op(e, OP_IFF, t1, t2); + return match_op(e, OP_EQ, t1, t2) && m.is_bool(t1); } bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const { @@ -1044,7 +1044,7 @@ bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) con } bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const { - return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2); + return match_op(e, OP_EQ, t1, t2); } bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const { diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h index 455f39c4f..729a30eb0 100644 --- a/src/ast/proofs/proof_utils.h +++ b/src/ast/proofs/proof_utils.h @@ -110,10 +110,10 @@ public: if (m.is_or(decl)) { mk_or_core(args, res); } - else if (m.is_iff(decl) && args.size() == 2) + else if (m.is_eq(decl) && args.size() == 2) // avoiding simplifying equalities. In particular, // we don't want (= (not a) (not b)) to be reduced to (= a b) - { res = m.mk_iff(args.get(0), args.get(1)); } + { res = m.mk_eq(args.get(0), args.get(1)); } else { brwr.mk_app(decl, args.size(), args.c_ptr(), res); } } diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 5cf25335b..46613a12e 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -39,7 +39,6 @@ br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co SASSERT(f->get_family_id() == m().get_basic_family_id()); switch (f->get_decl_kind()) { case OP_EQ: - case OP_IFF: SASSERT(num_args == 2); return mk_eq_core(args[0], args[1], result); case OP_DISTINCT: @@ -428,7 +427,7 @@ bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, exp neg = true; t = to_app(t)->get_arg(0); } - if (m().is_iff(t) || m().is_eq(t)) { + if (m().is_eq(t)) { bool modified = false; expr * new_lhs = simp_arg(to_app(t)->get_arg(0), neg_lits, pos_lits, modified); expr * new_rhs = simp_arg(to_app(t)->get_arg(1), neg_lits, pos_lits, modified); @@ -708,7 +707,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { expr *la, *lb, *ra, *rb; // fold (iff (iff a b) (iff (not a) b)) to false - if (m().is_iff(lhs, la, lb) && m().is_iff(rhs, ra, rb)) { + if (m().is_eq(lhs, la, lb) && m().is_eq(rhs, ra, rb)) { expr *n; if ((la == ra && ((m().is_not(rb, n) && n == lb) || (m().is_not(lb, n) && n == rb))) || diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 34e03c1ed..83ece2aae 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -81,7 +81,7 @@ public: bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); } ast_manager & m() const { return m_manager; } family_id get_fid() const { return m().get_basic_family_id(); } - bool is_eq(expr * t) const { return m().is_eq(t) || m().is_iff(t); } + bool is_eq(expr * t) const { return m().is_eq(t); } bool flat() const { return m_flat; } void set_flat(bool f) { m_flat = f; } diff --git a/src/ast/rewriter/der.cpp b/src/ast/rewriter/der.cpp index 021943585..54409e9c2 100644 --- a/src/ast/rewriter/der.cpp +++ b/src/ast/rewriter/der.cpp @@ -40,11 +40,8 @@ static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) { */ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { // (not (= VAR t)) and (not (iff VAR t)) cases - if (m_manager.is_not(e) && (m_manager.is_eq(to_app(e)->get_arg(0)) || m_manager.is_iff(to_app(e)->get_arg(0)))) { - app * eq = to_app(to_app(e)->get_arg(0)); - SASSERT(m_manager.is_eq(eq) || m_manager.is_iff(eq)); - expr * lhs = eq->get_arg(0); - expr * rhs = eq->get_arg(1); + expr *eq, * lhs, *rhs; + if (m_manager.is_not(e, eq) && m_manager.is_eq(eq, lhs, rhs)) { if (!is_var(lhs, num_decls) && !is_var(rhs, num_decls)) return false; if (!is_var(lhs, num_decls)) @@ -60,9 +57,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) { return true; } // (iff VAR t) and (iff (not VAR) t) cases - else if (m_manager.is_iff(e)) { - expr * lhs = to_app(e)->get_arg(0); - expr * rhs = to_app(e)->get_arg(1); + else if (m_manager.is_eq(e, lhs, rhs) && m_manager.is_bool(lhs)) { // (iff VAR t) case if (is_var(lhs, num_decls) || is_var(rhs, num_decls)) { if (!is_var(lhs, num_decls)) diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index 3592f84cd..2f1116299 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -259,7 +259,7 @@ private: result = m.mk_ite(t1, tt2, tt3); } } - else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) { + else if (m.is_eq(fml, t1, t2) && m.is_bool(t1)) { expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m); pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok); pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index f5a0ff0f7..912df0fc9 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -187,7 +187,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (st != BR_FAILED) return st; } - if (k == OP_EQ || k == OP_IFF) { + if (k == OP_EQ) { SASSERT(num == 2); st = apply_tamagotchi(args[0], args[1], result); if (st != BR_FAILED) diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index c8a1adcbe..e3530b4b5 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -154,8 +154,10 @@ bool static_features::is_diff_atom(expr const * e) const { bool static_features::is_gate(expr const * e) const { if (is_basic_expr(e)) { switch (to_app(e)->get_decl_kind()) { - case OP_ITE: case OP_AND: case OP_OR: case OP_IFF: case OP_XOR: case OP_IMPLIES: + case OP_ITE: case OP_AND: case OP_OR: case OP_XOR: case OP_IMPLIES: return true; + case OP_EQ: + return m_manager.is_bool(e); } } return false; @@ -207,7 +209,7 @@ void static_features::update_core(expr * e) { case OP_OR: m_num_ors++; break; - case OP_IFF: + case OP_EQ: m_num_iffs++; break; } @@ -418,7 +420,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite form_ctx_new = true; or_and_ctx_new = true; break; - case OP_IFF: + case OP_EQ: form_ctx_new = true; break; } diff --git a/src/model/model_implicant.cpp b/src/model/model_implicant.cpp index 3456c2746..0cdd80c11 100644 --- a/src/model/model_implicant.cpp +++ b/src/model/model_implicant.cpp @@ -172,7 +172,6 @@ void model_implicant::process_formula(app* e, ptr_vector& todo, ptr_vector case OP_FALSE: break; case OP_EQ: - case OP_IFF: if (args[0] == args[1]) { SASSERT(v); // no-op @@ -742,10 +741,6 @@ void model_implicant::eval_basic(app* e) { set_x(e); } break; - case OP_IFF: - VERIFY(m.is_iff(e, arg1, arg2)); - eval_eq(e, arg1, arg2); - break; case OP_ITE: VERIFY(m.is_ite(e, argCond, argThen, argElse)); if (is_true(argCond)) { diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 21317a07c..315765acc 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -146,12 +146,10 @@ void rule_properties::check_existential_tail() { else if (is_quantifier(e)) { tocheck.push_back(to_quantifier(e)->get_expr()); } - else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && - m.is_true(e1)) { + else if (m.is_eq(e, e1, e2) && m.is_true(e1)) { todo.push_back(e2); } - else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && - m.is_true(e2)) { + else if (m.is_eq(e, e1, e2) && m.is_true(e2)) { todo.push_back(e1); } else { diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 77b79ba04..c2cd94ee0 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -830,7 +830,7 @@ namespace pdr { flatten_and(state(), conjs); for (unsigned i = 0; i < conjs.size(); ++i) { expr* e = conjs[i].get(), *e1, *e2; - if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) { + if (m.is_eq(e, e1, e2)) { if (m.is_value(e2)) { model.insert(e1, e2); } diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 2e9ab693c..ea292a29e 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -869,7 +869,7 @@ namespace datalog { dm.set(*d, idx, BIT_1); result.intersect(dm, *d); } - else if ((m.is_eq(g, e1, e2) || m.is_iff(g, e1, e2)) && m.is_bool(e1)) { + else if (m.is_iff(g, e1, e2)) { udoc diff1, diff2; diff1.push_back(dm.allocateX()); diff2.push_back(dm.allocateX()); diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp index fc3eabc56..5feaed1fa 100644 --- a/src/muz/spacer/spacer_legacy_mev.cpp +++ b/src/muz/spacer/spacer_legacy_mev.cpp @@ -138,7 +138,6 @@ void model_evaluator::process_formula(app* e, ptr_vector& todo, ptr_vector case OP_FALSE: break; case OP_EQ: - case OP_IFF: if (args[0] == args[1]) { SASSERT(v); // no-op @@ -634,10 +633,6 @@ void model_evaluator::eval_basic(app* e) set_x(e); } break; - case OP_IFF: - VERIFY(m.is_iff(e, arg1, arg2)); - eval_eq(e, arg1, arg2); - break; case OP_XOR: VERIFY(m.is_xor(e, arg1, arg2)); eval_eq(e, arg1, arg2); diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index cb11afc9f..b4e5e7710 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -403,27 +403,26 @@ namespace spacer { public: test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {} - + void test_for_utvpi() { m_test_for_utvpi = true; } - - void operator()(expr* e) - { + + void operator()(expr* e) { if (!m_is_dl) { return; } if (a.is_le(e) || a.is_ge(e)) { m_is_dl = test_ineq(e); - } else if (m.is_eq(e)) { + } else if (m.is_eq(e)) { m_is_dl = test_eq(e); - } else if (is_non_arith_or_basic(e)) { + } else if (is_non_arith_or_basic(e)) { m_is_dl = false; - } else if (is_app(e)) { + } else if (is_app(e)) { app* a = to_app(e); for (unsigned i = 0; m_is_dl && i < a->get_num_args(); ++i) { m_is_dl = test_term(a->get_arg(i)); } } - + if (!m_is_dl) { char const* msg = "non-diff: "; if (m_test_for_utvpi) { @@ -432,12 +431,11 @@ namespace spacer { IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";); } } - + bool is_dl() const { return m_is_dl; } }; - -bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) -{ + + bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { test_diff_logic test(m); expr_fast_mark1 mark; for (unsigned i = 0; i < num_fmls; ++i) { @@ -445,9 +443,8 @@ bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) } return test.is_dl(); } - -bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) -{ + + bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { test_diff_logic test(m); test.test_for_utvpi(); expr_fast_mark1 mark; @@ -458,14 +455,13 @@ bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) } - void subst_vars (ast_manager& m, app_ref_vector const& vars, - model* M, expr_ref& fml) -{ + void subst_vars(ast_manager& m, + app_ref_vector const& vars, + model* M, expr_ref& fml) { expr_safe_replace sub (m); model_evaluator_util mev (m); mev.set_model(*M); - for (unsigned i = 0; i < vars.size (); i++) { - app* v = vars.get (i); + for (app * v : vars) { expr_ref val (m); VERIFY(mev.eval (v, val, true)); sub.insert (v, val); @@ -477,30 +473,23 @@ bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) * eliminate simple equalities using qe_lite * then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays */ -void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, + void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, const model_ref& M, bool reduce_all_selects, bool use_native_mbp, - bool dont_sub) -{ + bool dont_sub) { th_rewriter rw (m); TRACE ("spacer_mbp", - tout << "Before projection:\n"; - tout << mk_pp (fml, m) << "\n"; - tout << "Vars:\n"; - for (unsigned i = 0; i < vars.size(); ++i) { - tout << mk_pp(vars.get (i), m) << "\n"; - } - ); + tout << "Before projection:\n"; + tout << mk_pp (fml, m) << "\n"; + tout << "Vars:\n"; + for (app* v : vars) tout << mk_pp(v, m) << "\n";); { - // Ensure that top-level AND of fml is flat - expr_ref_vector flat(m); - flatten_and (fml, flat); - if (flat.size () == 1) - { fml = flat.get(0); } - else if (flat.size () > 1) - { fml = m.mk_and(flat.size(), flat.c_ptr()); } + // Ensure that top-level AND of fml is flat + expr_ref_vector flat(m); + flatten_and (fml, flat); + fml = mk_and(flat); } - + app_ref_vector arith_vars (m); app_ref_vector array_vars (m); array_util arr_u (m); @@ -511,77 +500,72 @@ void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, while (true) { params_ref p; qe_lite qe(m, p, false); - qe (vars, fml); - rw (fml); + qe (vars, fml); + rw (fml); + + TRACE ("spacer_mbp", + tout << "After qe_lite:\n"; + tout << mk_pp (fml, m) << "\n"; + tout << "Vars:\n"; + for (unsigned i = 0; i < vars.size(); ++i) { + tout << mk_pp(vars.get (i), m) << "\n"; + } + ); + SASSERT (!m.is_false (fml)); - TRACE ("spacer_mbp", - tout << "After qe_lite:\n"; - tout << mk_pp (fml, m) << "\n"; - tout << "Vars:\n"; - for (unsigned i = 0; i < vars.size(); ++i) { - tout << mk_pp(vars.get (i), m) << "\n"; - } - ); - SASSERT (!m.is_false (fml)); - - bool has_bool_vars = false; - - // sort out vars into bools, arith (int/real), and arrays - for (unsigned i = 0; i < vars.size (); i++) { - if (m.is_bool (vars.get (i))) { - // obtain the interpretation of the ith var using model completion - VERIFY (M->eval (vars.get (i), bval, true)); - bool_sub.insert (vars.get (i), bval); - has_bool_vars = true; + bool has_bool_vars = false; + + // sort out vars into bools, arith (int/real), and arrays + for (unsigned i = 0; i < vars.size (); i++) { + if (m.is_bool (vars.get (i))) { + // obtain the interpretation of the ith var using model completion + VERIFY (M->eval (vars.get (i), bval, true)); + bool_sub.insert (vars.get (i), bval); + has_bool_vars = true; } else if (arr_u.is_array(vars.get(i))) { - array_vars.push_back (vars.get (i)); + array_vars.push_back (vars.get (i)); } else { - SASSERT (ari_u.is_int (vars.get (i)) || ari_u.is_real (vars.get (i))); - arith_vars.push_back (vars.get (i)); - } + SASSERT (ari_u.is_int (vars.get (i)) || ari_u.is_real (vars.get (i))); + arith_vars.push_back (vars.get (i)); } - - // substitute Booleans - if (has_bool_vars) { - bool_sub (fml); - // -- bool_sub is not simplifying - rw (fml); - SASSERT (!m.is_false (fml)); - TRACE ("spacer_mbp", - tout << "Projected Booleans:\n" << mk_pp (fml, m) << "\n"; - ); - bool_sub.reset (); - } - + } + + // substitute Booleans + if (has_bool_vars) { + bool_sub (fml); + // -- bool_sub is not simplifying + rw (fml); + SASSERT (!m.is_false (fml)); TRACE ("spacer_mbp", - tout << "Array vars:\n"; - for (unsigned i = 0; i < array_vars.size (); ++i) { - tout << mk_pp (array_vars.get (i), m) << "\n"; - } - ); - - vars.reset (); - - // project arrays - { - scoped_no_proof _sp (m); - // -- local rewriter that is aware of current proof mode - th_rewriter srw(m); - qe::array_project (*M.get (), array_vars, fml, vars, reduce_all_selects); - SASSERT (array_vars.empty ()); - srw (fml); - SASSERT (!m.is_false (fml)); - } - - TRACE ("spacer_mbp", - tout << "extended model:\n"; - model_pp (tout, *M); - tout << "Auxiliary variables of index and value sorts:\n"; - for (unsigned i = 0; i < vars.size (); i++) { - tout << mk_pp (vars.get (i), m) << "\n"; - } - ); - + tout << "Projected Booleans:\n" << mk_pp (fml, m) << "\n"; + ); + bool_sub.reset (); + } + + TRACE ("spacer_mbp", + tout << "Array vars:\n"; + tout << array_vars;); + + vars.reset (); + + // project arrays + { + scoped_no_proof _sp (m); + // -- local rewriter that is aware of current proof mode + th_rewriter srw(m); + qe::array_project (*M.get (), array_vars, fml, vars, reduce_all_selects); + SASSERT (array_vars.empty ()); + srw (fml); + SASSERT (!m.is_false (fml)); + } + + TRACE ("spacer_mbp", + tout << "extended model:\n"; + model_pp (tout, *M); + tout << "Auxiliary variables of index and value sorts:\n"; + tout << vars; + ); + if (vars.empty()) { break; } } diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index 6894cf4fa..34e739bc3 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -42,7 +42,7 @@ namespace datalog { } bool mk_array_blast::is_store_def(expr* e, expr*& x, expr*& y) { - if (m.is_iff(e, x, y) || m.is_eq(e, x, y)) { + if (m.is_eq(e, x, y)) { if (!a.is_store(y)) { std::swap(x,y); } diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 4cbcc5712..9f6302e05 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -180,7 +180,7 @@ namespace datalog { } m_terms[n] = e; visited.mark(e); - if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) { + if (m.is_eq(e, e1, e2)) { m_uf.merge(e1->get_id(), e2->get_id()); } if (is_app(e)) { diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp index 133652c1d..42ae36564 100644 --- a/src/nlsat/tactic/goal2nlsat.cpp +++ b/src/nlsat/tactic/goal2nlsat.cpp @@ -198,7 +198,6 @@ struct goal2nlsat::imp { throw tactic_exception("apply simplify before applying nlsat"); case OP_AND: case OP_OR: - case OP_IFF: case OP_XOR: case OP_NOT: case OP_IMPLIES: diff --git a/src/parsers/util/cost_parser.cpp b/src/parsers/util/cost_parser.cpp index 765b8ade9..91362b37a 100644 --- a/src/parsers/util/cost_parser.cpp +++ b/src/parsers/util/cost_parser.cpp @@ -32,7 +32,7 @@ cost_parser::cost_parser(ast_manager & m): add_builtin_op("or", fid, OP_OR); add_builtin_op("ite", fid, OP_ITE); add_builtin_op("=", fid, OP_EQ); - add_builtin_op("iff", fid, OP_IFF); + add_builtin_op("iff", fid, OP_EQ); add_builtin_op("xor", fid, OP_XOR); fid = m_util.get_family_id(); diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index daed18f7a..3916e547c 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -614,7 +614,7 @@ namespace qe { else if (m.is_ite(a)) { nnf_ite(a, p); } - else if (m.is_iff(a) || (m.is_eq(a) && m.is_bool(a->get_arg(0)))) { + else if (m.is_iff(a)) { nnf_iff(a, p); } else if (m.is_xor(a)) { diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 6ecdfd835..2a14aa6f2 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -345,7 +345,7 @@ namespace eq { var* v; // (= VAR t), (iff VAR t), (iff (not VAR) t), (iff t (not VAR)) cases - if (m.is_eq(e, lhs, rhs) || m.is_iff(e, lhs, rhs)) { + if (m.is_eq(e, lhs, rhs)) { // (iff (not VAR) t) (iff t (not VAR)) cases if (!is_variable(lhs) && !is_variable(rhs) && m.is_bool(lhs)) { if (!is_neg_var(m, lhs, v)) { diff --git a/src/sat/tactic/atom2bool_var.cpp b/src/sat/tactic/atom2bool_var.cpp index e3c9b6767..b79eaa251 100644 --- a/src/sat/tactic/atom2bool_var.cpp +++ b/src/sat/tactic/atom2bool_var.cpp @@ -75,7 +75,7 @@ struct collect_boolean_interface_proc { continue; if (is_app(t) && to_app(t)->get_family_id() == m.get_basic_family_id() && to_app(t)->get_num_args() > 0) { decl_kind k = to_app(t)->get_decl_kind(); - if (k == OP_OR || k == OP_NOT || k == OP_IFF || ((k == OP_EQ || k == OP_ITE) && m.is_bool(to_app(t)->get_arg(1)))) { + if (k == OP_OR || k == OP_NOT || ((k == OP_EQ || k == OP_ITE) && m.is_bool(to_app(t)->get_arg(1)))) { unsigned num = to_app(t)->get_num_args(); for (unsigned i = 0; i < num; i++) { expr * arg = to_app(t)->get_arg(i); diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index ea9c5b4ea..75290946a 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -201,7 +201,6 @@ struct goal2sat::imp { case OP_NOT: case OP_OR: case OP_AND: - case OP_IFF: m_frame_stack.push_back(frame(to_app(t), root, sign, 0)); return false; case OP_ITE: @@ -630,7 +629,6 @@ struct goal2sat::imp { case OP_ITE: convert_ite(t, root, sign); break; - case OP_IFF: case OP_EQ: convert_iff(t, root, sign); break; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index c00fb93b1..c7ae7605f 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -500,8 +500,7 @@ unsigned asserted_formulas::propagate_values(unsigned i) { void asserted_formulas::update_substitution(expr* n, proof* pr) { expr* lhs, *rhs, *n1; - proof_ref pr1(m); - if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) { + if (is_ground(n) && m.is_eq(n, lhs, rhs)) { compute_depth(lhs); compute_depth(rhs); if (is_gt(lhs, rhs)) { @@ -511,12 +510,12 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) { } if (is_gt(rhs, lhs)) { TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";); - pr1 = m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr; - m_scoped_substitution.insert(rhs, lhs, pr1); + m_scoped_substitution.insert(rhs, lhs, m.proofs_enabled() ? m.mk_symmetry(pr) : nullptr); return; } TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";); } + proof_ref pr1(m); if (m.is_not(n, n1)) { pr1 = m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr; m_scoped_substitution.insert(n1, m.mk_false(), pr1); diff --git a/src/smt/cost_evaluator.cpp b/src/smt/cost_evaluator.cpp index 94151f2b3..0719d0961 100644 --- a/src/smt/cost_evaluator.cpp +++ b/src/smt/cost_evaluator.cpp @@ -47,8 +47,7 @@ float cost_evaluator::eval(expr * f) const { return 1.0f; return 0.0f; case OP_ITE: return E(0) != 0.0f ? E(1) : E(2); - case OP_EQ: - case OP_IFF: return E(0) == E(1) ? 1.0f : 0.0f; + case OP_EQ: return E(0) == E(1) ? 1.0f : 0.0f; case OP_XOR: return E(0) != E(1) ? 1.0f : 0.0f; case OP_IMPLIES: if (E(0) == 0.0f) diff --git a/src/smt/expr_context_simplifier.cpp b/src/smt/expr_context_simplifier.cpp index bce28420d..a57b0299f 100644 --- a/src/smt/expr_context_simplifier.cpp +++ b/src/smt/expr_context_simplifier.cpp @@ -110,13 +110,15 @@ void expr_context_simplifier::reduce_rec(app * a, expr_ref & result) { case OP_OR: reduce_or(a->get_num_args(), a->get_args(), result); return; - case OP_IFF: { - expr_ref tmp1(m_manager), tmp2(m_manager); - reduce_rec(a->get_arg(0), tmp1); - reduce_rec(a->get_arg(1), tmp2); - m_simp.mk_iff(tmp1.get(), tmp2.get(), result); - return; - } + case OP_EQ: + if (m_manager.is_iff(a)) { + expr_ref tmp1(m_manager), tmp2(m_manager); + reduce_rec(a->get_arg(0), tmp1); + reduce_rec(a->get_arg(1), tmp2); + m_simp.mk_iff(tmp1.get(), tmp2.get(), result); + return; + } + break; case OP_XOR: { expr_ref tmp1(m_manager), tmp2(m_manager); reduce_rec(a->get_arg(0), tmp1); @@ -580,7 +582,7 @@ void expr_strong_context_simplifier::simplify_model_based(expr* fml, expr_ref& r } assignment_map.insert(a, value); } - else if (m.is_iff(a, n1, n2) || m.is_eq(a, n1, n2)) { + else if (m.is_eq(a, n1, n2)) { lbool v1 = assignment_map.find(n1); lbool v2 = assignment_map.find(n2); if (v1 == l_undef || v2 == l_undef) { diff --git a/src/smt/smt_checker.cpp b/src/smt/smt_checker.cpp index ed80eaab7..1b6a5d370 100644 --- a/src/smt/smt_checker.cpp +++ b/src/smt/smt_checker.cpp @@ -61,8 +61,20 @@ namespace smt { return is_true ? any_arg(a, true) : all_args(a, false); case OP_AND: return is_true ? all_args(a, true) : any_arg(a, false); - case OP_IFF: - if (is_true) { + case OP_EQ: + if (!m_manager.is_iff(a)) { + enode * lhs = get_enode_eq_to(a->get_arg(0)); + enode * rhs = get_enode_eq_to(a->get_arg(1)); + if (lhs && rhs && m_context.is_relevant(lhs) && m_context.is_relevant(rhs)) { + if (is_true && lhs->get_root() == rhs->get_root()) + return true; + // if (!is_true && m_context.is_ext_diseq(lhs, rhs, 2)) + if (!is_true && m_context.is_diseq(lhs, rhs)) + return true; + } + return false; + } + else if (is_true) { return (check(a->get_arg(0), true) && check(a->get_arg(1), true)) || @@ -86,18 +98,6 @@ namespace smt { } return check(a->get_arg(1), is_true) && check(a->get_arg(2), is_true); } - case OP_EQ: { - enode * lhs = get_enode_eq_to(a->get_arg(0)); - enode * rhs = get_enode_eq_to(a->get_arg(1)); - if (lhs && rhs && m_context.is_relevant(lhs) && m_context.is_relevant(rhs)) { - if (is_true && lhs->get_root() == rhs->get_root()) - return true; - // if (!is_true && m_context.is_ext_diseq(lhs, rhs, 2)) - if (!is_true && m_context.is_diseq(lhs, rhs)) - return true; - } - return false; - } default: break; } diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 379846ed7..7984fd5f0 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -771,7 +771,7 @@ namespace smt { app * fact = to_app(m_manager.get_fact(pr)); app * n1_owner = n1->get_owner(); app * n2_owner = n2->get_owner(); - bool is_eq = m_manager.is_eq(fact) || m_manager.is_iff(fact); + bool is_eq = m_manager.is_eq(fact); if (!is_eq || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) { CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2), tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n"; @@ -794,7 +794,7 @@ namespace smt { TRACE("norm_eq_proof", tout << "#" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n"; tout << mk_ll_pp(pr, m_manager, true, false);); - SASSERT(m_manager.is_eq(fact) || m_manager.is_iff(fact)); + SASSERT(m_manager.is_eq(fact)); SASSERT((fact->get_arg(0) == n1->get_owner() && fact->get_arg(1) == n2->get_owner()) || (fact->get_arg(1) == n1->get_owner() && fact->get_arg(0) == n2->get_owner())); if (fact->get_arg(0) == n1_owner && fact->get_arg(1) == n2_owner) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index dc7c32cc1..f9ee900ff 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -34,9 +34,10 @@ namespace smt { switch (to_app(n)->get_decl_kind()) { case OP_AND: case OP_OR: - case OP_IFF: case OP_ITE: return true; + case OP_EQ: + return m.is_bool(to_app(n)->get_arg(0)); default: return false; } @@ -229,7 +230,7 @@ namespace smt { add_or_rel_watches(to_app(n)); break; } - case OP_IFF: { + case OP_EQ: { expr * lhs = to_app(n)->get_arg(0); expr * rhs = to_app(n)->get_arg(1); internalize(lhs, true); @@ -381,7 +382,7 @@ namespace smt { return; } - if (m_manager.is_eq(n)) + if (m_manager.is_eq(n) && !m_manager.is_iff(n)) internalize_eq(to_app(n), gate_ctx); else if (m_manager.is_distinct(n)) internalize_distinct(to_app(n), gate_ctx); @@ -538,9 +539,7 @@ namespace smt { bool _is_gate = is_gate(m_manager, n) || m_manager.is_not(n); // process args - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * arg = n->get_arg(i); + for (expr * arg : *n) { internalize(arg, _is_gate); } @@ -596,8 +595,9 @@ namespace smt { mk_or_cnstr(to_app(n)); add_or_rel_watches(to_app(n)); break; - case OP_IFF: - mk_iff_cnstr(to_app(n)); + case OP_EQ: + if (m_manager.is_iff(n)) + mk_iff_cnstr(to_app(n)); break; case OP_ITE: mk_ite_cnstr(to_app(n)); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 5e21c0dcc..4307d3fdf 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2315,9 +2315,6 @@ namespace smt { case OP_ITE: process_ite(to_app(curr), pol); break; - case OP_IFF: - process_iff(to_app(curr)); - break; case OP_EQ: if (m_manager.is_bool(to_app(curr)->get_arg(0))) { process_iff(to_app(curr)); diff --git a/src/smt/smt_quantifier_stat.cpp b/src/smt/smt_quantifier_stat.cpp index 7d73ea27c..8c7fd196e 100644 --- a/src/smt/smt_quantifier_stat.cpp +++ b/src/smt/smt_quantifier_stat.cpp @@ -82,11 +82,13 @@ namespace smt { if (depth > 0) m_case_split_factor *= (num_args + 1); break; - case OP_IFF: - if (depth == 0) - m_case_split_factor *= 4; - else - m_case_split_factor *= 9; + case OP_EQ: + if (m_manager.is_iff(n)) { + if (depth == 0) + m_case_split_factor *= 4; + else + m_case_split_factor *= 9; + } break; case OP_ITE: if (depth == 0) diff --git a/src/smt/smt_quick_checker.cpp b/src/smt/smt_quick_checker.cpp index 64c791a0e..72a720d98 100644 --- a/src/smt/smt_quick_checker.cpp +++ b/src/smt/smt_quick_checker.cpp @@ -311,11 +311,6 @@ namespace smt { return is_true ? any_arg(a, true) : all_args(a, false); case OP_AND: return is_true ? all_args(a, true) : any_arg(a, false); - case OP_IFF: - if (is_true) - return (check(a->get_arg(0), true) && check(a->get_arg(1), true)) || (check(a->get_arg(0), false) && check(a->get_arg(1), false)); - else - return (check(a->get_arg(0), true) && check(a->get_arg(1), false)) || (check(a->get_arg(0), false) && check(a->get_arg(1), true)); case OP_ITE: if (check(a->get_arg(0), true)) return check(a->get_arg(1), is_true); @@ -324,6 +319,13 @@ namespace smt { else return check(a->get_arg(1), is_true) && check(a->get_arg(2), is_true); case OP_EQ: + if (m_manager.is_iff(a)) { + if (is_true) + return (check(a->get_arg(0), true) && check(a->get_arg(1), true)) || (check(a->get_arg(0), false) && check(a->get_arg(1), false)); + else + return (check(a->get_arg(0), true) && check(a->get_arg(1), false)) || (check(a->get_arg(0), false) && check(a->get_arg(1), true)); + } + if (is_true) { return canonize(a->get_arg(0)) == canonize(a->get_arg(1)); } diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 89196808f..faedf0e0c 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -490,7 +490,6 @@ struct aig_manager::imp { case OP_NOT: case OP_OR: case OP_AND: - case OP_IFF: case OP_XOR: case OP_IMPLIES: case OP_ITE: @@ -582,9 +581,6 @@ struct aig_manager::imp { SASSERT(m.m().is_bool(fr.m_t->get_arg(0))); mk_iff(fr.m_spos); break; - case OP_IFF: - mk_iff(fr.m_spos); - break; case OP_XOR: mk_xor(fr.m_spos); break; diff --git a/src/tactic/core/cofactor_elim_term_ite.cpp b/src/tactic/core/cofactor_elim_term_ite.cpp index 2b3cb8414..1b435791c 100644 --- a/src/tactic/core/cofactor_elim_term_ite.cpp +++ b/src/tactic/core/cofactor_elim_term_ite.cpp @@ -87,7 +87,6 @@ struct cofactor_elim_term_ite::imp { case OP_TRUE: case OP_FALSE: case OP_ITE: - case OP_IFF: return; case OP_EQ: case OP_DISTINCT: diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 43da3bc00..27a5bdc94 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -486,7 +486,7 @@ bool expr_substitution_simplifier::is_gt(expr* lhs, expr* rhs) { void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) { expr* lhs, *rhs, *n1; - if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) { + if (is_ground(n) && m.is_eq(n, lhs, rhs)) { compute_depth(lhs); compute_depth(rhs); m_trail.push_back(lhs); diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index ce77f89d9..577db30cd 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -331,7 +331,6 @@ class elim_uncnstr_tactic : public tactic { return r; } return nullptr; - case OP_IFF: case OP_EQ: SASSERT(num == 2); return process_eq(f, args[0], args[1]); diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp index acd75d663..f579b7b4f 100644 --- a/src/tactic/core/solve_eqs_tactic.cpp +++ b/src/tactic/core/solve_eqs_tactic.cpp @@ -344,10 +344,7 @@ class solve_eqs_tactic : public tactic { } return false; } - - if (m().is_iff(f)) - return trivial_solve(to_app(f)->get_arg(0), to_app(f)->get_arg(1), var, def, pr); - + #if 0 if (not_bool_eq(f, var, def, pr)) return true; diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index 2abaae0e6..9c57fe791 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -176,7 +176,6 @@ class tseitin_cnf_tactic : public tactic { sign = !sign; goto start; case OP_OR: - case OP_IFF: l = nullptr; m_cache.find(to_app(n), l); SASSERT(l != 0); @@ -223,7 +222,6 @@ class tseitin_cnf_tactic : public tactic { goto start; } case OP_OR: - case OP_IFF: visited = false; push_frame(to_app(n)); return;