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
tst_substitution()16 void tst_substitution()
17 {
18 memory::initialize(0);
19 smt_params params;
20 params.m_model = true;
21
22 enable_trace("subst_bug");
23
24 ast_manager m;
25 reg_decl_plugins(m);
26
27 var_ref v1(m.mk_var(0, m.mk_bool_sort()), m);
28 var_ref v2(m.mk_var(1, m.mk_bool_sort()), m);
29 var_ref v3(m.mk_var(2, m.mk_bool_sort()), m);
30 var_ref v4(m.mk_var(3, m.mk_bool_sort()), m);
31
32 substitution subst(m);
33 subst.reserve(1,4);
34 unifier unif(m);
35
36 bool ok1 = unif(v1.get(), v2.get(), subst, false);
37 bool ok2 = unif(v2.get(), v1.get(), subst, false);
38 (void)ok1;
39 (void)ok2;
40
41 expr_ref res(m);
42
43 TRACE("substitution", subst.display(tout););
44 TRACE("substitution", tout << ok1 << " " << ok2 << "\n";);
45 subst.display(std::cout);
46 subst.apply(v1.get(), res);
47 TRACE("substitution", tout << mk_pp(res, m) << "\n";);
48
49 expr_ref q(m), body(m);
50 sort_ref_vector sorts(m);
51 svector<symbol> names;
52 sorts.push_back(m.mk_bool_sort());
53 names.push_back(symbol("dude"));
54 body = m.mk_and(m.mk_eq(v1,v2), m.mk_eq(v3,v4));
55 q = m.mk_forall(sorts.size(), sorts.data(), names.data(), body);
56 subst.apply(q, res);
57 TRACE("substitution", tout << mk_pp(q, m) << "\n->\n" << mk_pp(res, m) << "\n";);
58
59 }
60