mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-09-02 13:08:52 -07:00
parent 4b22434739
commit 95493f78f9
2 changed files with 26 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/sat/smt/sat_th.cpp
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Theory plugins
Theory plugin base classes
Author:
@ -26,12 +26,30 @@ namespace euf {
ctx(ctx)
{}
theory_var th_euf_solver::mk_var(enode * n) {
SASSERT(!is_attached_to_var(n));
euf::theory_var v = m_var2enode.size();
m_var2enode.push_back(n);
return v;
}
bool th_euf_solver::is_attached_to_var(enode* n) const {
theory_var v = n->get_th_var(get_id());
return v != null_theory_var && get_enode(v) == n;
}
theory_var th_euf_solver::get_th_var(expr* e) const {
return get_th_var(ctx.get_enode(e));
}
void th_euf_solver::push() {
m_var2enode_lim.push_back(m_var2enode.size());
}
void th_euf_solver::pop(unsigned num_scopes) {
unsigned new_lvl = m_var2enode_lim.size() - num_scopes;
m_var2enode.shrink(m_var2enode_lim[new_lvl]);
m_var2enode_lim.shrink(new_lvl);
}
}

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

@ -93,28 +93,17 @@ namespace euf {
euf::enode_vector m_var2enode;
unsigned_vector m_var2enode_lim;
public:
th_euf_solver(euf::solver& ctx, euf::theory_id id);
virtual ~th_euf_solver() {}
th_euf_solver(euf::solver& ctx, euf::theory_id id);
virtual euf::theory_var mk_var(enode * n) {
SASSERT(!is_attached_to_var(n));
euf::theory_var v = m_var2enode.size();
m_var2enode.push_back(n);
return v;
}
virtual theory_var mk_var(enode * n);
unsigned get_num_vars() const { return m_var2enode.size();}
enode* get_enode(theory_var v) const { return m_var2enode[v]; }
expr* get_expr(theory_var v) const { return get_enode(v)->get_owner(); }
theory_var get_th_var(enode* n) const { return n->get_th_var(get_id()); }
theory_var get_th_var(expr* e) const;
bool is_attached_to_var(enode* n) const {
theory_var v = n->get_th_var(get_id());
return v != null_theory_var && get_enode(v) == n;
}
bool is_attached_to_var(enode* n) const;
void push() override;
void pop(unsigned n) override;
};