mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

working on pb solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-14 18:04:05 -08:00
parent d8d77d943c
commit 06ae0db116
5 changed files with 144 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/ast/ast_smt_pp.cpp
View file

@ -1054,7 +1054,8 @@ void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, u
void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
ptr_vector<quantifier> ql;
decl_collector decls(m_manager);
ast_manager& m = m_manager;
decl_collector decls(m);
smt_renaming rn;
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
@ -1065,7 +1066,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
}
decls.visit(n);
if (m_manager.is_proof(n)) {
if (m.is_proof(n)) {
strm << "(";
}
if (m_benchmark_name != symbol::null) {
@ -1074,7 +1075,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
if (m_source_info != symbol::null && m_source_info != symbol("")) {
strm << "; :source { " << m_source_info << " }\n";
}
if (m_manager.is_bool(n)) {
if (m.is_bool(n)) {
strm << "(set-info :status " << m_status << ")\n";
}
if (m_category != symbol::null && m_category != symbol("")) {
@ -1091,7 +1092,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
for (unsigned i = 0; i < decls.get_num_sorts(); ++i) {
sort* s = decls.get_sorts()[i];
if (!(*m_is_declared)(s)) {
smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
p.pp_sort_decl(sort_mark, s);
}
}
@ -1099,7 +1100,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
for (unsigned i = 0; i < decls.get_num_decls(); ++i) {
func_decl* d = decls.get_func_decls()[i];
if (!(*m_is_declared)(d)) {
smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
p(d);
strm << "\n";
}
@ -1108,34 +1109,36 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
for (unsigned i = 0; i < decls.get_num_preds(); ++i) {
func_decl* d = decls.get_pred_decls()[i];
if (!(*m_is_declared)(d)) {
smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
smt_printer p(strm, m, ql, rn, m_logic, true, true, m_simplify_implies, 0);
p(d);
strm << "\n";
}
}
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
strm << "(assert\n";
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
p(m_assumptions[i].get());
strm << ")\n";
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
strm << "(assert\n ";
p(m_assumptions[i].get());
strm << ")\n";
}
for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {
strm << "(assert\n";
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
p(m_assumptions_star[i].get());
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
strm << "(assert\n ";
p(m_assumptions_star[i].get());
strm << ")\n";
}
smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, 0);
if (m_manager.is_bool(n)) {
strm << "(assert\n";
p(n);
strm << ")\n";
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 0);
if (m.is_bool(n)) {
if (!m.is_true(n)) {
strm << "(assert\n ";
p(n);
strm << ")\n";
}
strm << "(check-sat)\n";
}
else if (m_manager.is_proof(n)) {
else if (m.is_proof(n)) {
strm << "(proof\n";
p(n);
strm << "))\n";

38
src/opt/fu_malik.cpp
View file

@ -18,6 +18,8 @@ Notes:
--*/
#include "fu_malik.h"
#include "smtlogics/qfbv_tactic.h"
#include "tactic2solver.h"
/**
\brief Fu & Malik procedure for MaxSAT. This procedure is based on
@ -37,17 +39,18 @@ namespace opt {
struct fu_malik::imp {
ast_manager& m;
solver& s;
ref<solver> m_s;
expr_ref_vector m_soft;
expr_ref_vector m_orig_soft;
expr_ref_vector m_aux;
expr_ref_vector m_assignment;
unsigned m_upper_size;
solver& s() { return *m_s; }
imp(ast_manager& m, solver& s, expr_ref_vector const& soft):
m(m),
s(s),
m_s(&s),
m_soft(soft),
m_orig_soft(soft),
m_aux(m),
@ -78,13 +81,13 @@ namespace opt {
for (unsigned i = 0; i < m_soft.size(); ++i) {
assumptions.push_back(m.mk_not(m_aux[i].get()));
}
lbool is_sat = s.check_sat(assumptions.size(), assumptions.c_ptr());
lbool is_sat = s().check_sat(assumptions.size(), assumptions.c_ptr());
if (is_sat != l_false) {
return is_sat;
}
ptr_vector<expr> core;
s.get_unsat_core(core);
s().get_unsat_core(core);
// Update soft-constraints and aux_vars
for (unsigned i = 0; i < m_soft.size(); ++i) {
@ -101,7 +104,7 @@ namespace opt {
m_aux[i] = m.mk_fresh_const("aux", m.mk_bool_sort());
m_soft[i] = m.mk_or(m_soft[i].get(), block_var);
block_vars.push_back(block_var);
s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
}
assert_at_most_one(block_vars);
return l_false;
@ -111,7 +114,7 @@ namespace opt {
expr_ref has_one(m), has_zero(m), at_most_one(m);
mk_at_most_one(block_vars.size(), block_vars.c_ptr(), has_one, has_zero);
at_most_one = m.mk_or(has_one, has_zero);
s.assert_expr(at_most_one);
s().assert_expr(at_most_one);
}
void mk_at_most_one(unsigned n, expr* const * vars, expr_ref& has_one, expr_ref& has_zero) {
@ -129,15 +132,30 @@ namespace opt {
has_zero = m.mk_and(has_zero1, has_zero2);
}
}
void set_solver() {
solver& original_solver = s();
bool all_bv = false;
// retrieve goal from s()
// extract mk_qfbv_probe
// run probe on goals
// if result is "yes", then create teh qfbv_tactic.
if (all_bv) {
tactic* t = mk_qfbv_tactic(m);
m_s = mk_tactic2solver(m, t);
}
}
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
lbool operator()() {
lbool is_sat = s.check_sat(0,0);
set_solver();
lbool is_sat = s().check_sat(0,0);
if (!m_soft.empty() && is_sat == l_true) {
solver::scoped_push _sp(s);
solver::scoped_push _sp(s());
for (unsigned i = 0; i < m_soft.size(); ++i) {
m_aux.push_back(m.mk_fresh_const("p", m.mk_bool_sort()));
s.assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
s().assert_expr(m.mk_or(m_soft[i].get(), m_aux[i].get()));
}
lbool is_sat = l_true;
@ -150,7 +168,7 @@ namespace opt {
if (is_sat == l_true) {
// Get a list of satisfying m_soft
model_ref model;
s.get_model(model);
s().get_model(model);
m_assignment.reset();
for (unsigned i = 0; i < m_orig_soft.size(); ++i) {

109
src/smt/theory_card.cpp
View file

@ -136,6 +136,12 @@ namespace smt {
if (a == 0) return b;
if (b == 0) return a;
while (a != b) {
if (a == 0) {
return b;
}
if (b == 0) {
return a;
}
if (a < b) {
b %= a;
}
@ -171,7 +177,7 @@ namespace smt {
if (!args.empty()) {
unsigned g = abs(args[0].second);
for (unsigned i = 1; g > 1 && i < args.size(); ++i) {
g = gcd(g, args[i].second);
g = gcd(g, abs(args[i].second));
}
if (g > 1) {
int k = c->m_k;
@ -183,7 +189,7 @@ namespace smt {
k = abs(k);
k += (k % g);
k /= g;
k = -k;
c->m_k = -k;
}
for (unsigned i = 0; i < args.size(); ++i) {
args[i].second /= g;
@ -213,6 +219,7 @@ namespace smt {
void theory_card::collect_statistics(::statistics& st) const {
st.update("pb axioms", m_stats.m_num_axioms);
st.update("pb propagations", m_stats.m_num_propagations);
st.update("pb predicates", m_stats.m_num_predicates);
st.update("pb compilations", m_stats.m_num_compiles);
}
@ -316,6 +323,21 @@ namespace smt {
return curr_min;
}
int theory_card::get_max_delta(card& c) {
if (m_util.is_at_most_k(c.m_app)) {
return 1;
}
int max = 0;
context& ctx = get_context();
for (unsigned i = 0; i < c.m_args.size(); ++i) {
if (c.m_args[i].second > max && ctx.get_assignment(c.m_args[i].first) == l_undef) {
max = c.m_args[i].second;
}
}
return max;
}
int theory_card::accumulate_max(literal_vector& lits, card& c) {
context& ctx = get_context();
arg_t const& args = c.m_args;
@ -364,19 +386,17 @@ namespace smt {
lbool aval = ctx.get_assignment(abv);
if (min > k && aval != l_false) {
literal_vector& lits = get_lits();
lits.push_back(~literal(abv));
int curr_min = accumulate_min(lits, c);
SASSERT(curr_min > k);
add_clause(c, lits);
add_assign(c, lits, ~literal(abv));
}
else if (max <= k && aval != l_true) {
literal_vector& lits = get_lits();
lits.push_back(literal(abv));
int curr_max = accumulate_max(lits, c);
SASSERT(curr_max <= k);
add_clause(c, lits);
add_assign(c, lits, literal(abv));
}
else if (min == k && aval == l_true) {
else if (min <= k && k < min + get_max_delta(c) && aval == l_true) {
literal_vector& lits = get_lits();
lits.push_back(~literal(abv));
int curr_min = accumulate_min(lits, c);
@ -384,37 +404,70 @@ namespace smt {
add_clause(c, lits);
}
else {
SASSERT(curr_min == k);
for (unsigned i = 0; i < args.size(); ++i) {
bool_var bv = args[i].first;
int inc = args[i].second;
if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) {
literal_vector lits_save(lits); // add_clause has a side-effect on literals.
lits_save.push_back(literal(bv, inc > 0)); // avoid incrementing min.
add_clause(c, lits_save);
if (curr_min + inc > k && inc_min(inc, ctx.get_assignment(bv)) == l_undef) {
add_assign(c, lits, literal(bv, inc > 0));
}
}
}
}
else if (max == k + 1 && aval == l_false) {
else if (max - get_max_delta(c) <= k && k < max && aval == l_false) {
literal_vector& lits = get_lits();
lits.push_back(literal(abv));
int curr_max = accumulate_max(lits, c);
if (curr_max <= k) {
add_clause(c, lits);
}
else if (curr_max == k + 1) {
else {
for (unsigned i = 0; i < args.size(); ++i) {
bool_var bv = args[i].first;
int inc = args[i].second;
if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) {
literal_vector lits_save(lits); // add_clause has a side-effect on literals.
lits_save.push_back(literal(bv, inc < 0)); // avoid decrementing max.
add_clause(c, lits_save);
if (curr_max - abs(inc) <= k && dec_max(inc, ctx.get_assignment(bv)) == l_undef) {
add_assign(c, lits, literal(bv, inc < 0));
}
}
}
}
#if 0
else if (aval == l_true) {
SASSERT(min < k);
literal_vector& lits = get_lits();
int curr_min = accumulate_min(lits, c);
bool all_inc = curr_min == k;
unsigned num_incs = 0;
for (unsigned i = 0; all_inc && i < args.size(); ++i) {
bool_var bv = args[i].first;
int inc = args[i].second;
if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) {
all_inc = inc + min > k;
num_incs++;
}
}
if (num_incs > 0) {
std::cout << "missed T propgations " << num_incs << "\n";
}
}
else if (aval == l_false) {
literal_vector& lits = get_lits();
lits.push_back(literal(abv));
int curr_max = accumulate_max(lits, c);
bool all_dec = curr_max > k;
unsigned num_decs = 0;
for (unsigned i = 0; all_dec && i < args.size(); ++i) {
bool_var bv = args[i].first;
int inc = args[i].second;
if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) {
all_dec = inc + max <= k;
num_decs++;
}
}
if (num_decs > 0) {
std::cout << "missed F propgations " << num_decs << "\n";
}
}
#endif
}
void theory_card::assign_eh(bool_var v, bool is_true) {
@ -608,10 +661,14 @@ namespace smt {
}
bool theory_card::should_compile(card& c) {
#if 1
return false;
#else
if (!m_util.is_at_most_k(c.m_app)) {
return false;
}
return c.m_num_propagations >= c.m_compilation_threshold;
#endif
}
void theory_card::compile_at_most(card& c) {
@ -686,6 +743,19 @@ namespace smt {
return m_literals;
}
void theory_card::add_assign(card& c, literal_vector const& lits, literal l) {
literal_vector ls;
++c.m_num_propagations;
m_stats.m_num_propagations++;
context& ctx = get_context();
for (unsigned i = 0; i < lits.size(); ++i) {
ls.push_back(~lits[i]);
}
ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), ls.size(), ls.c_ptr(), l)));
}
void theory_card::add_clause(card& c, literal_vector const& lits) {
++c.m_num_propagations;
m_stats.m_num_axioms++;
@ -693,7 +763,8 @@ namespace smt {
TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
justification* js = 0;
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
IF_VERBOSE(1, ctx.display_literals_verbose(verbose_stream(), lits.size(), lits.c_ptr());
IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(),
lits.size(), lits.c_ptr());
verbose_stream() << "\n";);
// ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}

3
src/smt/theory_card.h
View file

@ -32,6 +32,7 @@ namespace smt {
struct stats {
unsigned m_num_axioms;
unsigned m_num_propagations;
unsigned m_num_predicates;
unsigned m_num_compiles;
void reset() { memset(this, 0, sizeof(*this)); }
@ -75,10 +76,12 @@ namespace smt {
void add_card(card* c);
void add_clause(card& c, literal_vector const& lits);
void add_assign(card& c, literal_vector const& lits, literal l);
literal_vector& get_lits();
int find_inc(bool_var bv, svector<std::pair<bool_var, int> >const& vars);
void propagate_assignment(card& c);
int get_max_delta(card& c);
int accumulate_max(literal_vector& lits, card& c);
int accumulate_min(literal_vector& lits, card& c);
lbool dec_max(int inc, lbool val);

1
src/util/region.h
View file

@ -53,6 +53,7 @@ public:
m_scopes.push_back(m_chuncks.size());
}
void pop_scope() {
unsigned old_size = m_scopes.back();
m_scopes.pop_back();