mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +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 85ff954bc6
commit 168c3eb363
1 changed files with 11 additions and 3 deletions
Show stats 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;
obj_map<expr, unsigned> m_weights;
double m_top_sum;
obj_hashtable<expr> 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