From 3fa81d65270731290a4e03293d92eeaaa1a38469 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 13 Nov 2022 13:25:19 -0800
Subject: [PATCH] bug fixes to elim-uncnstr2 tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/simplifiers/elim_unconstrained.cpp | 36 ++++++++++++++--------
src/ast/simplifiers/elim_unconstrained.h | 12 +++-----
2 files changed, 28 insertions(+), 20 deletions(-)
diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 94201dde7..caeaf2958 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -55,6 +55,12 @@ elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fml
m_inverter.set_is_var(is_var);
}
+bool elim_unconstrained::is_var_lt(int v1, int v2) const {
+ node const& n1 = get_node(v1);
+ node const& n2 = get_node(v2);
+ return n1.m_refcount < n2.m_refcount;
+}
+
void elim_unconstrained::eliminate() {
@@ -62,34 +68,39 @@ void elim_unconstrained::eliminate() {
expr_ref r(m), side_cond(m);
int v = m_heap.erase_min();
node& n = get_node(v);
- IF_VERBOSE(11, verbose_stream() << mk_pp(n.m_orig, m) << " @ " << n.m_refcount << "\n");
+ IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " @ " << n.m_refcount << "\n");
if (n.m_refcount == 0)
continue;
if (n.m_refcount > 1)
return;
- if (n.m_parents.empty())
+ if (n.m_parents.empty()) {
+ --n.m_refcount;
continue;
+ }
expr* e = get_parent(v);
for (expr* p : n.m_parents)
- IF_VERBOSE(11, verbose_stream() << "parent " << mk_pp(p, m) << "\n");
- if (!is_app(e))
- continue;
- if (!is_ground(e))
+ IF_VERBOSE(11, verbose_stream() << "parent " << mk_bounded_pp(p, m) << "\n");
+ if (!e || !is_app(e) || !is_ground(e)) {
+ --n.m_refcount;
continue;
+ }
app* t = to_app(e);
m_args.reset();
for (expr* arg : *to_app(t))
m_args.push_back(get_node(arg).m_term);
- if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond))
+ if (!m_inverter(t->get_decl(), m_args.size(), m_args.data(), r, side_cond)) {
+ --n.m_refcount;
continue;
+ }
+ --n.m_refcount;
SASSERT(r->get_sort() == t->get_sort());
m_stats.m_num_eliminated++;
n.m_refcount = 0;
SASSERT(r);
- m_trail.push_back(r);
gc(e);
+ m_root.setx(r->get_id(), e->get_id(), UINT_MAX);
get_node(e).m_term = r;
get_node(e).m_refcount++;
IF_VERBOSE(11, verbose_stream() << mk_pp(e, m) << "\n");
@@ -107,10 +118,6 @@ expr* elim_unconstrained::get_parent(unsigned n) const {
for (expr* p : get_node(n).m_parents)
if (get_node(p).m_refcount > 0 && get_node(p).m_term == get_node(p).m_orig)
return p;
- IF_VERBOSE(0, verbose_stream() << "term " << mk_pp(get_node(n).m_term, m) << "\n");
- for (expr* p : get_node(n).m_parents)
- IF_VERBOSE(0, verbose_stream() << "parent " << mk_pp(p, m) << "\n");
- UNREACHABLE();
return nullptr;
}
/**
@@ -123,6 +130,7 @@ void elim_unconstrained::init_nodes() {
m_trail.append(terms);
m_heap.reset();
m_frozen.reset();
+ m_root.reset();
// initialize nodes for terms in the original goal
init_terms(terms);
@@ -159,11 +167,13 @@ void elim_unconstrained::init_terms(expr_ref_vector const& terms) {
m_nodes.reserve(max_id + 1);
m_heap.reserve(max_id + 1);
+ m_root.reserve(max_id + 1, UINT_MAX);
for (expr* e : subterms_postorder::all(terms)) {
+ m_root.setx(e->get_id(), e->get_id(), UINT_MAX);
node& n = get_node(e);
if (n.m_term)
- continue;
+ continue;
n.m_orig = e;
n.m_term = e;
n.m_refcount = 0;
diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h
index 67d64027b..964c56244 100644
--- a/src/ast/simplifiers/elim_unconstrained.h
+++ b/src/ast/simplifiers/elim_unconstrained.h
@@ -32,7 +32,7 @@ class elim_unconstrained : public dependent_expr_simplifier {
elim_unconstrained& s;
var_lt(elim_unconstrained& s) : s(s) {}
bool operator()(int v1, int v2) const {
- return s.get_node(v1).m_refcount < s.get_node(v2).m_refcount;
+ return s.is_var_lt(v1, v2);
}
};
struct stats {
@@ -47,20 +47,18 @@ class elim_unconstrained : public dependent_expr_simplifier {
ptr_vector<expr> m_args;
expr_mark m_frozen;
stats m_stats;
+ unsigned_vector m_root;
- bool operator()(int v1, int v2) const { return get_node(v1).m_refcount < get_node(v2).m_refcount; }
-
+ bool is_var_lt(int v1, int v2) const;
node& get_node(unsigned n) { return m_nodes[n]; }
node const& get_node(unsigned n) const { return m_nodes[n]; }
- node& get_node(expr* t) { return m_nodes[t->get_id()]; }
- node const& get_node(expr* t) const { return m_nodes[t->get_id()]; }
+ node& get_node(expr* t) { return m_nodes[m_root[t->get_id()]]; }
+ node const& get_node(expr* t) const { return m_nodes[m_root[t->get_id()]]; }
unsigned get_refcount(expr* t) const { return get_node(t).m_refcount; }
void inc_ref(expr* t) { ++get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.increased(t->get_id()); }
void dec_ref(expr* t) { --get_node(t).m_refcount; if (is_uninterp_const(t)) m_heap.decreased(t->get_id()); }
void gc(expr* t);
expr* get_parent(unsigned n) const;
- void init_refcounts();
- void dec_refcounts(expr* t);
void init_terms(expr_ref_vector const& terms);
void init_nodes();
void eliminate();