mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

move to get_sort as method, add opt_lns pass, disable xor simplification unless configured, fix perf bug in model converter update trail

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-02 03:58:19 -08:00
parent c623e2db28
commit 4455f6caf8
36 changed files with 391 additions and 90 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/arith_decl_plugin.h
View file

@ -297,11 +297,11 @@ public:
bool is_power0(expr const * n) const { return is_app_of(n, m_afid, OP_POWER0); }
bool is_int(sort const * s) const { return is_sort_of(s, m_afid, INT_SORT); }
bool is_int(expr const * n) const { return is_int(get_sort(n)); }
bool is_int(expr const * n) const { return is_int(n->get_sort()); }
bool is_real(sort const * s) const { return is_sort_of(s, m_afid, REAL_SORT); }
bool is_real(expr const * n) const { return is_real(get_sort(n)); }
bool is_real(expr const * n) const { return is_real(n->get_sort()); }
bool is_int_real(sort const * s) const { return s->get_family_id() == m_afid; }
bool is_int_real(expr const * n) const { return is_int_real(get_sort(n)); }
bool is_int_real(expr const * n) const { return is_int_real(n->get_sort()); }
bool is_sin(expr const* n) const { return is_app_of(n, m_afid, OP_SIN); }
bool is_cos(expr const* n) const { return is_app_of(n, m_afid, OP_COS); }

2
src/ast/array_decl_plugin.h
View file

@ -144,7 +144,7 @@ public:
array_recognizers(family_id fid):m_fid(fid) {}
family_id get_family_id() const { return m_fid; }
bool is_array(sort* s) const { return is_sort_of(s, m_fid, ARRAY_SORT);}
bool is_array(expr* n) const { return is_array(get_sort(n)); }
bool is_array(expr* n) const { return is_array(n->get_sort()); }
bool is_select(expr* n) const { return is_app_of(n, m_fid, OP_SELECT); }
bool is_store(expr* n) const { return is_app_of(n, m_fid, OP_STORE); }
bool is_const(expr* n) const { return is_app_of(n, m_fid, OP_CONST_ARRAY); }

14
src/ast/ast.cpp
View file

