From b43965bf05ac2c01c26eb728623b7b183a63084f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 28 Jun 2022 09:42:28 -0700 Subject: [PATCH] make user propagator work with combined solver Then users don't have to specify SImpleSolver, but can use "Solver" --- src/solver/combined_solver.cpp | 42 ++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index bfe495b6e..29a5c0a8f 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -343,7 +343,49 @@ public: else return m_solver2->get_labels(r); } + + void user_propagate_init( + void* ctx, + user_propagator::push_eh_t& push_eh, + user_propagator::pop_eh_t& pop_eh, + user_propagator::fresh_eh_t& fresh_eh) override { + switch_inc_mode(); + m_solver2->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh); + } + + void user_propagate_register_fixed(user_propagator::fixed_eh_t& fixed_eh) override { + m_solver2->user_propagate_register_fixed(fixed_eh); + } + + void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { + m_solver2->user_propagate_register_final(final_eh); + } + + void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { + m_solver2->user_propagate_register_eq(eq_eh); + } + + void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { + m_solver2->user_propagate_register_diseq(diseq_eh); + } + + void user_propagate_register_expr(expr* e) override { + m_solver2->user_propagate_register_expr(e); + } + + void user_propagate_register_created(user_propagator::created_eh_t& r) override { + m_solver2->user_propagate_register_created(r); + } + + void user_propagate_register_decide(user_propagator::decide_eh_t& r) override { + m_solver2->user_propagate_register_decide(r); + } + + void user_propagate_clear() override { + m_solver2->user_propagate_clear(); + } + };