mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
add sat-euf
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
a7b51d04cd
commit
ecd3315a74
11 changed files with 474 additions and 52 deletions
8
src/sat/euf/CMakeLists.txt
Normal file
8
src/sat/euf/CMakeLists.txt
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
z3_add_component(sat_euf
|
||||
SOURCES
|
||||
euf_solver.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
sat
|
||||
sat_tactic
|
||||
euf
|
||||
)
|
||||
186
src/sat/euf/euf_solver.cpp
Normal file
186
src/sat/euf/euf_solver.cpp
Normal file
|
|
@ -0,0 +1,186 @@
|
|||
/*++
|
||||
Copyright (c) 2020 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
euf_solver.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Solver plugin for EUF
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2020-08-25
|
||||
|
||||
--*/
|
||||
#include "sat/euf/euf_solver.h"
|
||||
#include "sat/sat_solver.h"
|
||||
#include "tactic/tactic_exception.h"
|
||||
|
||||
namespace euf_sat {
|
||||
|
||||
bool solver::propagate(literal l, ext_constraint_idx idx) {
|
||||
UNREACHABLE();
|
||||
return true;
|
||||
}
|
||||
|
||||
void solver::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
|
||||
m_explain.reset();
|
||||
euf::enode* n = nullptr;
|
||||
bool sign = false;
|
||||
if (idx != 0) {
|
||||
auto p = m_var2node[l.var()];
|
||||
n = p.first;
|
||||
sign = l.sign() != p.second;
|
||||
}
|
||||
|
||||
switch (idx) {
|
||||
case 0:
|
||||
SASSERT(m_egraph.inconsistent());
|
||||
m_egraph.explain<unsigned>(m_explain);
|
||||
break;
|
||||
case 1:
|
||||
SASSERT(m_egraph.is_equality(n));
|
||||
m_egraph.explain_eq<unsigned>(m_explain, n->get_arg(0), n->get_arg(1), n->commutative());
|
||||
break;
|
||||
case 2:
|
||||
SASSERT(m.is_bool(n->get_owner()));
|
||||
m_egraph.explain_eq<unsigned>(m_explain, n, (sign ? m_false : m_true), false);
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
for (unsigned* idx : m_explain)
|
||||
r.push_back(sat::to_literal((unsigned)(idx - base_ptr())));
|
||||
}
|
||||
|
||||
void solver::asserted(literal l) {
|
||||
auto p = m_var2node[l.var()];
|
||||
bool sign = p.second != l.sign();
|
||||
euf::enode* n = p.first;
|
||||
expr* e = n->get_owner();
|
||||
if (m.is_eq(e) && !sign) {
|
||||
euf::enode* na = n->get_arg(0);
|
||||
euf::enode* nb = n->get_arg(1);
|
||||
m_egraph.merge(na, nb, base_ptr() + l.index());
|
||||
}
|
||||
else {
|
||||
euf::enode* nb = sign ? m_false : m_true;
|
||||
m_egraph.merge(n, nb, base_ptr() + l.index());
|
||||
}
|
||||
|
||||
// TBD: delay propagation?
|
||||
m_egraph.propagate();
|
||||
if (m_egraph.inconsistent()) {
|
||||
s().set_conflict(sat::justification::mk_ext_justification(s().scope_lvl(), 0));
|
||||
return;
|
||||
}
|
||||
for (euf::enode* eq : m_egraph.new_eqs()) {
|
||||
bool_var v = m_expr2var.to_bool_var(eq->get_owner());
|
||||
s().assign(literal(v, false), sat::justification::mk_ext_justification(s().scope_lvl(), 1));
|
||||
}
|
||||
for (euf::enode* p : m_egraph.new_lits()) {
|
||||
expr* e = p->get_owner();
|
||||
bool sign = m.is_false(p->get_root()->get_owner());
|
||||
SASSERT(m.is_bool(e));
|
||||
SASSERT(m.is_true(p->get_root()->get_owner()) || sign);
|
||||
bool_var v = m_expr2var.to_bool_var(e);
|
||||
s().assign(literal(v, sign), sat::justification::mk_ext_justification(s().scope_lvl(), 2));
|
||||
}
|
||||
}
|
||||
|
||||
sat::check_result solver::check() {
|
||||
return sat::CR_DONE;
|
||||
}
|
||||
void solver::push() {
|
||||
m_egraph.push();
|
||||
}
|
||||
void solver::pop(unsigned n) {
|
||||
m_egraph.pop(n);
|
||||
}
|
||||
void solver::pre_simplify() {}
|
||||
void solver::simplify() {}
|
||||
// have a way to replace l by r in all constraints
|
||||
void solver::clauses_modifed() {}
|
||||
lbool solver::get_phase(bool_var v) { return l_undef; }
|
||||
std::ostream& solver::display(std::ostream& out) const {
|
||||
m_egraph.display(out);
|
||||
return out;
|
||||
}
|
||||
std::ostream& solver::display_justification(std::ostream& out, ext_justification_idx idx) const { return out; }
|
||||
std::ostream& solver::display_constraint(std::ostream& out, ext_constraint_idx idx) const { return out; }
|
||||
void solver::collect_statistics(statistics& st) const {}
|
||||
sat::extension* solver::copy(sat::solver* s) { return nullptr; }
|
||||
sat::extension* solver::copy(sat::lookahead* s, bool learned) { return nullptr; }
|
||||
void solver::find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) {}
|
||||
void solver::gc() {}
|
||||
void solver::pop_reinit() {}
|
||||
bool solver::validate() { return true; }
|
||||
void solver::init_use_list(sat::ext_use_list& ul) {}
|
||||
bool solver::is_blocked(literal l, ext_constraint_idx) { return false; }
|
||||
bool solver::check_model(sat::model const& m) const { return true;}
|
||||
unsigned solver::max_var(unsigned w) const { return w; }
|
||||
|
||||
void solver::internalize(sat_internalizer& si, expr* e) {
|
||||
SASSERT(!si.is_bool_op(e));
|
||||
unsigned sz = m_stack.size();
|
||||
euf::enode* n = visit(si, e);
|
||||
while (m_stack.size() > sz) {
|
||||
loop:
|
||||
if (!m.inc())
|
||||
throw tactic_exception(m.limit().get_cancel_msg());
|
||||
frame & fr = m_stack.back();
|
||||
expr* e = fr.m_e;
|
||||
if (m_egraph.find(e)) {
|
||||
m_stack.pop_back();
|
||||
continue;
|
||||
}
|
||||
unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0;
|
||||
m_args.reset();
|
||||
while (fr.m_idx < num) {
|
||||
expr* arg = to_app(e)->get_arg(fr.m_idx);
|
||||
fr.m_idx++;
|
||||
n = visit(si, arg);
|
||||
if (!n)
|
||||
goto loop;
|
||||
m_args.push_back(n);
|
||||
}
|
||||
n = m_egraph.mk(e, num, m_args.c_ptr());
|
||||
attach_bool_var(si, n);
|
||||
}
|
||||
SASSERT(m_egraph.find(e));
|
||||
}
|
||||
|
||||
euf::enode* solver::visit(sat_internalizer& si, expr* e) {
|
||||
euf::enode* n = m_egraph.find(e);
|
||||
if (n)
|
||||
return n;
|
||||
if (si.is_bool_op(e)) {
|
||||
sat::literal lit = si.internalize(e);
|
||||
n = m_egraph.mk(e, 0, nullptr);
|
||||
attach_bool_var(lit.var(), lit.sign(), n);
|
||||
s().set_external(lit.var());
|
||||
return n;
|
||||
}
|
||||
if (is_app(e) && to_app(e)->get_num_args() > 0)
|
||||
return nullptr;
|
||||
n = m_egraph.mk(e, 0, nullptr);
|
||||
attach_bool_var(si, n);
|
||||
return n;
|
||||
}
|
||||
|
||||
void solver::attach_bool_var(sat_internalizer& si, euf::enode* n) {
|
||||
expr* e = n->get_owner();
|
||||
if (m.is_bool(e)) {
|
||||
sat::bool_var v = si.add_bool_var(e);
|
||||
attach_bool_var(v, false, n);
|
||||
}
|
||||
}
|
||||
|
||||
void solver::attach_bool_var(sat::bool_var v, bool sign, euf::enode* n) {
|
||||
m_var2node.reserve(v + 1);
|
||||
m_var2node[v] = euf::enode_bool_pair(n, sign);
|
||||
}
|
||||
|
||||
}
|
||||
98
src/sat/euf/euf_solver.h
Normal file
98
src/sat/euf/euf_solver.h
Normal file
|
|
@ -0,0 +1,98 @@
|
|||
/*++
|
||||
Copyright (c) 2020 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
euf_solver.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Solver plugin for EUF
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2020-08-25
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "sat/sat_extension.h"
|
||||
#include "ast/euf/euf_egraph.h"
|
||||
#include "sat/tactic/atom2bool_var.h"
|
||||
#include "sat/tactic/goal2sat.h"
|
||||
|
||||
namespace euf_sat {
|
||||
typedef sat::literal literal;
|
||||
typedef sat::ext_constraint_idx ext_constraint_idx;
|
||||
typedef sat::ext_justification_idx ext_justification_idx;
|
||||
typedef sat::literal_vector literal_vector;
|
||||
typedef sat::bool_var bool_var;
|
||||
|
||||
struct frame {
|
||||
expr* m_e;
|
||||
unsigned m_idx;
|
||||
frame(expr* e) : m_e(e), m_idx(0) {}
|
||||
};
|
||||
|
||||
class solver : public sat::extension {
|
||||
ast_manager& m;
|
||||
atom2bool_var& m_expr2var;
|
||||
euf::egraph m_egraph;
|
||||
sat::solver* m_solver;
|
||||
|
||||
euf::enode* m_true;
|
||||
euf::enode* m_false;
|
||||
svector<euf::enode_bool_pair> m_var2node;
|
||||
ptr_vector<unsigned> m_explain;
|
||||
euf::enode_vector m_args;
|
||||
svector<frame> m_stack;
|
||||
|
||||
sat::solver& s() { return *m_solver; }
|
||||
unsigned * base_ptr() { return reinterpret_cast<unsigned*>(this); }
|
||||
euf::enode* visit(sat_internalizer& si, expr* e);
|
||||
void attach_bool_var(sat_internalizer& si, euf::enode* n);
|
||||
void attach_bool_var(sat::bool_var v, bool sign, euf::enode* n);
|
||||
|
||||
public:
|
||||
solver(ast_manager& m, atom2bool_var& expr2var):
|
||||
m(m),
|
||||
m_expr2var(expr2var),
|
||||
m_egraph(m),
|
||||
m_solver(nullptr)
|
||||
{}
|
||||
|
||||
void set_solver(sat::solver* s) override { m_solver = s; }
|
||||
void set_lookahead(sat::lookahead* s) override { }
|
||||
double get_reward(literal l, ext_constraint_idx idx, sat::literal_occs_fun& occs) const override { return 0; }
|
||||
bool is_extended_binary(ext_justification_idx idx, literal_vector & r) override { return false; }
|
||||
|
||||
bool propagate(literal l, ext_constraint_idx idx) override;
|
||||
void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override;
|
||||
void asserted(literal l) override;
|
||||
sat::check_result check() override;
|
||||
void push() override;
|
||||
void pop(unsigned n) override;
|
||||
void pre_simplify() override;
|
||||
void simplify() override;
|
||||
// have a way to replace l by r in all constraints
|
||||
void clauses_modifed() override;
|
||||
lbool get_phase(bool_var v) override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
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;
|
||||
extension* copy(sat::lookahead* s, bool learned) override;
|
||||
void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) override;
|
||||
void gc() override;
|
||||
void pop_reinit() override;
|
||||
bool validate() override;
|
||||
void init_use_list(sat::ext_use_list& ul) override;
|
||||
bool is_blocked(literal l, ext_constraint_idx) override;
|
||||
bool check_model(sat::model const& m) const override;
|
||||
unsigned max_var(unsigned w) const override;
|
||||
|
||||
void internalize(sat_internalizer& si, expr* e);
|
||||
|
||||
};
|
||||
};
|
||||
|
|
@ -42,7 +42,7 @@ Notes:
|
|||
#include "tactic/generic_model_converter.h"
|
||||
#include<sstream>
|
||||
|
||||
struct goal2sat::imp {
|
||||
struct goal2sat::imp : public sat_internalizer {
|
||||
struct frame {
|
||||
app * m_t;
|
||||
unsigned m_root:1;
|
||||
|
|
@ -131,6 +131,18 @@ struct goal2sat::imp {
|
|||
return m_true;
|
||||
}
|
||||
|
||||
sat::bool_var add_bool_var(expr* t) override {
|
||||
sat::bool_var v = m_map.to_bool_var(t);
|
||||
if (v == sat::null_bool_var) {
|
||||
v = m_solver.add_var(true);
|
||||
m_map.insert(t, v);
|
||||
}
|
||||
else {
|
||||
m_solver.set_external(v);
|
||||
}
|
||||
return v;
|
||||
}
|
||||
|
||||
void convert_atom(expr * t, bool root, bool sign) {
|
||||
SASSERT(m.is_bool(t));
|
||||
sat::literal l;
|
||||
|
|
@ -149,7 +161,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
else {
|
||||
bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
|
||||
sat::bool_var v = m_solver.add_var(ext);
|
||||
v = m_solver.add_var(ext);
|
||||
m_map.insert(t, v);
|
||||
l = sat::literal(v, sign);
|
||||
TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
|
||||
|
|
@ -812,7 +824,7 @@ struct goal2sat::imp {
|
|||
}
|
||||
}
|
||||
|
||||
sat::literal internalize(expr* n) {
|
||||
sat::literal internalize(expr* n) override {
|
||||
SASSERT(m_result_stack.empty());
|
||||
process(n, false);
|
||||
SASSERT(m_result_stack.size() == 1);
|
||||
|
|
@ -820,6 +832,30 @@ struct goal2sat::imp {
|
|||
m_result_stack.reset();
|
||||
return result;
|
||||
}
|
||||
|
||||
bool is_bool_op(expr* t) const override {
|
||||
if (!is_app(t))
|
||||
return false;
|
||||
if (to_app(t)->get_family_id() == m.get_basic_family_id()) {
|
||||
switch (to_app(t)->get_decl_kind()) {
|
||||
case OP_OR:
|
||||
case OP_AND:
|
||||
case OP_TRUE:
|
||||
case OP_FALSE:
|
||||
case OP_NOT:
|
||||
return true;
|
||||
case OP_ITE:
|
||||
case OP_EQ:
|
||||
return m.is_bool(to_app(t)->get_arg(1));
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
else if (to_app(t)->get_family_id() == pb.get_family_id())
|
||||
return true;
|
||||
else
|
||||
return false;
|
||||
}
|
||||
|
||||
void process(expr * n) {
|
||||
m_result_stack.reset();
|
||||
|
|
|
|||
|
|
@ -34,6 +34,14 @@ Notes:
|
|||
#include "tactic/generic_model_converter.h"
|
||||
#include "sat/tactic/atom2bool_var.h"
|
||||
|
||||
|
||||
class sat_internalizer {
|
||||
public:
|
||||
virtual bool is_bool_op(expr* e) const = 0;
|
||||
virtual sat::literal internalize(expr* e) = 0;
|
||||
virtual sat::bool_var add_bool_var(expr* e) = 0;
|
||||
};
|
||||
|
||||
class goal2sat {
|
||||
struct imp;
|
||||
imp * m_imp;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue