mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

working on tab-context

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-01-24 12:50:19 -08:00
parent d3025569c2 afaef63bfa
commit 521382e37f
1 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/muz_qe/tab_context.cpp
View file

@ -171,9 +171,9 @@ namespace tb {
m_index(0), m_index(0),
m_num_vars(0), m_num_vars(0),
m_predicate_index(0), m_predicate_index(0),
m_next_rule(static_cast<unsigned>(-1)),
m_parent_rule(0), m_parent_rule(0),
m_parent_index(0), m_parent_index(0),
m_next_rule(static_cast<unsigned>(-1)),
m_ref(0) { m_ref(0) {
} }
@ -797,8 +797,7 @@ namespace tb {
m_sub2(m) {} m_sub2(m) {}
bool operator()(ref<clause>& tgt, ref<clause>& src, bool compute_subst, ref<clause>& result) { bool operator()(ref<clause>& tgt, ref<clause>& src, bool compute_subst, ref<clause>& result) {
unsigned idx = tgt->get_predicate_index(); return unify(*tgt, *src, compute_subst, result);
return new_unify(*tgt, *src, compute_subst, result);
} }
expr_ref_vector get_rule_subst(bool is_tgt) { expr_ref_vector get_rule_subst(bool is_tgt) {
@ -810,8 +809,7 @@ namespace tb {
} }
} }
bool new_unify(clause const& tgt, clause const& src, bool compute_subst, ref<clause>& result) { bool unify(clause const& tgt, clause const& src, bool compute_subst, ref<clause>& result) {
qe_lite qe(m); qe_lite qe(m);
reset(); reset();
unsigned idx = tgt.get_predicate_index(); unsigned idx = tgt.get_predicate_index();