mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
remove iff
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ecf15ab07d
commit
ff0f257102
|
@ -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;
|
||||
|
|
|
@ -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<builtin_name> & 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_vector<exp
|
|||
|
||||
bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
|
||||
if (is_rewrite(e)) {
|
||||
VERIFY (is_eq(to_app(e)->get_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<expr> 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;
|
||||
|
||||
|
|
|
@ -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); }
|
||||
|
|
|
@ -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());
|
||||
|
|
|
@ -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 << "=>";
|
||||
}
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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)) {
|
||||
|
|
|
@ -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)) {
|
||||
|
|
|
@ -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);
|
||||
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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 {
|
||||
|
|
|
@ -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); }
|
||||
}
|
||||
|
|
|
@ -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))) ||
|
||||
|
|
|
@ -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; }
|
||||
|
|
|
@ -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))
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -172,7 +172,6 @@ void model_implicant::process_formula(app* e, ptr_vector<expr>& 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)) {
|
||||
|
|
|
@ -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 {
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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());
|
||||
|
|
|
@ -138,7 +138,6 @@ void model_evaluator::process_formula(app* e, ptr_vector<expr>& 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);
|
||||
|
|
|
@ -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; }
|
||||
}
|
||||
|
||||
|
|
|
@ -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);
|
||||
}
|
||||
|
|
|
@ -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)) {
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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();
|
||||
|
|
|
@ -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)) {
|
||||
|
|
|
@ -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)) {
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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) {
|
||||
|
|
|
@ -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;
|
||||
}
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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));
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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));
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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);
|
||||
|
|
|
@ -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]);
|
||||
|
|
|
@ -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;
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue