mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

local

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-28 11:42:17 -08:00
parent 5fa5719c6f
commit 69d7d8ff87
3 changed files with 9 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_config.cpp
View file

@ -201,8 +201,10 @@ namespace sat {
m_pb_solver = PB_SOLVER; m_pb_solver = PB_SOLVER;
else if (s == symbol("segmented")) else if (s == symbol("segmented"))
m_pb_solver = PB_SEGMENTED; m_pb_solver = PB_SEGMENTED;
else if (s == symbol("binary_merge"))
m_pb_solver == PB_BINARY_MERGE;
else else
throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented"); throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented, binary_merge");
s = p.pb_resolve(); s = p.pb_resolve();
if (s == "cardinality") if (s == "cardinality")

8
src/sat/sat_config.h
View file

@ -57,7 +57,8 @@ namespace sat {
PB_CIRCUIT, PB_CIRCUIT,
PB_SORTING, PB_SORTING,
PB_TOTALIZER, PB_TOTALIZER,
PB_SEGMENTED PB_SEGMENTED,
PB_BINARY_MERGE
}; };
enum pb_resolve { enum pb_resolve {
@ -162,7 +163,6 @@ namespace sat {
bool m_drat_check_unsat; bool m_drat_check_unsat;
bool m_drat_check_sat; bool m_drat_check_sat;
pb_solver m_pb_solver;
bool m_card_solver; bool m_card_solver;
pb_resolve m_pb_resolve; pb_resolve m_pb_resolve;
pb_lemma_format m_pb_lemma_format; pb_lemma_format m_pb_lemma_format;
@ -182,6 +182,10 @@ namespace sat {
config(params_ref const & p); config(params_ref const & p);
void updt_params(params_ref const & p); void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d); static void collect_param_descrs(param_descrs & d);
private:
pb_solver m_pb_solver;
}; };
}; };

5
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -300,11 +300,6 @@ public:
sat_params p1(p); sat_params p1(p);
m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver()); m_params.set_bool("keep_cardinality_constraints", p1.cardinality_solver());
m_params.set_sym("pb.solver", p1.pb_solver()); m_params.set_sym("pb.solver", p1.pb_solver());
m_params.set_bool("keep_pb_constraints", m_solver.get_config().m_pb_solver == sat::PB_SOLVER);
m_params.set_bool("pb_num_system", m_solver.get_config().m_pb_solver == sat::PB_SORTING);
m_params.set_bool("pb_totalizer", m_solver.get_config().m_pb_solver == sat::PB_TOTALIZER);
m_params.set_bool("xor_solver", p1.xor_solver()); m_params.set_bool("xor_solver", p1.xor_solver());
m_solver.updt_params(m_params); m_solver.updt_params(m_params);
m_solver.set_incremental(is_incremental() && !override_incremental()); m_solver.set_incremental(is_incremental() && !override_incremental());