mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix pb rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f04e805fa4
commit
e7d43ed516
|
@ -15,9 +15,6 @@ Author:
|
|||
|
||||
Notes:
|
||||
|
||||
TBD: also keep track of which fresh constants are introduced
|
||||
to instruct model converter to delete them.
|
||||
|
||||
--*/
|
||||
#include "ast/rewriter/bit_blaster/bit_blaster_rewriter.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
|
@ -95,6 +92,8 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
|
|||
func_decl_ref_vector m_keys;
|
||||
expr_ref_vector m_values;
|
||||
unsigned_vector m_keyval_lim;
|
||||
func_decl_ref_vector m_newbits;
|
||||
unsigned_vector m_newbits_lim;
|
||||
|
||||
bool m_blast_mul;
|
||||
bool m_blast_add;
|
||||
|
@ -121,7 +120,8 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
|
|||
m_out(m),
|
||||
m_bindings(m),
|
||||
m_keys(m),
|
||||
m_values(m) {
|
||||
m_values(m),
|
||||
m_newbits(m) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
|
@ -163,6 +163,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
|
|||
|
||||
void push() {
|
||||
m_keyval_lim.push_back(m_keys.size());
|
||||
m_newbits_lim.push_back(m_newbits.size());
|
||||
}
|
||||
|
||||
unsigned get_num_scopes() const {
|
||||
|
@ -181,6 +182,10 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
|
|||
m_keys.resize(lim);
|
||||
m_values.resize(lim);
|
||||
m_keyval_lim.resize(new_sz);
|
||||
|
||||
lim = m_newbits_lim[new_sz];
|
||||
m_newbits.shrink(lim);
|
||||
m_newbits_lim.shrink(new_sz);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -189,10 +194,13 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
|
|||
void start_rewrite() {
|
||||
m_keypos = m_keys.size();
|
||||
}
|
||||
void end_rewrite(obj_map<func_decl, expr*>& const2bits) {
|
||||
|
||||
void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
|
||||
for (unsigned i = m_keypos; i < m_keys.size(); ++i) {
|
||||
const2bits.insert(m_keys[i].get(), m_values[i].get());
|
||||
}
|
||||
for (func_decl* f : m_newbits) newbits.push_back(f);
|
||||
|
||||
}
|
||||
|
||||
template<typename V>
|
||||
|
@ -215,6 +223,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
|
|||
m_out.reset();
|
||||
for (unsigned i = 0; i < bv_size; i++) {
|
||||
m_out.push_back(m().mk_fresh_const(0, b));
|
||||
m_newbits.push_back(to_app(m_out.back())->get_decl());
|
||||
}
|
||||
r = mk_mkbv(m_out);
|
||||
m_const2bits.insert(f, r);
|
||||
|
@ -650,7 +659,7 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
|
|||
void push() { m_cfg.push(); }
|
||||
void pop(unsigned s) { m_cfg.pop(s); }
|
||||
void start_rewrite() { m_cfg.start_rewrite(); }
|
||||
void end_rewrite(obj_map<func_decl, expr*>& const2bits) { m_cfg.end_rewrite(const2bits); }
|
||||
void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) { m_cfg.end_rewrite(const2bits, newbits); }
|
||||
unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
|
||||
};
|
||||
|
||||
|
@ -703,6 +712,6 @@ void bit_blaster_rewriter::start_rewrite() {
|
|||
m_imp->start_rewrite();
|
||||
}
|
||||
|
||||
void bit_blaster_rewriter::end_rewrite(obj_map<func_decl, expr*>& const2bits) {
|
||||
m_imp->end_rewrite(const2bits);
|
||||
void bit_blaster_rewriter::end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
|
||||
m_imp->end_rewrite(const2bits, newbits);
|
||||
}
|
||||
|
|
|
@ -33,13 +33,15 @@ public:
|
|||
ast_manager & m() const;
|
||||
unsigned get_num_steps() const;
|
||||
void cleanup();
|
||||
obj_map<func_decl, expr*> const& const2bits() const;
|
||||
void start_rewrite();
|
||||
void end_rewrite(obj_map<func_decl, expr*>& const2bits);
|
||||
void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits);
|
||||
void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
|
||||
void push();
|
||||
void pop(unsigned num_scopes);
|
||||
unsigned get_num_scopes() const;
|
||||
private:
|
||||
obj_map<func_decl, expr*> const& const2bits() const;
|
||||
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
@ -255,11 +255,11 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
|
|||
rational slack(0);
|
||||
m_args.reset();
|
||||
m_coeffs.reset();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
m_args.push_back(vec[i].first);
|
||||
m_coeffs.push_back(vec[i].second);
|
||||
SASSERT(vec[i].second.is_pos());
|
||||
slack += vec[i].second;
|
||||
for (auto const& kv : vec) {
|
||||
m_args.push_back(kv.first);
|
||||
m_coeffs.push_back(kv.second);
|
||||
SASSERT(kv.second.is_pos());
|
||||
slack += kv.second;
|
||||
all_unit &= m_coeffs.back().is_one();
|
||||
}
|
||||
if (is_eq) {
|
||||
|
@ -287,7 +287,9 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
|
|||
}
|
||||
else {
|
||||
expr_ref_vector conj(m), disj(m);
|
||||
for (unsigned i = 0; i < m_args.size(); ++i) {
|
||||
unsigned j = 0;
|
||||
sz = m_args.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
rational& c = m_coeffs[i];
|
||||
if (slack < c + k) {
|
||||
conj.push_back(m_args[i]);
|
||||
|
@ -299,29 +301,25 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
|
|||
disj.push_back(m_args[i]);
|
||||
}
|
||||
else {
|
||||
continue;
|
||||
m_args[j] = m_args[i];
|
||||
m_coeffs[j] = m_coeffs[i];
|
||||
++j;
|
||||
}
|
||||
m_args[i] = m_args.back();
|
||||
m_coeffs[i] = m_coeffs.back();
|
||||
--i;
|
||||
m_args.pop_back();
|
||||
m_coeffs.pop_back();
|
||||
}
|
||||
sz = m_coeffs.size();
|
||||
if (slack < k) {
|
||||
conj.push_back(m.mk_false());
|
||||
m_args.shrink(j);
|
||||
m_coeffs.shrink(j);
|
||||
sz = j;
|
||||
if (k.is_pos() && sz > 0 && slack >= k) {
|
||||
disj.push_back(m_util.mk_ge(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k));
|
||||
}
|
||||
else if (k.is_pos() && sz > 0) {
|
||||
conj.push_back(m_util.mk_ge(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k));
|
||||
if (!disj.empty()) {
|
||||
conj.push_back(mk_or(disj));
|
||||
}
|
||||
result = mk_and(conj);
|
||||
if (!disj.empty()) {
|
||||
disj.push_back(result);
|
||||
result = mk_or(disj);
|
||||
}
|
||||
if (!disj.empty() || conj.size() > 1) {
|
||||
|
||||
if (disj.size() > 1 || conj.size() > 1) {
|
||||
st = BR_REWRITE3;
|
||||
}
|
||||
}
|
||||
}
|
||||
break;
|
||||
}
|
||||
|
|
|
@ -45,25 +45,25 @@ void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::num
|
|||
}
|
||||
}
|
||||
// remove constants
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
unsigned j = 0, sz = args.size();
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
if (m_util.is_true(args[i].first)) {
|
||||
k -= args[i].second;
|
||||
std::swap(args[i], args[args.size()-1]);
|
||||
args.pop_back();
|
||||
--i;
|
||||
}
|
||||
else if (m_util.is_false(args[i].first)) {
|
||||
std::swap(args[i], args[args.size()-1]);
|
||||
args.pop_back();
|
||||
--i;
|
||||
// no-op
|
||||
}
|
||||
else {
|
||||
args[j++] = args[i];
|
||||
}
|
||||
}
|
||||
args.shrink(j);
|
||||
// sort and coalesce arguments:
|
||||
typename PBU::compare cmp;
|
||||
std::sort(args.begin(), args.end(), cmp);
|
||||
|
||||
// coallesce
|
||||
unsigned i, j;
|
||||
unsigned i;
|
||||
for (i = 0, j = 1; j < args.size(); ++j) {
|
||||
if (args[i].first == args[j].first) {
|
||||
args[i].second += args[j].second;
|
||||
|
|
|
@ -266,7 +266,7 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << "\n";
|
||||
IF_VERBOSE(5, verbose_stream() << "is-sat: " << is_sat << "\n";
|
||||
if (is_sat == l_true) {
|
||||
verbose_stream() << "Satisfying soft constraints\n";
|
||||
display_answer(verbose_stream());
|
||||
|
|
|
@ -17,6 +17,7 @@ Notes:
|
|||
|
||||
--*/
|
||||
|
||||
#include "util/gparams.h"
|
||||
#include "ast/for_each_expr.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/bv_decl_plugin.h"
|
||||
|
@ -125,7 +126,7 @@ namespace opt {
|
|||
m_box_index(UINT_MAX),
|
||||
m_optsmt(m),
|
||||
m_scoped_state(m),
|
||||
m_fm(m, "opt"),
|
||||
m_fm(alloc(generic_model_converter, m, "opt")),
|
||||
m_objective_refs(m),
|
||||
m_enable_sat(false),
|
||||
m_is_clausal(false),
|
||||
|
@ -277,9 +278,12 @@ namespace opt {
|
|||
if (is_sat != l_false) {
|
||||
s.get_model(m_model);
|
||||
s.get_labels(m_labels);
|
||||
if (is_sat == l_true) {
|
||||
validate_model();
|
||||
}
|
||||
}
|
||||
if (is_sat != l_true) {
|
||||
TRACE("opt", tout << m_hard_constraints << "\n";);
|
||||
TRACE("opt", tout << m_hard_constraints << "\n";);
|
||||
return is_sat;
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";);
|
||||
|
@ -308,6 +312,7 @@ namespace opt {
|
|||
break;
|
||||
}
|
||||
}
|
||||
if (is_sat == l_true) validate_model();
|
||||
return adjust_unknown(is_sat);
|
||||
}
|
||||
|
||||
|
@ -324,8 +329,8 @@ namespace opt {
|
|||
|
||||
void context::fix_model(model_ref& mdl) {
|
||||
if (mdl) {
|
||||
(*m_fm)(mdl);
|
||||
apply(m_model_converter, mdl);
|
||||
m_fm(mdl);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -568,7 +573,7 @@ namespace opt {
|
|||
|
||||
void context::init_solver() {
|
||||
setup_arith_solver();
|
||||
m_opt_solver = alloc(opt_solver, m, m_params, m_fm);
|
||||
m_opt_solver = alloc(opt_solver, m, m_params, *m_fm);
|
||||
m_opt_solver->set_logic(m_logic);
|
||||
m_solver = m_opt_solver.get();
|
||||
m_opt_solver->ensure_pb();
|
||||
|
@ -792,13 +797,13 @@ namespace opt {
|
|||
offset -= weight;
|
||||
}
|
||||
if (m.is_true(arg)) {
|
||||
IF_VERBOSE(1, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> true\n";);
|
||||
IF_VERBOSE(5, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> true\n";);
|
||||
}
|
||||
else if (weight.is_zero()) {
|
||||
// skip
|
||||
}
|
||||
else if (m.is_false(arg)) {
|
||||
IF_VERBOSE(1, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> false\n";);
|
||||
IF_VERBOSE(5, verbose_stream() << weight << ": " << mk_pp(m_objectives[index].m_terms[i].get(), m) << " |-> false\n";);
|
||||
offset += weight;
|
||||
}
|
||||
else {
|
||||
|
@ -924,8 +929,7 @@ namespace opt {
|
|||
TRACE("opt", tout << fmls << "\n";);
|
||||
m_hard_constraints.reset();
|
||||
expr_ref orig_term(m);
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
expr* fml = fmls[i];
|
||||
for (expr * fml : fmls) {
|
||||
app_ref tr(m);
|
||||
expr_ref_vector terms(m);
|
||||
vector<rational> weights;
|
||||
|
@ -1110,8 +1114,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
void context::internalize() {
|
||||
for (unsigned i = 0; i < m_objectives.size(); ++i) {
|
||||
objective & obj = m_objectives[i];
|
||||
for (objective & obj : m_objectives) {
|
||||
switch(obj.m_type) {
|
||||
case O_MINIMIZE: {
|
||||
app_ref tmp(m);
|
||||
|
@ -1397,21 +1400,21 @@ namespace opt {
|
|||
}
|
||||
|
||||
std::string context::to_string() const {
|
||||
return to_string(m_scoped_state.m_hard, m_scoped_state.m_objectives);
|
||||
return to_string(false, m_scoped_state.m_hard, m_scoped_state.m_objectives);
|
||||
}
|
||||
|
||||
std::string context::to_string_internal() const {
|
||||
return to_string(m_hard_constraints, m_objectives);
|
||||
return to_string(true, m_hard_constraints, m_objectives);
|
||||
}
|
||||
|
||||
std::string context::to_string(expr_ref_vector const& hard, vector<objective> const& objectives) const {
|
||||
std::string context::to_string(bool is_internal, expr_ref_vector const& hard, vector<objective> const& objectives) const {
|
||||
smt2_pp_environment_dbg env(m);
|
||||
ast_pp_util visitor(m);
|
||||
std::ostringstream out;
|
||||
visitor.collect(hard);
|
||||
model_converter_ref mc = concat(m_model_converter.get(), m_fm.get());
|
||||
|
||||
for (unsigned i = 0; i < objectives.size(); ++i) {
|
||||
objective const& obj = objectives[i];
|
||||
for (objective const& obj : objectives) {
|
||||
switch(obj.m_type) {
|
||||
case O_MAXIMIZE:
|
||||
case O_MINIMIZE:
|
||||
|
@ -1426,10 +1429,16 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
if (is_internal && mc) {
|
||||
mc->collect(visitor);
|
||||
}
|
||||
|
||||
param_descrs descrs;
|
||||
collect_param_descrs(descrs);
|
||||
m_params.display_smt2(out, "opt", descrs);
|
||||
visitor.display_decls(out);
|
||||
visitor.display_asserts(out, hard, m_pp_neat);
|
||||
for (unsigned i = 0; i < objectives.size(); ++i) {
|
||||
objective const& obj = objectives[i];
|
||||
for (objective const& obj : objectives) {
|
||||
switch(obj.m_type) {
|
||||
case O_MAXIMIZE:
|
||||
out << "(maximize ";
|
||||
|
@ -1464,15 +1473,33 @@ namespace opt {
|
|||
break;
|
||||
}
|
||||
}
|
||||
|
||||
param_descrs descrs;
|
||||
collect_param_descrs(descrs);
|
||||
m_params.display_smt2(out, "opt", descrs);
|
||||
|
||||
if (is_internal && mc) {
|
||||
mc->display(out);
|
||||
}
|
||||
|
||||
out << "(check-sat)\n";
|
||||
return out.str();
|
||||
}
|
||||
|
||||
void context::validate_model() {
|
||||
if (!gparams::get().get_bool("model_validate", false)) return;
|
||||
expr_ref_vector fmls(m);
|
||||
get_hard_constraints(fmls);
|
||||
expr_ref tmp(m);
|
||||
model_ref mdl;
|
||||
get_model(mdl);
|
||||
for (expr * f : fmls) {
|
||||
if (!mdl->eval(f, tmp) || !m.is_true(tmp)) {
|
||||
//IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n"));
|
||||
//IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n"));
|
||||
IF_VERBOSE(0, verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n");
|
||||
//IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *mdl, 0));
|
||||
IF_VERBOSE(11, verbose_stream() << to_string_internal() << "\n");
|
||||
exit(0);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void context::validate_maxsat(symbol const& id) {
|
||||
maxsmt& ms = *m_maxsmts.find(id);
|
||||
TRACE("opt", tout << "Validate: " << id << "\n";);
|
||||
|
@ -1551,8 +1578,8 @@ namespace opt {
|
|||
if (!m_arith.is_real(m_objectives[0].m_term)) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
|
||||
if (has_quantifiers(m_hard_constraints[i].get())) {
|
||||
for (expr* fml : m_hard_constraints) {
|
||||
if (has_quantifiers(fml)) {
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -155,7 +155,7 @@ namespace opt {
|
|||
vector<objective> m_objectives;
|
||||
model_ref m_model;
|
||||
model_converter_ref m_model_converter;
|
||||
generic_model_converter m_fm;
|
||||
generic_model_converter_ref m_fm;
|
||||
obj_map<func_decl, unsigned> m_objective_fns;
|
||||
obj_map<func_decl, expr*> m_objective_orig;
|
||||
func_decl_ref_vector m_objective_refs;
|
||||
|
@ -219,7 +219,7 @@ namespace opt {
|
|||
virtual expr_ref mk_le(unsigned i, model_ref& model);
|
||||
|
||||
virtual smt::context& smt_context() { return m_opt_solver->get_context(); }
|
||||
virtual generic_model_converter& fm() { return m_fm; }
|
||||
virtual generic_model_converter& fm() { return *m_fm; }
|
||||
virtual bool sat_enabled() const { return 0 != m_sat_solver.get(); }
|
||||
virtual solver& get_solver();
|
||||
virtual ast_manager& get_manager() const { return this->m; }
|
||||
|
@ -290,12 +290,13 @@ namespace opt {
|
|||
void display_objective(std::ostream& out, objective const& obj) const;
|
||||
void display_bounds(std::ostream& out, bounds_t const& b) const;
|
||||
|
||||
std::string to_string(expr_ref_vector const& hard, vector<objective> const& objectives) const;
|
||||
std::string to_string(bool is_internal, expr_ref_vector const& hard, vector<objective> const& objectives) const;
|
||||
std::string to_string_internal() const;
|
||||
|
||||
|
||||
void validate_lex();
|
||||
void validate_maxsat(symbol const& id);
|
||||
void validate_model();
|
||||
|
||||
void display_benchmark();
|
||||
|
||||
|
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#include "sat/ba_solver.h"
|
||||
#include "sat/sat_types.h"
|
||||
#include "util/mpz.h"
|
||||
#include "sat/sat_simplifier_params.hpp"
|
||||
|
||||
|
||||
namespace sat {
|
||||
|
@ -3013,19 +3014,21 @@ namespace sat {
|
|||
}
|
||||
|
||||
unsigned ba_solver::set_non_external() {
|
||||
sat_simplifier_params p(s().m_params);
|
||||
// set variables to be non-external if they are not used in theory constraints.
|
||||
unsigned ext = 0;
|
||||
for (unsigned v = 0; v < s().num_vars(); ++v) {
|
||||
bool incremental_mode = s().get_config().m_incremental && !p.override_incremental();
|
||||
incremental_mode |= s().tracking_assumptions();
|
||||
for (unsigned v = 0; !incremental_mode && v < s().num_vars(); ++v) {
|
||||
literal lit(v, false);
|
||||
if (s().is_external(v) &&
|
||||
m_cnstr_use_list[lit.index()].empty() &&
|
||||
m_cnstr_use_list[(~lit).index()].empty() &&
|
||||
!s().is_assumption(v)) {
|
||||
m_cnstr_use_list[(~lit).index()].empty()) {
|
||||
s().set_non_external(v);
|
||||
++ext;
|
||||
}
|
||||
}
|
||||
// ensure that lemmas use only external variables.
|
||||
// ensure that lemmas use only non-eliminated variables
|
||||
for (constraint* cp : m_learned) {
|
||||
constraint& c = *cp;
|
||||
if (c.was_removed()) continue;
|
||||
|
@ -4182,6 +4185,9 @@ namespace sat {
|
|||
bool ba_solver::check_model(model const& m) const {
|
||||
bool ok = true;
|
||||
for (constraint const* c : m_constraints) {
|
||||
if (c->is_pure() && c->lit() != null_literal && m[c->lit().var()] == (c->lit().sign() ? l_true : l_false)) {
|
||||
continue;
|
||||
}
|
||||
switch (eval(m, *c)) {
|
||||
case l_false:
|
||||
IF_VERBOSE(0, verbose_stream() << "failed checking " << c->id() << ": " << *c << "\n";);
|
||||
|
|
|
@ -2358,6 +2358,14 @@ namespace sat {
|
|||
idx--;
|
||||
}
|
||||
reset_unmark(old_size);
|
||||
if (m_core.size() > 1) {
|
||||
unsigned j = 0;
|
||||
for (unsigned i = 0; i < m_core.size(); ++i) {
|
||||
if (lvl(m_core[i]) > 0) m_core[j++] = m_core[i];
|
||||
}
|
||||
m_core.shrink(j);
|
||||
}
|
||||
|
||||
if (m_config.m_core_minimize) {
|
||||
if (m_min_core_valid && m_min_core.size() < m_core.size()) {
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat.updating core " << m_min_core.size() << " " << m_core.size() << ")\n";);
|
||||
|
|
|
@ -18,6 +18,7 @@ Notes:
|
|||
--*/
|
||||
|
||||
|
||||
#include "util/gparams.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_translation.h"
|
||||
#include "ast/ast_util.h"
|
||||
|
@ -584,7 +585,9 @@ private:
|
|||
}
|
||||
|
||||
bool internalize_var(expr* v, sat::bool_var_vector& bvars) {
|
||||
obj_map<func_decl, expr*> const& const2bits = m_bb_rewriter->const2bits();
|
||||
obj_map<func_decl, expr*> const2bits;
|
||||
ptr_vector<func_decl> newbits;
|
||||
m_bb_rewriter->end_rewrite(const2bits, newbits);
|
||||
expr* bv;
|
||||
bv_util bvutil(m);
|
||||
bool internalized = false;
|
||||
|
@ -803,12 +806,13 @@ private:
|
|||
}
|
||||
TRACE("sat", model_smt2_pp(tout, m, *mdl, 0););
|
||||
|
||||
// IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
|
||||
|
||||
#if 0
|
||||
IF_VERBOSE(0, verbose_streamm() << "Verifying solution\n";);
|
||||
if (!gparams::get().get_bool("model_validate", false)) return;
|
||||
IF_VERBOSE(0, verbose_stream() << "Verifying solution\n";);
|
||||
model_evaluator eval(*mdl);
|
||||
eval.set_model_completion(false);
|
||||
bool all_true = true;
|
||||
//unsigned i = 0;
|
||||
for (expr * f : m_fmls) {
|
||||
expr_ref tmp(m);
|
||||
eval(f, tmp);
|
||||
|
@ -819,19 +823,21 @@ private:
|
|||
IF_VERBOSE(0, verbose_stream() << "failed to verify: " << mk_pp(f, m) << "\n";);
|
||||
all_true = false;
|
||||
}
|
||||
else {
|
||||
VERIFY(m.is_true(tmp));
|
||||
}
|
||||
//IF_VERBOSE(0, verbose_stream() << (i++) << ": " << mk_pp(f, m) << "\n");
|
||||
}
|
||||
if (!all_true) {
|
||||
IF_VERBOSE(0, verbose_stream() << m_params << "\n";);
|
||||
IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"););
|
||||
IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mc0\n"););
|
||||
IF_VERBOSE(0, verbose_stream() << m_params << "\n");
|
||||
IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"));
|
||||
IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mc0\n"));
|
||||
//IF_VERBOSE(0, m_solver.display(verbose_stream()));
|
||||
IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n";);
|
||||
IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n");
|
||||
}
|
||||
else {
|
||||
IF_VERBOSE(0, verbose_stream() << "solution verified\n");
|
||||
// IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mcs\n"));
|
||||
// IF_VERBOSE(0, if (m_sat_mc) m_sat_mc->display(verbose_stream() << "sat_mc\n"));
|
||||
// IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
|
||||
}
|
||||
|
||||
#endif
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -31,10 +31,15 @@ template<bool TO_BOOL>
|
|||
struct bit_blaster_model_converter : public model_converter {
|
||||
func_decl_ref_vector m_vars;
|
||||
expr_ref_vector m_bits;
|
||||
func_decl_ref_vector m_newbits;
|
||||
|
||||
ast_manager & m() const { return m_vars.get_manager(); }
|
||||
|
||||
bit_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits):m_vars(m), m_bits(m) {
|
||||
bit_blaster_model_converter(
|
||||
ast_manager & m,
|
||||
obj_map<func_decl, expr*> const & const2bits,
|
||||
ptr_vector<func_decl> const& newbits):
|
||||
m_vars(m), m_bits(m), m_newbits(m) {
|
||||
for (auto const& kv : const2bits) {
|
||||
func_decl * v = kv.m_key;
|
||||
expr * bits = kv.m_value;
|
||||
|
@ -43,6 +48,8 @@ struct bit_blaster_model_converter : public model_converter {
|
|||
m_vars.push_back(v);
|
||||
m_bits.push_back(bits);
|
||||
}
|
||||
for (func_decl* f : newbits)
|
||||
m_newbits.push_back(f);
|
||||
}
|
||||
|
||||
virtual ~bit_blaster_model_converter() {
|
||||
|
@ -200,10 +207,11 @@ struct bit_blaster_model_converter : public model_converter {
|
|||
}
|
||||
|
||||
void display(std::ostream & out) override {
|
||||
for (func_decl * f : m_newbits)
|
||||
display_del(out, f);
|
||||
unsigned sz = m_vars.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
for (unsigned i = 0; i < sz; i++)
|
||||
display_add(out, m(), m_vars.get(i), m_bits.get(i));
|
||||
}
|
||||
}
|
||||
|
||||
void get_units(obj_map<expr, bool>& units) override {
|
||||
|
@ -211,7 +219,7 @@ struct bit_blaster_model_converter : public model_converter {
|
|||
}
|
||||
|
||||
protected:
|
||||
bit_blaster_model_converter(ast_manager & m):m_vars(m), m_bits(m) { }
|
||||
bit_blaster_model_converter(ast_manager & m):m_vars(m), m_bits(m), m_newbits(m) { }
|
||||
public:
|
||||
|
||||
model_converter * translate(ast_translation & translator) override {
|
||||
|
@ -220,16 +228,18 @@ public:
|
|||
res->m_vars.push_back(translator(v));
|
||||
for (expr* b : m_bits)
|
||||
res->m_bits.push_back(translator(b));
|
||||
for (func_decl* f : m_newbits)
|
||||
res->m_newbits.push_back(translator(f));
|
||||
return res;
|
||||
}
|
||||
};
|
||||
|
||||
model_converter * mk_bit_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits) {
|
||||
return const2bits.empty() ? nullptr : alloc(bit_blaster_model_converter<true>, m, const2bits);
|
||||
model_converter * mk_bit_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits, ptr_vector<func_decl> const& newbits) {
|
||||
return const2bits.empty() ? nullptr : alloc(bit_blaster_model_converter<true>, m, const2bits, newbits);
|
||||
}
|
||||
|
||||
model_converter * mk_bv1_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits) {
|
||||
return const2bits.empty() ? nullptr : alloc(bit_blaster_model_converter<false>, m, const2bits);
|
||||
model_converter * mk_bv1_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits, ptr_vector<func_decl> const& newbits) {
|
||||
return const2bits.empty() ? nullptr : alloc(bit_blaster_model_converter<false>, m, const2bits, newbits);
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -21,7 +21,7 @@ Notes:
|
|||
|
||||
#include "tactic/model_converter.h"
|
||||
|
||||
model_converter * mk_bit_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits);
|
||||
model_converter * mk_bv1_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits);
|
||||
model_converter * mk_bit_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits, ptr_vector<func_decl> const& newbits);
|
||||
model_converter * mk_bv1_blaster_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bits, ptr_vector<func_decl> const& newbits);
|
||||
|
||||
#endif
|
||||
|
|
|
@ -86,8 +86,9 @@ class bit_blaster_tactic : public tactic {
|
|||
|
||||
if (change && g->models_enabled()) {
|
||||
obj_map<func_decl, expr*> const2bits;
|
||||
m_rewriter->end_rewrite(const2bits);
|
||||
g->add(mk_bit_blaster_model_converter(m(), const2bits));
|
||||
ptr_vector<func_decl> newbits;
|
||||
m_rewriter->end_rewrite(const2bits, newbits);
|
||||
g->add(mk_bit_blaster_model_converter(m(), const2bits, newbits));
|
||||
}
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
|
|
|
@ -36,6 +36,7 @@ class bv1_blaster_tactic : public tactic {
|
|||
ast_manager & m_manager;
|
||||
bv_util m_util;
|
||||
obj_map<func_decl, expr*> m_const2bits;
|
||||
ptr_vector<func_decl> m_newbits;
|
||||
expr_ref_vector m_saved;
|
||||
expr_ref m_bit1;
|
||||
expr_ref m_bit0;
|
||||
|
@ -107,6 +108,7 @@ class bv1_blaster_tactic : public tactic {
|
|||
ptr_buffer<expr> bits;
|
||||
for (unsigned i = 0; i < bv_size; i++) {
|
||||
bits.push_back(m().mk_fresh_const(0, b));
|
||||
m_newbits.push_back(to_app(bits.back())->get_decl());
|
||||
}
|
||||
r = butil().mk_concat(bits.size(), bits.c_ptr());
|
||||
m_saved.push_back(r);
|
||||
|
@ -405,7 +407,7 @@ class bv1_blaster_tactic : public tactic {
|
|||
}
|
||||
|
||||
if (g->models_enabled())
|
||||
g->add(mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits));
|
||||
g->add(mk_bv1_blaster_model_converter(m(), m_rw.cfg().m_const2bits, m_rw.cfg().m_newbits));
|
||||
g->inc_depth();
|
||||
result.push_back(g.get());
|
||||
m_rw.cfg().cleanup();
|
||||
|
|
|
@ -23,6 +23,7 @@ Revision History:
|
|||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/expr_substitution.h"
|
||||
#include "tactic/goal_shared_occs.h"
|
||||
#include "ast/pb_decl_plugin.h"
|
||||
|
||||
class propagate_values_tactic : public tactic {
|
||||
struct imp {
|
||||
|
@ -129,10 +130,23 @@ class propagate_values_tactic : public tactic {
|
|||
}
|
||||
|
||||
TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
|
||||
push_result(new_curr, new_pr);
|
||||
|
||||
if (new_curr != curr)
|
||||
if (new_curr != curr) {
|
||||
m_modified = true;
|
||||
//if (has_pb(curr))
|
||||
// IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n");
|
||||
}
|
||||
push_result(new_curr, new_pr);
|
||||
}
|
||||
|
||||
bool has_pb(expr* e) {
|
||||
pb_util pb(m);
|
||||
if (pb.is_ge(e)) return true;
|
||||
if (m.is_or(e)) {
|
||||
for (expr* a : *to_app(e)) {
|
||||
if (pb.is_ge(a)) return true;
|
||||
}
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void operator()(goal_ref const & g,
|
||||
|
@ -206,6 +220,7 @@ class propagate_values_tactic : public tactic {
|
|||
SASSERT(m_goal->is_well_sorted());
|
||||
TRACE("propagate_values", tout << "end\n"; m_goal->display(tout););
|
||||
TRACE("propagate_values_core", m_goal->display_with_dependencies(tout););
|
||||
//IF_VERBOSE(0, m_goal->display(verbose_stream()));
|
||||
m_goal = 0;
|
||||
}
|
||||
};
|
||||
|
|
|
@ -23,6 +23,7 @@ Revision History:
|
|||
#include "util/cooperate.h"
|
||||
#include "tactic/goal_shared_occs.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/pb_decl_plugin.h"
|
||||
|
||||
class solve_eqs_tactic : public tactic {
|
||||
struct imp {
|
||||
|
@ -347,10 +348,8 @@ class solve_eqs_tactic : public tactic {
|
|||
|
||||
TRACE("solve_eqs",
|
||||
tout << "candidate vars:\n";
|
||||
ptr_vector<app>::iterator it = m_vars.begin();
|
||||
ptr_vector<app>::iterator end = m_vars.end();
|
||||
for (; it != end; ++it) {
|
||||
tout << mk_ismt2_pp(*it, m()) << " ";
|
||||
for (app* v : m_vars) {
|
||||
tout << mk_ismt2_pp(v, m()) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
}
|
||||
|
@ -492,11 +491,9 @@ class solve_eqs_tactic : public tactic {
|
|||
|
||||
TRACE("solve_eqs",
|
||||
tout << "ordered vars:\n";
|
||||
ptr_vector<app>::iterator it = m_ordered_vars.begin();
|
||||
ptr_vector<app>::iterator end = m_ordered_vars.end();
|
||||
for (; it != end; ++it) {
|
||||
SASSERT(m_candidate_vars.is_marked(*it));
|
||||
tout << mk_ismt2_pp(*it, m()) << " ";
|
||||
for (app* v : m_ordered_vars) {
|
||||
SASSERT(m_candidate_vars.is_marked(v));
|
||||
tout << mk_ismt2_pp(v, m()) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
m_candidate_vars.reset();
|
||||
|
@ -529,8 +526,7 @@ class solve_eqs_tactic : public tactic {
|
|||
m_subst->reset();
|
||||
TRACE("solve_eqs",
|
||||
tout << "after normalizing variables\n";
|
||||
for (unsigned i = 0; i < m_ordered_vars.size(); i++) {
|
||||
expr * v = m_ordered_vars[i];
|
||||
for (expr * v : m_ordered_vars) {
|
||||
expr * def = 0;
|
||||
proof * pr = 0;
|
||||
expr_dependency * dep = 0;
|
||||
|
@ -539,16 +535,15 @@ class solve_eqs_tactic : public tactic {
|
|||
});
|
||||
#if 0
|
||||
DEBUG_CODE({
|
||||
for (unsigned i = 0; i < m_ordered_vars.size(); i++) {
|
||||
expr * v = m_ordered_vars[i];
|
||||
expr * def = 0;
|
||||
proof * pr = 0;
|
||||
expr_dependency * dep = 0;
|
||||
m_norm_subst->find(v, def, pr, dep);
|
||||
SASSERT(def != 0);
|
||||
CASSERT("solve_eqs_bug", !occurs(v, def));
|
||||
}
|
||||
});
|
||||
for (expr * v : m_ordered_vars) {
|
||||
expr * def = 0;
|
||||
proof * pr = 0;
|
||||
expr_dependency * dep = 0;
|
||||
m_norm_subst->find(v, def, pr, dep);
|
||||
SASSERT(def != 0);
|
||||
CASSERT("solve_eqs_bug", !occurs(v, def));
|
||||
}
|
||||
});
|
||||
#endif
|
||||
}
|
||||
|
||||
|
@ -575,6 +570,13 @@ class solve_eqs_tactic : public tactic {
|
|||
}
|
||||
|
||||
m_r->operator()(f, new_f, new_pr, new_dep);
|
||||
#if 0
|
||||
pb_util pb(m());
|
||||
if (pb.is_ge(f) && f != new_f) {
|
||||
IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n");
|
||||
}
|
||||
#endif
|
||||
|
||||
TRACE("solve_eqs_subst", tout << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n";);
|
||||
m_num_steps += m_r->get_num_steps() + 1;
|
||||
if (m_produce_proofs)
|
||||
|
@ -592,12 +594,11 @@ class solve_eqs_tactic : public tactic {
|
|||
g.display(tout););
|
||||
#if 0
|
||||
DEBUG_CODE({
|
||||
for (unsigned i = 0; i < m_ordered_vars.size(); i++) {
|
||||
expr * v = m_ordered_vars[i];
|
||||
for (unsigned j = 0; j < g.size(); j++) {
|
||||
CASSERT("solve_eqs_bug", !occurs(v, g.form(j)));
|
||||
}
|
||||
}});
|
||||
for (expr* v : m_ordered_vars) {
|
||||
for (unsigned j = 0; j < g.size(); j++) {
|
||||
CASSERT("solve_eqs_bug", !occurs(v, g.form(j)));
|
||||
}
|
||||
}});
|
||||
#endif
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue