From 96ab83d944802e57398cd3ea31552487f5e39c82 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 26 Mar 2014 13:08:13 +0000 Subject: [PATCH] removed unnecessary changes for bvsls Signed-off-by: Christoph M. Wintersteiger --- src/tactic/portfolio/default_tactic.cpp | 6 ++---- src/tactic/portfolio/smt_strategic_solver.cpp | 5 +---- versions/z3-crsat-0.01.txt | 12 ------------ versions/z3-gsat-0.01.txt | 10 ---------- versions/z3-gsat-res-0.01.txt | 10 ---------- versions/z3-wsat-0.01.txt | 14 -------------- versions/z3-wsat-0.01b.txt | 14 -------------- versions/z3-wsat-0.01c.txt | 12 ------------ versions/z3-wsat-0.01d.txt | 11 ----------- versions/z3-wsat-0.01e.txt | 11 ----------- versions/z3-wsat-0.02.txt | 13 ------------- versions/z3-wsat-res-0.01.txt | 13 ------------- 12 files changed, 3 insertions(+), 128 deletions(-) delete mode 100644 versions/z3-crsat-0.01.txt delete mode 100644 versions/z3-gsat-0.01.txt delete mode 100644 versions/z3-gsat-res-0.01.txt delete mode 100644 versions/z3-wsat-0.01.txt delete mode 100644 versions/z3-wsat-0.01b.txt delete mode 100644 versions/z3-wsat-0.01c.txt delete mode 100644 versions/z3-wsat-0.01d.txt delete mode 100644 versions/z3-wsat-0.01e.txt delete mode 100644 versions/z3-wsat-0.02.txt delete mode 100644 versions/z3-wsat-res-0.01.txt diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 53da9a159..1cab40093 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -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), diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index f63b4fd8c..a2f8a97f7 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -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") diff --git a/versions/z3-crsat-0.01.txt b/versions/z3-crsat-0.01.txt deleted file mode 100644 index 49e1a1525..000000000 --- a/versions/z3-crsat-0.01.txt +++ /dev/null @@ -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 \ No newline at end of file diff --git a/versions/z3-gsat-0.01.txt b/versions/z3-gsat-0.01.txt deleted file mode 100644 index eb806a67f..000000000 --- a/versions/z3-gsat-0.01.txt +++ /dev/null @@ -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 \ No newline at end of file diff --git a/versions/z3-gsat-res-0.01.txt b/versions/z3-gsat-res-0.01.txt deleted file mode 100644 index 6a211f2bc..000000000 --- a/versions/z3-gsat-res-0.01.txt +++ /dev/null @@ -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 \ No newline at end of file diff --git a/versions/z3-wsat-0.01.txt b/versions/z3-wsat-0.01.txt deleted file mode 100644 index fec38518d..000000000 --- a/versions/z3-wsat-0.01.txt +++ /dev/null @@ -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. \ No newline at end of file diff --git a/versions/z3-wsat-0.01b.txt b/versions/z3-wsat-0.01b.txt deleted file mode 100644 index 8bcf2ffeb..000000000 --- a/versions/z3-wsat-0.01b.txt +++ /dev/null @@ -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. \ No newline at end of file diff --git a/versions/z3-wsat-0.01c.txt b/versions/z3-wsat-0.01c.txt deleted file mode 100644 index 223560e08..000000000 --- a/versions/z3-wsat-0.01c.txt +++ /dev/null @@ -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 \ No newline at end of file diff --git a/versions/z3-wsat-0.01d.txt b/versions/z3-wsat-0.01d.txt deleted file mode 100644 index 072191370..000000000 --- a/versions/z3-wsat-0.01d.txt +++ /dev/null @@ -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 \ No newline at end of file diff --git a/versions/z3-wsat-0.01e.txt b/versions/z3-wsat-0.01e.txt deleted file mode 100644 index b018c5e0d..000000000 --- a/versions/z3-wsat-0.01e.txt +++ /dev/null @@ -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 \ No newline at end of file diff --git a/versions/z3-wsat-0.02.txt b/versions/z3-wsat-0.02.txt deleted file mode 100644 index 34dcb157c..000000000 --- a/versions/z3-wsat-0.02.txt +++ /dev/null @@ -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 \ No newline at end of file diff --git a/versions/z3-wsat-res-0.01.txt b/versions/z3-wsat-res-0.01.txt deleted file mode 100644 index 575180a59..000000000 --- a/versions/z3-wsat-res-0.01.txt +++ /dev/null @@ -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 \ No newline at end of file