mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 08:23:17 +00:00
Code Activity

BV-SLS optimization

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-19 12:32:57 +00:00
parent 6b37b847a0
commit 75bae1b00c
1 changed files with 11 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/tactic/sls/sls_tracker.h
View file

@ -89,6 +89,7 @@ private:
unsigned m_track_unsat; unsigned m_track_unsat;
obj_map<expr, unsigned> m_weights; obj_map<expr, unsigned> m_weights;
double m_top_sum; double m_top_sum;
obj_hashtable<expr> m_temp_seen;
public: public:
sls_tracker(ast_manager & m, bv_util & bvu, unsynch_mpz_manager & mm, powers & p) : 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++) for (unsigned i = 0; i < sz; i++)
{ {
expr * e = as[i]; expr * e = as[i];
@ -630,7 +632,14 @@ public:
app * a = to_app(n); app * a = to_app(n);
expr * const * args = a->get_args(); expr * const * args = a->get_args();
for (unsigned i = 0; i < a->get_num_args(); i++) 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)) else if (m_manager.is_not(n))
{ {
@ -638,8 +647,7 @@ public:
app * a = to_app(n); app * a = to_app(n);
SASSERT(a->get_num_args() == 1); SASSERT(a->get_num_args() == 1);
expr * child = a->get_arg(0); expr * child = a->get_arg(0);
if (m_manager.is_and(child) || m_manager.is_or(child)) SASSERT(!m_manager.is_and(child) && !m_manager.is_or(child));
NOT_IMPLEMENTED_YET();
setup_occs(child, true); setup_occs(child, true);
} }
else else