1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "smt/smt_context.h"
8 #include "ast/ast_pp.h"
9 #include "model/model_v2_pp.h"
10 #include "ast/reg_decl_plugins.h"
11 #include "smt/theory_pb.h"
12 #include "ast/rewriter/th_rewriter.h"
13
populate_literals(unsigned k,smt::literal_vector & lits)14 static unsigned populate_literals(unsigned k, smt::literal_vector& lits) {
15 ENSURE(k < (1u << lits.size()));
16 unsigned t = 0;
17 for (unsigned i = 0; i < lits.size(); ++i) {
18 if (k & (1 << i)) {
19 lits[i] = smt::true_literal;
20 t++;
21 }
22 else {
23 lits[i] = smt::false_literal;
24 }
25 }
26 return t;
27 }
28
29 class pb_fuzzer {
30 ast_manager& m;
31 random_gen rand;
32 smt_params params;
33 smt::context ctx;
34 expr_ref_vector vars;
35
36 public:
pb_fuzzer(ast_manager & m)37 pb_fuzzer(ast_manager& m): m(m), rand(0), ctx(m, params), vars(m) {
38 params.m_model = true;
39 unsigned N = 3;
40 for (unsigned i = 0; i < N; ++i) {
41 std::stringstream strm;
42 strm << "b" << i;
43 vars.push_back(m.mk_const(symbol(strm.str()), m.mk_bool_sort()));
44 std::cout << "(declare-const " << strm.str() << " Bool)\n";
45 }
46 }
47
fuzz()48 void fuzz() {
49 enable_trace("pb");
50 unsigned nr = 0;
51 for (unsigned i = 0; i < 100000; ++i) {
52 fuzz_round(nr, 2);
53 }
54 }
55
56 private:
57
add_ineq()58 void add_ineq() {
59 pb_util pb(m);
60 expr_ref fml(m), tmp(m);
61 th_rewriter rw(m);
62 vector<rational> coeffs(vars.size());
63 expr_ref_vector args(vars);
64 while (true) {
65 rational k(rand(6));
66 for (unsigned i = 0; i < coeffs.size(); ++i) {
67 int v = 3 - rand(5);
68 coeffs[i] = rational(v);
69 if (coeffs[i].is_neg()) {
70 args[i] = m.mk_not(args[i].get());
71 coeffs[i].neg();
72 k += coeffs[i];
73 }
74 }
75 fml = pb.mk_ge(args.size(), coeffs.data(), args.data(), k);
76 rw(fml, tmp);
77 rw(tmp, tmp);
78 if (pb.is_ge(tmp)) {
79 fml = tmp;
80 break;
81 }
82 }
83 std::cout << "(assert " << fml << ")\n";
84 ctx.assert_expr(fml);
85 std::cout << ";asserted\n";
86 }
87
88
89
fuzz_round(unsigned & num_rounds,unsigned lvl)90 void fuzz_round(unsigned& num_rounds, unsigned lvl) {
91 unsigned num_rounds2 = 0;
92 lbool is_sat = l_true;
93 std::cout << "(push 1)\n";
94 ctx.push();
95 unsigned r = 0;
96 while (is_sat == l_true && r <= num_rounds + 1) {
97 add_ineq();
98 std::cout << "(check-sat)\n";
99 is_sat = ctx.check();
100 if (lvl > 0 && is_sat == l_true) {
101 fuzz_round(num_rounds2, lvl-1);
102 }
103 ++r;
104 }
105 num_rounds = r;
106 std::cout << "; number of rounds: " << num_rounds << " level: " << lvl << "\n";
107 ctx.pop(1);
108 std::cout << "(pop 1)\n";
109 }
110
111 };
112
113
114
fuzz_pb()115 static void fuzz_pb()
116 {
117 ast_manager m;
118 reg_decl_plugins(m);
119 pb_fuzzer fuzzer(m);
120 fuzzer.fuzz();
121 }
122
tst_theory_pb()123 void tst_theory_pb() {
124
125 fuzz_pb();
126
127 ast_manager m;
128 smt_params params;
129 params.m_model = true;
130 reg_decl_plugins(m);
131 expr_ref tmp(m);
132
133 enable_trace("pb");
134 for (unsigned N = 4; N < 11; ++N) {
135 for (unsigned i = 0; i < (1u << N); ++i) {
136 smt::literal_vector lits(N, smt::false_literal);
137 unsigned k = populate_literals(i, lits);
138 std::cout << "k:" << k << " " << N << "\n";
139 std::cout.flush();
140 TRACE("pb", tout << "k " << k << ": " << lits << "\n";);
141
142 {
143 smt::context ctx(m, params);
144 ctx.push();
145 smt::literal l = smt::theory_pb::assert_ge(ctx, k+1, lits.size(), lits.data());
146 if (l != smt::false_literal) {
147 ctx.assign(l, nullptr, false);
148 TRACE("pb", tout << "assign: " << l << "\n";
149 ctx.display(tout););
150 VERIFY(l_false == ctx.check());
151 }
152 ctx.pop(1);
153 }
154 {
155 smt::context ctx(m, params);
156 ctx.push();
157 smt::literal l = smt::theory_pb::assert_ge(ctx, k, lits.size(), lits.data());
158 ENSURE(l != smt::false_literal);
159 ctx.assign(l, nullptr, false);
160 TRACE("pb", ctx.display(tout););
161 VERIFY(l_true == ctx.check());
162 ctx.pop(1);
163 }
164 }
165 }
166 }
167