From 75bae1b00c507dc4a85d7e9046063611b611507a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 19 Dec 2014 12:32:57 +0000 Subject: [PATCH] BV-SLS optimization Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/sls_tracker.h | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 73355197a..89ef57871 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -89,6 +89,7 @@ private: unsigned m_track_unsat; obj_map m_weights; double m_top_sum; + obj_hashtable m_temp_seen; public: sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : @@ -440,6 +441,7 @@ public: } } + m_temp_seen.reset(); for (unsigned i = 0; i < sz; i++) { expr * e = as[i]; @@ -630,7 +632,14 @@ public: app * a = to_app(n); expr * const * args = a->get_args(); for (unsigned i = 0; i < a->get_num_args(); i++) - setup_occs(args[i]); + { + expr * child = args[i]; + if (!m_temp_seen.contains(child)) + { + setup_occs(child, false); + m_temp_seen.insert(child); + } + } } else if (m_manager.is_not(n)) { @@ -638,8 +647,7 @@ public: app * a = to_app(n); SASSERT(a->get_num_args() == 1); expr * child = a->get_arg(0); - if (m_manager.is_and(child) || m_manager.is_or(child)) - NOT_IMPLEMENTED_YET(); + SASSERT(!m_manager.is_and(child) && !m_manager.is_or(child)); setup_occs(child, true); } else