1
2 /*++
3 Copyright (c) 2015 Microsoft Corporation
4
5 --*/
6
7 #include "ast/expr_substitution.h"
8 #include "smt/params/smt_params.h"
9 #include "ast/substitution/substitution.h"
10 #include "ast/substitution/unifier.h"
11 #include "ast/bv_decl_plugin.h"
12 #include "ast/ast_pp.h"
13 #include "ast/arith_decl_plugin.h"
14 #include "ast/reg_decl_plugins.h"
15 #include "ast/rewriter/th_rewriter.h"
16
mk_bv_xor(bv_util & bv,expr * a,expr * b)17 expr* mk_bv_xor(bv_util& bv, expr* a, expr* b) {
18 expr* args[2];
19 args[0] = a;
20 args[1] = b;
21 return bv.mk_bv_xor(2, args);
22 }
23
mk_bv_and(bv_util & bv,expr * a,expr * b)24 expr* mk_bv_and(bv_util& bv, expr* a, expr* b) {
25 expr* args[2];
26 args[0] = a;
27 args[1] = b;
28 ast_manager& m = bv.get_manager();
29 return m.mk_app(bv.get_family_id(), OP_BAND, 2, args);
30 }
31
tst_expr_substitution()32 void tst_expr_substitution() {
33 memory::initialize(0);
34 ast_manager m;
35 reg_decl_plugins(m);
36 bv_util bv(m);
37
38 expr_ref a(m), b(m), c(m), d(m);
39 expr_ref x(m);
40 expr_ref new_a(m);
41 proof_ref pr(m);
42 x = m.mk_const(symbol("x"), bv.mk_sort(8));
43 a = mk_bv_and(bv, mk_bv_xor(bv, x,bv.mk_numeral(8,8)), mk_bv_xor(bv,x,x));
44 b = x;
45 c = bv.mk_bv_sub(x, bv.mk_numeral(4, 8));
46
47 expr_substitution subst(m);
48 th_rewriter rw(m);
49
50 std::cout << mk_pp(c, m) << "\n";
51
52 // normalizing c does not help.
53 rw(c, d, pr);
54
55 std::cout << mk_pp(d, m) << "\n";
56
57
58 // This portion diverges. It attempts to replace x by (bvadd #xfc x), which contains x.
59 // subst.insert(b, d);
60
61 // std::cout << mk_pp(a, m) << "\n";
62 // rw.set_substitution(&subst);
63
64 // enable_trace("th_rewriter_step");
65 // rw(a, new_a, pr);
66
67 // std::cout << mk_pp(new_a, m) << "\n";
68
69 }
70