From 992d150b8180c8d0e5b059e3c4c186f35dae7d7c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 25 Apr 2014 17:17:47 +0100 Subject: [PATCH] BVSLS comments Signed-off-by: Christoph M. Wintersteiger --- src/tactic/sls/sls_params.pyg | 2 +- src/tactic/sls/sls_tracker.h | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/tactic/sls/sls_params.pyg b/src/tactic/sls/sls_params.pyg index ad7a22675..bf5bd181a 100644 --- a/src/tactic/sls/sls_params.pyg +++ b/src/tactic/sls/sls_params.pyg @@ -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') diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h index 4356bcc9b..d58f94af2 100644 --- a/src/tactic/sls/sls_tracker.h +++ b/src/tactic/sls/sls_tracker.h @@ -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); }