mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

delay internalization, relevancy (#4707)

Browse source 
* delay evaluation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Update bv_solver.cpp

* delay internalize

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* compiler warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove gc

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add bv delay option

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-23 17:12:01 -07:00 • committed by GitHub
parent 1e7998f03a
commit 7c2bdfe3fb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
21 changed files with 584 additions and 122 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/sat/dimacs.cpp
View file

@ -260,17 +260,6 @@ namespace dimacs {
m_record.m_tag = drat_record::tag_t::is_clause;
m_record.m_status = sat::status::th(false, theory_id);
break;
case 'g':
// parse garbage collected Boolean variable
++in;
skip_whitespace(in);
b = parse_int(in, err);
e = parse_int(in, err);
if (e != 0 || b <= 0)
throw lex_error();
m_record.m_tag = drat_record::tag_t::is_var_gc;
m_record.m_node_id = b;
break;
case 'e':
// parse expression definition
parse_ast(drat_record::tag_t::is_node);

2
src/sat/dimacs.h
View file

@ -53,7 +53,7 @@ namespace dimacs {
};
struct drat_record {
enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def, is_var_gc };
enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def };
tag_t m_tag{ tag_t::is_clause };
// a clause populates m_lits and m_status
// a node populates m_node_id, m_name, m_args

21
src/sat/sat_drat.cpp
View file

@ -257,22 +257,6 @@ namespace sat {
}
}
void drat::gc_var(bool_var v) {
sat::literal l(v, false);
// TBD: we want to remove all clauses that mention v.
std::cout << "GC " << v << "\n";
m_watches[l.index()].reset();
m_watches[(~l).index()].reset();
if (m_assignment[l.var()] != l_undef) {
unsigned j = 0;
for (literal lit : m_units)
if (lit.var() != v)
m_units[j++] = lit;
m_units.shrink(j);
m_assignment[l.var()] = l_undef;
}
}
void drat::bool_def(bool_var v, unsigned n) {
if (m_out)
(*m_out) << "b " << v << " " << n << " 0\n";
@ -293,11 +277,6 @@ namespace sat {
(*m_out) << " 0\n";
}
void drat::log_gc_var(bool_var v) {
if (m_out)
(*m_out) << "g " << v << " 0\n";
}
void drat::log_adhoc(std::function<void(std::ostream&)>& fn) {
if (m_out)
fn(*m_out);

4
src/sat/sat_drat.h
View file

@ -131,8 +131,6 @@ namespace sat {
void add(literal_vector const& c); // add learned clause
void add(unsigned sz, literal const* lits, status st);
void gc_var(bool_var v);
// support for SMT - connect Boolean variables with AST nodes
// associate AST node id with Boolean variable v
void bool_def(bool_var v, unsigned n);
@ -142,8 +140,6 @@ namespace sat {
void def_add_arg(unsigned arg);
void def_end();
void log_gc_var(bool_var v);
// ad-hoc logging until a format is developed
void log_adhoc(std::function<void(std::ostream&)>& fn);

3
src/sat/smt/CMakeLists.txt
View file

@ -12,6 +12,7 @@ z3_add_component(sat_smt
ba_solver.cpp
ba_xor.cpp
bv_ackerman.cpp
bv_delay_internalize.cpp
bv_internalize.cpp
bv_invariant.cpp
bv_solver.cpp
@ -20,7 +21,9 @@ z3_add_component(sat_smt
euf_invariant.cpp
euf_model.cpp
euf_proof.cpp
euf_relevancy.cpp
euf_solver.cpp
sat_dual_solver.cpp
sat_th.cpp
xor_solver.cpp
COMPONENT_DEPENDENCIES

146
src/sat/smt/bv_delay_internalize.cpp Normal file
View file

@ -0,0 +1,146 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
bv_delay_internalize.cpp
Abstract:
Checking of relevant bv nodes, and if required delay axiomatize
Author:
Nikolaj Bjorner (nbjorner) 2020-09-22
--*/
#include "sat/smt/bv_solver.h"
#include "sat/smt/euf_solver.h"
namespace bv {
bool solver::check_delay_internalized(euf::enode* n) {
expr* e = n->get_expr();
SASSERT(bv.is_bv(e));
SASSERT(get_internalize_mode(e) != internalize_mode::no_delay_i);
switch (to_app(e)->get_decl_kind()) {
case OP_BMUL:
return check_mul(n);
default:
return check_eval(n);
}
return true;
}
bool solver::should_bit_blast(expr* e) {
return bv.get_bv_size(e) <= 10;
}
void solver::eval_args(euf::enode* n, vector<rational>& args) {
rational val;
for (euf::enode* arg : euf::enode_args(n)) {
theory_var v = arg->get_th_var(get_id());
VERIFY(get_fixed_value(v, val));
args.push_back(val);
}
}
bool solver::check_mul(euf::enode* n) {
SASSERT(n->num_args() >= 2);
app* e = to_app(n->get_expr());
rational val, val_mul(1);
vector<rational> args;
eval_args(n, args);
for (rational const& val_arg : args)
val_mul *= val_arg;
theory_var v = n->get_th_var(get_id());
VERIFY(get_fixed_value(v, val));
val_mul = mod(val_mul, power2(get_bv_size(v)));
IF_VERBOSE(12, verbose_stream() << "check_mul " << mk_bounded_pp(n->get_expr(), m) << " " << args << " = " << val_mul << " =? " << val << "\n");
if (val_mul == val)
return true;
// Some possible approaches:
// check base cases: val_mul = 0 or val = 0, some values in product are 1,
// check discrepancies in low-order bits
// Add axioms for multiplication when fixing high-order bits to 0
// Hensel lifting:
// The idea is dual to fixing high-order bits. Fix the low order bits where multiplication
// is correct, and propagate on the next bit that shows a discrepancy.
// check Montgommery properties: (x*y) mod p = (x mod p)*(y mod p) for small primes p
// check ranges lo <= x <= hi, lo' <= y <= hi', lo*lo' < x*y <= hi*hi' for non-overflowing values.
// check tangets hi >= y >= y0 and hi' >= x => x*y >= x*y0
// compute S-polys for a set of constraints.
set_delay_internalize(e, internalize_mode::no_delay_i);
internalize_circuit(e, v);
return false;
}
bool solver::check_eval(euf::enode* n) {
expr_ref_vector args(m);
expr_ref r1(m), r2(m);
rational val;
app* a = to_app(n->get_expr());
theory_var v = n->get_th_var(get_id());
VERIFY(get_fixed_value(v, val));
r1 = bv.mk_numeral(val, get_bv_size(v));
SASSERT(bv.is_bv(a));
for (euf::enode* arg : euf::enode_args(n)) {
SASSERT(bv.is_bv(arg->get_expr()));
theory_var v_arg = arg->get_th_var(get_id());
VERIFY(get_fixed_value(v_arg, val));
args.push_back(bv.mk_numeral(val, get_bv_size(v_arg)));
}
r2 = m.mk_app(a->get_decl(), args);
ctx.get_rewriter()(r2);
if (r1 == r2)
return true;
set_delay_internalize(a, internalize_mode::no_delay_i);
internalize_circuit(a, v);
return false;
}
void solver::set_delay_internalize(expr* e, internalize_mode mode) {
if (!m_delay_internalize.contains(e))
ctx.push(insert_obj_map<euf::solver, expr, internalize_mode>(m_delay_internalize, e));
m_delay_internalize.insert(e, mode);
}
solver::internalize_mode solver::get_internalize_mode(expr* e) {
if (!bv.is_bv(e))
return internalize_mode::no_delay_i;
if (!get_config().m_bv_delay)
return internalize_mode::no_delay_i;
switch (to_app(e)->get_decl_kind()) {
case OP_BMUL:
case OP_BSMUL_NO_OVFL:
case OP_BSMUL_NO_UDFL:
case OP_BUMUL_NO_OVFL:
case OP_BSMOD_I:
case OP_BUREM_I:
case OP_BSREM_I:
case OP_BUDIV_I:
case OP_BSDIV_I: {
if (should_bit_blast(e))
return internalize_mode::no_delay_i;
internalize_mode mode = internalize_mode::init_bits_i;
if (!m_delay_internalize.find(e, mode))
set_delay_internalize(e, mode);
return mode;
}
default:
return internalize_mode::no_delay_i;
}
}
}

34
src/sat/smt/bv_internalize.cpp
View file

@ -148,15 +148,23 @@ namespace bv {
bool solver::post_visit(expr* e, bool sign, bool root) {
euf::enode* n = expr2enode(e);
app* a = to_app(e);
SASSERT(!n || !n->is_attached_to(get_id()));
bool suppress_args = !get_config().m_bv_reflect && !m.is_considered_uninterpreted(a->get_decl());
if (!n)
if (!n)
n = mk_enode(e, suppress_args);
SASSERT(!n->is_attached_to(get_id()));
theory_var v = mk_var(n);
SASSERT(n->is_attached_to(get_id()));
if (internalize_mode::init_bits_i == get_internalize_mode(a))
mk_bits(n->get_th_var(get_id()));
else
internalize_circuit(a, v);
return true;
}
bool solver::internalize_circuit(app* a, theory_var v) {
std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref_vector& bits)> bin;
std::function<void(unsigned sz, expr* const* xs, expr* const* ys, expr_ref& bit)> ebin;
@ -507,30 +515,30 @@ namespace bv {
init_bits(n, bits);
}
void solver::internalize_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
SASSERT(n->get_num_args() == 2);
void solver::internalize_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
SASSERT(e->get_num_args() == 2);
expr_ref_vector arg1_bits(m), arg2_bits(m), bits(m);
get_arg_bits(n, 0, arg1_bits);
get_arg_bits(n, 1, arg2_bits);
get_arg_bits(e, 0, arg1_bits);
get_arg_bits(e, 1, arg2_bits);
SASSERT(arg1_bits.size() == arg2_bits.size());
fn(arg1_bits.size(), arg1_bits.c_ptr(), arg2_bits.c_ptr(), bits);
init_bits(n, bits);
init_bits(e, bits);
}
void solver::internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
SASSERT(n->get_num_args() >= 2);
void solver::internalize_ac_binary(app* e, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn) {
SASSERT(e->get_num_args() >= 2);
expr_ref_vector bits(m), new_bits(m), arg_bits(m);
unsigned i = n->get_num_args() - 1;
get_arg_bits(n, i, bits);
unsigned i = e->get_num_args() - 1;
get_arg_bits(e, i, bits);
for (; i-- > 0; ) {
arg_bits.reset();
get_arg_bits(n, i, arg_bits);
get_arg_bits(e, i, arg_bits);
SASSERT(arg_bits.size() == bits.size());
new_bits.reset();
fn(arg_bits.size(), arg_bits.c_ptr(), bits.c_ptr(), new_bits);
bits.swap(new_bits);
}
init_bits(n, bits);
init_bits(e, bits);
TRACE("bv_verbose", tout << arg_bits << " " << bits << " " << new_bits << "\n";);
}

11
src/sat/smt/bv_solver.cpp
View file

@ -378,7 +378,7 @@ namespace bv {
break;
}
ctx.get_drat().add(lits, status());
ctx.get_drat().log_gc_var(leq.var()); // TBD, a proper way would be to delete the lemma after use.
// TBD, a proper way would be to delete the lemma after use.
}
void solver::asserted(literal l) {
@ -493,7 +493,14 @@ namespace bv {
sat::check_result solver::check() {
force_push();
SASSERT(m_prop_queue.size() == m_prop_queue_head);
return sat::check_result::CR_DONE;
bool ok = true;
for (auto kv : m_delay_internalize) {
if (ctx.is_relevant(kv.m_key) &&
kv.m_value == internalize_mode::init_bits_i &&
!check_delay_internalized(expr2enode(kv.m_key)))
ok = false;
}
return ok ? sat::check_result::CR_DONE : sat::check_result::CR_CONTINUE;
}
void solver::push_core() {

19
src/sat/smt/bv_solver.h
View file

@ -53,9 +53,9 @@ namespace bv {
struct bv_justification {
enum kind_t { eq2bit, ne2bit, bit2eq, bit2ne };
kind_t m_kind;
unsigned m_idx{ UINT_MAX };
theory_var m_v1{ euf::null_theory_var };
theory_var m_v2 { euf::null_theory_var };
unsigned m_idx{ UINT_MAX };
sat::literal m_consequent;
sat::literal m_antecedent;
bv_justification(theory_var v1, theory_var v2, sat::literal c, sat::literal a) :
@ -267,6 +267,7 @@ namespace bv {
void init_bits(expr* e, expr_ref_vector const & bits);
void mk_bits(theory_var v);
void add_def(sat::literal def, sat::literal l);
bool internalize_circuit(app* a, theory_var v);
void internalize_unary(app* n, std::function<void(unsigned, expr* const*, expr_ref_vector&)>& fn);
void internalize_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
void internalize_ac_binary(app* n, std::function<void(unsigned, expr* const*, expr* const*, expr_ref_vector&)>& fn);
@ -288,6 +289,21 @@ namespace bv {
void assert_int2bv_axiom(app* n);
void assert_ackerman(theory_var v1, theory_var v2);
// delay internalize
enum class internalize_mode {
no_delay_i,
init_bits_i
};
obj_map<expr, internalize_mode> m_delay_internalize;
bool should_bit_blast(expr * n);
bool check_delay_internalized(euf::enode* n);
bool check_mul(euf::enode* n);
bool check_eval(euf::enode* n);
internalize_mode get_internalize_mode(expr* e);
void set_delay_internalize(expr* e, internalize_mode mode);
void eval_args(euf::enode* n, vector<rational>& args);
// solving
theory_var find(theory_var v) const { return m_find.find(v); }
void find_wpos(theory_var v);
@ -302,6 +318,7 @@ namespace bv {
bool propagate_eq_occurs(eq_occurs const& occ);
numeral const& power2(unsigned i) const;
// invariants
bool check_zero_one_bits(theory_var v);
void check_missing_propagation() const;

84
src/sat/smt/euf_relevancy.cpp Normal file
View file

@ -0,0 +1,84 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
euf_relevancy.cpp
Abstract:
Features for relevancy tracking.
A reduced (minimal) implicant is extracted by running a dual solver.
Then the literals in the implicant are used as a basis for marking
subterms relevant.
Author:
Nikolaj Bjorner (nbjorner) 2020-09-22
--*/
#include "sat/smt/euf_solver.h"
namespace euf {
void solver::ensure_dual_solver() {
if (!m_dual_solver)
m_dual_solver = alloc(sat::dual_solver, s().rlimit());
}
void solver::add_root(unsigned n, sat::literal const* lits) {
bool_var v = s().add_var(false);
ensure_dual_solver();
m_dual_solver->add_root(sat::literal(v, false), n, lits);
}
void solver::add_aux(unsigned n, sat::literal const* lits) {
ensure_dual_solver();
m_dual_solver->add_aux(n, lits);
}
void solver::track_relevancy(sat::bool_var v) {
ensure_dual_solver();
m_dual_solver->track_relevancy(v);
}
bool solver::init_relevancy() {
m_relevant_expr_ids.reset();
bool_vector visited;
ptr_vector<expr> todo;
if (!m_dual_solver)
return true;
if (!(*m_dual_solver)(s()))
return false;
unsigned max_id = 0;
for (enode* n : m_egraph.nodes())
max_id = std::max(max_id, n->get_expr_id());
m_relevant_expr_ids.resize(max_id + 1, false);
auto const& core = m_dual_solver->core();
for (auto lit : core) {
expr* e = m_var2expr.get(lit.var(), nullptr);
if (e)
todo.push_back(e);
}
for (unsigned i = 0; i < todo.size(); ++i) {
expr* e = todo[i];
if (visited.get(e->get_id(), false))
continue;
visited.setx(e->get_id(), true, false);
if (!si.is_bool_op(e))
m_relevant_expr_ids.setx(e->get_id(), true, false);
if (!is_app(e))
continue;
for (expr* arg : *to_app(e))
if (!visited.get(arg->get_id(), false))
todo.push_back(arg);
}
TRACE("euf",
for (enode* n : m_egraph.nodes())
if (is_relevant(n))
tout << "relevant " << mk_bounded_pp(n->get_expr(), m) << "\n";);
return true;
}
}

4
src/sat/smt/euf_solver.cpp
View file

@ -342,6 +342,10 @@ namespace euf {
TRACE("euf", s().display(tout););
bool give_up = false;
bool cont = false;
if (!init_relevancy())
give_up = true;
for (auto* e : m_solvers)
switch (e->check()) {
case sat::check_result::CR_CONTINUE: cont = true; break;

104
src/sat/smt/euf_solver.h
View file

@ -25,6 +25,7 @@ Author:
#include "sat/sat_extension.h"
#include "sat/smt/atom2bool_var.h"
#include "sat/smt/sat_th.h"
#include "sat/smt/sat_dual_solver.h"
#include "sat/smt/euf_ackerman.h"
#include "smt/params/smt_params.h"
@ -37,14 +38,14 @@ namespace euf {
class constraint {
public:
enum class kind_t { conflict, eq, lit};
enum class kind_t { conflict, eq, lit };
private:
kind_t m_kind;
public:
constraint(kind_t k) : m_kind(k) {}
kind_t kind() const { return m_kind; }
static constraint& from_idx(size_t z) {
return *reinterpret_cast<constraint*>(sat::constraint_base::idx2mem(z));
static constraint& from_idx(size_t z) {
return *reinterpret_cast<constraint*>(sat::constraint_base::idx2mem(z));
}
size_t to_index() const { return sat::constraint_base::mem2base(this); }
};
@ -76,7 +77,7 @@ namespace euf {
return reinterpret_cast<size_t>(UNTAG(size_t*, p));
}
ast_manager& m;
ast_manager& m;
sat::sat_internalizer& si;
smt_params m_config;
euf::egraph m_egraph;
@ -85,28 +86,29 @@ namespace euf {
th_rewriter m_rewriter;
func_decl_ref_vector m_unhandled_functions;
sat::solver* m_solver { nullptr };
sat::lookahead* m_lookahead { nullptr };
ast_manager* m_to_m;
sat::solver* m_solver{ nullptr };
sat::lookahead* m_lookahead{ nullptr };
ast_manager* m_to_m;
sat::sat_internalizer* m_to_si;
scoped_ptr<euf::ackerman> m_ackerman;
scoped_ptr<sat::dual_solver> m_dual_solver;
ptr_vector<expr> m_var2expr;
ptr_vector<size_t> m_explain;
unsigned m_num_scopes { 0 };
unsigned m_num_scopes{ 0 };
unsigned_vector m_var_trail;
svector<scope> m_scopes;
scoped_ptr_vector<th_solver> m_solvers;
ptr_vector<th_solver> m_id2solver;
constraint* m_conflict { nullptr };
constraint* m_eq { nullptr };
constraint* m_lit { nullptr };
constraint* m_conflict{ nullptr };
constraint* m_eq{ nullptr };
constraint* m_lit{ nullptr };
// internalization
bool visit(expr* e) override;
bool visited(expr* e) override;
bool post_visit(expr* e, bool sign, bool root) override;
bool post_visit(expr* e, bool sign, bool root) override;
sat::literal attach_lit(sat::literal lit, expr* e);
void add_distinct_axiom(app* e, euf::enode* const* args);
void add_not_distinct_axiom(app* e, euf::enode* const* args);
@ -117,7 +119,7 @@ namespace euf {
// replay
expr_ref_vector m_reinit_exprs;
void start_reinit(unsigned num_scopes);
void finish_reinit();
@ -135,7 +137,7 @@ namespace euf {
bool include_func_interp(func_decl* f);
void register_macros(model& mdl);
void dependencies2values(deps_t& deps, expr_ref_vector& values, model_ref& mdl);
void collect_dependencies(deps_t& deps);
void collect_dependencies(deps_t& deps);
void values2model(deps_t const& deps, expr_ref_vector const& values, model_ref& mdl);
// solving
@ -149,17 +151,24 @@ namespace euf {
void log_antecedents(literal l, literal_vector const& r);
void drat_log_decl(func_decl* f);
obj_hashtable<ast> m_drat_asts;
bool m_drat_initialized{ false };
void init_drat();
// relevancy
bool_vector m_relevant_expr_ids;
void ensure_dual_solver();
bool init_relevancy();
// invariant
void check_eqc_bool_assignment() const;
void check_missing_bool_enode_propagation() const;
void check_missing_bool_enode_propagation() const;
void check_missing_eq_propagation() const;
// diagnosis
std::ostream& display_justification_ptr(std::ostream& out, size_t* j) const;
// constraints
constraint& mk_constraint(constraint*& c, constraint::kind_t k);
constraint& conflict_constraint() { return mk_constraint(m_conflict, constraint::kind_t::conflict); }
constraint& eq_constraint() { return mk_constraint(m_eq, constraint::kind_t::eq); }
@ -168,25 +177,26 @@ namespace euf {
public:
solver(ast_manager& m, sat::sat_internalizer& si, params_ref const& p = params_ref());
~solver() override {
if (m_conflict) dealloc(sat::constraint_base::mem2base_ptr(m_conflict));
if (m_eq) dealloc(sat::constraint_base::mem2base_ptr(m_eq));
if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
}
~solver() override {
if (m_conflict) dealloc(sat::constraint_base::mem2base_ptr(m_conflict));
if (m_eq) dealloc(sat::constraint_base::mem2base_ptr(m_eq));
if (m_lit) dealloc(sat::constraint_base::mem2base_ptr(m_lit));
}
struct scoped_set_translate {
solver& s;
scoped_set_translate(solver& s, ast_manager& m, sat::sat_internalizer& si) :
s(s) {
s.m_to_m = &m;
s.m_to_si = &si;
}
~scoped_set_translate() {
s.m_to_m = &s.m;
s.m_to_si = &s.si;
}
};
struct scoped_set_translate {
solver& s;
scoped_set_translate(solver& s, ast_manager& m, sat::sat_internalizer& si) :
s(s) {
s.m_to_m = &m;
s.m_to_si = &si;
}
~scoped_set_translate() {
s.m_to_m = &s.m;
s.m_to_si = &s.si;
}
};
// accessors
sat::solver& s() { return *m_solver; }
sat::solver const& s() const { return *m_solver; }
sat::sat_internalizer& get_si() { return si; }
@ -194,11 +204,11 @@ namespace euf {
enode* get_enode(expr* e) { return m_egraph.find(e); }
sat::literal expr2literal(expr* e) const { return literal(si.to_bool_var(e), false); }
sat::literal enode2literal(enode* e) const { return expr2literal(e->get_expr()); }
smt_params const& get_config() { return m_config; }
smt_params const& get_config() const { return m_config; }
region& get_region() { return m_trail.get_region(); }
egraph& get_egraph() { return m_egraph; }
template <typename C>
void push(C const& c) { m_trail.push(c); }
void push(C const& c) { m_trail.push(c); }
euf_trail_stack& get_trail_stack() { return m_trail; }
void updt_params(params_ref const& p);
@ -214,7 +224,7 @@ namespace euf {
bool set_root(literal l, literal r) override;
void flush_roots() override;
void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r, bool probing) override;
void get_antecedents(literal l, ext_justification_idx idx, literal_vector& r, bool probing) override;
void add_antecedent(enode* a, enode* b);
void asserted(literal l) override;
sat::check_result check() override;
@ -229,8 +239,8 @@ namespace euf {
std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override;
std::ostream& display_constraint(std::ostream& out, ext_constraint_idx idx) const override;
void collect_statistics(statistics& st) const override;
extension* copy(sat::solver* s) override;
void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override;
extension* copy(sat::solver* s) override;
void find_mutexes(literal_vector& lits, vector<literal_vector>& mutexes) override;
void gc() override;
void pop_reinit() override;
bool validate() override;
@ -239,12 +249,12 @@ namespace euf {
bool check_model(sat::model const& m) const override;
unsigned max_var(unsigned w) const override;
bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
bool use_drat() { return s().get_config().m_drat && (init_drat(), true); }
sat::drat& get_drat() { return s().get_drat(); }
// decompile
bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;
std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) override;
bool to_formulas(std::function<expr_ref(sat::literal)>& l2e, expr_ref_vector& fmls) override;
@ -262,10 +272,20 @@ namespace euf {
bool is_shared(euf::enode* n) const;
void drat_log_node(expr* n);
// relevancy
bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; }
void add_root(unsigned n, sat::literal const* lits);
void add_aux(unsigned n, sat::literal const* lits);
void track_relevancy(sat::bool_var v);
bool is_relevant(expr* e) const { return m_relevant_expr_ids.get(e->get_id(), true); }
bool is_relevant(enode* n) const { return m_relevant_expr_ids.get(n->get_expr_id(), true); }
// model construction
void update_model(model_ref& mdl);
func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }
};
// diagnostics
func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }
};
};
inline std::ostream& operator<<(std::ostream& out, euf::solver const& s) {

96
src/sat/smt/sat_dual_solver.cpp Normal file
View file

@ -0,0 +1,96 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_dual_solver.cpp
Abstract:
Solver for obtaining implicant.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#include "sat/smt/sat_dual_solver.h"
namespace sat {
dual_solver::dual_solver(reslimit& l):
m_solver(params_ref(), l)
{}
void dual_solver::push() {
m_solver.user_push();
m_roots_lim.push_back(m_roots.size());
m_tracked_lim.push_back(m_tracked_stack.size());
}
void dual_solver::pop(unsigned num_scopes) {
m_solver.user_pop(num_scopes);
unsigned old_sz = m_roots_lim.size() - num_scopes;
m_roots.shrink(m_roots_lim[old_sz]);
m_roots_lim.shrink(old_sz);
for (unsigned v = m_tracked_stack.size(); v-- > m_tracked_lim[old_sz]; )
m_is_tracked[v] = false;
m_tracked_stack.shrink(m_tracked_lim[old_sz]);
m_tracked_lim.shrink(old_sz);
}
bool_var dual_solver::ext2var(bool_var v) {
bool_var w = m_ext2var.get(v, null_bool_var);
if (null_bool_var == w) {
w = m_solver.mk_var();
m_ext2var.setx(v, w, null_bool_var);
m_var2ext.setx(w, v, null_bool_var);
}
return w;
}
void dual_solver::track_relevancy(bool_var v) {
v = ext2var(v);
if (!m_is_tracked.get(v, false)) {
m_is_tracked.setx(v, true, false);
m_tracked_stack.push_back(v);
}
}
literal dual_solver::ext2lit(literal lit) {
return literal(ext2var(lit.var()), lit.sign());
}
literal dual_solver::lit2ext(literal lit) {
return literal(m_var2ext[lit.var()], lit.sign());
}
void dual_solver::add_root(literal lit, unsigned sz, literal const* clause) {
for (unsigned i = 0; i < sz; ++i)
m_solver.mk_clause(ext2lit(lit), ~ext2lit(clause[i]), status::input());
m_roots.push_back(~ext2lit(lit));
}
void dual_solver::add_aux(unsigned sz, literal const* clause) {
m_lits.reset();
for (unsigned i = 0; i < sz; ++i)
m_lits.push_back(ext2lit(clause[i]));
m_solver.mk_clause(sz, m_lits.c_ptr(), status::input());
}
bool dual_solver::operator()(solver const& s) {
m_solver.user_push();
m_solver.add_clause(m_roots.size(), m_roots.c_ptr(), status::input());
m_lits.reset();
for (bool_var v : m_tracked_stack)
m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
lbool is_sat = m_solver.check(m_lits.size(), m_lits.c_ptr());
m_core.reset();
if (is_sat == l_false)
for (literal lit : m_solver.get_core())
m_core.push_back(lit2ext(lit));
TRACE("euf", m_solver.display(tout << m_core << "\n"););
m_solver.user_pop(1);
return is_sat == l_false;
}
}

64
src/sat/smt/sat_dual_solver.h Normal file
View file

@ -0,0 +1,64 @@
/*++
Copyright (c) 2020 Microsoft Corporation
Module Name:
sat_dual_solver.h
Abstract:
Solver for obtaining implicant.
Author:
Nikolaj Bjorner (nbjorner) 2020-08-25
--*/
#pragma once
#include "sat/sat_solver.h"
namespace sat {
class dual_solver {
solver m_solver;
literal_vector m_roots, m_lits, m_core;
bool_var_vector m_is_tracked;
unsigned_vector m_tracked_stack;
unsigned_vector m_ext2var;
unsigned_vector m_var2ext;
unsigned_vector m_roots_lim, m_tracked_lim;
void add_literal(literal lit);
bool_var ext2var(bool_var v);
bool_var var2ext(bool_var v);
literal ext2lit(literal lit);
literal lit2ext(literal lit);
public:
dual_solver(reslimit& l);
void push();
void pop(unsigned num_scopes);
/*
* track model relevancy for variable
*/
void track_relevancy(bool_var v);
/*
* Add a root clause from the input problem.
* At least one literal has to be satisfied in every root.
*/
void add_root(literal lit, unsigned sz, literal const* clause);
/*
* Add auxiliary clauses that originate from compiling definitions.
*/
void add_aux(unsigned sz, literal const* clause);
/*
* Extract a minimized subset of relevant literals from a model for s.
*/
bool operator()(solver const& s);
literal_vector const& core() const { return m_core; }
};
}

2
src/sat/smt/sat_th.h
View file

@ -107,8 +107,6 @@ namespace euf {
*/
virtual bool is_shared(theory_var v) const { return false; }
};
class th_euf_solver : public th_solver {

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

@ -74,9 +74,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
func_decl_ref_vector m_unhandled_funs;
bool m_default_external;
bool m_xor_solver;
bool m_euf;
bool m_drat;
bool m_euf { false };
bool m_drat { false };
bool m_is_redundant { false };
bool m_top_level { false };
sat::literal_vector aig_lits;
imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external):
@ -113,45 +114,60 @@ struct goal2sat::imp : public sat::sat_internalizer {
sat::status mk_status() const {
return sat::status::th(m_is_redundant, m.get_basic_family_id());
}
bool top_level_relevant() {
return m_top_level && m_euf && ensure_euf()->relevancy_enabled();
}
void add_dual_def(unsigned n, sat::literal const* lits) {
if (top_level_relevant())
ensure_euf()->add_aux(n, lits);
}
void add_dual_root(unsigned n, sat::literal const* lits) {
if (top_level_relevant())
ensure_euf()->add_root(n, lits);
}
void mk_clause(sat::literal l) {
TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
m_solver.add_clause(1, &l, mk_status());
mk_clause(1, &l);
}
void mk_clause(sat::literal l1, sat::literal l2) {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
m_solver.add_clause(l1, l2, mk_status());
sat::literal lits[2] = { l1, l2 };
mk_clause(2, lits);
}
void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
m_solver.add_clause(l1, l2, l3, mk_status());
sat::literal lits[3] = { l1, l2, l3 };
mk_clause(3, lits);
}
void mk_clause(unsigned num, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
m_solver.add_clause(num, lits, mk_status());
void mk_clause(unsigned n, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
add_dual_def(n, lits);
m_solver.add_clause(n, lits, mk_status());
}
void mk_root_clause(sat::literal l) {
TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
m_solver.add_clause(1, &l, m_is_redundant ? mk_status() : sat::status::input());
mk_root_clause(1, &l);
}
void mk_root_clause(sat::literal l1, sat::literal l2) {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
m_solver.add_clause(l1, l2, m_is_redundant ? mk_status() : sat::status::input());
sat::literal lits[2] = { l1, l2 };
mk_root_clause(2, lits);
}
void mk_root_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
m_solver.add_clause(l1, l2, l3, m_is_redundant ? mk_status() : sat::status::input());
sat::literal lits[3] = { l1, l2, l3 };
mk_root_clause(3, lits);
}
void mk_root_clause(unsigned num, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
m_solver.add_clause(num, lits, m_is_redundant ? mk_status() : sat::status::input());
void mk_root_clause(unsigned n, sat::literal * lits) {
TRACE("goal2sat", tout << "mk_root_clause: "; for (unsigned i = 0; i < n; i++) tout << lits[i] << " "; tout << "\n";);
add_dual_root(n, lits);
m_solver.add_clause(n, lits, m_is_redundant ? mk_status() : sat::status::input());
}
sat::bool_var add_var(bool is_ext, expr* n) {
@ -161,6 +177,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
v = m_solver.add_var(is_ext);
log_node(n);
log_def(v, n);
if (top_level_relevant() && !is_bool_op(n))
ensure_euf()->track_relevancy(v);
return v;
}
@ -603,9 +621,15 @@ struct goal2sat::imp : public sat::sat_internalizer {
SASSERT(m_euf);
TRACE("goal2sat", tout << "convert-euf " << mk_bounded_pp(e, m, 2) << " root " << root << "\n";);
euf::solver* euf = ensure_euf();
sat::literal lit = euf->internalize(e, sign, root, m_is_redundant);
sat::literal lit;
{
flet<bool> _top(m_top_level, false);
lit = euf->internalize(e, sign, root, m_is_redundant);
}
if (lit == sat::null_literal)
return;
if (top_level_relevant())
euf->track_relevancy(lit.var());
if (root)
mk_root_clause(lit);
else
@ -757,6 +781,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
sat::literal internalize(expr* n, bool redundant) override {
flet<bool> _top(m_top_level, false);
unsigned sz = m_result_stack.size();
(void)sz;
SASSERT(n->get_ref_count() > 0);
@ -797,6 +822,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
}
void process(expr * n) {
flet<bool> _top(m_top_level, true);
VERIFY(m_result_stack.empty());
TRACE("goal2sat", tout << "assert: " << mk_bounded_pp(n, m, 3) << "\n";);
process(n, true, m_is_redundant);

3
src/shell/drat_frontend.cpp
View file

@ -311,9 +311,6 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
bool_var2expr.reserve(r.m_node_id+1);
bool_var2expr.set(r.m_node_id, exprs.get(r.m_args[0]));
break;
case dimacs::drat_record::tag_t::is_var_gc:
drat_checker.gc_var(r.m_node_id);
break;
default:
UNREACHABLE();
break;

1
src/smt/params/smt_params_helper.pyg
View file

@ -46,6 +46,7 @@ def_module_params(module_name='smt',
('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'),
('bv.eq_axioms', BOOL, True, 'add dynamic equality axioms'),
('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'),
('bv.delay', BOOL, True, 'delay internalize expensive bit-vector operations'),
('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'),
('arith.cheap_eqs', BOOL, True, 'false - do not run, true - run cheap equality heuristic'),
('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'),

2
src/smt/params/theory_bv_params.cpp
View file

@ -27,6 +27,7 @@ void theory_bv_params::updt_params(params_ref const & _p) {
m_bv_reflect = p.bv_reflect();
m_bv_enable_int2bv2int = p.bv_enable_int2bv();
m_bv_eq_axioms = p.bv_eq_axioms();
m_bv_delay = p.bv_delay();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
@ -40,4 +41,5 @@ void theory_bv_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_bv_eq_axioms);
DISPLAY_PARAM(m_bv_blast_max_size);
DISPLAY_PARAM(m_bv_enable_int2bv2int);
DISPLAY_PARAM(m_bv_delay);
}

4
src/smt/params/theory_bv_params.h
View file

@ -35,6 +35,7 @@ struct theory_bv_params {
unsigned m_bv_blast_max_size;
bool m_bv_enable_int2bv2int;
bool m_bv_watch_diseq;
bool m_bv_delay;
theory_bv_params(params_ref const & p = params_ref()):
m_bv_mode(bv_solver_id::BS_BLASTER),
m_hi_div0(false),
@ -44,7 +45,8 @@ struct theory_bv_params {
m_bv_eq_axioms(true),
m_bv_blast_max_size(INT_MAX),
m_bv_enable_int2bv2int(true),
m_bv_watch_diseq(false) {
m_bv_watch_diseq(false),
m_bv_delay(true) {
updt_params(p);
}

23
src/util/vector.h
View file

@ -515,6 +515,18 @@ public:
}
}
void init(vector<T, CallDestructors> const& other) {
if (this == &other)
return;
reset();
append(other);
}
void init(SZ sz, T const* data) {
reset();
append(sz, data);
}
T * c_ptr() const {
return m_data;
}
@ -637,3 +649,14 @@ struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> >
template<typename Hash>
struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
template<typename T>
inline std::ostream& operator<<(std::ostream& out, vector<T> const& v) {
bool first = true;
for (auto const& t : v) {
if (first) first = false; else out << " ";
out << t;
}
return out;
}