mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Merge branch 'bvsls' of https://git01.codeplex.com/z3 into bvsls

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-03-20 17:20:12 +00:00
parent 041427b530 202eb7b0ef
commit 5f040e7480
3 changed files with 26 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/sls/sls_compilation_settings.h
View file

@ -43,7 +43,7 @@ Notes:
#define _RESTART_LIMIT_ 10
// 0 = initialize with all zero, 1 initialize with random value
#define _RESTART_INIT_ 0
// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid
// 0 = even intervals, 1 = pseudo luby, 2 = real luby, 3 = armin, 4 = rapid, 5 = minisat
#define _RESTART_SCHEME_ 1
// base value c for armin restart scheme using c^inner - only applies for _RESTART_SCHEME_ 3
#define _RESTART_CONST_ARMIN_ 3.0
@ -105,6 +105,10 @@ Notes:
// 0 = initialize with one, 1 = initialize with number of assertions
#define _UCT_INIT_ 1
// do we gradually reduce the touched values of _UCT_?
#define _UCT_FORGET_ 0
#define _UCT_FORGET_FACTOR_ 0.5
// shall we use addition/subtraction?
#define _USE_ADDSUB_ 1

3
src/tactic/sls/sls_tactic.cpp
View file

@ -26,7 +26,6 @@ Notes:
#include"elim_uncnstr_tactic.h"
#include"nnf_tactic.h"
#include"stopwatch.h"
#include"sls_tactic.h"
#include"sls_params.hpp"
#include"sls_engine.h"
@ -163,7 +162,7 @@ tactic * mk_preamble(ast_manager & m, params_ref const & p) {
// Andreas: It would be cool to get rid of shared top level assertions but which simplification is doing this?
//mk_ctx_simplify_tactic(m, ctx_p),
// Andreas: This one at least eliminates top level duplicates ...
mk_simplify_tactic(m),
//mk_simplify_tactic(m),
// Andreas: How does a NNF actually look like? Can it contain ITE operators?
mk_nnf_tactic(m, p));
}

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

@ -276,6 +276,20 @@ public:
}
#endif
void uct_forget(goal_ref const & g) {
expr * e;
unsigned touched_old, touched_new;
for (unsigned i = 0; i < g->size(); i++)
{
e = g->form(i);
touched_old = m_scores.find(e).touched;
touched_new = (unsigned)((touched_old - 1) * _UCT_FORGET_FACTOR_ + 1);
m_scores.find(e).touched = touched_new;
m_touched += touched_new - touched_old;
}
}
void initialize(app * n) {
// Build score table
if (!m_scores.contains(n)) {
@ -1196,6 +1210,8 @@ public:
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched)/vscore.touched);
#elif _UCT_ == 2
double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz;
#elif _UCT_ == 3
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16));
#endif
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
}
@ -1203,7 +1219,7 @@ public:
if (pos == static_cast<unsigned>(-1))
return m_temp_constants;
#if _UCT_ == 1
#if _UCT_ == 1 || _UCT_ == 3
m_scores.find(g->form(pos)).touched++;
m_touched++;
#elif _UCT_ == 2
@ -1344,6 +1360,8 @@ public:
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log((double)m_touched) / vscore.touched);
#elif _UCT_ == 2
double q = vscore.score + (_UCT_CONSTANT_ * (flip - vscore.touched)) / sz;
#elif _UCT_ == 3
double q = vscore.score + _UCT_CONSTANT_ * sqrt(log(m_touched)/vscore.touched) + (get_random_uint(16) * 0.1 / (2<<16));
#endif
if (q > max && m_mpz_manager.neq(get_value(e), m_one) ) { max = q; pos = i; }
}
@ -1351,7 +1369,7 @@ public:
if (pos == static_cast<unsigned>(-1))
return 0;
#if _UCT_ == 1
#if _UCT_ == 1 || _UCT_ == 3
m_scores.find(g->form(pos)).touched++;
m_touched++;
#elif _UCT_ == 2