mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-06 07:15:47 +00:00
Code Activity

removed unnecessary changes for bvsls

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-03-26 13:08:13 +00:00
parent 52390989dd
commit 96ab83d944
12 changed files with 3 additions and 128 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/portfolio/default_tactic.cpp
View file

@ -28,12 +28,10 @@ Notes:
#include"probe_arith.h"
#include"quant_tactics.h"
#include"qffpa_tactic.h"
#include"sls_tactic.h"
tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
tactic * st = using_params(and_then(mk_simplify_tactic(m),
cond(mk_is_qfbv_probe(), mk_qfbv_sls_tactic(m),
// cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m),
tactic * st = using_params(and_then(mk_simplify_tactic(m),
cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m),
cond(mk_is_qflia_probe(), mk_qflia_tactic(m),
cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),

5
src/tactic/portfolio/smt_strategic_solver.cpp
View file

@ -37,14 +37,11 @@ Notes:
#include"horn_tactic.h"
#include"smt_solver.h"
#include"sls_tactic.h"
tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
if (logic=="QF_UF")
return mk_qfuf_tactic(m, p);
else if (logic=="QF_BV")
// return mk_qfbv_tactic(m, p);
return mk_qfbv_sls_tactic(m, p);
return mk_qfbv_tactic(m, p);
else if (logic=="QF_IDL")
return mk_qfidl_tactic(m, p);
else if (logic=="QF_LIA")

12
versions/z3-crsat-0.01.txt
View file

@ -1,12 +0,0 @@
More focused (_FOCUS_ == 2) WalkSAT version.
Variables are chosen among candidates in only one unsatisfied bit-vector term.
Flip rate slightly slower; probably due to larger hash-table and recursive formula structure.
No restarts.
#define _CNF_ 0
#define _BFS_ 1
#define _FOCUS_ 3
#define _RESTARTS_ 0
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0

10
versions/z3-gsat-0.01.txt
View file

@ -1,10 +0,0 @@
Basic GSAT version.
No restarts.
#define _CNF_ 0
#define _BFS_ 0
#define _FOCUS_ 0
#define _RESTARTS_ 0
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0

10
versions/z3-gsat-res-0.01.txt
View file

@ -1,10 +0,0 @@
Basic GSAT version corresponding to Christoph's original code.
Restarts after 100 plateaus.
#define _CNF_ 0
#define _BFS_ 0
#define _FOCUS_ 0
#define _RESTARTS_ 1
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0

14
versions/z3-wsat-0.01.txt
View file

@ -1,14 +0,0 @@
Basic WalkSAT version.
Variables are chosen among candidates in only ONE top level assertion.
Flip rate increased by roughly 10%-300%.
No restarts.
#define _CNF_ 0
#define _BFS_ 1
#define _FOCUS_ 1
#define _RESTARTS_ 0
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0
BUGGY VERSION! Uses wrong value for modulo operation in assertion selection.

14
versions/z3-wsat-0.01b.txt
View file

@ -1,14 +0,0 @@
Basic WalkSAT version.
Variables are chosen among candidates in only ONE top level assertion.
Chooses a random top level assertion instead of using a BFS approach (_BFS_ == 0).
No restarts.
#define _CNF_ 0
#define _BFS_ 0
#define _FOCUS_ 1
#define _RESTARTS_ 0
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0
BUGGY VERSION! Uses wrong value for modulo operation in assertion selection.

12
versions/z3-wsat-0.01c.txt
View file

@ -1,12 +0,0 @@
Basic WalkSAT version.
Variables are chosen among candidates in only ONE top level assertion.
AND is scored by average; OR is scored by inverse multiplication.
No restarts.
#define _CNF_ 0
#define _BFS_ 1
#define _FOCUS_ 1
#define _RESTARTS_ 0
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 1
#define _SCORE_OR_MUL_ 1

11
versions/z3-wsat-0.01d.txt
View file

@ -1,11 +0,0 @@
Basic WalkSAT version.
Variables are chosen among candidates in only ONE top level assertion with MINIMAL top_score.
No restarts.
#define _CNF_ 0
#define _BFS_ 2
#define _FOCUS_ 1
#define _RESTARTS_ 0
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0

11
versions/z3-wsat-0.01e.txt
View file

@ -1,11 +0,0 @@
Basic WalkSAT version.
Variables are chosen among candidates in only ONE top level assertion with MAXIMAL top_score.
No restarts.
#define _CNF_ 0
#define _BFS_ 3
#define _FOCUS_ 1
#define _RESTARTS_ 0
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0

13
versions/z3-wsat-0.02.txt
View file

@ -1,13 +0,0 @@
Basic WalkSAT version.
Variables are chosen among candidates in only ONE top level assertion.
Score function reduced to 0/1.
No restarts.
#define _CNF_ 0
#define _BFS_ 1
#define _FOCUS_ 1
#define _RESTARTS_ 0
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0
#define _WEIGHTED_DIST_ 1

13
versions/z3-wsat-res-0.01.txt
View file

@ -1,13 +0,0 @@
Basic WalkSAT version.
Variables are chosen among candidates in only ONE top level assertion.
Flip rate increased by roughly 10%-300% compared to GSAT.
Restarts after 100 plateaus.
Fps slightly decreased due to restarts.
#define _CNF_ 0
#define _BFS_ 1
#define _FOCUS_ 1
#define _RESTARTS_ 1
#define _TIMELIMIT_ 300
#define _SCORE_AND_AVG_ 0
#define _SCORE_OR_MUL_ 0