From 84475ff142c5a4ed51d9a056b89046a6e8b13ac8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Aug 2020 10:05:17 -0700 Subject: [PATCH] fix #4637 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 5 ++++- src/smt/user_propagator.h | 23 ++++++++++------------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index fad9673b7..4d51c5615 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2864,7 +2864,10 @@ namespace z3 { assert(e.is_bool()); Z3_optimize_assert_and_track(ctx(), m_opt, e, t); } - + void add(expr const& e, char const* p) { + assert(e.is_bool()); + add(e, ctx().bool_const(p)); + } handle add_soft(expr const& e, unsigned weight) { assert(e.is_bool()); auto str = std::to_string(weight); diff --git a/src/smt/user_propagator.h b/src/smt/user_propagator.h index 45f25a487..eb4df07b4 100644 --- a/src/smt/user_propagator.h +++ b/src/smt/user_propagator.h @@ -9,7 +9,7 @@ Abstract: User-propagator plugin. Adds user plugins to propagate based on - terms receiving fixed values. + terms receiving fixed values or equalities. Author: @@ -17,8 +17,6 @@ Author: Notes: -- could also be complemented with disequalities to fixed values to narrow range of variables. - --*/ @@ -49,16 +47,15 @@ namespace smt { void reset() { memset(this, 0, sizeof(*this)); } }; - void* m_user_context; - solver::push_eh_t m_push_eh; - solver::pop_eh_t m_pop_eh; - solver::fresh_eh_t m_fresh_eh; - solver::final_eh_t m_final_eh; - solver::fixed_eh_t m_fixed_eh; - solver::eq_eh_t m_eq_eh; - solver::eq_eh_t m_diseq_eh; + void* m_user_context; + solver::push_eh_t m_push_eh; + solver::pop_eh_t m_pop_eh; + solver::fresh_eh_t m_fresh_eh; + solver::final_eh_t m_final_eh; + solver::fixed_eh_t m_fixed_eh; + solver::eq_eh_t m_eq_eh; + solver::eq_eh_t m_diseq_eh; solver::context_obj* m_api_context { nullptr }; - unsigned m_qhead { 0 }; vector m_prop; unsigned_vector m_prop_lim; @@ -78,7 +75,7 @@ namespace smt { * \brief initial setup for user propagator. */ void add( - void* ctx, + void* ctx, solver::push_eh_t& push_eh, solver::pop_eh_t& pop_eh, solver::fresh_eh_t& fresh_eh) {