1 /*++
2 Copyright (c) 2015 Microsoft Corporation
3
4 --*/
5
6 #include "util/trace.h"
7 #include "util/vector.h"
8 #include "ast/ast.h"
9 #include "ast/ast_pp.h"
10 #include "util/statistics.h"
11 #include "ast/reg_decl_plugins.h"
12 #include "ast/rewriter/pb2bv_rewriter.h"
13 #include "smt/smt_kernel.h"
14 #include "model/model_smt2_pp.h"
15 #include "smt/params/smt_params.h"
16 #include "ast/ast_util.h"
17 #include "ast/pb_decl_plugin.h"
18 #include "ast/rewriter/th_rewriter.h"
19 #include "tactic/fd_solver/fd_solver.h"
20 #include "solver/solver.h"
21 #include "ast/arith_decl_plugin.h"
22
test1()23 static void test1() {
24 ast_manager m;
25 reg_decl_plugins(m);
26 pb_util pb(m);
27 params_ref p;
28 pb2bv_rewriter rw(m, p);
29 expr_ref_vector vars(m);
30 unsigned N = 5;
31 for (unsigned i = 0; i < N; ++i) {
32 std::stringstream strm;
33 strm << "b" << i;
34 vars.push_back(m.mk_const(symbol(strm.str()), m.mk_bool_sort()));
35 }
36
37 for (unsigned k = 1; k <= N; ++k) {
38 expr_ref fml(m), result(m);
39 proof_ref proof(m);
40 fml = pb.mk_at_least_k(vars.size(), vars.data(), k);
41 rw(true, fml, result, proof);
42 std::cout << fml << " |-> " << result << "\n";
43 }
44 expr_ref_vector lemmas(m);
45 rw.flush_side_constraints(lemmas);
46 std::cout << lemmas << "\n";
47 }
48
test_semantics(ast_manager & m,expr_ref_vector const & vars,vector<rational> const & coeffs,unsigned k,unsigned kind)49 static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k, unsigned kind) {
50 pb_util pb(m);
51 params_ref p;
52 pb2bv_rewriter rw(m, p);
53 unsigned N = vars.size();
54 expr_ref fml1(m), fml2(m), result1(m), result2(m);
55 proof_ref proof(m);
56 expr_ref_vector lemmas(m);
57 th_rewriter th_rw(m);
58
59 switch (kind) {
60 case 0: fml1 = pb.mk_ge(vars.size(), coeffs.data(), vars.data(), rational(k)); break;
61 case 1: fml1 = pb.mk_le(vars.size(), coeffs.data(), vars.data(), rational(k)); break;
62 default: fml1 = pb.mk_eq(vars.size(), coeffs.data(), vars.data(), rational(k)); break;
63 }
64 rw(true, fml1, result1, proof);
65 rw.flush_side_constraints(lemmas);
66 std::cout << "lemmas: " << lemmas << "\n";
67 std::cout << "simplified: " << result1 << "\n";
68 for (unsigned values = 0; values < static_cast<unsigned>(1 << N); ++values) {
69 smt_params fp;
70 smt::kernel solver(m, fp);
71 expr_ref_vector tf(m);
72 for (unsigned i = 0; i < N; ++i) {
73 bool is_true = 0 != (values & (1 << i));
74 tf.push_back(is_true ? m.mk_true() : m.mk_false());
75 solver.assert_expr(is_true ? vars[i] : m.mk_not(vars[i]));
76 }
77
78 solver.assert_expr(lemmas);
79 switch (kind) {
80 case 0: fml2 = pb.mk_ge(tf.size(), coeffs.data(), tf.data(), rational(k)); break;
81 case 1: fml2 = pb.mk_le(tf.size(), coeffs.data(), tf.data(), rational(k)); break;
82 default: fml2 = pb.mk_eq(tf.size(), coeffs.data(), tf.data(), rational(k)); break;
83 }
84 std::cout << fml1 << " " << fml2 << "\n";
85 th_rw(fml2, result2, proof);
86 ENSURE(m.is_true(result2) || m.is_false(result2));
87 lbool res = solver.check();
88 VERIFY(res == l_true);
89 solver.assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
90 res = solver.check();
91 if (res != l_false) {
92 IF_VERBOSE(0, solver.display(verbose_stream());
93 verbose_stream() << vars << " k: " << k << " kind: " << kind << "\n";
94 for (auto const& c : coeffs) verbose_stream() << c << "\n";
95 );
96 }
97 VERIFY(res == l_false);
98 }
99 }
100
test_semantics(ast_manager & m,expr_ref_vector const & vars,vector<rational> const & coeffs,unsigned k)101 static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k) {
102 test_semantics(m, vars, coeffs, k, 0);
103 test_semantics(m, vars, coeffs, k, 1);
104 test_semantics(m, vars, coeffs, k, 2);
105 }
106
test2()107 static void test2() {
108 ast_manager m;
109 reg_decl_plugins(m);
110 expr_ref_vector vars(m);
111 unsigned N = 4;
112 for (unsigned i = 0; i < N; ++i) {
113 std::stringstream strm;
114 strm << "b" << i;
115 vars.push_back(m.mk_const(symbol(strm.str()), m.mk_bool_sort()));
116 }
117 for (unsigned coeff = 0; coeff < static_cast<unsigned>(1 << N); ++coeff) {
118 vector<rational> coeffs;
119 for (unsigned i = 0; i < N; ++i) {
120 bool is_one = 0 != (coeff & (1 << i));
121 coeffs.push_back(is_one ? rational(1) : rational(2));
122 }
123 for (unsigned i = 0; i <= N; ++i) {
124 test_semantics(m, vars, coeffs, i);
125 }
126 }
127 }
128
129
test_solver_semantics(ast_manager & m,expr_ref_vector const & vars,vector<rational> const & coeffs,unsigned k,unsigned kind)130 static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k, unsigned kind) {
131 pb_util pb(m);
132 params_ref p;
133 unsigned N = vars.size();
134 expr_ref fml1(m), fml2(m), result1(m), result2(m);
135 proof_ref proof(m);
136 th_rewriter th_rw(m);
137
138 switch (kind) {
139 case 0: fml1 = pb.mk_ge(vars.size(), coeffs.data(), vars.data(), rational(k)); break;
140 case 1: fml1 = pb.mk_le(vars.size(), coeffs.data(), vars.data(), rational(k)); break;
141 default: fml1 = pb.mk_eq(vars.size(), coeffs.data(), vars.data(), rational(k)); break;
142 }
143 result1 = m.mk_fresh_const("xx", m.mk_bool_sort());
144 for (unsigned values = 0; values < static_cast<unsigned>(1 << N); ++values) {
145 ref<solver> slv = mk_fd_solver(m, p);
146 expr_ref_vector tf(m);
147 for (unsigned i = 0; i < N; ++i) {
148 bool is_true = 0 != (values & (1 << i));
149 tf.push_back(is_true ? m.mk_true() : m.mk_false());
150 slv->assert_expr(is_true ? vars[i] : m.mk_not(vars[i]));
151 }
152 slv->assert_expr(m.mk_eq(result1, fml1));
153
154 switch (kind) {
155 case 0: fml2 = pb.mk_ge(tf.size(), coeffs.data(), tf.data(), rational(k)); break;
156 case 1: fml2 = pb.mk_le(tf.size(), coeffs.data(), tf.data(), rational(k)); break;
157 default: fml2 = pb.mk_eq(tf.size(), coeffs.data(), tf.data(), rational(k)); break;
158 }
159 std::cout << fml1 << " " << fml2 << "\n";
160 th_rw(fml2, result2, proof);
161 ENSURE(m.is_true(result2) || m.is_false(result2));
162 lbool res = slv->check_sat(0,nullptr);
163 VERIFY(res == l_true);
164 slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get());
165 res = slv->check_sat(0,nullptr);
166 VERIFY(res == l_false);
167 }
168 }
169
test_solver_semantics(ast_manager & m,expr_ref_vector const & vars,vector<rational> const & coeffs,unsigned k)170 static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector<rational> const& coeffs, unsigned k) {
171 test_solver_semantics(m, vars, coeffs, k, 0);
172 test_solver_semantics(m, vars, coeffs, k, 1);
173 test_solver_semantics(m, vars, coeffs, k, 2);
174 }
175
test3()176 static void test3() {
177 ast_manager m;
178 reg_decl_plugins(m);
179 expr_ref_vector vars(m);
180 unsigned N = 4;
181 for (unsigned i = 0; i < N; ++i) {
182 std::stringstream strm;
183 strm << "b" << i;
184 vars.push_back(m.mk_const(symbol(strm.str()), m.mk_bool_sort()));
185 }
186 for (unsigned coeff = 0; coeff < static_cast<unsigned>(1 << N); ++coeff) {
187 vector<rational> coeffs;
188 for (unsigned i = 0; i < N; ++i) {
189 bool is_one = 0 != (coeff & (1 << i));
190 coeffs.push_back(is_one ? rational(1) : rational(2));
191 }
192 for (unsigned i = 0; i <= N; ++i) {
193 test_solver_semantics(m, vars, coeffs, i);
194 }
195 }
196 }
197
test4()198 static void test4() {
199 ast_manager m;
200 reg_decl_plugins(m);
201 arith_util arith(m);
202 expr_ref a(m.mk_const(symbol("a"), arith.mk_int()), m);
203 expr_ref b(m.mk_const(symbol("b"), arith.mk_int()), m);
204 expr_ref eq(m.mk_eq(a,b), m);
205 std::cout << "is_atom: " << is_atom(m, eq) << "\n";
206 }
207
tst_pb2bv()208 void tst_pb2bv() {
209 test1();
210 test2();
211 test3();
212 test4();
213 }
214
215