1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3 
4 Module Name:
5 
6     smt_lookahead.cpp
7 
8 Abstract:
9 
10     Lookahead cuber for SMT
11 
12 Author:
13 
14     nbjorner 2019-05-27.
15 
16 Revision History:
17 
18 --*/
19 
20 #include <cmath>
21 #include "ast/ast_pp.h"
22 #include "ast/ast_ll_pp.h"
23 #include "smt/smt_lookahead.h"
24 #include "smt/smt_context.h"
25 
26 namespace smt {
27 
lookahead(context & ctx)28     lookahead::lookahead(context& ctx):
29         ctx(ctx), m(ctx.get_manager()) {}
30 
get_score()31     double lookahead::get_score() {
32         double score = 0;
33         for (clause* cp : ctx.m_aux_clauses) {
34             unsigned nf = 0, nu = 0;
35             bool is_taut = false;
36             for (literal lit : *cp) {
37                 switch (ctx.get_assignment(lit)) {
38                 case l_false:
39                     if (ctx.get_assign_level(lit) > 0) {
40                         ++nf;
41                     }
42                     break;
43                 case l_true:
44                     is_taut = true;
45                     break;
46                 default:
47                     ++nu;
48                     break;
49                 }
50             }
51             if (!is_taut && nf > 0) {
52                 score += pow(0.5, static_cast<double>(nu));
53             }
54         }
55         return score;
56     }
57 
58     struct lookahead::compare {
59         context& ctx;
comparesmt::lookahead::compare60         compare(context& ctx): ctx(ctx) {}
61 
operator ()smt::lookahead::compare62         bool operator()(bool_var v1, bool_var v2) const {
63             return ctx.get_activity(v1) > ctx.get_activity(v2);
64         }
65     };
66 
choose(unsigned budget)67     expr_ref lookahead::choose(unsigned budget) {
68         ctx.pop_to_base_lvl();
69         unsigned sz = ctx.m_bool_var2expr.size();
70         bool_var best_v = null_bool_var;
71         double best_score = -1;
72         svector<bool_var> vars;
73         for (bool_var v = 0; v < static_cast<bool_var>(sz); ++v) {
74             expr* b = ctx.bool_var2expr(v);
75             if (b && ctx.get_assignment(v) == l_undef) {
76                 vars.push_back(v);
77             }
78         }
79         compare comp(ctx);
80         std::sort(vars.begin(), vars.end(), comp);
81 
82         unsigned nf = 0, nc = 0, ns = 0, n = 0;
83         for (bool_var v : vars) {
84             if (!ctx.bool_var2expr(v))
85                 continue;
86             if (!m.inc())
87                 break;
88             literal lit(v, false);
89             ctx.propagate();
90             if (ctx.inconsistent())
91                 return expr_ref(m.mk_false(), m);
92             ctx.push_scope();
93             ctx.assign(lit, b_justification::mk_axiom(), true);
94             ctx.propagate();
95             bool inconsistent = ctx.inconsistent();
96             double score1 = get_score();
97             ctx.pop_scope(1);
98             if (inconsistent) {
99                 ctx.assign(~lit, b_justification::mk_axiom(), false);
100                 ctx.propagate();
101                 ++nf;
102                 continue;
103             }
104 
105             ctx.propagate();
106             if (ctx.inconsistent())
107                 return expr_ref(m.mk_false(), m);
108             ctx.push_scope();
109             ctx.assign(~lit, b_justification::mk_axiom(), true);
110             ctx.propagate();
111             inconsistent = ctx.inconsistent();
112             double score2 = get_score();
113             ctx.pop_scope(1);
114             if (inconsistent) {
115                 ctx.assign(lit, b_justification::mk_axiom(), false);
116                 ctx.propagate();
117                 ++nf;
118                 continue;
119             }
120             double score = score1 + score2 + 1024*score1*score2;
121 
122             if (score <= 1.1*best_score && best_score <= 1.1*score) {
123                 if (ctx.get_random_value() % (++n) == 0) {
124                     best_score = score;
125                     best_v = v;
126                 }
127                 ns = 0;
128             }
129             else if (score > best_score && (ctx.get_random_value() % 2) == 0) {
130                 n = 0;
131                 best_score = score;
132                 best_v = v;
133                 ns = 0;
134             }
135             ++nc;
136             ++ns;
137             if (ns > budget) {
138                 break;
139             }
140         }
141         expr_ref result(m);
142         if (ctx.inconsistent()) {
143             result = m.mk_false();
144         }
145         else if (best_v != null_bool_var) {
146             result = ctx.bool_var2expr(best_v);
147         }
148         else {
149             result = m.mk_true();
150         }
151         return result;
152     }
153 
choose_rec(unsigned depth)154     expr_ref_vector lookahead::choose_rec(unsigned depth) {
155         expr_ref_vector trail(m), result(m);
156         choose_rec(trail, result, depth, 2000);
157         return result;
158     }
159 
choose_rec(expr_ref_vector & trail,expr_ref_vector & result,unsigned depth,unsigned budget)160     void lookahead::choose_rec(expr_ref_vector & trail, expr_ref_vector& result, unsigned depth, unsigned budget) {
161 
162         expr_ref r = choose(budget);
163         if (m.is_true(r))
164             result.push_back(mk_and(trail));
165         else if (m.is_false(r))
166             ;
167         else {
168             auto recurse = [&]() {
169                 trail.push_back(r);
170                 if (depth <= 1 || !m.inc()) {
171                     result.push_back(mk_and(trail));
172                 }
173                 else {
174                     ctx.push();
175                     ctx.assert_expr(r);
176                     ctx.propagate();
177                     choose_rec(trail, result, depth-1, 2 * (budget / 3));
178                     ctx.pop(1);
179                 }
180                 trail.pop_back();
181             };
182             recurse();
183             r = m.mk_not(r);
184             recurse();
185         }
186     }
187 }
188