mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
types
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d6848175eb
commit
828fc72754
|
@ -3882,7 +3882,7 @@ namespace z3 {
|
|||
|
||||
|
||||
public:
|
||||
user_propagator_base(context* c) : s(nullptr), c(c) {}
|
||||
user_propagator_base(Z3_context c) : s(nullptr), c(c) {}
|
||||
|
||||
user_propagator_base(solver* s): s(s), c(nullptr) {
|
||||
Z3_solver_propagate_init(ctx(), *s, this, push_eh, pop_eh, fresh_eh);
|
||||
|
|
|
@ -275,7 +275,6 @@ namespace array {
|
|||
* e1 = e2 or select(e1, diff(e1,e2)) != select(e2, diff(e1, e2))
|
||||
*/
|
||||
bool solver::assert_extensionality(expr* e1, expr* e2) {
|
||||
TRACE("array", tout << "extensionality-axiom: " << mk_bounded_pp(e1, m) << " == " << mk_bounded_pp(e2, m) << "\n";);
|
||||
++m_stats.m_num_extensionality_axiom;
|
||||
func_decl_ref_vector const& funcs = sort2diff(e1->get_sort());
|
||||
expr_ref_vector args1(m), args2(m);
|
||||
|
@ -290,6 +289,7 @@ namespace array {
|
|||
expr_ref sel2(a.mk_select(args2), m);
|
||||
literal lit1 = eq_internalize(e1, e2);
|
||||
literal lit2 = eq_internalize(sel1, sel2);
|
||||
TRACE("array", tout << "extensionality-axiom: " << mk_bounded_pp(e1, m) << " == " << mk_bounded_pp(e2, m) << "\n" << lit1 << " " << ~lit2 << "\n";);
|
||||
return add_clause(lit1, ~lit2);
|
||||
}
|
||||
|
||||
|
|
|
@ -277,9 +277,15 @@ namespace euf {
|
|||
if (!tt && !mdl.is_true(e))
|
||||
continue;
|
||||
IF_VERBOSE(0,
|
||||
verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
|
||||
for (auto* arg : euf::enode_args(n))
|
||||
verbose_stream() << bpp(arg) << "\n" << mdl(arg->get_expr()) << "\n";);
|
||||
verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
|
||||
for (auto* arg : euf::enode_args(n)) {
|
||||
expr_ref val = mdl(arg->get_expr());
|
||||
expr_ref sval(m);
|
||||
th_rewriter rw(m);
|
||||
rw(val, sval);
|
||||
verbose_stream() << bpp(arg) << "\n" << sval << "\n";
|
||||
|
||||
});
|
||||
CTRACE("euf", first,
|
||||
tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
|
||||
s().display(tout);
|
||||
|
|
Loading…
Reference in a new issue