1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 diff_logic.cpp
7
8 Abstract:
9
10 Unit tests for difference logic
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2006-11-22.
15
16 Revision History:
17
18 --*/
19 #ifdef _WINDOWS
20 #include "util/rational.h"
21 #include "smt/diff_logic.h"
22 #include "smt/smt_literal.h"
23 #include "util/util.h"
24 #include "util/debug.h"
25
26 struct diff_logic_ext {
27 typedef rational numeral;
28 typedef smt::literal explanation;
29 };
30
31 template class dl_graph<diff_logic_ext>;
32
33 typedef dl_graph<diff_logic_ext> dlg;
34
35 struct tst_dl_functor {
36 smt::literal_vector m_literals;
operator ()tst_dl_functor37 void operator()(smt::literal l) {
38 m_literals.push_back(l);
39 }
40 };
41
tst1()42 static void tst1() {
43 dlg g;
44 smt::literal l;
45 g.init_var(1);
46 g.init_var(2);
47 g.init_var(3);
48 g.enable_edge(g.add_edge(1, 2, rational(1), l));
49 g.enable_edge(g.add_edge(2, 3, rational(2), l));
50 g.push();
51 g.enable_edge(g.add_edge(1, 3, rational(4), l));
52 g.init_var(4);
53 g.enable_edge(g.add_edge(1, 4, rational(5), l));
54 g.enable_edge(g.add_edge(4, 2, rational(0), l));
55 g.pop(1);
56 }
57
tst2()58 static void tst2() {
59 dlg g;
60 rational w;
61 smt::literal l1(1);
62 smt::literal l2(2);
63 smt::literal l3(3);
64 smt::literal l4(4);
65 smt::literal l5(5);
66 smt::literal l6(6);
67 g.init_var(0);
68 g.init_var(1);
69 g.init_var(2);
70 g.init_var(3);
71 g.init_var(4);
72 smt::literal d;
73 ENSURE(g.enable_edge(g.add_edge(1, 2, rational(-1), l1)));
74 ENSURE(g.get_edge_weight(1, 2, w, d) && w == rational(-1));
75 ENSURE(!g.get_edge_weight(2, 3, w, d));
76 ENSURE(g.enable_edge(g.add_edge(2, 3, rational(-2), l2)));
77 ENSURE(g.enable_edge(g.add_edge(1, 4, rational(1), l3)));
78 ENSURE(g.get_edge_weight(1, 2, w, d) && w == rational(-1));
79 ENSURE(g.get_edge_weight(1, 4, w, d) && w == rational(1));
80 ENSURE(!g.get_edge_weight(1, 3, w, d));
81 ENSURE(g.enable_edge(g.add_edge(2, 4, rational(10), l6)));
82 ENSURE(g.is_feasible_dbg());
83 g.push();
84 ENSURE(g.enable_edge(g.add_edge(3, 0, rational(2), l4)));
85 ENSURE(!g.enable_edge(g.add_edge(0, 1, rational(-1), l5)));
86 ENSURE(!g.is_feasible_dbg());
87 TRACE("diff_logic", g.display(tout););
88 struct proc {
89 bool_vector found;
90 proc():
91 found(7, false) {
92 }
93 void operator()(smt::literal l) {
94 found[l.var()] = true;
95 }
96 };
97 proc p;
98 g.traverse_neg_cycle(true, p);
99 ENSURE(p.found[0] == false);
100 ENSURE(p.found[1] == true);
101 ENSURE(p.found[2] == true);
102 ENSURE(p.found[3] == false);
103 ENSURE(p.found[4] == true);
104 ENSURE(p.found[5] == true);
105 ENSURE(p.found[6] == false);
106 g.pop(1);
107 ENSURE(g.is_feasible_dbg());
108 TRACE("diff_logic", g.display(tout););
109 }
110
add_edge(dlg & g,dl_var src,dl_var dst,int weight,unsigned lit)111 static int add_edge(dlg& g, dl_var src, dl_var dst, int weight, unsigned lit) {
112 int id = g.add_edge(src, dst, rational(weight), smt::literal(lit));
113 bool ok = g.enable_edge(id);
114 ENSURE(ok);
115 return id;
116 }
117
tst3()118 static void tst3() {
119 dlg g;
120 for (unsigned i = 1; i <= 10; ++i) {
121 g.init_var(i);
122 }
123 add_edge(g, 1, 2, 1, 12);
124 add_edge(g, 1, 3, 1, 13);
125 add_edge(g, 1, 4, 1, 14);
126 add_edge(g, 2, 5, 1, 25);
127 add_edge(g, 2, 6, 1, 26);
128 add_edge(g, 3, 5, 1, 35);
129 add_edge(g, 4, 5, 1, 45);
130 add_edge(g, 4, 6, 1, 46);
131 int xy = add_edge(g, 5, 6, 1, 56);
132 add_edge(g, 5, 7, 1, 57);
133 add_edge(g, 5, 9, 1, 59);
134 add_edge(g, 6, 7, 1, 67);
135 add_edge(g, 6, 8, 1, 68);
136 add_edge(g, 6, 9, 1, 69);
137 add_edge(g, 6, 10, 1, 610);
138 add_edge(g, 8, 10, 1, 810);
139 add_edge(g, 9, 10, 1, 910);
140 TRACE("diff_logic", g.display(tout););
141
142 int e38 = g.add_edge(3, 8, rational(3), smt::literal(38));
143 std::cout << "Edge: " << e38 << "\n";
144
145 svector<edge_id> subsumed;
146 g.find_subsumed(xy, subsumed);
147
148 for (unsigned i = 0; i < subsumed.size(); ++i) {
149 std::cout << "subsumed: " << subsumed[i] << "\n";
150 ENSURE(e38 == subsumed[i]);
151
152 tst_dl_functor tst_fn;
153
154 g.explain_subsumed_lazy(xy, subsumed[i], tst_fn);
155
156 for (unsigned j = 0; j < tst_fn.m_literals.size(); ++j) {
157 std::cout << tst_fn.m_literals[j] << " ";
158 }
159 std::cout << "\n";
160
161 }
162
163
164 }
165
tst_diff_logic()166 void tst_diff_logic() {
167 //tst1();
168 //tst2();
169 //tst3();
170 }
171 #else
tst_diff_logic()172 void tst_diff_logic() {
173 }
174 #endif
175