mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

working on mus-mss

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-29 15:34:48 -07:00
parent 3da60804fc
commit 5fdb58348e
1 changed files with 15 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/opt/maxres.cpp
View file

@ -78,6 +78,7 @@ private:
expr_ref_vector m_B; expr_ref_vector m_B;
expr_ref_vector m_asms; expr_ref_vector m_asms;
obj_map<expr, rational> m_asm2weight; obj_map<expr, rational> m_asm2weight;
obj_map<expr, lbool> m_asm2value;
ptr_vector<expr> m_new_core; ptr_vector<expr> m_new_core;
mus m_mus; mus m_mus;
mss m_mss; mss m_mss;
@ -285,6 +286,7 @@ public:
lbool mus_mss2_solver() { lbool mus_mss2_solver() {
m_all_cores = true; m_all_cores = true;
//m_add_upper_bound_block = true; //m_add_upper_bound_block = true;
bool maximize_assignment = false;
init(); init();
init_local(); init_local();
sls(); sls();
@ -333,19 +335,24 @@ public:
// ss - satisfying subset // ss - satisfying subset
// cs - correction set (complement of it). // cs - correction set (complement of it).
// //
if (maximize_assignment) {
exprs ss, cs; exprs ss, cs;
is_sat = get_mss(cores, ss, cs); is_sat = get_mss(cores, ss, cs);
if (is_sat != l_true) return is_sat; if (is_sat != l_true) return is_sat;
update_mss_model(); update_mss_model();
}
// //
// block the hard constraints corresponding to the cores. // block the hard constraints corresponding to the cores.
// block the soft constraints corresponding to the cs. // block the soft constraints corresponding to the cs
// The original cs is not disjoint from the cores, // obtained from the current best model.
// after the cores are blocked, the soft constraints //
// are changed. // TBD: model must be updated with definitions for the
// fresh variables.
// //
is_sat = process_unsat(cores); is_sat = process_unsat(cores);
if (is_sat != l_true) return is_sat; if (is_sat != l_true) return is_sat;
exprs cs;
get_current_correction_set(cs); get_current_correction_set(cs);
is_sat = process_sat(cs); is_sat = process_sat(cs);
if (is_sat != l_true) return is_sat; if (is_sat != l_true) return is_sat;