mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-21 10:04:02 -08:00
commit df492e200f
99 changed files with 1659 additions and 702 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/proto_model/numeral_factory.cpp
View file

@ -31,7 +31,7 @@ arith_factory::arith_factory(ast_manager & m):
arith_factory::~arith_factory() {
}
app * arith_factory::mk_value(rational const & val, bool is_int) {
app * arith_factory::mk_num_value(rational const & val, bool is_int) {
return numeral_factory::mk_value(val, is_int ? m_util.mk_int() : m_util.mk_real());
}
@ -47,6 +47,6 @@ app * bv_factory::mk_value_core(rational const & val, sort * s) {
return m_util.mk_numeral(val, s);
}
app * bv_factory::mk_value(rational const & val, unsigned bv_size) {
app * bv_factory::mk_num_value(rational const & val, unsigned bv_size) {
return numeral_factory::mk_value(val, m_util.mk_sort(bv_size));
}

4
src/smt/proto_model/numeral_factory.h
View file

@ -38,7 +38,7 @@ public:
arith_factory(ast_manager & m);
virtual ~arith_factory();
app * mk_value(rational const & val, bool is_int);
app * mk_num_value(rational const & val, bool is_int);
};
class bv_factory : public numeral_factory {
@ -50,7 +50,7 @@ public:
bv_factory(ast_manager & m);
virtual ~bv_factory();
app * mk_value(rational const & val, unsigned bv_size);
app * mk_num_value(rational const & val, unsigned bv_size);
};
#endif /* NUMERAL_FACTORY_H_ */

200
src/smt/smt_consequences.cpp
View file

@ -56,36 +56,7 @@ namespace smt {
s.insert(lit.var());
}
else {
b_justification js = get_justification(lit.var());
switch (js.get_kind()) {
case b_justification::CLAUSE: {
clause * cls = js.get_clause();
if (!cls) break;
unsigned num_lits = cls->get_num_literals();
for (unsigned j = 0; j < num_lits; ++j) {
literal lit2 = cls->get_literal(j);
if (lit2.var() != lit.var()) {
s |= m_antecedents.find(lit2.var());
}
}
break;
}
case b_justification::BIN_CLAUSE: {
s |= m_antecedents.find(js.get_literal().var());
break;
}
case b_justification::AXIOM: {
break;
}
case b_justification::JUSTIFICATION: {
literal_vector literals;
m_conflict_resolution->justification2literals(js.get_justification(), literals);
for (unsigned j = 0; j < literals.size(); ++j) {
s |= m_antecedents.find(literals[j].var());
}
break;
}
}
justify(lit, s);
}
m_antecedents.insert(lit.var(), s);
TRACE("context", display_literal_verbose(tout, lit);
@ -122,6 +93,39 @@ namespace smt {
}
}
void context::justify(literal lit, index_set& s) {
b_justification js = get_justification(lit.var());
switch (js.get_kind()) {
case b_justification::CLAUSE: {
clause * cls = js.get_clause();
if (!cls) break;
unsigned num_lits = cls->get_num_literals();
for (unsigned j = 0; j < num_lits; ++j) {
literal lit2 = cls->get_literal(j);
if (lit2.var() != lit.var()) {
s |= m_antecedents.find(lit2.var());
}
}
break;
}
case b_justification::BIN_CLAUSE: {
s |= m_antecedents.find(js.get_literal().var());
break;
}
case b_justification::AXIOM: {
break;
}
case b_justification::JUSTIFICATION: {
literal_vector literals;
m_conflict_resolution->justification2literals(js.get_justification(), literals);
for (unsigned j = 0; j < literals.size(); ++j) {
s |= m_antecedents.find(literals[j].var());
}
break;
}
}
}
void context::extract_fixed_consequences(unsigned& start, obj_map<expr, expr*>& vars, index_set const& assumptions, expr_ref_vector& conseq) {
pop_to_search_lvl();
SASSERT(!inconsistent());
@ -369,6 +373,142 @@ namespace smt {
<< ")\n";
}
void context::extract_cores(expr_ref_vector const& asms, vector<expr_ref_vector>& cores, unsigned& min_core_size) {
index_set _asms, _nasms;
u_map<expr*> var2expr;
for (unsigned i = 0; i < asms.size(); ++i) {
literal lit = get_literal(asms[i]);
_asms.insert(lit.index());
_nasms.insert((~lit).index());
var2expr.insert(lit.var(), asms[i]);
}
m_antecedents.reset();
literal_vector const& lits = assigned_literals();
for (unsigned i = 0; i < lits.size(); ++i) {
literal lit = lits[i];
index_set s;
if (_asms.contains(lit.index())) {
s.insert(lit.var());
}
else {
justify(lit, s);
}
m_antecedents.insert(lit.var(), s);
if (_nasms.contains(lit.index())) {
expr_ref_vector core(m_manager);
index_set::iterator it = s.begin(), end = s.end();
for (; it != end; ++it) {
core.push_back(var2expr[*it]);
}
core.push_back(var2expr[lit.var()]);
cores.push_back(core);
min_core_size = std::min(min_core_size, core.size());
}
}
}
void context::preferred_sat(literal_vector& lits) {
bool retry = true;
while (retry) {
retry = false;
for (unsigned i = 0; i < lits.size(); ++i) {
literal lit = lits[i];
if (lit == null_literal || get_assignment(lit) != l_undef) {
continue;
}
push_scope();
assign(lit, b_justification::mk_axiom(), true);
while (!propagate()) {
lits[i] = null_literal;
retry = true;
if (!resolve_conflict() || inconsistent()) {
SASSERT(inconsistent());
return;
}
}
}
}
}
void context::display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size) {
unsigned num_true = 0, num_false = 0, num_undef = 0;
for (unsigned i = 0; i < asms.size(); ++i) {
literal lit = get_literal(asms[i]);
if (get_assignment(lit) == l_false) {
++num_false;
}
if (get_assignment(lit) == l_true) {
++num_true;
}
if (get_assignment(lit) == l_undef) {
++num_undef;
}
}
out << "(smt.preferred-sat true: " << num_true << " false: " << num_false << " undef: " << num_undef << " min core: " << min_core_size << ")\n";
}
lbool context::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
pop_to_base_lvl();
cores.reset();
setup_context(false);
internalize_assertions();
if (m_asserted_formulas.inconsistent() || inconsistent()) {
return l_false;
}
scoped_mk_model smk(*this);
init_search();
flet<bool> l(m_searching, true);
unsigned level = m_scope_lvl;
unsigned min_core_size = UINT_MAX;
lbool is_sat = l_true;
unsigned num_restarts = 0;
while (true) {
if (m_manager.canceled()) {
is_sat = l_undef;
break;
}
literal_vector lits;
for (unsigned i = 0; i < asms.size(); ++i) {
lits.push_back(get_literal(asms[i]));
}
preferred_sat(lits);
if (inconsistent()) {
SASSERT(m_scope_lvl == level);
is_sat = l_false;
break;
}
extract_cores(asms, cores, min_core_size);
IF_VERBOSE(1, display_partial_assignment(verbose_stream(), asms, min_core_size););
if (min_core_size <= 10) {
is_sat = l_undef;
break;
}
is_sat = bounded_search();
if (!restart(is_sat, level)) {
break;
}
++num_restarts;
if (num_restarts >= min_core_size) {
is_sat = l_undef;
while (num_restarts <= 10*min_core_size) {
is_sat = bounded_search();
if (!restart(is_sat, level)) {
break;
}
++num_restarts;
}
break;
}
}
end_search();
return check_finalize(is_sat);
}
struct neg_literal {
unsigned negate(unsigned i) {
return (~to_literal(i)).index();

162
src/smt/smt_context.cpp
View file

@ -1111,6 +1111,8 @@ namespace smt {
if (r1 == r2) {
TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
//return false;
theory_id t1 = r1->m_th_var_list.get_th_id();
if (t1 == null_theory_id) return false;
return get_theory(t1)->use_diseqs();
@ -3293,19 +3295,6 @@ namespace smt {
m_num_conflicts_since_restart = 0;
}
struct context::scoped_mk_model {
context & m_ctx;
scoped_mk_model(context & ctx):m_ctx(ctx) {
m_ctx.m_proto_model = 0;
m_ctx.m_model = 0;
}
~scoped_mk_model() {
if (m_ctx.m_proto_model.get() != 0) {
m_ctx.m_model = m_ctx.m_proto_model->mk_model();
m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
}
}
};
lbool context::search() {
#ifndef _EXTERNAL_RELEASE
@ -3333,79 +3322,10 @@ namespace smt {
TRACE("search_bug", tout << "status: " << status << ", inconsistent: " << inconsistent() << "\n";);
TRACE("assigned_literals_per_lvl", display_num_assigned_literals_per_lvl(tout);
tout << ", num_assigned: " << m_assigned_literals.size() << "\n";);
if (m_last_search_failure != OK) {
if (status != l_false) {
// build candidate model before returning
mk_proto_model(status);
// status = l_undef;
}
if (!restart(status, curr_lvl)) {
break;
}
bool force_restart = false;
if (status == l_false) {
break;
}
else if (status == l_true) {
SASSERT(!inconsistent());
mk_proto_model(l_true);
// possible outcomes DONE l_true, DONE l_undef, CONTINUE
quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value());
if (cmr == quantifier_manager::SAT) {
// done
break;
}
if (cmr == quantifier_manager::UNKNOWN) {
IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";);
// giving up
m_last_search_failure = QUANTIFIERS;
status = l_undef;
break;
}
status = l_undef;
force_restart = true;
}
SASSERT(status == l_undef);
inc_limits();
if (force_restart || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
SASSERT(!inconsistent());
IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
<< " :decisions " << m_stats.m_num_decisions
<< " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
verbose_stream() << " :restart-outer " << m_restart_outer_threshold;
}
if (m_fparams.m_restart_adaptive) {
verbose_stream() << " :agility " << m_agility;
}
verbose_stream() << ")" << std::endl; verbose_stream().flush(););
// execute the restart
m_stats.m_num_restarts++;
if (m_scope_lvl > curr_lvl) {
pop_scope(m_scope_lvl - curr_lvl);
SASSERT(at_search_level());
}
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end && !inconsistent(); ++it)
(*it)->restart_eh();
TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
if (!inconsistent()) {
m_qmanager->restart_eh();
}
if (inconsistent()) {
VERIFY(!resolve_conflict());
status = l_false;
break;
}
}
if (m_fparams.m_simplify_clauses)
simplify_clauses();
if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART)
del_inactive_lemmas();
}
TRACE("search_lite", tout << "status: " << status << "\n";);
@ -3419,6 +3339,80 @@ namespace smt {
end_search();
return status;
}
bool context::restart(lbool& status, unsigned curr_lvl) {
if (m_last_search_failure != OK) {
if (status != l_false) {
// build candidate model before returning
mk_proto_model(status);
// status = l_undef;
}
return false;
}
if (status == l_false) {
return false;
}
if (status == l_true) {
SASSERT(!inconsistent());
mk_proto_model(l_true);
// possible outcomes DONE l_true, DONE l_undef, CONTINUE
quantifier_manager::check_model_result cmr = m_qmanager->check_model(m_proto_model.get(), m_model_generator->get_root2value());
if (cmr == quantifier_manager::SAT) {
// done
status = l_true;
return false;
}
if (cmr == quantifier_manager::UNKNOWN) {
IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";);
// giving up
m_last_search_failure = QUANTIFIERS;
status = l_undef;
return false;
}
}
inc_limits();
if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
SASSERT(!inconsistent());
IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations
<< " :decisions " << m_stats.m_num_decisions
<< " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {
verbose_stream() << " :restart-outer " << m_restart_outer_threshold;
}
if (m_fparams.m_restart_adaptive) {
verbose_stream() << " :agility " << m_agility;
}
verbose_stream() << ")" << std::endl; verbose_stream().flush(););
// execute the restart
m_stats.m_num_restarts++;
if (m_scope_lvl > curr_lvl) {
pop_scope(m_scope_lvl - curr_lvl);
SASSERT(at_search_level());
}
ptr_vector<theory>::iterator it = m_theory_set.begin();
ptr_vector<theory>::iterator end = m_theory_set.end();
for (; it != end && !inconsistent(); ++it)
(*it)->restart_eh();
TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
if (!inconsistent()) {
m_qmanager->restart_eh();
}
if (inconsistent()) {
VERIFY(!resolve_conflict());
status = l_false;
return false;
}
}
if (m_fparams.m_simplify_clauses)
simplify_clauses();
if (m_fparams.m_lemma_gc_strategy == LGC_AT_RESTART)
del_inactive_lemmas();
status = l_undef;
return true;
}
void context::tick(unsigned & counter) const {
counter++;

27
src/smt/smt_context.h
View file

@ -200,7 +200,20 @@ namespace smt {
model_ref m_model;
std::string m_unknown;
void mk_proto_model(lbool r);
struct scoped_mk_model;
struct scoped_mk_model {
context & m_ctx;
scoped_mk_model(context & ctx):m_ctx(ctx) {
m_ctx.m_proto_model = 0;
m_ctx.m_model = 0;
}
~scoped_mk_model() {
if (m_ctx.m_proto_model.get() != 0) {
m_ctx.m_model = m_ctx.m_proto_model->mk_model();
m_ctx.m_proto_model = 0; // proto_model is not needed anymore.
}
}
};
// -----------------------------------
//
@ -234,7 +247,6 @@ namespace smt {
return m_params;
}
bool get_cancel_flag() { return !m_manager.limit().inc(); }
region & get_region() {
@ -1056,6 +1068,8 @@ namespace smt {
void inc_limits();
bool restart(lbool& status, unsigned curr_lvl);
void tick(unsigned & counter) const;
lbool bounded_search();
@ -1367,6 +1381,13 @@ namespace smt {
void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars,
expr_ref_vector const& conseq, expr_ref_vector const& unfixed);
void justify(literal lit, index_set& s);
void extract_cores(expr_ref_vector const& asms, vector<expr_ref_vector>& cores, unsigned& min_core_size);
void preferred_sat(literal_vector& literals);
void display_partial_assignment(std::ostream& out, expr_ref_vector const& asms, unsigned min_core_size);
public:
context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());
@ -1410,6 +1431,8 @@ namespace smt {
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, expr_ref_vector& unfixed);
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
lbool setup_and_check(bool reset_cancel = true);

3
src/smt/smt_context_inv.cpp
View file

@ -322,6 +322,9 @@ namespace smt {
bool context::check_th_diseq_propagation() const {
TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
int num = get_num_bool_vars();
if (inconsistent()) {
return true;
}
for (bool_var v = 0; v < num; v++) {
if (has_enode(v)) {
enode * n = bool_var2enode(v);

12
src/smt/smt_context_stat.cpp
View file

@ -32,7 +32,7 @@ namespace smt {
return static_cast<unsigned>(acc / m_lemmas.size());
}
void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) {
static void acc_num_occs(clause * cls, unsigned_vector & lit2num_occs) {
unsigned num_lits = cls->get_num_literals();
for (unsigned i = 0; i < num_lits; i++) {
literal l = cls->get_literal(i);
@ -40,7 +40,7 @@ namespace smt {
}
}
void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
static void acc_num_occs(clause_vector const & v, unsigned_vector & lit2num_occs) {
clause_vector::const_iterator it = v.begin();
clause_vector::const_iterator end = v.end();
for (; it != end; ++it)
@ -79,7 +79,7 @@ namespace smt {
out << (m_assigned_literals.size() - n) << "]";
}
void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) {
static void acc_var_num_occs(clause * cls, unsigned_vector & var2num_occs) {
unsigned num_lits = cls->get_num_literals();
for (unsigned i = 0; i < num_lits; i++) {
literal l = cls->get_literal(i);
@ -87,7 +87,7 @@ namespace smt {
}
}
void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
static void acc_var_num_occs(clause_vector const & v, unsigned_vector & var2num_occs) {
clause_vector::const_iterator it = v.begin();
clause_vector::const_iterator end = v.end();
for (; it != end; ++it)
@ -114,7 +114,7 @@ namespace smt {
out << "\n";
}
void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) {
static void acc_var_num_min_occs(clause * cls, unsigned_vector & var2num_min_occs) {
unsigned num_lits = cls->get_num_literals();
bool_var min_var = cls->get_literal(0).var();
for (unsigned i = 1; i < num_lits; i++) {
@ -125,7 +125,7 @@ namespace smt {
var2num_min_occs[min_var]++;
}
void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
static void acc_var_num_min_occs(clause_vector const & v, unsigned_vector & var2num_min_occs) {
clause_vector::const_iterator it = v.begin();
clause_vector::const_iterator end = v.end();
for (; it != end; ++it)

4
src/smt/smt_internalizer.cpp
View file

@ -335,7 +335,7 @@ namespace smt {
}
}
bool find_arg(app * n, expr * t, expr * & other) {
static bool find_arg(app * n, expr * t, expr * & other) {
SASSERT(n->get_num_args() == 2);
if (n->get_arg(0) == t) {
other = n->get_arg(1);
@ -348,7 +348,7 @@ namespace smt {
return false;
}
bool check_args(app * n, expr * t1, expr * t2) {
static bool check_args(app * n, expr * t1, expr * t2) {
SASSERT(n->get_num_args() == 2);
return (n->get_arg(0) == t1 && n->get_arg(1) == t2) || (n->get_arg(1) == t1 && n->get_arg(0) == t2);
}

9
src/smt/smt_kernel.cpp
View file

@ -115,6 +115,11 @@ namespace smt {
return m_kernel.get_consequences(assumptions, vars, conseq, unfixed);
}
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
return m_kernel.preferred_sat(asms, cores);
}
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return m_kernel.find_mutexes(vars, mutexes);
}
@ -282,6 +287,10 @@ namespace smt {
return m_imp->get_consequences(assumptions, vars, conseq, unfixed);
}
lbool kernel::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {
return m_imp->preferred_sat(asms, cores);
}
lbool kernel::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return m_imp->find_mutexes(vars, mutexes);
}

7
src/smt/smt_kernel.h
View file

@ -133,11 +133,16 @@ namespace smt {
lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars,
expr_ref_vector& conseq, expr_ref_vector& unfixed);
/*
/**
\brief find mutually exclusive variables.
*/
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes);
/**
\brief Preferential SAT.
*/
lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
/**
\brief Return the model associated with the last check command.
*/

3
src/smt/smt_model_checker.cpp
View file

@ -363,9 +363,6 @@ namespace smt {
}
}
struct scoped_set_relevancy {
};
bool model_checker::check(proto_model * md, obj_map<enode, app *> const & root2value) {
SASSERT(md != 0);
m_root2value = &root2value;

2
src/smt/smt_model_finder.cpp
View file

@ -498,7 +498,7 @@ namespace smt {
m_bvsimp = static_cast<bv_simplifier_plugin*>(s.get_plugin(m.mk_family_id("bv")));
}
~auf_solver() {
virtual ~auf_solver() {
flush_nodes();
reset_eval_cache();
}

8
src/smt/smt_setup.cpp
View file

@ -188,7 +188,7 @@ namespace smt {
}
}
void check_no_arithmetic(static_features const & st, char const * logic) {
static void check_no_arithmetic(static_features const & st, char const * logic) {
if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0)
throw default_exception("Benchmark constains arithmetic, but specified loging does not support it.");
}
@ -231,21 +231,21 @@ namespace smt {
(st.m_num_arith_eqs + st.m_num_arith_ineqs) > st.m_num_uninterpreted_constants * 9;
}
bool is_in_diff_logic(static_features const & st) {
static bool is_in_diff_logic(static_features const & st) {
return
st.m_num_arith_eqs == st.m_num_diff_eqs &&
st.m_num_arith_terms == st.m_num_diff_terms &&
st.m_num_arith_ineqs == st.m_num_diff_ineqs;
}
bool is_diff_logic(static_features const & st) {
static bool is_diff_logic(static_features const & st) {
return
is_in_diff_logic(st) &&
(st.m_num_diff_ineqs > 0 || st.m_num_diff_eqs > 0 || st.m_num_diff_terms > 0)
;
}
void check_no_uninterpreted_functions(static_features const & st, char const * logic) {
static void check_no_uninterpreted_functions(static_features const & st, char const * logic) {
if (st.m_num_uninterpreted_functions != 0)
throw default_exception("Benchmark contains uninterpreted function symbols, but specified logic does not support them.");
}

2
src/smt/theory_arith.h
View file

@ -1080,7 +1080,7 @@ namespace smt {
virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker, bool& has_shared);
virtual inf_eps_rational<inf_rational> value(theory_var v);
virtual theory_var add_objective(app* term);
virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val);
expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_numeral const& val);
void enable_record_conflict(expr* bound);
void record_conflict(unsigned num_lits, literal const * lits,
unsigned num_eqs, enode_pair const * eqs,

4
src/smt/theory_arith_aux.h
View file

@ -417,8 +417,8 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::atom::display(theory_arith<Ext> const& th, std::ostream& out) const {
literal l(get_bool_var(), !m_is_true);
out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " ";
out << l << ":";
// out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << get_k() << " ";
// out << l << ":";
th.get_context().display_detailed_literal(out, l);
}

10
src/smt/theory_arith_core.h
View file

@ -1069,7 +1069,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::flush_bound_axioms() {
CTRACE("arith", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
CTRACE("arith_verbose", !m_new_atoms.empty(), tout << "flush bound axioms\n";);
while (!m_new_atoms.empty()) {
ptr_vector<atom> atoms;
@ -1084,7 +1084,7 @@ namespace smt {
--i;
}
}
CTRACE("arith", !atoms.empty(),
CTRACE("arith", atoms.size() > 1,
for (unsigned i = 0; i < atoms.size(); ++i) {
atoms[i]->display(*this, tout); tout << "\n";
});
@ -1292,7 +1292,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::assign_eh(bool_var v, bool is_true) {
TRACE("arith", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
TRACE("arith_verbose", tout << "p" << v << " := " << (is_true?"true":"false") << "\n";);
atom * a = get_bv2a(v);
if (!a) return;
SASSERT(get_context().get_assignment(a->get_bool_var()) != l_undef);
@ -3043,12 +3043,14 @@ namespace smt {
m_stats.m_conflicts++;
m_num_conflicts++;
TRACE("arith_conflict",
tout << "scope: " << ctx.get_scope_level() << "\n";
for (unsigned i = 0; i < num_literals; i++) {
ctx.display_detailed_literal(tout, lits[i]);
tout << " ";
if (coeffs_enabled()) {
tout << "bound: " << bounds.lit_coeffs()[i] << "\n";
}
tout << "\n";
}
for (unsigned i = 0; i < num_eqs; i++) {
tout << "#" << eqs[i].first->get_owner_id() << "=#" << eqs[i].second->get_owner_id() << " ";
@ -3229,7 +3231,7 @@ namespace smt {
TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";);
num = floor(num);
}
return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(var2expr(v))));
return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(var2expr(v))));
}
// -----------------------------------

2
src/smt/theory_bv.cpp
View file

@ -1583,7 +1583,7 @@ namespace smt {
#endif
get_fixed_value(v, val);
SASSERT(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(val, get_bv_size(v)));
return alloc(expr_wrapper_proc, m_factory->mk_num_value(val, get_bv_size(v)));
}
void theory_bv::display_var(std::ostream & out, theory_var v) const {

6
src/smt/theory_dense_diff_logic.h
View file

@ -198,7 +198,7 @@ namespace smt {
void del_vars(unsigned old_num_vars);
void init_model();
bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);
expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict);
expr_ref mk_ineq(theory_var v, inf_eps const& val, bool is_strict);
#ifdef Z3DEBUG
bool check_vector_sizes() const;
bool check_matrix() const;
@ -270,8 +270,8 @@ namespace smt {
virtual inf_eps_rational<inf_rational> maximize(theory_var v, expr_ref& blocker, bool& has_shared);
virtual inf_eps_rational<inf_rational> value(theory_var v);
virtual theory_var add_objective(app* term);
virtual expr_ref mk_gt(theory_var v, inf_rational const& val);
virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val);
virtual expr_ref mk_gt(theory_var v, inf_eps const& val);
expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val);
// -----------------------------------
//

13
src/smt/theory_dense_diff_logic_def.h
View file

@ -828,7 +828,7 @@ namespace smt {
SASSERT(v != null_theory_var);
numeral const & val = m_assignment[v];
rational num = val.get_rational().to_rational() + m_epsilon * val.get_infinitesimal().to_rational();
return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int(v)));
}
// TBD: code is common to both sparse and dense difference logic solvers.
@ -1002,9 +1002,10 @@ namespace smt {
m_assignment[i] = a;
// TBD: if epsilon is != 0, then adjust a by some small fraction.
}
blocker = mk_gt(v, r);
inf_eps result(rational(0), r);
blocker = mk_gt(v, result);
IF_VERBOSE(10, verbose_stream() << blocker << "\n";);
return inf_eps(rational(0), r);
return result;
}
default:
TRACE("opt", tout << "unbounded\n"; );
@ -1034,18 +1035,18 @@ namespace smt {
}
template<typename Ext>
expr_ref theory_dense_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
expr_ref theory_dense_diff_logic<Ext>::mk_gt(theory_var v, inf_eps const& val) {
return mk_ineq(v, val, true);
}
template<typename Ext>
expr_ref theory_dense_diff_logic<Ext>::mk_ge(
filter_model_converter& fm, theory_var v, inf_rational const& val) {
filter_model_converter& fm, theory_var v, inf_eps const& val) {
return mk_ineq(v, val, false);
}
template<typename Ext>
expr_ref theory_dense_diff_logic<Ext>::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) {
expr_ref theory_dense_diff_logic<Ext>::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) {
ast_manager& m = get_manager();
objective_term const& t = m_objectives[v];
expr_ref e(m), f(m), f2(m);

7
src/smt/theory_diff_logic.h
View file

@ -324,14 +324,15 @@ namespace smt {
virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared);
virtual inf_eps value(theory_var v);
virtual theory_var add_objective(app* term);
virtual expr_ref mk_gt(theory_var v, inf_rational const& val);
virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val);
expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val);
bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective);
private:
expr_ref mk_ineq(theory_var v, inf_rational const& val, bool is_strict);
expr_ref mk_gt(theory_var v, inf_eps const& val);
expr_ref mk_ineq(theory_var v, inf_eps const& val, bool is_strict);
virtual void new_eq_eh(theory_var v1, theory_var v2, justification& j);

13
src/smt/theory_diff_logic_def.h
View file

@ -905,7 +905,7 @@ model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator &
numeral val = m_graph.get_assignment(v);
rational num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational();
TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(n->get_owner())));
return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, m_util.is_int(n->get_owner())));
}
template<typename Ext>
@ -1242,7 +1242,8 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
rational r = rational(val.first) + m_delta*rational(val.second);
m_graph.set_assignment(i, numeral(r));
}
blocker = mk_gt(v, r);
inf_eps r1(rational(0), r);
blocker = mk_gt(v, r1);
return inf_eps(rational(0), r + m_objective_consts[v]);
}
default:
@ -1273,7 +1274,7 @@ theory_var theory_diff_logic<Ext>::add_objective(app* term) {
}
template<typename Ext>
expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_rational const& val, bool is_strict) {
expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) {
ast_manager& m = get_manager();
objective_term const& t = m_objectives[v];
expr_ref e(m), f(m), f2(m);
@ -1304,7 +1305,7 @@ expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_rational const& val,
return f;
}
inf_rational new_val = val; // - inf_rational(m_objective_consts[v]);
inf_eps new_val = val; // - inf_rational(m_objective_consts[v]);
e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f));
if (new_val.get_infinitesimal().is_neg()) {
@ -1328,12 +1329,12 @@ expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_rational const& val,
}
template<typename Ext>
expr_ref theory_diff_logic<Ext>::mk_gt(theory_var v, inf_rational const& val) {
expr_ref theory_diff_logic<Ext>::mk_gt(theory_var v, inf_eps const& val) {
return mk_ineq(v, val, true);
}
template<typename Ext>
expr_ref theory_diff_logic<Ext>::mk_ge(filter_model_converter& fm, theory_var v, inf_rational const& val) {
expr_ref theory_diff_logic<Ext>::mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) {
return mk_ineq(v, val, false);
}

1
src/smt/theory_opt.h
View file

@ -33,7 +33,6 @@ namespace smt {
virtual inf_eps value(theory_var) = 0;
virtual inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) = 0;
virtual theory_var add_objective(app* term) = 0;
virtual expr_ref mk_ge(filter_model_converter& fm, theory_var v, inf_eps const& val) { UNREACHABLE(); return expr_ref(*((ast_manager*)0)); }
bool is_linear(ast_manager& m, expr* term);
bool is_numeral(arith_util& a, expr* term);
};

135
src/smt/theory_seq.cpp
View file

@ -2235,8 +2235,9 @@ bool theory_seq::add_stoi_axiom(expr* e) {
context& ctx = get_context();
expr* n;
rational val;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_stoi(e, n));
if (get_value(e, val) && !m_stoi_axioms.contains(val)) {
if (get_num_value(e, val) && !m_stoi_axioms.contains(val)) {
m_stoi_axioms.insert(val);
if (!val.is_minus_one()) {
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
@ -2252,15 +2253,72 @@ bool theory_seq::add_stoi_axiom(expr* e) {
return true;
}
}
if (upper_bound(n, val) && get_length(n, val) && val.is_pos() && !m_stoi_axioms.contains(val)) {
zstring s;
SASSERT(val.is_unsigned());
unsigned sz = val.get_unsigned();
expr_ref len1(m), len2(m), ith_char(m), num(m), coeff(m);
expr_ref_vector nums(m);
len1 = m_util.str.mk_length(n);
len2 = m_autil.mk_int(sz);
literal lit = mk_eq(len1, len2, false);
literal_vector lits;
lits.push_back(~lit);
for (unsigned i = 0; i < sz; ++i) {
ith_char = mk_nth(n, m_autil.mk_int(i));
lits.push_back(~is_digit(ith_char));
nums.push_back(digit2int(ith_char));
}
for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
--i;
coeff = m_autil.mk_int(c);
nums[i] = m_autil.mk_mul(coeff, nums[i].get());
}
num = m_autil.mk_add(nums.size(), nums.c_ptr());
lits.push_back(mk_eq(e, num, false));
++m_stats.m_add_axiom;
m_new_propagation = true;
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.mark_as_relevant(lits[i]);
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
m_stoi_axioms.insert(val);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
}
return false;
}
literal theory_seq::is_digit(expr* ch) {
bv_util bv(m);
literal isd = mk_literal(mk_skolem(symbol("seq.is_digit"), ch, 0, 0, m.mk_bool_sort()));
expr_ref d2i = digit2int(ch);
expr_ref _lo(bv.mk_ule(bv.mk_numeral(rational('0'), bv.mk_sort(8)), ch), m);
expr_ref _hi(bv.mk_ule(ch, bv.mk_numeral(rational('9'), bv.mk_sort(8))), m);
literal lo = mk_literal(_lo);
literal hi = mk_literal(_hi);
add_axiom(~lo, ~hi, isd);
add_axiom(~isd, lo);
add_axiom(~isd, hi);
for (unsigned i = 0; i < 10; ++i) {
add_axiom(~mk_eq(ch, bv.mk_numeral(rational('0'+i), bv.mk_sort(8)), false), mk_eq(d2i, m_autil.mk_int(i), false));
}
return isd;
}
expr_ref theory_seq::digit2int(expr* ch) {
return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, 0, 0, m_autil.mk_int()), m);
}
bool theory_seq::add_itos_axiom(expr* e) {
context& ctx = get_context();
rational val;
expr* n;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, n));
if (get_value(n, val)) {
if (get_num_value(n, val)) {
if (!m_itos_axioms.contains(val)) {
m_itos_axioms.insert(val);
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
@ -2282,6 +2340,9 @@ bool theory_seq::add_itos_axiom(expr* e) {
else {
// stoi(itos(n)) = n
app_ref e2(m_util.str.mk_stoi(e), m);
if (ctx.e_internalized(e2) && ctx.get_enode(e2)->get_root() == ctx.get_enode(n)->get_root()) {
return false;
}
add_axiom(mk_eq(e2, n, false));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
@ -2464,22 +2525,27 @@ void theory_seq::init_model(model_generator & mg) {
class theory_seq::seq_value_proc : public model_value_proc {
enum source_t { unit_source, int_source, string_source };
theory_seq& th;
sort* m_sort;
svector<model_value_dependency> m_dependencies;
ptr_vector<expr> m_strings;
svector<bool> m_source;
svector<source_t> m_source;
public:
seq_value_proc(theory_seq& th, sort* s): th(th), m_sort(s) {
}
virtual ~seq_value_proc() {}
void add_dependency(enode* n) {
void add_unit(enode* n) {
m_dependencies.push_back(model_value_dependency(n));
m_source.push_back(true);
m_source.push_back(unit_source);
}
void add_int(enode* n) {
m_dependencies.push_back(model_value_dependency(n));
m_source.push_back(int_source);
}
void add_string(expr* n) {
m_strings.push_back(n);
m_source.push_back(false);
m_source.push_back(string_source);
}
virtual void get_dependencies(buffer<model_value_dependency> & result) {
result.append(m_dependencies.size(), m_dependencies.c_ptr());
@ -2504,11 +2570,13 @@ public:
unsigned sz;
for (unsigned i = 0; i < m_source.size(); ++i) {
if (m_source[i]) {
switch (m_source[i]) {
case unit_source: {
VERIFY(bv.is_numeral(values[j++], val, sz));
sbuffer.push_back(val.get_unsigned());
break;
}
else {
case string_source: {
dependency* deps = 0;
expr_ref tmp = th.canonize(m_strings[k], deps);
zstring zs;
@ -2519,17 +2587,34 @@ public:
TRACE("seq", tout << "Not a string: " << tmp << "\n";);
}
++k;
break;
}
case int_source: {
std::ostringstream strm;
arith_util arith(th.m);
VERIFY(arith.is_numeral(values[j++], val));
if (val.is_neg()) strm << "-";
strm << abs(val);
zstring zs(strm.str().c_str());
add_buffer(sbuffer, zs);
break;
}
}
}
result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr()));
}
else {
for (unsigned i = 0; i < m_source.size(); ++i) {
if (m_source[i]) {
switch (m_source[i]) {
case unit_source:
args.push_back(th.m_util.str.mk_unit(values[j++]));
}
else {
break;
case string_source:
args.push_back(m_strings[k++]);
break;
case int_source:
UNREACHABLE();
break;
}
}
result = th.mk_concat(args, m_sort);
@ -2567,7 +2652,12 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
TRACE("seq", tout << mk_pp(c, m) << "\n";);
if (m_util.str.is_unit(c, c1)) {
if (ctx.e_internalized(c1)) {
sv->add_dependency(ctx.get_enode(c1));
sv->add_unit(ctx.get_enode(c1));
}
}
else if (m_util.str.is_itos(c, c1)) {
if (ctx.e_internalized(c1)) {
sv->add_int(ctx.get_enode(c1));
}
}
else if (m_util.str.is_string(c)) {
@ -2741,7 +2831,8 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
}
else if (m_util.str.is_itos(e, e1)) {
rational val;
if (get_value(e1, val)) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
if (get_num_value(e1, val)) {
TRACE("seq", tout << mk_pp(e, m) << " -> " << val << "\n";);
expr_ref num(m), res(m);
num = m_autil.mk_numeral(val, true);
@ -2916,7 +3007,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
expr_ref len_t(m_util.str.mk_length(t), m);
literal offset_ge_len = mk_literal(m_autil.mk_ge(mk_sub(offset, len_t), zero));
add_axiom(offset_ge_len, mk_eq(i, minus_one, false));
add_axiom(~offset_ge_len, mk_eq(i, minus_one, false));
expr_ref x = mk_skolem(m_indexof_left, t, s, offset);
expr_ref y = mk_skolem(m_indexof_right, t, s, offset);
@ -3024,7 +3115,7 @@ void theory_seq::add_itos_length_axiom(expr* len) {
unsigned num_char1 = 1, num_char2 = 1;
rational len1, len2;
rational ten(10);
if (get_value(n, len1)) {
if (get_num_value(n, len1)) {
bool neg = len1.is_neg();
if (neg) len1.neg();
num_char1 = neg?2:1;
@ -3038,7 +3129,7 @@ void theory_seq::add_itos_length_axiom(expr* len) {
}
SASSERT(len1 <= upper);
}
if (get_value(len, len2) && len2.is_unsigned()) {
if (get_num_value(len, len2) && len2.is_unsigned()) {
num_char2 = len2.get_unsigned();
}
unsigned num_char = std::max(num_char1, num_char2);
@ -3172,18 +3263,17 @@ static theory_mi_arith* get_th_arith(context& ctx, theory_id afid, expr* e) {
}
}
bool theory_seq::get_value(expr* e, rational& val) const {
bool theory_seq::get_num_value(expr* e, rational& val) const {
context& ctx = get_context();
theory_mi_arith* tha = get_th_arith(ctx, m_autil.get_family_id(), e);
expr_ref _val(m);
if (!tha) return false;
enode* next = ctx.get_enode(e), *n;
enode* next = ctx.get_enode(e), *n = next;
do {
n = next;
if (tha->get_value(n, _val) && m_autil.is_numeral(_val, val) && val.is_int()) {
if (tha->get_value(next, _val) && m_autil.is_numeral(_val, val) && val.is_int()) {
return true;
}
next = n->get_next();
next = next->get_next();
}
while (next != n);
return false;
@ -3692,7 +3782,10 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (is_skolem(symbol("seq.split"), e)) {
// propagate equalities
}
else if (is_skolem(symbol("seq.is_digit"), e)) {
}
else {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
UNREACHABLE();
}
}

4
src/smt/theory_seq.h
View file

@ -499,6 +499,8 @@ namespace smt {
void add_in_re_axiom(expr* n);
bool add_stoi_axiom(expr* n);
bool add_itos_axiom(expr* n);
literal is_digit(expr* ch);
expr_ref digit2int(expr* ch);
void add_itos_length_axiom(expr* n);
literal mk_literal(expr* n);
literal mk_eq_empty(expr* n, bool phase = true);
@ -512,7 +514,7 @@ namespace smt {
// arithmetic integration
bool get_value(expr* s, rational& val) const;
bool get_num_value(expr* s, rational& val) const;
bool lower_bound(expr* s, rational& lo) const;
bool upper_bound(expr* s, rational& hi) const;
bool get_length(expr* s, rational& val) const;

2
src/smt/theory_utvpi_def.h
View file

@ -901,7 +901,7 @@ namespace smt {
bool is_int = a.is_int(n->get_owner());
rational num = mk_value(v, is_int);
TRACE("utvpi", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int));
return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int));
}
/**

577
src/smt/theory_wmaxsat.cpp
View file

@ -21,294 +21,351 @@ Notes:
#include "smt_context.h"
#include "ast_pp.h"
#include "theory_wmaxsat.h"
#include "smt_justification.h"
namespace smt {
theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc):
theory(m.mk_family_id("weighted_maxsat")),
m_mc(mc),
m_vars(m),
m_fmls(m),
m_zweights(m_mpz),
m_old_values(m_mpz),
m_zcost(m_mpz),
m_zmin_cost(m_mpz),
m_found_optimal(false),
m_propagate(false),
m_normalize(false),
m_den(1)
{}
theory_wmaxsat::~theory_wmaxsat() {
m_old_values.reset();
}
/**
\brief return the complement of variables that are currently assigned.
*/
void theory_wmaxsat::get_assignment(svector<bool>& result) {
result.reset();
theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc):
theory(m.mk_family_id("weighted_maxsat")),
m_mc(mc),
m_vars(m),
m_fmls(m),
m_zweights(m_mpz),
m_old_values(m_mpz),
m_zcost(m_mpz),
m_zmin_cost(m_mpz),
m_found_optimal(false),
m_propagate(false),
m_normalize(false),
m_den(1)
{}
if (!m_found_optimal) {
for (unsigned i = 0; i < m_vars.size(); ++i) {
result.push_back(false);
}
theory_wmaxsat::~theory_wmaxsat() {
m_old_values.reset();
}
else {
std::sort(m_cost_save.begin(), m_cost_save.end());
for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) {
if (j < m_cost_save.size() && m_cost_save[j] == static_cast<theory_var>(i)) {
/**
\brief return the complement of variables that are currently assigned.
*/
void theory_wmaxsat::get_assignment(svector<bool>& result) {
result.reset();
if (!m_found_optimal) {
for (unsigned i = 0; i < m_vars.size(); ++i) {
result.push_back(false);
++j;
}
else {
result.push_back(true);
}
}
else {
std::sort(m_cost_save.begin(), m_cost_save.end());
for (unsigned i = 0,j = 0; i < m_vars.size(); ++i) {
if (j < m_cost_save.size() && m_cost_save[j] == static_cast<theory_var>(i)) {
result.push_back(false);
++j;
}
else {
result.push_back(true);
}
}
}
TRACE("opt",
tout << "cost save: ";
for (unsigned i = 0; i < m_cost_save.size(); ++i) {
tout << m_cost_save[i] << " ";
}
tout << "\nvars: ";
for (unsigned i = 0; i < m_vars.size(); ++i) {
tout << mk_pp(m_vars[i].get(), get_manager()) << " ";
}
tout << "\nassignment: ";
for (unsigned i = 0; i < result.size(); ++i) {
tout << result[i] << " ";
}
tout << "\n";);
}
TRACE("opt",
tout << "cost save: ";
for (unsigned i = 0; i < m_cost_save.size(); ++i) {
tout << m_cost_save[i] << " ";
}
tout << "\nvars: ";
for (unsigned i = 0; i < m_vars.size(); ++i) {
tout << mk_pp(m_vars[i].get(), get_manager()) << " ";
}
tout << "\nassignment: ";
for (unsigned i = 0; i < result.size(); ++i) {
tout << result[i] << " ";
}
tout << "\n";);
}
void theory_wmaxsat::init_search_eh() {
m_propagate = true;
}
expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w, bool is_true) {
context & ctx = get_context();
ast_manager& m = get_manager();
app_ref var(m), wfml(m);
var = m.mk_fresh_const("w", m.mk_bool_sort());
m_mc.insert(var->get_decl());
wfml = m.mk_or(var, fml);
ctx.assert_expr(wfml);
m_rweights.push_back(w);
m_vars.push_back(var);
m_fmls.push_back(fml);
m_assigned.push_back(false);
if (!is_true) {
m_rmin_cost += w;
void theory_wmaxsat::init_search_eh() {
m_propagate = true;
}
m_normalize = true;
return ctx.bool_var2expr(register_var(var, true));
}
bool_var theory_wmaxsat::register_var(app* var, bool attach) {
context & ctx = get_context();
bool_var bv;
SASSERT(!ctx.e_internalized(var));
enode* x = ctx.mk_enode(var, false, true, true);
if (ctx.b_internalized(var)) {
bv = ctx.get_bool_var(var);
expr* theory_wmaxsat::assert_weighted(expr* fml, rational const& w) {
context & ctx = get_context();
ast_manager& m = get_manager();
app_ref var(m), wfml(m);
var = m.mk_fresh_const("w", m.mk_bool_sort());
m_mc.insert(var->get_decl());
wfml = m.mk_or(var, fml);
ctx.assert_expr(wfml);
m_rweights.push_back(w);
m_vars.push_back(var);
m_fmls.push_back(fml);
m_assigned.push_back(false);
m_enabled.push_back(true);
m_normalize = true;
bool_var bv = register_var(var, true);
TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";
tout << wfml << "\n";);
return var;
}
else {
bv = ctx.mk_bool_var(var);
}
ctx.set_enode_flag(bv, true);
if (attach) {
ctx.set_var_theory(bv, get_id());
theory_var v = mk_var(x);
ctx.attach_th_var(x, this, v);
m_bool2var.insert(bv, v);
SASSERT(v == static_cast<theory_var>(m_var2bool.size()));
m_var2bool.push_back(bv);
SASSERT(ctx.bool_var2enode(bv));
}
return bv;
}
rational const& theory_wmaxsat::get_min_cost() {
unsynch_mpq_manager mgr;
scoped_mpq q(mgr);
mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator());
m_rmin_cost = rational(q);
return m_rmin_cost;
}
void theory_wmaxsat::assign_eh(bool_var v, bool is_true) {
TRACE("opt", tout << "Assign " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << " " << is_true << "\n";);
if (is_true) {
if (m_normalize) normalize();
void theory_wmaxsat::disable_var(expr* var) {
context& ctx = get_context();
theory_var tv = m_bool2var[v];
if (m_assigned[tv]) return;
scoped_mpz w(m_mpz);
w = m_zweights[tv];
ctx.push_trail(numeral_trail(m_zcost, m_old_values));
ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
ctx.push_trail(value_trail<context, bool>(m_assigned[tv]));
m_zcost += w;
m_costs.push_back(tv);
m_assigned[tv] = true;
if (m_zcost > m_zmin_cost) {
block();
SASSERT(ctx.b_internalized(var));
bool_var bv = ctx.get_bool_var(var);
theory_var tv = m_bool2var[bv];
m_enabled[tv] = false;
TRACE("opt", tout << "disable: v" << tv << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";);
}
bool_var theory_wmaxsat::register_var(app* var, bool attach) {
context & ctx = get_context();
bool_var bv;
SASSERT(!ctx.e_internalized(var));
enode* x = ctx.mk_enode(var, false, true, true);
if (ctx.b_internalized(var)) {
bv = ctx.get_bool_var(var);
}
}
}
final_check_status theory_wmaxsat::final_check_eh() {
if (m_normalize) normalize();
return FC_DONE;
}
void theory_wmaxsat::reset_eh() {
theory::reset_eh();
reset_local();
}
void theory_wmaxsat::reset_local() {
m_vars.reset();
m_fmls.reset();
m_rweights.reset();
m_rmin_cost.reset();
m_rcost.reset();
m_zweights.reset();
m_zcost.reset();
m_zmin_cost.reset();
m_cost_save.reset();
m_bool2var.reset();
m_var2bool.reset();
m_propagate = false;
m_found_optimal = false;
m_assigned.reset();
}
void theory_wmaxsat::propagate() {
context& ctx = get_context();
for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) {
bool_var bv = m_var2bool[i];
lbool asgn = ctx.get_assignment(bv);
if (asgn == l_true) {
assign_eh(bv, true);
else {
bv = ctx.mk_bool_var(var);
}
ctx.set_enode_flag(bv, true);
if (attach) {
ctx.set_var_theory(bv, get_id());
theory_var v = mk_var(x);
ctx.attach_th_var(x, this, v);
m_bool2var.insert(bv, v);
SASSERT(v == static_cast<theory_var>(m_var2bool.size()));
m_var2bool.push_back(bv);
SASSERT(ctx.bool_var2enode(bv));
}
return bv;
}
m_propagate = false;
}
bool theory_wmaxsat::is_optimal() const {
return !m_found_optimal || m_zcost < m_zmin_cost;
}
expr_ref theory_wmaxsat::mk_block() {
++m_stats.m_num_blocks;
ast_manager& m = get_manager();
expr_ref_vector disj(m);
compare_cost compare_cost(*this);
svector<theory_var> costs(m_costs);
std::sort(costs.begin(), costs.end(), compare_cost);
scoped_mpz weight(m_mpz);
m_mpz.reset(weight);
for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) {
weight += m_zweights[costs[i]];
disj.push_back(m.mk_not(m_vars[costs[i]].get()));
}
if (is_optimal()) {
rational theory_wmaxsat::get_cost() {
unsynch_mpq_manager mgr;
scoped_mpq q(mgr);
mgr.set(q, m_zmin_cost, m_den.to_mpq().numerator());
rational rw = rational(q);
m_zmin_cost = weight;
m_found_optimal = true;
mgr.set(q, m_zcost, m_den.to_mpq().numerator());
return rational(q);
}
void theory_wmaxsat::init_min_cost(rational const& r) {
m_rmin_cost = r;
m_zmin_cost = (m_rmin_cost * m_den).to_mpq().numerator();
}
void theory_wmaxsat::assign_eh(bool_var v, bool is_true) {
if (is_true) {
if (m_normalize) normalize();
context& ctx = get_context();
theory_var tv = m_bool2var[v];
if (m_assigned[tv] || !m_enabled[tv]) return;
scoped_mpz w(m_mpz);
w = m_zweights[tv];
ctx.push_trail(numeral_trail(m_zcost, m_old_values));
ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
ctx.push_trail(value_trail<context, bool>(m_assigned[tv]));
m_zcost += w;
TRACE("opt", tout << "Assign v" << tv << " weight: " << w << " cost: " << m_zcost << " " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << "\n";);
m_costs.push_back(tv);
m_assigned[tv] = true;
if (m_zcost >= m_zmin_cost) {
block();
}
else {
m_can_propagate = true;
}
}
}
final_check_status theory_wmaxsat::final_check_eh() {
if (m_normalize) normalize();
// std::cout << "cost: " << m_zcost << " min cost: " << m_zmin_cost << "\n";
return FC_DONE;
}
void theory_wmaxsat::reset_eh() {
theory::reset_eh();
reset_local();
}
void theory_wmaxsat::reset_local() {
m_vars.reset();
m_fmls.reset();
m_rweights.reset();
m_rmin_cost.reset();
m_zweights.reset();
m_zcost.reset();
m_zmin_cost.reset();
m_cost_save.reset();
m_cost_save.append(m_costs);
m_bool2var.reset();
m_var2bool.reset();
m_propagate = false;
m_can_propagate = false;
m_found_optimal = false;
m_assigned.reset();
m_enabled.reset();
}
void theory_wmaxsat::propagate() {
context& ctx = get_context();
for (unsigned i = 0; m_propagate && i < m_vars.size(); ++i) {
bool_var bv = m_var2bool[i];
lbool asgn = ctx.get_assignment(bv);
if (asgn == l_true) {
assign_eh(bv, true);
}
}
m_propagate = false;
//while (m_found_optimal && max_unassigned_is_blocked() && !ctx.inconsistent()) { }
m_can_propagate = false;
}
bool theory_wmaxsat::is_optimal() const {
return !m_found_optimal || m_zcost < m_zmin_cost;
}
expr_ref theory_wmaxsat::mk_block() {
++m_stats.m_num_blocks;
ast_manager& m = get_manager();
expr_ref_vector disj(m);
compare_cost compare_cost(*this);
svector<theory_var> costs(m_costs);
std::sort(costs.begin(), costs.end(), compare_cost);
scoped_mpz weight(m_mpz);
m_mpz.reset(weight);
for (unsigned i = 0; i < costs.size() && m_mpz.lt(weight, m_zmin_cost); ++i) {
theory_var tv = costs[i];
if (m_enabled[tv]) {
weight += m_zweights[tv];
disj.push_back(m.mk_not(m_vars[tv].get()));
}
}
if (is_optimal()) {
m_found_optimal = true;
m_cost_save.reset();
m_cost_save.append(m_costs);
TRACE("opt",
tout << "costs: ";
for (unsigned i = 0; i < m_costs.size(); ++i) {
tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
}
tout << "\n";
//get_context().display(tout);
);
}
expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
TRACE("opt",
tout << "costs: ";
for (unsigned i = 0; i < m_costs.size(); ++i) {
tout << mk_pp(get_enode(m_costs[i])->get_owner(), get_manager()) << " ";
}
tout << "\n";
get_context().display(tout);
);
tout << result << " weight: " << weight << "\n";
tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";);
return result;
}
expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
TRACE("opt",
tout << result << " weight: " << weight << "\n";
tout << "cost: " << m_zcost << " min-cost: " << m_zmin_cost << "\n";);
return result;
}
expr_ref theory_wmaxsat::mk_optimal_block(svector<bool_var> const& ws, rational const& weight) {
ast_manager& m = get_manager();
expr_ref_vector disj(m);
rational new_w = weight*m_den;
m_zmin_cost = new_w.to_mpq().numerator();
m_cost_save.reset();
for (unsigned i = 0; i < ws.size(); ++i) {
bool_var bv = ws[i];
theory_var v = m_bool2var[bv];
m_cost_save.push_back(v);
disj.push_back(m.mk_not(m_vars[v].get()));
}
expr_ref result(m.mk_or(disj.size(), disj.c_ptr()), m);
return result;
}
void theory_wmaxsat::restart_eh() {}
void theory_wmaxsat::block() {
if (m_vars.empty()) {
return;
void theory_wmaxsat::block() {
if (m_vars.empty()) {
return;
}
++m_stats.m_num_blocks;
context& ctx = get_context();
literal_vector lits;
compare_cost compare_cost(*this);
svector<theory_var> costs(m_costs);
std::sort(costs.begin(), costs.end(), compare_cost);
scoped_mpz weight(m_mpz);
m_mpz.reset(weight);
for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) {
weight += m_zweights[costs[i]];
lits.push_back(literal(m_var2bool[costs[i]]));
}
TRACE("opt", ctx.display_literals_verbose(tout, lits); tout << "\n";);
ctx.set_conflict(
ctx.mk_justification(
ext_theory_conflict_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, 0, 0, 0)));
}
bool theory_wmaxsat::max_unassigned_is_blocked() {
context& ctx = get_context();
unsigned max_unassigned = m_max_unassigned_index;
if (max_unassigned < m_sorted_vars.size() &&
m_zcost + m_zweights[m_sorted_vars[max_unassigned]] < m_zmin_cost) {
return false;
}
// update value of max-unassigned
while (max_unassigned < m_sorted_vars.size() &&
ctx.get_assignment(m_var2bool[m_sorted_vars[max_unassigned]]) != l_undef) {
++max_unassigned;
}
//
if (max_unassigned > m_max_unassigned_index) {
ctx.push_trail(value_trail<context, unsigned>(m_max_unassigned_index));
m_max_unassigned_index = max_unassigned;
}
if (max_unassigned < m_sorted_vars.size() &&
m_zcost + m_zweights[m_sorted_vars[max_unassigned]] >= m_zmin_cost) {
theory_var tv = m_sorted_vars[max_unassigned];
propagate(m_var2bool[tv]);
m_max_unassigned_index++;
return true;
}
return false;
}
++m_stats.m_num_blocks;
context& ctx = get_context();
literal_vector lits;
compare_cost compare_cost(*this);
svector<theory_var> costs(m_costs);
std::sort(costs.begin(), costs.end(), compare_cost);
scoped_mpz weight(m_mpz);
m_mpz.reset(weight);
for (unsigned i = 0; i < costs.size() && weight < m_zmin_cost; ++i) {
weight += m_zweights[costs[i]];
lits.push_back(~literal(m_var2bool[costs[i]]));
}
TRACE("opt",
ast_manager& m = get_manager();
tout << "block: ";
for (unsigned i = 0; i < lits.size(); ++i) {
expr_ref tmp(m);
ctx.literal2expr(lits[i], tmp);
tout << tmp << " ";
}
tout << "\n";
);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
void theory_wmaxsat::propagate(bool_var v) {
++m_stats.m_num_propagations;
context& ctx = get_context();
literal_vector lits;
literal lit(v, true);
SASSERT(ctx.get_assignment(lit) == l_undef);
for (unsigned i = 0; i < m_costs.size(); ++i) {
bool_var w = m_var2bool[m_costs[i]];
lits.push_back(literal(w));
}
TRACE("opt",
ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr());
ctx.display_literal_verbose(tout << " --> ", lit););
region& r = ctx.get_region();
ctx.assign(lit, ctx.mk_justification(
ext_theory_propagation_justification(
get_id(), r, lits.size(), lits.c_ptr(), 0, 0, lit, 0, 0)));
}
void theory_wmaxsat::normalize() {
m_den = rational::one();
for (unsigned i = 0; i < m_rweights.size(); ++i) {
m_den = lcm(m_den, denominator(m_rweights[i]));
void theory_wmaxsat::normalize() {
m_den = rational::one();
for (unsigned i = 0; i < m_rweights.size(); ++i) {
if (m_enabled[i]) {
m_den = lcm(m_den, denominator(m_rweights[i]));
}
}
m_den = lcm(m_den, denominator(m_rmin_cost));
SASSERT(!m_den.is_zero());
m_zweights.reset();
m_sorted_vars.reset();
for (unsigned i = 0; i < m_rweights.size(); ++i) {
rational r = m_rweights[i]*m_den;
SASSERT(r.is_int());
mpq const& q = r.to_mpq();
m_zweights.push_back(q.numerator());
m_sorted_vars.push_back(i);
}
compare_cost compare_cost(*this);
std::sort(m_sorted_vars.begin(), m_sorted_vars.end(), compare_cost);
m_max_unassigned_index = 0;
m_zcost.reset();
rational r = m_rmin_cost * m_den;
m_zmin_cost = r.to_mpq().numerator();
m_normalize = false;
}
m_den = lcm(m_den, denominator(m_rmin_cost));
SASSERT(!m_den.is_zero());
m_zweights.reset();
for (unsigned i = 0; i < m_rweights.size(); ++i) {
rational r = m_rweights[i]*m_den;
SASSERT(r.is_int());
mpq const& q = r.to_mpq();
m_zweights.push_back(q.numerator());
}
rational r = m_rcost* m_den;
m_zcost = r.to_mpq().numerator();
r = m_rmin_cost * m_den;
m_zmin_cost = r.to_mpq().numerator();
m_normalize = false;
}
};

30
src/smt/theory_wmaxsat.h
View file

@ -28,6 +28,7 @@ namespace smt {
class theory_wmaxsat : public theory {
struct stats {
unsigned m_num_blocks;
unsigned m_num_propagations;
void reset() { memset(this, 0, sizeof(*this)); }
stats() { reset(); }
};
@ -39,27 +40,31 @@ namespace smt {
scoped_mpz_vector m_zweights;
scoped_mpz_vector m_old_values;
svector<theory_var> m_costs; // set of asserted theory variables
unsigned m_max_unassigned_index; // index of literal that is not yet assigned and has maximal weight.
svector<theory_var> m_sorted_vars; // set of all theory variables, sorted by cost
svector<theory_var> m_cost_save; // set of asserted theory variables
rational m_rcost; // current sum of asserted costs
rational m_rmin_cost; // current maximal cost assignment.
scoped_mpz m_zcost; // current sum of asserted costs
scoped_mpz m_zmin_cost; // current maximal cost assignment.
bool m_found_optimal;
u_map<theory_var> m_bool2var; // bool_var -> theory_var
svector<bool_var> m_var2bool; // theory_var -> bool_var
bool m_propagate;
bool m_propagate;
bool m_can_propagate;
bool m_normalize;
rational m_den; // lcm of denominators for rational weights.
svector<bool> m_assigned;
svector<bool> m_assigned, m_enabled;
stats m_stats;
public:
theory_wmaxsat(ast_manager& m, filter_model_converter& mc);
virtual ~theory_wmaxsat();
void get_assignment(svector<bool>& result);
virtual void init_search_eh();
expr* assert_weighted(expr* fml, rational const& w, bool is_true);
expr* assert_weighted(expr* fml, rational const& w);
void disable_var(expr* var);
bool_var register_var(app* var, bool attach);
rational const& get_min_cost();
rational get_cost();
void init_min_cost(rational const& r);
class numeral_trail : public trail<context> {
typedef scoped_mpz T;
T & m_value;
@ -79,6 +84,8 @@ namespace smt {
m_old_values.shrink(m_old_values.size() - 1);
}
};
virtual void init_search_eh();
virtual void assign_eh(bool_var v, bool is_true);
virtual final_check_status final_check_eh();
virtual bool use_diseqs() const {
@ -95,23 +102,30 @@ namespace smt {
virtual void new_eq_eh(theory_var v1, theory_var v2) { }
virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
virtual void display(std::ostream& out) const {}
virtual void restart_eh();
virtual void collect_statistics(::statistics & st) const {
st.update("wmaxsat num blocks", m_stats.m_num_blocks);
st.update("wmaxsat num props", m_stats.m_num_propagations);
}
virtual bool can_propagate() {
return m_propagate;
return m_propagate || m_can_propagate;
}
virtual void propagate();
bool is_optimal() const;
expr_ref mk_block();
expr_ref mk_optimal_block(svector<bool_var> const& ws, rational const& weight);
private:
void block();
void propagate(bool_var v);
void normalize();
bool max_unassigned_is_blocked();
class compare_cost {
theory_wmaxsat& m_th;