mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

move to scoped state, change default parameter for sls until bv is debugged

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-05-11 18:39:36 -07:00
parent e9a11bd93b
commit cad1e5cab3
3 changed files with 15 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/opt/opt_context.cpp
View file

@ -991,11 +991,11 @@ namespace opt {
free_func_visitor visitor(m); free_func_visitor visitor(m);
std::ostringstream out; std::ostringstream out;
#define PP(_e_) ast_smt2_pp(out, _e_, env); #define PP(_e_) ast_smt2_pp(out, _e_, env);
for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) {
visitor.collect(m_hard_constraints[i]); visitor.collect(m_scoped_state.m_hard[i]);
} }
for (unsigned i = 0; i < m_objectives.size(); ++i) { for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
objective const& obj = m_objectives[i]; objective const& obj = m_scoped_state.m_objectives[i];
switch(obj.m_type) { switch(obj.m_type) {
case O_MAXIMIZE: case O_MAXIMIZE:
case O_MINIMIZE: case O_MINIMIZE:
@ -1023,13 +1023,13 @@ namespace opt {
PP(*it); PP(*it);
out << "\n"; out << "\n";
} }
for (unsigned i = 0; i < m_hard_constraints.size(); ++i) { for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) {
out << "(assert "; out << "(assert ";
PP(m_hard_constraints[i]); PP(m_scoped_state.m_hard[i]);
out << ")\n"; out << ")\n";
} }
for (unsigned i = 0; i < m_objectives.size(); ++i) { for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
objective const& obj = m_objectives[i]; objective const& obj = m_scoped_state.m_objectives[i];
switch(obj.m_type) { switch(obj.m_type) {
case O_MAXIMIZE: case O_MAXIMIZE:
out << "(maximize "; out << "(maximize ";

2
src/opt/opt_params.pyg
View file

@ -12,7 +12,7 @@ def_module_params('opt',
('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'pbmax', 'bcd2', 'wpm2', 'bvsls', 'sls'"), ('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'pbmax', 'bcd2', 'wpm2', 'bvsls', 'sls'"),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'), ('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'),
('sls_engine', SYMBOL, 'bv', "SLS engine. Either 'bv' or 'pb'"), ('sls_engine', SYMBOL, 'pb', "SLS engine. Either 'bv' or 'pb'"),
('elim_01', BOOL, True, 'eliminate 01 variables'), ('elim_01', BOOL, True, 'eliminate 01 variables'),
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)') ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)')

31
src/opt/weighted_maxsat.cpp
View file

@ -576,10 +576,9 @@ namespace opt {
// lower bounds. // lower bounds.
class pbmax : public maxsmt_solver_base { class pbmax : public maxsmt_solver_base {
bool m_use_aux;
public: public:
pbmax(solver* s, ast_manager& m, bool use_aux): pbmax(solver* s, ast_manager& m):
maxsmt_solver_base(s, m), m_use_aux(use_aux) { maxsmt_solver_base(s, m) {
} }
virtual ~pbmax() {} virtual ~pbmax() {}
@ -598,20 +597,8 @@ namespace opt {
app_ref b(m); app_ref b(m);
expr_ref_vector nsoft(m); expr_ref_vector nsoft(m);
init(); init();
if (m_use_aux) {
s().push();
}
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
if (m_use_aux) { nsoft.push_back(mk_not(m_soft[i].get()));
b = m.mk_fresh_const("b", m.mk_bool_sort());
m_mc->insert(b->get_decl());
fml = m.mk_or(m_soft[i].get(), b);
s().assert_expr(fml);
nsoft.push_back(b);
}
else {
nsoft.push_back(mk_not(m_soft[i].get()));
}
} }
lbool is_sat = l_true; lbool is_sat = l_true;
while (l_true == is_sat) { while (l_true == is_sat) {
@ -643,9 +630,6 @@ namespace opt {
is_sat = l_true; is_sat = l_true;
m_lower = m_upper; m_lower = m_upper;
} }
if (m_use_aux) {
s().pop(1);
}
TRACE("opt", tout << "lower: " << m_lower << "\n";); TRACE("opt", tout << "lower: " << m_lower << "\n";);
return is_sat; return is_sat;
} }
@ -1008,14 +992,11 @@ namespace opt {
if (m_maxsmt) { if (m_maxsmt) {
return *m_maxsmt; return *m_maxsmt;
} }
if (m_engine == symbol("pwmax")) { if (m_engine == symbol("pbmax")) {
m_maxsmt = alloc(pbmax, s.get(), m, true); m_maxsmt = alloc(pbmax, s.get(), m);
}
else if (m_engine == symbol("pbmax")) {
m_maxsmt = alloc(pbmax, s.get(), m, false);
} }
else if (m_engine == symbol("wpm2")) { else if (m_engine == symbol("wpm2")) {
maxsmt_solver_base* s2 = alloc(pbmax, s.get(), m, false); maxsmt_solver_base* s2 = alloc(pbmax, s.get(), m);
m_maxsmt = alloc(wpm2, s.get(), m, s2); m_maxsmt = alloc(wpm2, s.get(), m, s2);
} }
else if (m_engine == symbol("bcd2")) { else if (m_engine == symbol("bcd2")) {