1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 sls_tactic.h
7
8 Abstract:
9
10 A Stochastic Local Search (SLS) tactic
11
12 Author:
13
14 Christoph (cwinter) 2012-02-29
15
16 Notes:
17
18 --*/
19 #include "ast/normal_forms/nnf.h"
20 #include "tactic/core/solve_eqs_tactic.h"
21 #include "tactic/bv/bv_size_reduction_tactic.h"
22 #include "tactic/bv/max_bv_sharing_tactic.h"
23 #include "tactic/core/simplify_tactic.h"
24 #include "tactic/core/propagate_values_tactic.h"
25 #include "tactic/core/ctx_simplify_tactic.h"
26 #include "tactic/core/elim_uncnstr_tactic.h"
27 #include "tactic/core/nnf_tactic.h"
28 #include "util/stopwatch.h"
29 #include "tactic/sls/sls_tactic.h"
30 #include "tactic/sls/sls_params.hpp"
31 #include "tactic/sls/sls_engine.h"
32
33 class sls_tactic : public tactic {
34 ast_manager & m;
35 params_ref m_params;
36 sls_engine * m_engine;
37
38 public:
sls_tactic(ast_manager & _m,params_ref const & p)39 sls_tactic(ast_manager & _m, params_ref const & p):
40 m(_m),
41 m_params(p) {
42 m_engine = alloc(sls_engine, m, p);
43 }
44
translate(ast_manager & m)45 tactic * translate(ast_manager & m) override {
46 return alloc(sls_tactic, m, m_params);
47 }
48
~sls_tactic()49 ~sls_tactic() override {
50 dealloc(m_engine);
51 }
52
updt_params(params_ref const & p)53 void updt_params(params_ref const & p) override {
54 m_params = p;
55 m_engine->updt_params(p);
56 }
57
collect_param_descrs(param_descrs & r)58 void collect_param_descrs(param_descrs & r) override {
59 sls_params::collect_param_descrs(r);
60 }
61
operator ()(goal_ref const & g,goal_ref_buffer & result)62 void operator()(goal_ref const & g,
63 goal_ref_buffer & result) override {
64 result.reset();
65
66 TRACE("sls", g->display(tout););
67 tactic_report report("sls", *g);
68
69 model_converter_ref mc;
70 m_engine->operator()(g, mc);
71 g->add(mc.get());
72 g->inc_depth();
73 result.push_back(g.get());
74 }
75
cleanup()76 void cleanup() override {
77 sls_engine * d = alloc(sls_engine, m, m_params);
78 std::swap(d, m_engine);
79 dealloc(d);
80 }
81
collect_statistics(statistics & st) const82 void collect_statistics(statistics & st) const override {
83 m_engine->collect_statistics(st);
84 }
85
reset_statistics()86 void reset_statistics() override {
87 m_engine->reset_statistics();
88 }
89
90 };
91
mk_sls_tactic(ast_manager & m,params_ref const & p)92 static tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
93 return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported.
94 clean(alloc(sls_tactic, m, p)));
95 }
96
97
mk_preamble(ast_manager & m,params_ref const & p)98 static tactic * mk_preamble(ast_manager & m, params_ref const & p) {
99 params_ref main_p;
100 main_p.set_bool("elim_and", true);
101 // main_p.set_bool("pull_cheap_ite", true);
102 main_p.set_bool("push_ite_bv", true);
103 main_p.set_bool("blast_distinct", true);
104 main_p.set_bool("hi_div0", true);
105
106 params_ref simp2_p = p;
107 simp2_p.set_bool("som", true);
108 simp2_p.set_bool("pull_cheap_ite", true);
109 simp2_p.set_bool("push_ite_bv", false);
110 simp2_p.set_bool("local_ctx", true);
111 simp2_p.set_uint("local_ctx_limit", 10000000);
112
113 params_ref hoist_p;
114 hoist_p.set_bool("hoist_mul", true);
115 hoist_p.set_bool("som", false);
116
117 params_ref gaussian_p;
118 // conservative gaussian elimination.
119 gaussian_p.set_uint("gaussian_max_occs", 2);
120
121 params_ref ctx_p;
122 ctx_p.set_uint("max_depth", 32);
123 ctx_p.set_uint("max_steps", 5000000);
124 return and_then(and_then(mk_simplify_tactic(m),
125 mk_propagate_values_tactic(m),
126 using_params(mk_solve_eqs_tactic(m), gaussian_p),
127 mk_elim_uncnstr_tactic(m),
128 mk_bv_size_reduction_tactic(m),
129 using_params(mk_simplify_tactic(m), simp2_p)),
130 using_params(mk_simplify_tactic(m), hoist_p),
131 mk_max_bv_sharing_tactic(m),
132 mk_nnf_tactic(m, p));
133 }
134
mk_qfbv_sls_tactic(ast_manager & m,params_ref const & p)135 tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) {
136 tactic * t = and_then(mk_preamble(m, p), mk_sls_tactic(m, p));
137 t->updt_params(p);
138 return t;
139 }
140