mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

add missing process_eq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-12 18:43:57 -08:00
parent 0b83732b82
commit 3d570aaa0a
1 changed files with 26 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/ast/converters/expr_inverter.cpp
View file

@ -22,9 +22,32 @@ Author:
#include "ast/converters/expr_inverter.h"
class basic_expr_inverter : public iexpr_inverter {
iexpr_inverter& inv;
bool process_eq(func_decl* f, expr* arg1, expr* arg2, expr_ref& r) {
expr* v;
expr* t;
if (uncnstr(arg1))
v = arg1, t = arg2;
else if (uncnstr(arg2))
v = arg2, t = arg1;
else
return false;
expr_ref d(m);
if (!inv.mk_diff(t, d))
return false;
mk_fresh_uncnstr_var_for(f, r);
if (m_mc)
add_def(v, m.mk_ite(t, t, d));
return true;
}
public:
basic_expr_inverter(ast_manager& m) : iexpr_inverter(m) {}
basic_expr_inverter(ast_manager& m, iexpr_inverter& inv) : iexpr_inverter(m), inv(inv) {}
/**
* if (c, x, x') -> fresh
@ -104,7 +127,7 @@ public:
return false;
case OP_EQ:
SASSERT(num == 2);
// return process_eq(f, args[0], args[1]);
return process_eq(f, args[0], args[1], r);
default:
return false;
}
@ -726,7 +749,7 @@ expr_inverter::expr_inverter(ast_manager& m): iexpr_inverter(m) {
auto* b = alloc(bv_expr_inverter, m);
auto* ar = alloc(array_expr_inverter, m, *this);
auto* dt = alloc(dt_expr_inverter, m);
m_inverters.setx(m.get_basic_family_id(), alloc(basic_expr_inverter, m), nullptr);
m_inverters.setx(m.get_basic_family_id(), alloc(basic_expr_inverter, m, *this), nullptr);
m_inverters.setx(a->get_fid(), a, nullptr);
m_inverters.setx(b->get_fid(), b, nullptr);
m_inverters.setx(ar->get_fid(), ar, nullptr);