mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

BVSLS comments

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-04-25 17:17:47 +01:00
parent 7d18a17bb3
commit 992d150b81
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/sls/sls_params.pyg
View file

@ -19,7 +19,7 @@ def_module_params('sls',
('restart_base', UINT, 100, 'base restart interval given by moves per run'),
('restart_init', BOOL, 0, 'initialize to 0 or random value (= 1) after restart'),
('early_prune', BOOL, 1, 'use early pruning for score prediction'),
('random_offset', BOOL, 1, 'use random offset vor candidate evaluation'),
('random_offset', BOOL, 1, 'use random offset for candidate evaluation'),
('rescore', BOOL, 1, 'rescore/normalize top-level score every base restart interval'),
('track_unsat', BOOL, 0, 'keep a list of unsat assertions as done in SAT - currently disabled internally'),
('random_seed', UINT, 0, 'random seed')

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

@ -831,7 +831,9 @@ 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)) // Precondition: Assertion set is in NNF.
// Precondition: Assertion set is in NNF.
// Also: careful about the unsat assertion scaling further down.
if (m_manager.is_and(child) || m_manager.is_or(child))
NOT_IMPLEMENTED_YET();
res = score_bool(child, true);
}