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