@ -420,14 +420,14 @@ quantifier::quantifier(unsigned num_decls, sort * const * decl_sorts, symbol con
//
// -----------------------------------
sort * get_sort(expr const * n) {
switch(n->get_kind()) {
sort* expr::get_sort() const {
switch (get_kind()) {
case AST_APP:
return to_app(n)->get_decl()->get_range();
return to_app(this)->get_decl()->get_range();
case AST_VAR:
return to_var(n)->get_sort();
return to_var(this)->_get_sort();
case AST_QUANTIFIER:
return to_quantifier(n)->get_sort();
return to_quantifier(this)->_get_sort();
default:
UNREACHABLE();
return nullptr;
@ -2513,7 +2513,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
sort* s = nullptr;
if (k == lambda_k) {
array_util autil(*this);
s = autil.mk_array_sort(num_decls, decl_sorts, ::get_sort(body));
s = autil.mk_array_sort(num_decls, decl_sorts, body->get_sort());
}
else {
s = mk_bool_sort();
@ -2541,7 +2541,7 @@ quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sort
unsigned sz = quantifier::get_obj_size(num_decls, 0, 0);
void * mem = allocate_node(sz);
array_util autil(*this);
sort* s = autil.mk_array_sort(num_decls, decl_sorts, ::get_sort(body));
sort* s = autil.mk_array_sort(num_decls, decl_sorts, body->get_sort());
quantifier * new_node = new (mem) quantifier(num_decls, decl_sorts, decl_names, body, s);
quantifier * r = register_node(new_node);
if (m_trace_stream && r == new_node) {

12
src/ast/ast.h
View file

@ -668,6 +668,8 @@ protected:
expr(ast_kind k):ast(k) {}
public:
sort* get_sort() const;
};
// -----------------------------------
@ -719,6 +721,7 @@ public:
unsigned get_size() const { return get_obj_size(get_num_args()); }
expr * const * begin() const { return m_args; }
expr * const * end() const { return m_args + m_num_args; }
sort * _get_sort() const { return get_decl()->get_range(); }
unsigned get_depth() const { return flags()->m_depth; }
bool is_ground() const { return flags()->m_ground; }
@ -807,7 +810,7 @@ class var : public expr {
var(unsigned idx, sort * s):expr(AST_VAR), m_idx(idx), m_sort(s) {}
public:
unsigned get_idx() const { return m_idx; }
sort * get_sort() const { return m_sort; }
sort * _get_sort() const { return m_sort; }
unsigned get_size() const { return get_obj_size(); }
};
@ -863,7 +866,7 @@ public:
symbol const & get_decl_name(unsigned idx) const { return get_decl_names()[idx]; }
expr * get_expr() const { return m_expr; }
sort * get_sort() const { return m_sort; }
sort * _get_sort() const { return m_sort; }
unsigned get_depth() const { return m_depth; }
@ -1391,14 +1394,13 @@ inline bool has_labels(expr const * n) {
else return false;
}
sort * get_sort(expr const * n);
class basic_recognizers {
family_id m_fid;
public:
basic_recognizers(family_id fid):m_fid(fid) {}
bool is_bool(sort const * s) const { return is_sort_of(s, m_fid, BOOL_SORT); }
bool is_bool(expr const * n) const { return is_bool(get_sort(n)); }
bool is_bool(expr const * n) const { return is_bool(n->get_sort()); }
bool is_or(expr const * n) const { return is_app_of(n, m_fid, OP_OR); }
bool is_implies(expr const * n) const { return is_app_of(n, m_fid, OP_IMPLIES); }
bool is_and(expr const * n) const { return is_app_of(n, m_fid, OP_AND); }
@ -1733,7 +1735,7 @@ protected:
}
public:
sort * get_sort(expr const * n) const { return ::get_sort(n); }
sort * get_sort(expr const * n) const { return n->get_sort(); }
void check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const;
void check_sorts_core(ast const * n) const;
bool check_sorts(ast const * n) const;

2
src/ast/bv_decl_plugin.h
View file

@ -300,7 +300,7 @@ public:
bool is_zero(expr const * e) const;
bool is_one(expr const* e) const;
bool is_bv_sort(sort const * s) const;
bool is_bv(expr const* e) const { return is_bv_sort(get_sort(e)); }
bool is_bv(expr const* e) const { return is_bv_sort(e->get_sort()); }
bool is_concat(expr const * e) const { return is_app_of(e, get_fid(), OP_CONCAT); }
bool is_extract(func_decl const * f) const { return is_decl_of(f, get_fid(), OP_EXTRACT); }

65
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -43,6 +43,8 @@ struct enum2bv_rewriter::imp {
ast_manager& m;
datatype_util m_dt;
bv_util m_bv;
bool m_enable_unate { false };
unsigned m_unate_bound { 30 };
rw_cfg(imp& i, ast_manager & m) :
m_imp(i),
@ -51,6 +53,38 @@ struct enum2bv_rewriter::imp {
m_bv(m)
{}
bool is_unate(sort* s) {
if (!m_enable_unate)
return false;
unsigned nc = m_dt.get_datatype_num_constructors(s);
return 1 < nc && nc <= m_unate_bound;
}
expr* value2bv(unsigned idx, sort* s) {
unsigned bv_size = get_bv_size(s);
sort_ref bv_sort(m_bv.mk_sort(bv_size), m);
if (is_unate(s))
return m_bv.mk_numeral(rational((1 << idx) - 1), bv_sort);
else
return m_bv.mk_numeral(rational(idx), bv_sort);
}
void constrain_domain(expr* x, sort* s, sort* bv_sort) {
unsigned domain_size = m_dt.get_datatype_num_constructors(s);
if (is_unate(s)) {
expr_ref one(m_bv.mk_numeral(rational::one(), 1), m);
for (unsigned i = 0; i + 2 < domain_size; ++i) {
m_imp.m_bounds.push_back(m.mk_implies(m.mk_eq(one, m_bv.mk_extract(i + 1, i + 1, x)),
m.mk_eq(one, m_bv.mk_extract(i, i, x))));
}
}
else {
if (!is_power_of_two(domain_size) || domain_size == 1) {
m_imp.m_bounds.push_back(m_bv.mk_ule(x, value2bv(domain_size - 1, s)));
}
}
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
expr_ref a0(m), a1(m);
expr_ref_vector _args(m);
@ -65,7 +99,7 @@ struct enum2bv_rewriter::imp {
}
else if (m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) {
unsigned idx = m_dt.get_recognizer_constructor_idx(f);
a1 = m_bv.mk_numeral(rational(idx), get_sort(a0));
a1 = value2bv(idx, a0->get_sort());
result = m.mk_eq(a0, a1);
return BR_DONE;
}
@ -92,7 +126,7 @@ struct enum2bv_rewriter::imp {
void check_for_fd(unsigned n, expr* const* args) {
for (unsigned i = 0; i < n; ++i) {
if (m_imp.is_fd(get_sort(args[i]))) {
if (m_imp.is_fd(args[i]->get_sort())) {
throw_non_fd(args[i]);
}
}
@ -100,11 +134,12 @@ struct enum2bv_rewriter::imp {
bool reduce_arg(expr* a, expr_ref& result) {
sort* s = get_sort(a);
sort* s = a->get_sort();
if (!m_imp.is_fd(s)) {
return false;
}
unsigned bv_size = get_bv_size(s);
sort_ref bv_sort(m_bv.mk_sort(bv_size), m);
if (is_var(a)) {
result = m.mk_var(to_var(a)->get_idx(), m_bv.mk_sort(bv_size));
@ -114,7 +149,7 @@ struct enum2bv_rewriter::imp {
func_decl* f = to_app(a)->get_decl();
if (m_dt.is_constructor(f)) {
unsigned idx = m_dt.get_constructor_idx(f);
result = m_bv.mk_numeral(idx, bv_size);
result = value2bv(idx, s);
}
else if (is_uninterp_const(a)) {
func_decl* f_fresh;
@ -125,17 +160,14 @@ struct enum2bv_rewriter::imp {
// create a fresh variable, add bounds constraints for it.
unsigned nc = m_dt.get_datatype_num_constructors(s);
result = m.mk_fresh_const(f->get_name(), m_bv.mk_sort(bv_size));
result = m.mk_fresh_const(f->get_name(), bv_sort);
f_fresh = to_app(result)->get_decl();
if (!is_power_of_two(nc) || nc == 1) {
m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size)));
}
constrain_domain(result, s, bv_sort);
expr_ref f_def(m);
ptr_vector<func_decl> const& cs = *m_dt.get_datatype_constructors(s);
f_def = m.mk_const(cs[nc-1]);
for (unsigned i = nc - 1; i > 0; ) {
--i;
f_def = m.mk_ite(m.mk_eq(result, m_bv.mk_numeral(i,bv_size)), m.mk_const(cs[i]), f_def);
for (unsigned i = nc - 1; i-- > 0; ) {
f_def = m.mk_ite(m.mk_eq(result, value2bv(i, s)), m.mk_const(cs[i]), f_def);
}
m_imp.m_enum2def.insert(f, f_def);
m_imp.m_enum2bv.insert(f, f_fresh);
@ -169,11 +201,10 @@ struct enum2bv_rewriter::imp {
sort* s = q->get_decl_sort(i);
if (m_imp.is_fd(s)) {
unsigned bv_size = get_bv_size(s);
m_sorts.push_back(m_bv.mk_sort(bv_size));
unsigned nc = m_dt.get_datatype_num_constructors(s);
if (!is_power_of_two(nc) || nc == 1) {
bounds.push_back(m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_bv.mk_numeral(nc-1, bv_size)));
}
sort* bv_sort = m_bv.mk_sort(bv_size);
m_sorts.push_back(bv_sort);
expr_ref var(m.mk_var(q->get_num_decls()-i-1, bv_sort), m);
constrain_domain(var, s, bv_sort);
found = true;
}
else {
@ -209,6 +240,8 @@ struct enum2bv_rewriter::imp {
unsigned get_bv_size(sort* s) {
unsigned nc = m_dt.get_datatype_num_constructors(s);
if (is_unate(s))
return nc - 1;
unsigned bv_size = 1;
while ((unsigned)(1 << bv_size) < nc) {
++bv_size;

2
src/ast/seq_decl_plugin.cpp
View file

@ -874,7 +874,7 @@ void seq_util::str::get_concat_units(expr* e, expr_ref_vector& es) const {
}
app* seq_util::str::mk_is_empty(expr* s) const {
return m.mk_eq(s, mk_empty(get_sort(s)));
return m.mk_eq(s, mk_empty(s->get_sort()));
}

13
src/ast/seq_decl_plugin.h
View file

@ -229,11 +229,11 @@ public:
bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
bool is_re(sort* s, sort*& seq) const { return is_sort_of(s, m_fid, RE_SORT) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_seq(expr* e) const { return is_seq(m.get_sort(e)); }
bool is_seq(expr* e) const { return is_seq(e->get_sort()); }
bool is_seq(sort* s, sort*& seq) const { return is_seq(s) && (seq = to_sort(s->get_parameter(0).get_ast()), true); }
bool is_re(expr* e) const { return is_re(m.get_sort(e)); }
bool is_re(expr* e, sort*& seq) const { return is_re(m.get_sort(e), seq); }
bool is_char(expr* e) const { return is_char(m.get_sort(e)); }
bool is_re(expr* e) const { return is_re(e->get_sort()); }
bool is_re(expr* e, sort*& seq) const { return is_re(e->get_sort(), seq); }
bool is_char(expr* e) const { return is_char(e->get_sort()); }
bool is_const_char(expr* e, unsigned& c) const;
bool is_const_char(expr* e) const { unsigned c; return is_const_char(e, c); }
bool is_char_le(expr const* e) const;
@ -344,12 +344,11 @@ public:
bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_FROM_CODE); }
bool is_string_term(expr const * n) const {
sort * s = get_sort(n);
return u.is_string(s);
return u.is_string(n->get_sort());
}
bool is_non_string_sequence(expr const * n) const {
sort * s = get_sort(n);
sort * s = n->get_sort();
return (u.is_seq(s) && !u.is_string(s));
}

2
src/muz/spacer/spacer_antiunify.cpp
View file

@ -132,7 +132,7 @@ void anti_unifier::operator()(expr *e1, expr *e2, expr_ref &res,
unsigned num_arg2 = n2->get_num_args();
if (n1->get_decl() != n2->get_decl() || num_arg1 != num_arg2) {
expr_ref v(m);
v = m.mk_var(m_subs.size(), get_sort(n1));
v = m.mk_var(m_subs.size(), n1->get_sort());
m_pinned.push_back(v);
m_subs.push_back(expr_pair(n1, n2));
m_cache.insert(n1, n2, v);

6
src/muz/spacer/spacer_context.cpp
View file

@ -119,7 +119,7 @@ void pob::get_skolems(app_ref_vector &v) {
for (unsigned i = 0, sz = m_binding.size(); i < sz; ++i) {
expr* e;
e = m_binding.get(i);
v.push_back (mk_zk_const (get_ast_manager(), i, get_sort(e)));
v.push_back (mk_zk_const (get_ast_manager(), i, e->get_sort()));
}
}
@ -237,7 +237,7 @@ void derivation::exist_skolemize(expr* fml, app_ref_vector& vars, expr_ref& res)
expr_safe_replace sub(m);
for (unsigned i = 0, sz = vars.size(); i < sz; ++i) {
expr* e = vars.get(i);
sub.insert(e, mk_zk_const(m, i, get_sort(e)));
sub.insert(e, mk_zk_const(m, i, e->get_sort()));
}
sub(fml, res);
}
@ -541,7 +541,7 @@ void lemma::mk_expr_core() {
ptr_buffer<sort> sorts;
svector<symbol> names;
for (app* z : zks) {
sorts.push_back(get_sort(z));
sorts.push_back(z->get_sort());
names.push_back(z->get_decl()->get_name());
}
m_body = m.mk_quantifier(forall_k, zks.size(),

4
src/muz/spacer/spacer_generalizers.cpp
View file

@ -195,8 +195,8 @@ public:
void operator()(app* a)
{
if (a->get_family_id() == null_family_id && m_au.is_array(a)) {
if (m_sort && m_sort != get_sort(a)) { return; }
if (!m_sort) { m_sort = get_sort(a); }
if (m_sort && m_sort != a->get_sort()) { return; }
if (!m_sort) { m_sort = a->get_sort(); }
m_symbs.insert(a->get_decl());
}
}

2
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -230,7 +230,7 @@ namespace spacer {
if (a.is_numeral(e)) return false;
if (!var || var == e) {
var = e;
val = a.mk_numeral(rational(1), get_sort(e));
val = a.mk_numeral(rational(1), e->get_sort());
return true;
}
return false;

4
src/muz/spacer/spacer_quant_generalizer.cpp
View file

@ -226,7 +226,7 @@ expr* times_minus_one(expr *e, arith_util &arith) {
expr *r;
if (arith.is_times_minus_one (e, r)) { return r; }
return arith.mk_mul(arith.mk_numeral(rational(-1), arith.is_int(get_sort(e))), e);
return arith.mk_mul(arith.mk_numeral(rational(-1), arith.is_int(e->get_sort())), e);
}
}
@ -502,7 +502,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) {
expr_ref_vector abs_cube(m);
var_ref var(m);
var = m.mk_var (m_offset, get_sort(term));
var = m.mk_var (m_offset, term->get_sort());
mk_abs_cube(lemma, term, var, gnd_cube, abs_cube, lb, ub, stride);
if (abs_cube.empty()) {return false;}

2
src/muz/transforms/dl_mk_array_eq_rewrite.cpp
View file

@ -65,7 +65,7 @@ namespace datalog {
for(unsigned i = nb_predicates; i < tail_size; i++) {
expr* cond = r.get_tail(i);
expr* e1, *e2;
if (m.is_eq(cond, e1, e2) && m_a.is_array(get_sort(e1))) {
if (m.is_eq(cond, e1, e2) && m_a.is_array(e1->get_sort())) {
array_eq_classes.merge(e1, e2);
}
else {

20
src/muz/transforms/dl_mk_array_instantiation.cpp
View file

@ -103,12 +103,12 @@ namespace datalog {
expr_ref_vector new_args(m);
for(unsigned i=0;i<old_head->get_num_args();i++) {
expr*arg = old_head->get_arg(i);
if(m_a.is_array(get_sort(arg))) {
if(m_a.is_array(arg->get_sort())) {
for(unsigned k=0; k< m_ctx.get_params().xform_instantiate_arrays_nb_quantifier();k++) {
expr_ref_vector dummy_args(m);
dummy_args.push_back(arg);
for(unsigned i=0;i<get_array_arity(get_sort(arg));i++) {
dummy_args.push_back(m.mk_var(cnt, get_array_domain(get_sort(arg), i)));
for(unsigned i=0;i<get_array_arity(arg->get_sort());i++) {
dummy_args.push_back(m.mk_var(cnt, get_array_domain(arg->get_sort(), i)));
cnt++;
}
expr_ref select(m);
@ -140,7 +140,7 @@ namespace datalog {
}
//If it is a select, then add it to selects
if(m_a.is_select(f)) {
SASSERT(!m_a.is_array(get_sort(e)));
SASSERT(!m_a.is_array(e->get_sort()));
selects.insert_if_not_there(f->get_arg(0), ptr_vector<expr>());
selects[f->get_arg(0)].push_back(e);
}
@ -148,7 +148,7 @@ namespace datalog {
if(m_a.is_store(f)) {
eq_classes.merge(e, f->get_arg(0));
}
else if(m.is_eq(f) && m_a.is_array(get_sort(f->get_arg(0)))) {
else if(m.is_eq(f) && m_a.is_array(f->get_arg(0)->get_sort())) {
eq_classes.merge(f->get_arg(0), f->get_arg(1));
}
}
@ -180,7 +180,7 @@ namespace datalog {
}
sort_ref_vector new_sorts(m);
for(unsigned i=0;i<new_args.size();i++)
new_sorts.push_back(get_sort(new_args[i].get()));
new_sorts.push_back(new_args.get(i)->get_sort());
expr_ref res(m);
func_decl_ref fun_decl(m);
fun_decl = m.mk_func_decl(symbol((old_pred->get_decl()->get_name().str()+"!inst").c_str()), new_sorts.size(), new_sorts.c_ptr(), old_pred->get_decl()->get_range());
@ -196,7 +196,7 @@ namespace datalog {
var*result;
if(!done_selects.find(select, result)) {
ownership.push_back(select);
result = m.mk_var(cnt, get_sort(select));
result = m.mk_var(cnt, select->get_sort());
cnt++;
done_selects.insert(select, result);
}
@ -230,8 +230,8 @@ namespace datalog {
if(all_selects.empty()) {
expr_ref_vector dummy_args(m);
dummy_args.push_back(array);
for(unsigned i=0;i<get_array_arity(get_sort(array));i++) {
dummy_args.push_back(m.mk_var(cnt, get_array_domain(get_sort(array), i)));
for(unsigned i=0;i<get_array_arity(array->get_sort());i++) {
dummy_args.push_back(m.mk_var(cnt, get_array_domain(array->get_sort(), i)));
cnt++;
}
all_selects.push_back(m_a.mk_select(dummy_args.size(), dummy_args.c_ptr()));
@ -247,7 +247,7 @@ namespace datalog {
vector<expr_ref_vector> arg_correspondance;
for(unsigned i=0;i<nb_old_args;i++) {
expr_ref arg(old_pred->get_arg(i), m);
if(m_a.is_array(get_sort(arg))) {
if(m_a.is_array(arg->get_sort())) {
vector<expr_ref_vector> arg_possibilities(m_ctx.get_params().xform_instantiate_arrays_nb_quantifier(), retrieve_all_selects(arg));
arg_correspondance.append(arg_possibilities);
if(!m_ctx.get_params().xform_instantiate_arrays_enforce()) {

1
src/opt/CMakeLists.txt
View file

@ -5,6 +5,7 @@ z3_add_component(opt
maxsmt.cpp
opt_cmds.cpp
opt_context.cpp
opt_lns.cpp
opt_pareto.cpp
opt_parse.cpp
optsmt.cpp

30
src/opt/maxres.cpp
View file

@ -62,6 +62,7 @@ Notes:
#include "smt/smt_solver.h"
#include "opt/opt_context.h"
#include "opt/opt_params.hpp"
#include "opt/opt_lns.h"
#include "opt/maxsmt.h"
#include "opt/maxres.h"
@ -107,9 +108,9 @@ private:
// this option is disabled if SAT core is used.
bool m_pivot_on_cs; // prefer smaller correction set to core.
bool m_dump_benchmarks; // display benchmarks (into wcnf format)
bool m_enable_lns { false }; // enable LNS improvements
unsigned m_lns_conflicts { 1000 }; // number of conflicts used for LNS improvement
std::string m_trace_id;
typedef ptr_vector<expr> exprs;
@ -201,6 +202,7 @@ public:
if (!init()) return l_undef;
is_sat = init_local();
trace();
improve_model();
if (is_sat != l_true) return is_sat;
while (m_lower < m_upper) {
TRACE("opt_verbose",
@ -730,7 +732,29 @@ public:
add(fml);
}
void improve_model() {
if (!m_enable_lns)
return;
model_ref mdl;
s().get_model(mdl);
if (mdl)
update_assignment(mdl);
}
void improve_model(model_ref& mdl) {
if (!m_enable_lns)
return;
flet<bool> _disable_lns(m_enable_lns, false);
std::function<void(model_ref&)> update_model = [&](model_ref& mdl) {
update_assignment(mdl);
};
lns lns(s(), update_model);
lns.set_conflicts(m_lns_conflicts);
lns.climb(mdl, m_asms);
}
void update_assignment(model_ref & mdl) {
improve_model(mdl);
mdl->set_model_completion(true);
unsigned correction_set_size = 0;
for (expr* a : m_asms) {
@ -818,6 +842,8 @@ public:
m_pivot_on_cs = p.maxres_pivot_on_correction_set();
m_wmax = p.maxres_wmax();
m_dump_benchmarks = p.dump_benchmarks();
m_enable_lns = p.enable_lns() && m_c.sat_enabled();
m_lns_conflicts = p.lns_conflicts();
}
lbool init_local() {

3
src/opt/maxsmt.h
View file

@ -73,9 +73,6 @@ namespace opt {
rational m_upper;
model_ref m_model;
svector<symbol> m_labels;
//const expr_ref_vector m_soft;
//vector<rational> m_weights;
//bool_vector m_assignment; // truth assignment to soft constraints
params_ref m_params; // config
public:

168
src/opt/opt_lns.cpp Normal file
View file

@ -0,0 +1,168 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
opt_lns.cpp
Abstract:
"large" neighborhood search for maxsat problem instances.
Author:
Nikolaj Bjorner (nbjorner) 2021-02-01
--*/
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "opt/maxsmt.h"
#include "opt/opt_lns.h"
#include "sat/sat_params.hpp"
#include <algorithm>
namespace opt {
lns::lns(solver& s, std::function<void(model_ref& mdl)>& update_model)
: m(s.get_manager()),
s(s),
m_hardened(m),
m_soft(m),
m_update_model(update_model)
{}
void lns::set_lns_params() {
params_ref p;
p.set_sym("phase", symbol("frozen"));
p.set_uint("restart.initial", 1000000);
p.set_uint("max_conflicts", m_max_conflicts);
p.set_uint("simplify.delay", 1000000);
s.updt_params(p);
}
void lns::save_defaults(params_ref& p) {
sat_params sp(p);
p.set_sym("phase", sp.phase());
p.set_uint("restart.initial", sp.restart_initial());
p.set_uint("max_conflicts", sp.max_conflicts());
p.set_uint("simplify.delay", sp.simplify_delay());
}
unsigned lns::climb(model_ref& mdl, expr_ref_vector const& asms) {
m_num_improves = 0;
params_ref old_p(s.get_params());
save_defaults(old_p);
set_lns_params();
setup_assumptions(mdl, asms);
unsigned num_improved = improve_linear(mdl);
// num_improved += improve_rotate(mdl, asms);
s.updt_params(old_p);
IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n");
return num_improved;
}
void lns::setup_assumptions(model_ref& mdl, expr_ref_vector const& asms) {
m_hardened.reset();
m_soft.reset();
for (expr* a : asms) {
if (mdl->is_true(a))
m_hardened.push_back(a);
else
m_soft.push_back(a);
}
}
unsigned lns::improve_rotate(model_ref& mdl, expr_ref_vector const& asms) {
unsigned num_improved = 0;
repeat:
setup_assumptions(mdl, asms);
unsigned sz = m_hardened.size();
for (unsigned i = 0; i < sz; ++i) {
expr_ref tmp(m_hardened.get(i), m);
m_hardened[i] = m.mk_not(tmp);
unsigned reward = improve_linear(mdl);
if (reward > 1) {
num_improved += (reward - 1);
goto repeat;
}
setup_assumptions(mdl, asms);
}
return num_improved;
}
unsigned lns::improve_linear(model_ref& mdl) {
unsigned num_improved = 0;
unsigned max_conflicts = m_max_conflicts;
while (m.inc()) {
unsigned reward = improve_step(mdl);
if (reward == 0)
break;
num_improved += reward;
m_max_conflicts *= 3;
m_max_conflicts /= 2;
set_lns_params();
}
m_max_conflicts = max_conflicts;
return num_improved;
}
unsigned lns::improve_step(model_ref& mdl) {
unsigned num_improved = 0;
for (unsigned i = 0; m.inc() && i < m_soft.size(); ++i) {
switch (improve_step(mdl, soft(i))) {
case l_undef:
break;
case l_false:
TRACE("opt", tout << "pruned " << mk_bounded_pp(soft(i), m) << "\n";);
m_hardened.push_back(m.mk_not(soft(i)));
for (unsigned k = i; k + 1 < m_soft.size(); ++k)
m_soft[k] = soft(k + 1);
m_soft.pop_back();
--i;
break;
case l_true: {
unsigned k = 0, offset = 0;
for (unsigned j = 0; j < m_soft.size(); ++j) {
if (mdl->is_true(soft(j))) {
if (j <= i)
++offset;
++m_num_improves;
TRACE("opt", tout << "improved " << mk_bounded_pp(soft(j), m) << "\n";);
m_hardened.push_back(soft(j));
++num_improved;
}
else {
m_soft[k++] = soft(j);
}
}
m_soft.shrink(k);
i -= offset;
IF_VERBOSE(1, verbose_stream() << "(opt.lns :num-improves " << m_num_improves << " :remaining-soft " << m_soft.size() << ")\n");
m_update_model(mdl);
break;
}
}
}
return num_improved;
}
lbool lns::improve_step(model_ref& mdl, expr* e) {
m_hardened.push_back(e);
lbool r = s.check_sat(m_hardened);
m_hardened.pop_back();
if (r == l_true)
s.get_model(mdl);
#if 0
if (r == l_false) {
expr_ref_vector core(m);
s.get_unsat_core(core);
std::cout << "core size " << core.size() << "\n";
if (core.size() == 4)
std::cout << core << "\n";
}
#endif
return r;
}
};

52
src/opt/opt_lns.h Normal file
View file

@ -0,0 +1,52 @@
/*++
Copyright (c) 2014 Microsoft Corporation
Module Name:
opt_lns.h
Abstract:
"large" neighborhood search for maxsat problem instances.
Start with a model that we assume satisfies at least one of the soft constraint assumptions.
Attempt to improve the model locally by invoking the SAT solver with a phase
fixed to be the assignment that solved the previous instance.
Local improvement is performed by hardening each soft constraint in turn.
The soft constraints are assumed sorted by weight, such that the highest
weight soft constraint is first, followed by soft constraints of lower weight.
Author:
Nikolaj Bjorner (nbjorner) 2021-02-01
--*/
#pragma once
namespace opt {
class lns {
ast_manager& m;
solver& s;
expr_ref_vector m_hardened;
expr_ref_vector m_soft;
unsigned m_max_conflicts { 1000 };
unsigned m_num_improves { 0 };
std::function<void(model_ref& m)> m_update_model;
expr* soft(unsigned i) const { return m_soft[i]; }
void set_lns_params();
void save_defaults(params_ref& p);
unsigned improve_step(model_ref& mdl);
lbool improve_step(model_ref& mdl, expr* e);
unsigned improve_linear(model_ref& mdl);
unsigned improve_rotate(model_ref& mdl, expr_ref_vector const& asms);
void setup_assumptions(model_ref& mdl, expr_ref_vector const& asms);
public:
lns(solver& s, std::function<void(model_ref&)>& update_model);
void set_conflicts(unsigned c) { m_max_conflicts = c; }
unsigned climb(model_ref& mdl, expr_ref_vector const& asms);
};
};

4
src/opt/opt_params.pyg
View file

@ -9,7 +9,9 @@ def_module_params('opt',
('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'),
('enable_lns', BOOL, False, 'enable LNS during weighted maxsat'),
('lns_conflicts', UINT, 1000, 'initial conflict count for LNS search'),
('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
('elim_01', BOOL, True, 'eliminate 01 variables'),
('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),

8
src/qe/mbp/mbp_term_graph.cpp
View file

@ -42,7 +42,7 @@ namespace mbp {
namespace {
struct sort_lt_proc {
bool operator()(const expr* a, const expr *b) const {
return get_sort(a)->get_id() < get_sort(b)->get_id();
return a->get_sort()->get_id() < b->get_sort()->get_id();
}
};
}
@ -266,7 +266,7 @@ namespace mbp {
expr *a = nullptr, *b = nullptr;
// deal with equality using sort of range
if (m.is_eq (lit, a, b)) {
return get_sort (a)->get_family_id();
return a->get_sort()->get_family_id();
}
// extract family_id of top level app
else if (is_app(lit)) {
@ -919,9 +919,9 @@ namespace mbp {
unsigned i = 0;
unsigned sz = reps.size();
while (i < sz) {
sort* last_sort = get_sort(reps.get(i));
sort* last_sort = res.get(i)->get_sort();
unsigned j = i + 1;
while (j < sz && last_sort == get_sort(reps.get(j))) {++j;}
while (j < sz && last_sort == reps.get(j)->get_sort()) {++j;}
if (j - i == 2) {
expr_ref d(m);
d = mk_neq(m, reps.get(i), reps.get(i+1));

4
src/qe/qe_lite.cpp
View file

@ -291,9 +291,9 @@ namespace qel {
if (m.is_eq(e, lhs, rhs) && trivial_solve(lhs, rhs, e, vs, ts)) {
return true;
}
family_id fid = get_sort(e)->get_family_id();
family_id fid = e->get_sort()->get_family_id();
if (m.is_eq(e, lhs, rhs)) {
fid = get_sort(lhs)->get_family_id();
fid = lhs->get_sort()->get_family_id();
}
auto* p = m_solvers.get_plugin(fid);
if (p) {

2
src/sat/sat_big.cpp
View file

@ -198,7 +198,7 @@ namespace sat {
s.m_mc.stackv().reset(); // TBD: brittle code
s.add_ate(~u, v);
if (find_binary_watch(wlist, ~v)) {
IF_VERBOSE(10, verbose_stream() << "binary: " << ~u << "\n");
IF_VERBOSE(20, verbose_stream() << "binary: " << ~u << "\n");
s.assign_unit(~u);
}
// could turn non-learned non-binary tautology into learned binary.

2
src/sat/sat_config.cpp
View file

@ -60,6 +60,8 @@ namespace sat {
m_phase = PS_SAT_CACHING;
else if (s == symbol("random"))
m_phase = PS_RANDOM;
else if (s == symbol("frozen"))
m_phase = PS_FROZEN;
else
throw sat_param_exception("invalid phase selection strategy: always_false, always_true, basic_caching, caching, random");

1
src/sat/sat_config.h
View file

@ -28,6 +28,7 @@ namespace sat {
PS_ALWAYS_FALSE,
PS_BASIC_CACHING,
PS_SAT_CACHING,
PS_FROZEN,
PS_RANDOM
};

3
src/sat/sat_model_converter.cpp
View file

@ -222,7 +222,6 @@ namespace sat {
e.m_clause.append(c.size(), c.begin());
}
void model_converter::insert(entry & e, clause const & c) {
SASSERT(c.contains(e.var()));
SASSERT(m_entries.begin() <= &e);
@ -345,7 +344,7 @@ namespace sat {
void model_converter::flush(model_converter & src) {
VERIFY(this != &src);
m_entries.append(src.m_entries);
m_exposed_lim = src.m_exposed_lim;
m_exposed_lim += src.m_exposed_lim;
src.m_entries.reset();
src.m_exposed_lim = 0;
}

8
src/sat/sat_solver.cpp
View file

@ -1682,6 +1682,9 @@ namespace sat {
case PS_BASIC_CACHING:
phase = m_phase[next];
break;
case PS_FROZEN:
phase = m_best_phase[next];
break;
case PS_SAT_CACHING:
if (m_search_state == s_unsat) {
phase = m_phase[next];
@ -2071,6 +2074,7 @@ namespace sat {
if (!was_eliminated(v)) {
m_model[v] = value(v);
m_phase[v] = value(v) == l_true;
m_best_phase[v] = value(v) == l_true;
}
}
TRACE("sat_mc_bug", m_mc.display(tout););
@ -2847,6 +2851,8 @@ namespace sat {
}
void solver::updt_phase_of_vars() {
if (m_config.m_phase == PS_FROZEN)
return;
unsigned from_lvl = m_conflict_lvl;
unsigned head = from_lvl == 0 ? 0 : m_scopes[from_lvl - 1].m_trail_lim;
unsigned sz = m_trail.size();
@ -2912,6 +2918,8 @@ namespace sat {
case PS_ALWAYS_FALSE:
for (auto& p : m_phase) p = false;
break;
case PS_FROZEN:
break;
case PS_BASIC_CACHING:
switch (m_rephase_lim % 4) {
case 0:

12
src/sat/smt/ba_solver.cpp
View file

@ -1437,6 +1437,10 @@ namespace sat {
bool ba_solver::init_watch(constraint& c) {
if (c.is_xr()) {
std::cout << c.is_xr() << "\n";
}
return !inconsistent() && c.init_watch(*this);
}
@ -2064,8 +2068,10 @@ namespace sat {
for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]);
for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]);
unit_strengthen();
extract_xor();
merge_xor();
if (s().get_config().m_xor_solver) {
extract_xor();
merge_xor();
}
cleanup_clauses();
cleanup_constraints();
update_pure();
@ -2073,6 +2079,8 @@ namespace sat {
}
while (count < 10 && (m_simplify_change || trail_sz < s().init_trail_size()));
gc();
// validate_eliminated();
IF_VERBOSE(1,

3
src/sat/tactic/goal2sat.cpp
View file

@ -72,7 +72,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
expr_ref_vector m_trail;
func_decl_ref_vector m_unhandled_funs;
bool m_default_external;
bool m_xor_solver;
bool m_xor_solver { false };
bool m_euf { false };
bool m_drat { false };
bool m_is_redundant { false };
@ -1020,6 +1020,7 @@ void sat2goal::mc::flush_gmc() {
expr_ref_vector tail(m);
expr_ref def(m);
auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); };
for (unsigned i = 0; i < updates.size(); ++i) {
sat::literal l = updates[i];
if (l == sat::null_literal) {

2
src/smt/smt_model_finder.cpp
View file

@ -1558,7 +1558,7 @@ namespace smt {
// See Section 4.1 in the paper "Complete Quantifier Instantiation"
node* S_q_i = slv.get_uvar(q, m_var_i);
for (enode* n : ctx->enodes()) {
if (ctx->is_relevant(n) && get_sort(n->get_owner()) == s) {
if (ctx->is_relevant(n) && n->get_owner()->get_sort() == s) {
S_q_i->insert(n->get_owner(), n->get_generation());
}
}

12
src/tactic/bv/dt2bv_tactic.cpp
View file

@ -41,7 +41,7 @@ class dt2bv_tactic : public tactic {
obj_hashtable<sort> m_non_fd_sorts;
bool is_fd(expr* a) { return is_fd(get_sort(a)); }
bool is_fd(expr* a) { return is_fd(a->get_sort()); }
bool is_fd(sort* a) { return m_dt.is_enum_sort(a); }
struct check_fd {
@ -59,14 +59,14 @@ class dt2bv_tactic : public tactic {
}
else if (m_t.m_dt.is_recognizer(a->get_decl()) &&
m_t.is_fd(a->get_arg(0))) {
m_t.m_fd_sorts.insert(get_sort(a->get_arg(0)));
m_t.m_fd_sorts.insert(a->get_arg(0)->get_sort());
}
else if (m_t.is_fd(a) && a->get_num_args() > 0) {
m_t.m_non_fd_sorts.insert(get_sort(a));
m_t.m_non_fd_sorts.insert(a->get_sort());
args_cannot_be_fd(a);
}
else if (m_t.is_fd(a)) {
m_t.m_fd_sorts.insert(get_sort(a));
m_t.m_fd_sorts.insert(a->get_sort());
}
else {
args_cannot_be_fd(a);
@ -76,14 +76,14 @@ class dt2bv_tactic : public tactic {
void args_cannot_be_fd(app* a) {
for (expr* arg : *a) {
if (m_t.is_fd(arg)) {
m_t.m_non_fd_sorts.insert(get_sort(arg));
m_t.m_non_fd_sorts.insert(arg->get_sort());
}
}
}
void operator()(var * v) {
if (m_t.is_fd(v)) {
m_t.m_fd_sorts.insert(get_sort(v));
m_t.m_fd_sorts.insert(v->get_sort());
}
}

2
src/tactic/core/reduce_invertible_tactic.cpp
View file

@ -242,7 +242,7 @@ private:
if (mc) {
ensure_mc(mc);
expr_ref num(m_bv.mk_numeral(mdl, get_sort(fst_arg)), m);
expr_ref num(m_bv.mk_numeral(mdl, fst_arg->get_sort()), m);
for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) {
(*mc)->add(a->get_arg(i), num);
}

4
src/tactic/fpa/qffp_tactic.cpp
View file

@ -48,7 +48,7 @@ struct is_non_fp_qfnra_predicate {
if (fid != null_family_id && fid != fu.get_family_id())
throw found();
sort * s = get_sort(n);
sort * s = n->get_sort();
if (fid == fu.get_family_id()) {
if (!fu.is_float(s) && !fu.is_rm(s) &&
to_app(n)->get_decl_kind() != OP_FPA_TO_REAL)
@ -123,7 +123,7 @@ struct is_non_qffp_predicate {
void operator()(quantifier *) { throw found(); }
void operator()(app * n) {
sort * s = get_sort(n);
sort * s = n->get_sort();
if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s))
throw found();
family_id fid = n->get_family_id();

2
src/tactic/fpa/qffplra_tactic.cpp
View file

@ -57,7 +57,7 @@ struct is_non_qffplra_predicate {
void operator()(quantifier *) { throw found(); }
void operator()(app * n) {
sort * s = get_sort(n);
sort * s = n->get_sort();
if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s))
throw found();
family_id fid = n->get_family_id();

2
src/tactic/generic_model_converter.cpp
View file

@ -18,6 +18,7 @@ Notes:
--*/
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/for_each_expr.h"
#include "ast/ast_util.h"
#include "ast/occurs.h"
@ -31,6 +32,7 @@ Notes:
generic_model_converter::~generic_model_converter() {
}
void generic_model_converter::add(func_decl * d, expr* e) {
VERIFY(e);
VERIFY(d->get_range() == m.get_sort(e));