mirror of
https://github.com/Z3Prover/z3
synced 2025-08-31 23:34:55 +00:00
Parallel solving (#7771)
* very basic setup * ensure solve_eqs is fully disabled when smt.solve_eqs=false, #7743 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * respect smt configuration parameter in elim_unconstrained simplifier Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * indentation * add bash files for test runs * add option to selectively disable variable solving for only ground expressions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove verbose output Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix #7745 axioms for len(substr(...)) escaped due to nested rewriting * ensure atomic constraints are processed by arithmetic solver * #7739 optimization add simplification rule for at(x, offset) = "" Introducing j just postpones some rewrites that prevent useful simplifications. Z3 already uses common sub-expressions. The example highlights some opportunities for simplification, noteworthy at(..) = "". The example is solved in both versions after adding this simplification. * fix unsound len(substr) axiom Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * FreshConst is_sort (#7748) * #7750 add pre-processing simplification * Add parameter validation for selected API functions * updates to ac-plugin fix incrementality bugs by allowing destructive updates during saturation at the cost of redoing saturation after a pop. * enable passive, add check for bloom up-to-date * add top-k fixed-sized min-heap priority queue for top scoring literals * set up worker thread batch manager for multithreaded batch cubes paradigm, need to debug as I am getting segfault still * fix bug in parallel solving batch setup * fix bug * allow for internalize implies * disable pre-processing during cubing * debugging * remove default constructor * remove a bunch of string copies * Update euf_ac_plugin.cpp include reduction rules in forward simplification * Update euf_completion.cpp try out restricting scope of equalities added by instantation * Update smt_parallel.cpp Drop non-relevant units from shared structures. * process cubes as lists of individual lits * merge * Add support for Algebraic Datatypes in JavaScript/TypeScript bindings (#7734) * Initial plan * Add datatype type definitions to types.ts (work in progress) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype type definitions with working TypeScript compilation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement core datatype functionality with TypeScript compilation success Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Complete datatype implementation with full Context integration and tests Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * chipping away at the new code structure * comments * debug infinite recursion and split cubes on existing split atoms that aren't in the cube * share lemmas, learn from unsat core, try to debug a couple of things, there was a subtle bug that i have a hard time repro'ing * merge * fix #7603: race condition in Ctrl-C handling (#7755) * fix #7603: race condition in Ctrl-C handling * fix race in cancel_eh * fix build * add arithemtic saturation * add an option to register callback on quantifier instantiation Suppose a user propagator encodes axioms using quantifiers and uses E-matching for instantiation. If it wants to implement a custom priority scheme or drop some instances based on internal checks it can register a callback with quantifier instantiation * missing new closure Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add Z3_solver_propagate_on_binding to ml callback declarations Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add python file Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> * debug under defined calls Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * more untangle params Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * precalc parameters to define the eval order Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename a Python file Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add on_binding callbacks across APIs update release notes, add to Java, .Net, C++ * use jboolean in Native interface Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * register on_binding attribute Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix java build for java bindings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * avoid interferring side-effects in function calls Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove theory_str and classes that are only used by it * remove automata from python build Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove ref to theory_str Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * get the finest factorizations before project Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * rename add_lcs to add_lc Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * resolve bad bug about l2g and g2l translators using wrong global context. add some debug prints * initial attempt at dynamically switching from greedy to frugal splitting strategy in return_cubes. need to test. also there is some bug where the threads take forever to cancel? * Update RELEASE_NOTES.md * resolve bug about not translating managers correctly for the second phase of the greedy cubing, and the frugal fallback --------- Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> Signed-off-by: Lev Nachmanson <levnach@Levs-MacBook-Pro.local> Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com> Co-authored-by: humnrdble <83878671+humnrdble@users.noreply.github.com> Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt> Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Ilana Shapiro
GitHub
parent
2169364b6d
commit
6044389446
80 changed files with 474 additions and 15087 deletions
|
|
@ -46,7 +46,6 @@ z3_add_component(rewriter
|
|||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
params
|
||||
automata
|
||||
interval
|
||||
polynomial
|
||||
)
|
||||
|
|
|
|||
|
|
@ -29,8 +29,6 @@ Authors:
|
|||
#include "ast/rewriter/var_subst.h"
|
||||
#include "ast/rewriter/expr_safe_replace.h"
|
||||
#include "params/seq_rewriter_params.hpp"
|
||||
#include "math/automata/automaton.h"
|
||||
#include "math/automata/symbolic_automata_def.h"
|
||||
|
||||
|
||||
expr_ref sym_expr::accept(expr* e) {
|
||||
|
|
@ -83,320 +81,6 @@ struct display_expr1 {
|
|||
}
|
||||
};
|
||||
|
||||
class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
|
||||
ast_manager& m;
|
||||
expr_solver& m_solver;
|
||||
expr_ref m_var;
|
||||
typedef sym_expr* T;
|
||||
public:
|
||||
sym_expr_boolean_algebra(ast_manager& m, expr_solver& s):
|
||||
m(m), m_solver(s), m_var(m) {}
|
||||
|
||||
T mk_false() override {
|
||||
expr_ref fml(m.mk_false(), m);
|
||||
return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary
|
||||
}
|
||||
T mk_true() override {
|
||||
expr_ref fml(m.mk_true(), m);
|
||||
return sym_expr::mk_pred(fml, m.mk_bool_sort());
|
||||
}
|
||||
T mk_and(T x, T y) override {
|
||||
seq_util u(m);
|
||||
if (x->is_char() && y->is_char()) {
|
||||
if (x->get_char() == y->get_char()) {
|
||||
return x;
|
||||
}
|
||||
if (m.are_distinct(x->get_char(), y->get_char())) {
|
||||
expr_ref fml(m.mk_false(), m);
|
||||
return sym_expr::mk_pred(fml, x->get_sort());
|
||||
}
|
||||
}
|
||||
unsigned lo1, hi1, lo2, hi2;
|
||||
if (x->is_range() && y->is_range() &&
|
||||
u.is_const_char(x->get_lo(), lo1) && u.is_const_char(x->get_hi(), hi1) &&
|
||||
u.is_const_char(y->get_lo(), lo2) && u.is_const_char(y->get_hi(), hi2)) {
|
||||
lo1 = std::max(lo1, lo2);
|
||||
hi1 = std::min(hi1, hi2);
|
||||
if (lo1 > hi1) {
|
||||
expr_ref fml(m.mk_false(), m);
|
||||
return sym_expr::mk_pred(fml, x->get_sort());
|
||||
}
|
||||
expr_ref _start(u.mk_char(lo1), m);
|
||||
expr_ref _stop(u.mk_char(hi1), m);
|
||||
return sym_expr::mk_range(_start, _stop);
|
||||
}
|
||||
|
||||
sort* s = x->get_sort();
|
||||
if (m.is_bool(s)) s = y->get_sort();
|
||||
var_ref v(m.mk_var(0, s), m);
|
||||
expr_ref fml1 = x->accept(v);
|
||||
expr_ref fml2 = y->accept(v);
|
||||
if (m.is_true(fml1)) {
|
||||
return y;
|
||||
}
|
||||
if (m.is_true(fml2)) {
|
||||
return x;
|
||||
}
|
||||
if (fml1 == fml2) {
|
||||
return x;
|
||||
}
|
||||
if (is_complement(fml1, fml2)) {
|
||||
expr_ref ff(m.mk_false(), m);
|
||||
return sym_expr::mk_pred(ff, x->get_sort());
|
||||
}
|
||||
expr_ref fml(m);
|
||||
bool_rewriter br(m);
|
||||
br.mk_and(fml1, fml2, fml);
|
||||
return sym_expr::mk_pred(fml, x->get_sort());
|
||||
}
|
||||
|
||||
bool is_complement(expr* f1, expr* f2) {
|
||||
expr* f = nullptr;
|
||||
return
|
||||
(m.is_not(f1, f) && f == f2) ||
|
||||
(m.is_not(f2, f) && f == f1);
|
||||
}
|
||||
|
||||
T mk_or(T x, T y) override {
|
||||
if (x->is_char() && y->is_char() &&
|
||||
x->get_char() == y->get_char()) {
|
||||
return x;
|
||||
}
|
||||
if (x == y) return x;
|
||||
var_ref v(m.mk_var(0, x->get_sort()), m);
|
||||
expr_ref fml1 = x->accept(v);
|
||||
expr_ref fml2 = y->accept(v);
|
||||
if (m.is_false(fml1)) return y;
|
||||
if (m.is_false(fml2)) return x;
|
||||
bool_rewriter br(m);
|
||||
expr_ref fml(m);
|
||||
br.mk_or(fml1, fml2, fml);
|
||||
return sym_expr::mk_pred(fml, x->get_sort());
|
||||
}
|
||||
|
||||
T mk_and(unsigned sz, T const* ts) override {
|
||||
switch (sz) {
|
||||
case 0: return mk_true();
|
||||
case 1: return ts[0];
|
||||
default: {
|
||||
T t = ts[0];
|
||||
for (unsigned i = 1; i < sz; ++i) {
|
||||
t = mk_and(t, ts[i]);
|
||||
}
|
||||
return t;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
T mk_or(unsigned sz, T const* ts) override {
|
||||
switch (sz) {
|
||||
case 0: return mk_false();
|
||||
case 1: return ts[0];
|
||||
default: {
|
||||
T t = ts[0];
|
||||
for (unsigned i = 1; i < sz; ++i) {
|
||||
t = mk_or(t, ts[i]);
|
||||
}
|
||||
return t;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
lbool is_sat(T x) override {
|
||||
unsigned lo, hi;
|
||||
seq_util u(m);
|
||||
|
||||
if (x->is_char()) {
|
||||
return l_true;
|
||||
}
|
||||
if (x->is_range() && u.is_const_char(x->get_lo(), lo) && u.is_const_char(x->get_hi(), hi)) {
|
||||
return (lo <= hi) ? l_true : l_false;
|
||||
}
|
||||
if (x->is_not() && x->get_arg()->is_range() && u.is_const_char(x->get_arg()->get_lo(), lo) && 0 < lo) {
|
||||
return l_true;
|
||||
}
|
||||
if (!m_var || m_var->get_sort() != x->get_sort()) {
|
||||
m_var = m.mk_fresh_const("x", x->get_sort());
|
||||
}
|
||||
expr_ref fml = x->accept(m_var);
|
||||
if (m.is_true(fml)) {
|
||||
return l_true;
|
||||
}
|
||||
if (m.is_false(fml)) {
|
||||
return l_false;
|
||||
}
|
||||
return m_solver.check_sat(fml);
|
||||
}
|
||||
|
||||
T mk_not(T x) override {
|
||||
return sym_expr::mk_not(m, x);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
re2automaton::re2automaton(ast_manager& m): m(m), u(m), m_ba(nullptr), m_sa(nullptr) {}
|
||||
|
||||
void re2automaton::set_solver(expr_solver* solver) {
|
||||
m_solver = solver;
|
||||
m_ba = alloc(sym_expr_boolean_algebra, m, *solver);
|
||||
m_sa = alloc(symbolic_automata_t, sm, *m_ba.get());
|
||||
}
|
||||
|
||||
eautomaton* re2automaton::mk_product(eautomaton* a1, eautomaton* a2) {
|
||||
return m_sa->mk_product(*a1, *a2);
|
||||
}
|
||||
|
||||
eautomaton* re2automaton::operator()(expr* e) {
|
||||
eautomaton* r = re2aut(e);
|
||||
if (r) {
|
||||
r->compress();
|
||||
bool_rewriter br(m);
|
||||
TRACE(seq, display_expr1 disp(m); r->display(tout << mk_pp(e, m) << " -->\n", disp););
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
bool re2automaton::is_unit_char(expr* e, expr_ref& ch) {
|
||||
zstring s;
|
||||
expr* c = nullptr;
|
||||
if (u.str.is_string(e, s) && s.length() == 1) {
|
||||
ch = u.mk_char(s[0]);
|
||||
return true;
|
||||
}
|
||||
if (u.str.is_unit(e, c)) {
|
||||
ch = c;
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
eautomaton* re2automaton::re2aut(expr* e) {
|
||||
SASSERT(u.is_re(e));
|
||||
expr *e0, *e1, *e2;
|
||||
scoped_ptr<eautomaton> a, b;
|
||||
unsigned lo, hi;
|
||||
zstring s1, s2;
|
||||
if (u.re.is_to_re(e, e1)) {
|
||||
return seq2aut(e1);
|
||||
}
|
||||
else if (u.re.is_concat(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
|
||||
return eautomaton::mk_concat(*a, *b);
|
||||
}
|
||||
else if (u.re.is_union(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
|
||||
return eautomaton::mk_union(*a, *b);
|
||||
}
|
||||
else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
|
||||
a->add_final_to_init_moves();
|
||||
a->add_init_to_final_states();
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
|
||||
a->add_final_to_init_moves();
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_opt(e, e1) && (a = re2aut(e1))) {
|
||||
a = eautomaton::mk_opt(*a);
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_range(e, e1, e2)) {
|
||||
expr_ref _start(m), _stop(m);
|
||||
if (is_unit_char(e1, _start) &&
|
||||
is_unit_char(e2, _stop)) {
|
||||
TRACE(seq, tout << "Range: " << _start << " " << _stop << "\n";);
|
||||
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
|
||||
return a.detach();
|
||||
}
|
||||
else {
|
||||
// if e1/e2 are not unit, (re.range e1 e2) is defined to be the empty language
|
||||
return alloc(eautomaton, sm);
|
||||
}
|
||||
}
|
||||
else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
|
||||
return m_sa->mk_complement(*a);
|
||||
}
|
||||
else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
|
||||
scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
|
||||
b = eautomaton::mk_epsilon(sm);
|
||||
while (hi > lo) {
|
||||
scoped_ptr<eautomaton> c = eautomaton::mk_concat(*a, *b);
|
||||
b = eautomaton::mk_union(*eps, *c);
|
||||
--hi;
|
||||
}
|
||||
while (lo > 0) {
|
||||
b = eautomaton::mk_concat(*a, *b);
|
||||
--lo;
|
||||
}
|
||||
return b.detach();
|
||||
}
|
||||
else if (u.re.is_loop(e, e1, lo) && (a = re2aut(e1))) {
|
||||
b = eautomaton::clone(*a);
|
||||
b->add_final_to_init_moves();
|
||||
b->add_init_to_final_states();
|
||||
while (lo > 0) {
|
||||
b = eautomaton::mk_concat(*a, *b);
|
||||
--lo;
|
||||
}
|
||||
return b.detach();
|
||||
}
|
||||
else if (u.re.is_empty(e)) {
|
||||
return alloc(eautomaton, sm);
|
||||
}
|
||||
else if (u.re.is_full_seq(e)) {
|
||||
expr_ref tt(m.mk_true(), m);
|
||||
sort *seq_s = nullptr, *char_s = nullptr;
|
||||
VERIFY (u.is_re(e->get_sort(), seq_s));
|
||||
VERIFY (u.is_seq(seq_s, char_s));
|
||||
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
|
||||
return eautomaton::mk_loop(sm, _true);
|
||||
}
|
||||
else if (u.re.is_full_char(e)) {
|
||||
expr_ref tt(m.mk_true(), m);
|
||||
sort *seq_s = nullptr, *char_s = nullptr;
|
||||
VERIFY (u.is_re(e->get_sort(), seq_s));
|
||||
VERIFY (u.is_seq(seq_s, char_s));
|
||||
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
|
||||
a = alloc(eautomaton, sm, _true);
|
||||
return a.detach();
|
||||
}
|
||||
else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
|
||||
eautomaton* r = m_sa->mk_product(*a, *b);
|
||||
TRACE(seq, display_expr1 disp(m); a->display(tout << "a:", disp); b->display(tout << "b:", disp); r->display(tout << "intersection:", disp););
|
||||
return r;
|
||||
}
|
||||
else {
|
||||
TRACE(seq, tout << "not handled " << mk_pp(e, m) << "\n";);
|
||||
}
|
||||
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
eautomaton* re2automaton::seq2aut(expr* e) {
|
||||
SASSERT(u.is_seq(e));
|
||||
zstring s;
|
||||
expr* e1, *e2;
|
||||
scoped_ptr<eautomaton> a, b;
|
||||
if (u.str.is_concat(e, e1, e2) && (a = seq2aut(e1)) && (b = seq2aut(e2))) {
|
||||
return eautomaton::mk_concat(*a, *b);
|
||||
}
|
||||
else if (u.str.is_unit(e, e1)) {
|
||||
return alloc(eautomaton, sm, sym_expr::mk_char(m, e1));
|
||||
}
|
||||
else if (u.str.is_empty(e)) {
|
||||
return eautomaton::mk_epsilon(sm);
|
||||
}
|
||||
else if (u.str.is_string(e, s)) {
|
||||
unsigned init = 0;
|
||||
eautomaton::moves mvs;
|
||||
unsigned_vector final;
|
||||
final.push_back(s.length());
|
||||
for (unsigned k = 0; k < s.length(); ++k) {
|
||||
// reference count?
|
||||
mvs.push_back(eautomaton::move(sm, k, k+1, sym_expr::mk_char(m, u.str.mk_char(s, k))));
|
||||
}
|
||||
return alloc(eautomaton, sm, init, final, mvs);
|
||||
}
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
void seq_rewriter::updt_params(params_ref const & p) {
|
||||
seq_rewriter_params sp(p);
|
||||
|
|
@ -2721,46 +2405,6 @@ void seq_rewriter::add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned
|
|||
|
||||
}
|
||||
|
||||
bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
|
||||
seq.reset();
|
||||
unsigned state = aut.init();
|
||||
uint_set visited;
|
||||
eautomaton::moves mvs;
|
||||
unsigned_vector states;
|
||||
aut.get_epsilon_closure(state, states);
|
||||
bool has_final = false;
|
||||
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
|
||||
has_final = aut.is_final_state(states[i]);
|
||||
}
|
||||
aut.get_moves_from(state, mvs, true);
|
||||
while (!has_final) {
|
||||
if (mvs.size() != 1) {
|
||||
return false;
|
||||
}
|
||||
if (visited.contains(state)) {
|
||||
return false;
|
||||
}
|
||||
if (aut.is_final_state(mvs[0].src())) {
|
||||
return false;
|
||||
}
|
||||
visited.insert(state);
|
||||
sym_expr* t = mvs[0].t();
|
||||
if (!t || !t->is_char()) {
|
||||
return false;
|
||||
}
|
||||
seq.push_back(str().mk_unit(t->get_char()));
|
||||
state = mvs[0].dst();
|
||||
mvs.reset();
|
||||
aut.get_moves_from(state, mvs, true);
|
||||
states.reset();
|
||||
has_final = false;
|
||||
aut.get_epsilon_closure(state, states);
|
||||
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
|
||||
has_final = aut.is_final_state(states[i]);
|
||||
}
|
||||
}
|
||||
return mvs.empty();
|
||||
}
|
||||
|
||||
bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
|
||||
seq.reset();
|
||||
|
|
|
|||
|
|
@ -26,8 +26,6 @@ Notes:
|
|||
#include "util/params.h"
|
||||
#include "util/lbool.h"
|
||||
#include "util/sign.h"
|
||||
#include "math/automata/automaton.h"
|
||||
#include "math/automata/symbolic_automata.h"
|
||||
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, expr_ref_pair_vector const& es) {
|
||||
|
|
@ -81,33 +79,15 @@ public:
|
|||
void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
|
||||
};
|
||||
|
||||
#if 0
|
||||
|
||||
class expr_solver {
|
||||
public:
|
||||
virtual ~expr_solver() = default;
|
||||
virtual lbool check_sat(expr* e) = 0;
|
||||
};
|
||||
#endif
|
||||
|
||||
typedef automaton<sym_expr, sym_expr_manager> eautomaton;
|
||||
class re2automaton {
|
||||
typedef boolean_algebra<sym_expr*> boolean_algebra_t;
|
||||
typedef symbolic_automata<sym_expr, sym_expr_manager> symbolic_automata_t;
|
||||
ast_manager& m;
|
||||
sym_expr_manager sm;
|
||||
seq_util u;
|
||||
scoped_ptr<expr_solver> m_solver;
|
||||
scoped_ptr<boolean_algebra_t> m_ba;
|
||||
scoped_ptr<symbolic_automata_t> m_sa;
|
||||
|
||||
bool is_unit_char(expr* e, expr_ref& ch);
|
||||
eautomaton* re2aut(expr* e);
|
||||
eautomaton* seq2aut(expr* e);
|
||||
public:
|
||||
re2automaton(ast_manager& m);
|
||||
eautomaton* operator()(expr* e);
|
||||
void set_solver(expr_solver* solver);
|
||||
bool has_solver() const { return m_solver; }
|
||||
eautomaton* mk_product(eautomaton *a1, eautomaton *a2);
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Cheap rewrite rules for seq constraints
|
||||
|
|
@ -150,7 +130,7 @@ class seq_rewriter {
|
|||
seq_util m_util;
|
||||
arith_util m_autil;
|
||||
bool_rewriter m_br;
|
||||
re2automaton m_re2aut;
|
||||
// re2automaton m_re2aut;
|
||||
op_cache m_op_cache;
|
||||
expr_ref_vector m_es, m_lhs, m_rhs;
|
||||
bool m_coalesce_chars;
|
||||
|
|
@ -340,7 +320,7 @@ class seq_rewriter {
|
|||
|
||||
void add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond);
|
||||
bool is_sequence(expr* e, expr_ref_vector& seq);
|
||||
bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
|
||||
// bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
|
||||
bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
|
||||
bool reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
|
||||
bool reduce_back(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
|
||||
|
|
@ -360,7 +340,8 @@ class seq_rewriter {
|
|||
|
||||
public:
|
||||
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
|
||||
m_util(m), m_autil(m), m_br(m, p), m_re2aut(m), m_op_cache(m), m_es(m),
|
||||
m_util(m), m_autil(m), m_br(m, p), // m_re2aut(m),
|
||||
m_op_cache(m), m_es(m),
|
||||
m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
|
||||
}
|
||||
ast_manager & m() const { return m_util.get_manager(); }
|
||||
|
|
@ -371,8 +352,6 @@ public:
|
|||
void updt_params(params_ref const & p);
|
||||
static void get_param_descrs(param_descrs & r);
|
||||
|
||||
void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
|
||||
bool has_solver() { return m_re2aut.has_solver(); }
|
||||
|
||||
bool coalesce_chars() const { return m_coalesce_chars; }
|
||||
|
||||
|
|
|
|||
|
|
@ -933,9 +933,6 @@ struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
|
|||
return m_cfg.mk_eq(a, b);
|
||||
}
|
||||
|
||||
void set_solver(expr_solver* solver) {
|
||||
m_cfg.m_seq_rw.set_solver(solver);
|
||||
}
|
||||
};
|
||||
|
||||
th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
|
||||
|
|
@ -1057,10 +1054,6 @@ expr_ref th_rewriter::mk_eq(expr* a, expr* b) {
|
|||
return m_imp->mk_eq(a, b);
|
||||
}
|
||||
|
||||
void th_rewriter::set_solver(expr_solver* solver) {
|
||||
m_imp->set_solver(solver);
|
||||
}
|
||||
|
||||
|
||||
bool th_rewriter::reduce_quantifier(quantifier * old_q,
|
||||
expr * new_body,
|
||||
|
|
|
|||
|
|
@ -74,7 +74,6 @@ public:
|
|||
expr_dependency * get_used_dependencies();
|
||||
void reset_used_dependencies();
|
||||
|
||||
void set_solver(expr_solver* solver);
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -253,10 +253,14 @@ namespace euf {
|
|||
auto n = m_egraph.find(t);
|
||||
if (!n)
|
||||
return;
|
||||
ptr_vector<expr> args;
|
||||
expr_ref_vector args(m);
|
||||
expr_mark visited;
|
||||
for (auto s : enode_class(n)) {
|
||||
expr_ref r(s->get_expr(), m);
|
||||
m_rewriter(r);
|
||||
if (visited.is_marked(r))
|
||||
continue;
|
||||
visited.mark(r);
|
||||
args.push_back(r);
|
||||
}
|
||||
expr_ref cong(m);
|
||||
|
|
@ -288,8 +292,10 @@ namespace euf {
|
|||
propagate_rules();
|
||||
propagate_closures();
|
||||
IF_VERBOSE(11, verbose_stream() << "propagate " << m_stats.m_num_instances << "\n");
|
||||
if (!should_stop())
|
||||
propagate_arithmetic();
|
||||
if (!m_should_propagate && !should_stop())
|
||||
propagate_all_rules();
|
||||
propagate_all_rules();
|
||||
}
|
||||
TRACE(euf, m_egraph.display(tout));
|
||||
}
|
||||
|
|
@ -310,16 +316,14 @@ namespace euf {
|
|||
for (auto* ch : enode_args(n))
|
||||
m_nodes_to_canonize.push_back(ch);
|
||||
};
|
||||
expr* x = nullptr, * y = nullptr;
|
||||
expr* x = nullptr, * y = nullptr, * nf = nullptr;
|
||||
if (m.is_eq(f, x, y)) {
|
||||
expr_ref x1(x, m);
|
||||
expr_ref y1(y, m);
|
||||
m_rewriter(x1);
|
||||
m_rewriter(y1);
|
||||
|
||||
add_quantifiers(x1);
|
||||
add_quantifiers(x);
|
||||
add_quantifiers(y1);
|
||||
enode* a = mk_enode(x1);
|
||||
enode* a = mk_enode(x);
|
||||
enode* b = mk_enode(y1);
|
||||
|
||||
if (a->get_root() == b->get_root())
|
||||
|
|
@ -331,42 +335,28 @@ namespace euf {
|
|||
m_egraph.merge(a, b, to_ptr(push_pr_dep(pr, d)));
|
||||
m_egraph.propagate();
|
||||
m_should_propagate = true;
|
||||
|
||||
#if 0
|
||||
auto a1 = mk_enode(x);
|
||||
auto b1 = mk_enode(y);
|
||||
|
||||
if (a->get_root() != a1->get_root()) {
|
||||
add_children(a1);;
|
||||
m_egraph.merge(a, a1, nullptr);
|
||||
m_egraph.propagate();
|
||||
}
|
||||
|
||||
if (b->get_root() != b1->get_root()) {
|
||||
add_children(b1);
|
||||
m_egraph.merge(b, b1, nullptr);
|
||||
m_egraph.propagate();
|
||||
}
|
||||
#endif
|
||||
|
||||
if (m_side_condition_solver && a->get_root() != b->get_root())
|
||||
m_side_condition_solver->add_constraint(f, pr, d);
|
||||
IF_VERBOSE(1, verbose_stream() << "eq: " << a->get_root_id() << " " << b->get_root_id() << " "
|
||||
<< x1 << " == " << y1 << "\n");
|
||||
<< mk_pp(x, m) << " == " << y1 << "\n");
|
||||
}
|
||||
else if (m.is_not(f, f)) {
|
||||
enode* n = mk_enode(f);
|
||||
else if (m.is_not(f, nf)) {
|
||||
expr_ref f1(nf, m);
|
||||
m_rewriter(f1);
|
||||
enode* n = mk_enode(f1);
|
||||
if (m.is_false(n->get_root()->get_expr()))
|
||||
return;
|
||||
add_quantifiers(f);
|
||||
add_quantifiers(f1);
|
||||
auto n_false = mk_enode(m.mk_false());
|
||||
auto j = to_ptr(push_pr_dep(pr, d));
|
||||
m_egraph.new_diseq(n, j);
|
||||
m_egraph.merge(n, n_false, j);
|
||||
m_egraph.propagate();
|
||||
add_children(n);
|
||||
m_should_propagate = true;
|
||||
if (m_side_condition_solver)
|
||||
m_side_condition_solver->add_constraint(f, pr, d);
|
||||
IF_VERBOSE(1, verbose_stream() << "not: " << mk_pp(f, m) << "\n");
|
||||
IF_VERBOSE(1, verbose_stream() << "not: " << nf << "\n");
|
||||
}
|
||||
else {
|
||||
enode* n = mk_enode(f);
|
||||
|
|
@ -631,6 +621,88 @@ namespace euf {
|
|||
}
|
||||
}
|
||||
|
||||
//
|
||||
// extract shared arithmetic terms T
|
||||
// extract shared variables V
|
||||
// add t = rewriter(t) to E-graph
|
||||
// solve for V by solver producing theta
|
||||
// add theta to E-graph
|
||||
// add theta to canonize (?)
|
||||
//
|
||||
void completion::propagate_arithmetic() {
|
||||
ptr_vector<expr> shared_terms, shared_vars;
|
||||
expr_mark visited;
|
||||
arith_util a(m);
|
||||
bool merged = false;
|
||||
for (auto n : m_egraph.nodes()) {
|
||||
expr* e = n->get_expr();
|
||||
if (!is_app(e))
|
||||
continue;
|
||||
app* t = to_app(e);
|
||||
bool is_arith = a.is_arith_expr(t);
|
||||
for (auto arg : *t) {
|
||||
bool is_arith_arg = a.is_arith_expr(arg);
|
||||
if (is_arith_arg == is_arith)
|
||||
continue;
|
||||
if (visited.is_marked(arg))
|
||||
continue;
|
||||
visited.mark(arg);
|
||||
if (is_arith_arg)
|
||||
shared_terms.push_back(arg);
|
||||
else
|
||||
shared_vars.push_back(arg);
|
||||
}
|
||||
}
|
||||
for (auto t : shared_terms) {
|
||||
auto tn = m_egraph.find(t);
|
||||
|
||||
if (!tn)
|
||||
continue;
|
||||
expr_ref r(t, m);
|
||||
m_rewriter(r);
|
||||
if (r == t)
|
||||
continue;
|
||||
auto n = m_egraph.find(t);
|
||||
auto t_root = tn->get_root();
|
||||
if (n && n->get_root() == t_root)
|
||||
continue;
|
||||
|
||||
if (!n)
|
||||
n = mk_enode(r);
|
||||
TRACE(euf_completion, tout << "propagate-arith: " << mk_pp(t, m) << " -> " << r << "\n");
|
||||
|
||||
m_egraph.merge(tn, n, nullptr);
|
||||
merged = true;
|
||||
}
|
||||
visited.reset();
|
||||
for (auto v : shared_vars) {
|
||||
if (visited.is_marked(v))
|
||||
continue;
|
||||
visited.mark(v);
|
||||
vector<side_condition_solver::solution> sol;
|
||||
expr_ref term(m), guard(m);
|
||||
sol.push_back({ v, term, guard });
|
||||
m_side_condition_solver->solve_for(sol);
|
||||
for (auto [v, t, g] : sol) {
|
||||
if (!t)
|
||||
continue;
|
||||
visited.mark(v);
|
||||
auto a = mk_enode(v);
|
||||
auto b = mk_enode(t);
|
||||
if (a->get_root() == b->get_root())
|
||||
continue;
|
||||
TRACE(euf_completion, tout << "propagate-arith: " << m_egraph.bpp(a) << " -> " << m_egraph.bpp(b) << "\n");
|
||||
IF_VERBOSE(1, verbose_stream() << "propagate-arith: " << m_egraph.bpp(a) << " -> " << m_egraph.bpp(b) << "\n");
|
||||
m_egraph.merge(a, b, nullptr); // TODO guard justifies reason.
|
||||
merged = true;
|
||||
}
|
||||
}
|
||||
if (merged) {
|
||||
m_egraph.propagate();
|
||||
m_should_propagate = true;
|
||||
}
|
||||
}
|
||||
|
||||
void completion::propagate_closures() {
|
||||
for (auto [q, clos] : m_closures) {
|
||||
expr* body = clos.second;
|
||||
|
|
|
|||
|
|
@ -187,6 +187,7 @@ namespace euf {
|
|||
expr_ref get_canonical(quantifier* q, proof_ref& pr, expr_dependency_ref& d);
|
||||
obj_map<quantifier, std::pair<ptr_vector<expr>, expr*>> m_closures;
|
||||
|
||||
void propagate_arithmetic();
|
||||
expr_dependency* explain_eq(enode* a, enode* b);
|
||||
proof_ref prove_eq(enode* a, enode* b);
|
||||
proof_ref prove_conflict();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue