mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
adding ematching engine, fixing seq_unicode
This commit is contained in:
parent
db17ae03c6
commit
680b185872
|
@ -3,6 +3,7 @@ z3_add_component(euf
|
|||
euf_enode.cpp
|
||||
euf_etable.cpp
|
||||
euf_egraph.cpp
|
||||
euf_mam.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
ast
|
||||
util
|
||||
|
|
|
@ -247,6 +247,8 @@ namespace euf {
|
|||
*/
|
||||
bool are_diseq(enode* a, enode* b) const;
|
||||
|
||||
enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) { UNREACHABLE(); return nullptr; }
|
||||
|
||||
/**
|
||||
\brief Maintain and update cursor into propagated consequences.
|
||||
The result of get_literal() is a pair (n, is_eq)
|
||||
|
@ -279,6 +281,11 @@ namespace euf {
|
|||
template <typename T>
|
||||
void explain_eq(ptr_vector<T>& justifications, enode* a, enode* b);
|
||||
enode_vector const& nodes() const { return m_nodes; }
|
||||
|
||||
ast_manager& get_manager() { return m; }
|
||||
bool is_relevant(enode* n) const { return true; } // TODO
|
||||
bool resource_limits_exceeded() const { return false; } // TODO
|
||||
|
||||
void invariant();
|
||||
void copy_from(egraph const& src, std::function<void*(void*)>& copy_justification);
|
||||
struct e_pp {
|
||||
|
|
|
@ -18,6 +18,7 @@ Author:
|
|||
#include "util/vector.h"
|
||||
#include "util/id_var_list.h"
|
||||
#include "util/lbool.h"
|
||||
#include "util/approx_set.h"
|
||||
#include "ast/ast.h"
|
||||
#include "ast/euf/euf_justification.h"
|
||||
|
||||
|
@ -60,6 +61,9 @@ namespace euf {
|
|||
th_var_list m_th_vars;
|
||||
justification m_justification;
|
||||
unsigned m_num_args{ 0 };
|
||||
signed char m_lbl_hash { -1 }; // It is different from -1, if enode is used in a pattern
|
||||
approx_set m_lbls;
|
||||
approx_set m_plbls;
|
||||
enode* m_args[0];
|
||||
|
||||
friend class enode_args;
|
||||
|
@ -138,6 +142,7 @@ namespace euf {
|
|||
lbool value() const { return m_value; }
|
||||
unsigned bool_var() const { return m_bool_var; }
|
||||
bool is_cgr() const { return this == m_cg; }
|
||||
enode* get_cg() const { return m_cg; }
|
||||
bool commutative() const { return m_commutative; }
|
||||
void mark_interpreted() { SASSERT(num_args() == 0); m_interpreted = true; }
|
||||
bool merge_enabled() const { return m_merge_enabled; }
|
||||
|
@ -183,6 +188,16 @@ namespace euf {
|
|||
unsigned get_expr_id() const { return m_expr->get_id(); }
|
||||
unsigned get_root_id() const { return m_root->m_expr->get_id(); }
|
||||
bool children_are_roots() const;
|
||||
enode* get_next() const { return m_next; }
|
||||
|
||||
bool has_lbl_hash() const { UNREACHABLE(); return false; } // TODO
|
||||
unsigned char get_lbl_hash() const { UNREACHABLE(); return 0; } // TOD0
|
||||
void set_lbl_hash(egraph& e) { UNREACHABLE(); }
|
||||
approx_set & get_lbls() { return m_lbls; }
|
||||
approx_set & get_plbls() { return m_plbls; }
|
||||
const approx_set & get_lbls() const { return m_lbls; }
|
||||
const approx_set & get_plbls() const { return m_plbls; }
|
||||
|
||||
|
||||
theory_var get_th_var(theory_id id) const { return m_th_vars.find(id); }
|
||||
theory_var get_closest_th_var(theory_id id) const;
|
||||
|
|
3968
src/ast/euf/euf_mam.cpp
Normal file
3968
src/ast/euf/euf_mam.cpp
Normal file
File diff suppressed because it is too large
Load diff
66
src/ast/euf/euf_mam.h
Normal file
66
src/ast/euf/euf_mam.h
Normal file
|
@ -0,0 +1,66 @@
|
|||
/*++
|
||||
Copyright (c) 2006 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
euf_mam.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Matching Abstract Machine
|
||||
|
||||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2007-02-13.
|
||||
Nikolaj Bjorner (nbjorner) 2021-01-22.
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "ast/ast.h"
|
||||
#include "ast/euf/euf_egraph.h"
|
||||
#include <functional>
|
||||
|
||||
namespace euf {
|
||||
|
||||
/**
|
||||
\brief Matching Abstract Machine (MAM)
|
||||
*/
|
||||
class mam {
|
||||
friend class mam_impl;
|
||||
|
||||
mam() {}
|
||||
|
||||
public:
|
||||
|
||||
static mam * mk(egraph & ctx,
|
||||
std::function<void(quantifier*, app*, unsigned, enode* const*, unsigned)>& add_instance);
|
||||
|
||||
virtual ~mam() {}
|
||||
|
||||
virtual void add_pattern(quantifier * q, app * mp) = 0;
|
||||
|
||||
virtual void push_scope() = 0;
|
||||
|
||||
virtual void pop_scope(unsigned num_scopes) = 0;
|
||||
|
||||
virtual void match() = 0;
|
||||
|
||||
virtual void rematch(bool use_irrelevant = false) = 0;
|
||||
|
||||
virtual bool has_work() const = 0;
|
||||
|
||||
virtual void add_eq_eh(enode * r1, enode * r2) = 0;
|
||||
|
||||
virtual void reset() = 0;
|
||||
|
||||
virtual std::ostream& display(std::ostream& out) = 0;
|
||||
|
||||
virtual void on_match(quantifier * q, app * pat, unsigned num_bindings, enode * const * bindings, unsigned max_generation) = 0;
|
||||
|
||||
virtual bool is_shared(enode * n) const = 0;
|
||||
|
||||
virtual bool check_missing_instances() = 0;
|
||||
};
|
||||
};
|
||||
|
|
@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation
|
|||
|
||||
Module Name:
|
||||
|
||||
a_solver.cpp
|
||||
q_solver.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
|
@ -15,18 +15,21 @@ Author:
|
|||
|
||||
--*/
|
||||
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/well_sorted.h"
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
#include "ast/normal_forms/pull_quant.h"
|
||||
#include "sat/smt/q_solver.h"
|
||||
#include "sat/smt/euf_solver.h"
|
||||
#include "sat/smt/sat_th.h"
|
||||
#include "ast/normal_forms/pull_quant.h"
|
||||
#include "ast/well_sorted.h"
|
||||
|
||||
|
||||
namespace q {
|
||||
|
||||
solver::solver(euf::solver& ctx, family_id fid) :
|
||||
th_euf_solver(ctx, ctx.get_manager().get_family_name(fid), fid),
|
||||
m_mbqi(ctx, *this)
|
||||
m_mbqi(ctx, *this),
|
||||
m_expanded(ctx.get_manager())
|
||||
{
|
||||
}
|
||||
|
||||
|
@ -34,12 +37,19 @@ namespace q {
|
|||
expr* e = bool_var2expr(l.var());
|
||||
if (!is_forall(e) && !is_exists(e))
|
||||
return;
|
||||
if (l.sign() == is_forall(e))
|
||||
add_clause(~l, skolemize(to_quantifier(e)));
|
||||
else {
|
||||
// add_clause(~l, specialize(to_quantifier(e)));
|
||||
ctx.push_vec(m_universal, l);
|
||||
quantifier* q = to_quantifier(e);
|
||||
|
||||
auto const& exp = expand(q);
|
||||
if (exp.size() > 1) {
|
||||
for (expr* e : exp)
|
||||
add_clause(~l, ctx.internalize(e, l.sign(), false, false));
|
||||
return;
|
||||
}
|
||||
|
||||
if (l.sign() == is_forall(e))
|
||||
add_clause(~l, skolemize(q));
|
||||
else
|
||||
ctx.push_vec(m_universal, l);
|
||||
m_stats.m_num_quantifier_asserts++;
|
||||
}
|
||||
|
||||
|
@ -204,4 +214,26 @@ namespace q {
|
|||
return g;
|
||||
}
|
||||
|
||||
expr_ref_vector const& solver::expand(quantifier* q) {
|
||||
m_expanded.reset();
|
||||
if (is_forall(q))
|
||||
flatten_and(q->get_expr(), m_expanded);
|
||||
else if (is_exists(q))
|
||||
flatten_or(q->get_expr(), m_expanded);
|
||||
else
|
||||
UNREACHABLE();
|
||||
|
||||
if (m_expanded.size() > 1) {
|
||||
for (unsigned i = m_expanded.size(); i-- > 0; ) {
|
||||
expr_ref tmp(m.update_quantifier(q, m_expanded.get(i)), m);
|
||||
ctx.get_rewriter()(tmp);
|
||||
m_expanded[i] = tmp;
|
||||
}
|
||||
return m_expanded;
|
||||
}
|
||||
m_expanded.reset();
|
||||
m_expanded.push_back(q);
|
||||
return m_expanded;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -3,7 +3,7 @@ Copyright (c) 2020 Microsoft Corporation
|
|||
|
||||
Module Name:
|
||||
|
||||
a_solver.h
|
||||
q_solver.h
|
||||
|
||||
Abstract:
|
||||
|
||||
|
@ -45,12 +45,15 @@ namespace q {
|
|||
sat::literal_vector m_universal;
|
||||
obj_map<sort, expr*> m_unit_table;
|
||||
mutable ptr_vector<expr> m_todo;
|
||||
expr_ref_vector m_expanded;
|
||||
|
||||
sat::literal instantiate(quantifier* q, bool negate, std::function<expr* (quantifier*, unsigned)>& mk_var);
|
||||
sat::literal skolemize(quantifier* q);
|
||||
sat::literal specialize(quantifier* q);
|
||||
void init_units();
|
||||
expr* get_unit(sort* s);
|
||||
|
||||
expr_ref_vector const& expand(quantifier* q);
|
||||
|
||||
public:
|
||||
|
||||
|
|
|
@ -27,6 +27,7 @@ namespace smt {
|
|||
m_bb(m, ctx().get_fparams())
|
||||
{
|
||||
m_enabled = gparams::get_value("unicode") == "true";
|
||||
m_bits2char = symbol("bits2char");
|
||||
}
|
||||
|
||||
struct seq_unicode::reset_bits : public trail<context> {
|
||||
|
@ -48,24 +49,52 @@ namespace smt {
|
|||
return (m_bits.size() > (unsigned)v) && !m_bits[v].empty();
|
||||
}
|
||||
|
||||
/**
|
||||
* Initialize bits associated with theory variable v.
|
||||
* add also the equality bits2char(char2bit(e, 0),..., char2bit(e, 15)) = e
|
||||
* to have congruence closure propagate equalities when the bits of two vectors
|
||||
* end up having the same values. This, together with congruence closure over char2bit
|
||||
* should ensure that two characters have the same bit-vector assignments if and only
|
||||
* if they are equal. Nevertheless, the code also checks for these constraints
|
||||
* independently and adds Ackerman axioms on demand.
|
||||
*/
|
||||
|
||||
void seq_unicode::init_bits(theory_var v) {
|
||||
if (has_bits(v))
|
||||
return;
|
||||
|
||||
expr* e = th.get_expr(v);
|
||||
m_bits.reserve(v + 1);
|
||||
auto& bits = m_bits[v];
|
||||
expr* e = th.get_expr(v);
|
||||
while ((unsigned) v >= m_ebits.size())
|
||||
m_ebits.push_back(expr_ref_vector(m));
|
||||
|
||||
ctx().push_trail(reset_bits(*this, v));
|
||||
auto& ebits = m_ebits[v];
|
||||
SASSERT(ebits.empty());
|
||||
for (unsigned i = 0; i < zstring::num_bits(); ++i)
|
||||
ebits.push_back(seq.mk_char_bit(e, i));
|
||||
ctx().internalize(ebits.c_ptr(), ebits.size(), true);
|
||||
for (expr* arg : ebits)
|
||||
bits.push_back(literal(ctx().get_bool_var(arg)));
|
||||
for (literal bit : bits)
|
||||
ctx().mark_as_relevant(bit);
|
||||
|
||||
bool is_bits2char = seq.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == m_bits2char;
|
||||
if (is_bits2char) {
|
||||
for (expr* arg : *to_app(e)) {
|
||||
ebits.push_back(arg);
|
||||
bits.push_back(literal(ctx().get_bool_var(arg)));
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < zstring::num_bits(); ++i)
|
||||
ebits.push_back(seq.mk_char_bit(e, i));
|
||||
ctx().internalize(ebits.c_ptr(), ebits.size(), true);
|
||||
for (expr* arg : ebits)
|
||||
bits.push_back(literal(ctx().get_bool_var(arg)));
|
||||
for (literal bit : bits)
|
||||
ctx().mark_as_relevant(bit);
|
||||
expr_ref bits2char(seq.mk_skolem(m_bits2char, ebits.size(), ebits.c_ptr(), m.get_sort(e)), m);
|
||||
ctx().mark_as_relevant(bits2char);
|
||||
enode* n1 = th.ensure_enode(e);
|
||||
enode* n2 = th.ensure_enode(bits2char);
|
||||
justification* j = ctx().mk_justification(ext_theory_eq_propagation_justification(th.get_id(), ctx().get_region(), 0, nullptr, 0, nullptr, n1, n2));
|
||||
ctx().assign_eq(n1, n2, eq_justification(j));
|
||||
}
|
||||
++m_stats.m_num_blast;
|
||||
}
|
||||
|
||||
|
@ -74,6 +103,8 @@ namespace smt {
|
|||
VERIFY(seq.is_char_le(term, x, y));
|
||||
theory_var v1 = ctx().get_enode(x)->get_th_var(th.get_id());
|
||||
theory_var v2 = ctx().get_enode(y)->get_th_var(th.get_id());
|
||||
init_bits(v1);
|
||||
init_bits(v2);
|
||||
auto const& b1 = get_ebits(v1);
|
||||
auto const& b2 = get_ebits(v2);
|
||||
expr_ref e(m);
|
||||
|
@ -232,6 +263,7 @@ namespace smt {
|
|||
enode* n = th.ensure_enode(seq.mk_char(zstring::max_char()));
|
||||
theory_var w = n->get_th_var(th.get_id());
|
||||
SASSERT(has_bits(w));
|
||||
init_bits(v);
|
||||
auto const& mbits = get_ebits(w);
|
||||
auto const& bits = get_ebits(v);
|
||||
expr_ref le(m);
|
||||
|
@ -247,6 +279,8 @@ namespace smt {
|
|||
literal eq = th.mk_literal(m.mk_eq(th.get_expr(v), th.get_expr(w)));
|
||||
ctx().mark_as_relevant(eq);
|
||||
literal_vector lits;
|
||||
init_bits(v);
|
||||
init_bits(w);
|
||||
auto& a = get_ebits(v);
|
||||
auto& b = get_ebits(w);
|
||||
for (unsigned i = a.size(); i-- > 0; ) {
|
||||
|
|
|
@ -44,6 +44,7 @@ namespace smt {
|
|||
bool m_enabled { false };
|
||||
bit_blaster m_bb;
|
||||
stats m_stats;
|
||||
symbol m_bits2char;
|
||||
|
||||
struct reset_bits;
|
||||
|
||||
|
|
|
@ -66,13 +66,13 @@ private:
|
|||
value * m_values;
|
||||
};
|
||||
|
||||
ckind kind() const { return static_cast<ckind>(m_kind); }
|
||||
enum ckind kind() const { return static_cast<enum ckind>(m_kind); }
|
||||
|
||||
unsigned idx() const { SASSERT(kind() != ROOT); return m_idx; }
|
||||
unsigned size() const { SASSERT(kind() == ROOT); return m_size; }
|
||||
cell * next() const { SASSERT(kind() != ROOT); return m_next; }
|
||||
value const & elem() const { SASSERT(kind() == SET || kind() == PUSH_BACK); return m_elem; }
|
||||
cell(ckind k):m_ref_count(1), m_kind(k), m_size(0), m_values(nullptr) {}
|
||||
cell(enum ckind k):m_ref_count(1), m_kind(k), m_size(0), m_values(nullptr) {}
|
||||
};
|
||||
|
||||
value_manager & m_vmanager;
|
||||
|
|
Loading…
Reference in a new issue