mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #4805

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-11-20 12:11:38 -08:00
parent 1269776777
commit 1b768c9b3a
3 changed files with 29 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/theory_pb.cpp
View file

@ -436,6 +436,7 @@ namespace smt {
theory_pb::theory_pb(context& ctx): theory_pb::theory_pb(context& ctx):
theory(ctx, ctx.get_manager().mk_family_id("pb")), theory(ctx, ctx.get_manager().mk_family_id("pb")),
m_params(ctx.get_fparams()), m_params(ctx.get_fparams()),
m_mpz_trail(m_mpz_mgr),
pb(ctx.get_manager()), pb(ctx.get_manager()),
m_restart_lim(3), m_restart_lim(3),
m_restart_inc(0), m_restart_inc(0),
@ -1106,8 +1107,10 @@ namespace smt {
and/or relatively few compared to number of argumets. and/or relatively few compared to number of argumets.
*/ */
void theory_pb::assign_ineq(ineq& c, bool is_true) { void theory_pb::assign_ineq(ineq& c, bool is_true) {
ctx.push_trail(value_trail<context, scoped_mpz>(c.m_max_sum)); m_mpz_trail.push_back(c.m_max_sum);
ctx.push_trail(value_trail<context, scoped_mpz>(c.m_min_sum)); m_mpz_trail.push_back(c.m_min_sum);
ctx.push_trail(scoped_value_trail<context, scoped_mpz, scoped_mpz_vector>(c.m_max_sum, m_mpz_trail));
ctx.push_trail(scoped_value_trail<context, scoped_mpz, scoped_mpz_vector>(c.m_min_sum, m_mpz_trail));
ctx.push_trail(value_trail<context, unsigned>(c.m_nfixed)); ctx.push_trail(value_trail<context, unsigned>(c.m_nfixed));
SASSERT(c.is_ge()); SASSERT(c.is_ge());

1
src/smt/theory_pb.h
View file

@ -271,6 +271,7 @@ namespace smt {
svector<var_info> m_var_infos; svector<var_info> m_var_infos;
mutable unsynch_mpz_manager m_mpz_mgr; // Simplex: manager mpz numerals mutable unsynch_mpz_manager m_mpz_mgr; // Simplex: manager mpz numerals
scoped_mpz_vector m_mpz_trail;
unsigned_vector m_ineqs_trail; unsigned_vector m_ineqs_trail;
unsigned_vector m_ineqs_lim; unsigned_vector m_ineqs_lim;
literal_vector m_literals; // temporary vector literal_vector m_literals; // temporary vector

23
src/util/trail.h
View file

@ -56,6 +56,29 @@ public:
} }
}; };
template<typename Ctx, typename T, typename Ts>
class scoped_value_trail : public trail<Ctx> {
T & m_value;
Ts & m_values;
public:
scoped_value_trail(T & value, Ts& values):
m_value(value),
m_values(values) {
}
~scoped_value_trail() override {
}
void undo(Ctx & ctx) override {
m_value = m_values.back();
m_values.pop_back();
}
};
template<typename Ctx> template<typename Ctx>
class reset_flag_trail : public trail<Ctx> { class reset_flag_trail : public trail<Ctx> {
bool & m_value; bool & m_value;