mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

redo bindings/fingerprints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-05 10:15:56 -07:00
parent 281fb67d88
commit 33f4e65fa9
6 changed files with 145 additions and 180 deletions
Download patch file Download diff file Expand all files Collapse all files

87
src/sat/smt/q_clause.h
View file

@ -22,6 +22,7 @@ Author:
#include "ast/euf/euf_enode.h"
#include "sat/smt/euf_solver.h"
namespace q {
struct lit {
@ -35,14 +36,40 @@ namespace q {
std::ostream& display(std::ostream& out) const;
};
struct binding;
struct clause {
unsigned m_index;
vector<lit> m_lits;
quantifier_ref m_q;
unsigned m_watch = 0;
sat::literal m_literal = sat::null_literal;
q::quantifier_stat* m_stat = nullptr;
binding* m_bindings = nullptr;
clause(ast_manager& m, unsigned idx) : m_index(idx), m_q(m) {}
std::ostream& display(euf::solver& ctx, std::ostream& out) const;
lit const& operator[](unsigned i) const { return m_lits[i]; }
lit& operator[](unsigned i) { return m_lits[i]; }
unsigned size() const { return m_lits.size(); }
unsigned num_decls() const { return m_q->get_num_decls(); }
unsigned index() const { return m_index; }
quantifier* q() const { return m_q; }
};
struct binding : public dll_base<binding> {
clause* c;
app* m_pattern;
unsigned m_max_generation;
unsigned m_min_top_generation;
unsigned m_max_top_generation;
euf::enode* m_nodes[0];
binding(app* pat, unsigned max_generation, unsigned min_top, unsigned max_top):
binding(clause& c, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top):
c(&c),
m_pattern(pat),
m_max_generation(max_generation),
m_min_top_generation(min_top),
@ -53,29 +80,49 @@ namespace q {
euf::enode* operator[](unsigned i) const { return m_nodes[i]; }
std::ostream& display(euf::solver& ctx, unsigned num_nodes, std::ostream& out) const;
unsigned size() const { return c->num_decls(); }
quantifier* q() const { return c->m_q; }
bool eq(binding const& other) const {
if (q() != other.q())
return false;
for (unsigned i = size(); i-- > 0; )
if ((*this)[i] != other[i])
return false;
return true;
}
};
struct clause {
unsigned m_index;
vector<lit> m_lits;
quantifier_ref m_q;
unsigned m_watch = 0;
sat::literal m_literal = sat::null_literal;
q::quantifier_stat* m_stat = nullptr;
binding* m_bindings = nullptr;
clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {}
std::ostream& display(euf::solver& ctx, std::ostream& out) const;
lit const& operator[](unsigned i) const { return m_lits[i]; }
lit& operator[](unsigned i) { return m_lits[i]; }
unsigned size() const { return m_lits.size(); }
unsigned num_decls() const { return m_q->get_num_decls(); }
unsigned index() const { return m_index; }
quantifier* q() const { return m_q; }
struct binding_khasher {
unsigned operator()(binding const* f) const { return f->q()->get_id(); }
};
struct binding_chasher {
unsigned operator()(binding const* f, unsigned idx) const { return f->m_nodes[idx]->hash(); }
};
struct binding_hash_proc {
unsigned operator()(binding const* f) const {
return get_composite_hash<binding*, binding_khasher, binding_chasher>(const_cast<binding*>(f), f->size());
}
};
struct binding_eq_proc {
bool operator()(binding const* a, binding const* b) const { return a->eq(*b); }
};
typedef ptr_hashtable<binding, binding_hash_proc, binding_eq_proc> bindings;
inline std::ostream& operator<<(std::ostream& out, binding const& f) {
out << "[fp " << f.q()->get_id() << ":";
for (unsigned i = 0; i < f.size(); ++i)
out << " " << f[i]->get_expr_id();
return out << "]";
}
struct justification {
expr* m_lhs, *m_rhs;
bool m_sign;