1
2 #include "Test/UnitTesting.hpp"
3 #include "Test/SyntaxSugar.hpp"
4 #include "Indexing/TermSharing.hpp"
5 #include "Inferences/GaussianVariableElimination.hpp"
6 #include "Inferences/InterpretedEvaluation.hpp"
7 #include "Kernel/Ordering.hpp"
8
9 #define UNIT_ID GaussianVariableElimination
10 UT_CREATE;
11 using namespace std;
12 using namespace Kernel;
13 using namespace Inferences;
14
15 #include "Test/SyntaxSugar.hpp"
16
17 //TODO factor out
clause(std::initializer_list<reference_wrapper<Literal>> ls)18 Clause& clause(std::initializer_list<reference_wrapper<Literal>> ls) {
19 static Inference testInf = Kernel::NonspecificInference0(UnitInputType::ASSUMPTION, InferenceRule::INPUT);
20 Clause& out = *new(ls.size()) Clause(ls.size(), testInf);
21 auto l = ls.begin();
22 for (int i = 0; i < ls.size(); i++) {
23 out[i] = &l->get();
24 l++;
25 }
26 return out;
27 }
28
exactlyEq(const Clause & lhs,const Clause & rhs,const Stack<unsigned> & perm)29 bool exactlyEq(const Clause& lhs, const Clause& rhs, const Stack<unsigned>& perm) {
30 for (int j = 0; j < perm.size(); j++) {
31 if (!Indexing::TermSharing::equals(lhs[j], rhs[perm[j]])) {
32 return false;
33 }
34 }
35 return true;
36 }
37
38
permEq(const Clause & lhs,const Clause & rhs,Stack<unsigned> & perm,unsigned idx)39 bool permEq(const Clause& lhs, const Clause& rhs, Stack<unsigned>& perm, unsigned idx) {
40 if (exactlyEq(lhs, rhs, perm)) {
41 return true;
42 }
43 for (int i = idx; i < perm.size(); i++) {
44 swap(perm[i], perm[idx]);
45
46
47 if (permEq(lhs,rhs, perm, idx+1)) return true;
48
49 swap(perm[i], perm[idx]);
50 }
51
52 return false;
53 }
54
55 //TODO factor out
operator ==(const Clause & lhs,const Clause & rhs)56 bool operator==(const Clause& lhs, const Clause& rhs) {
57 if (lhs.size() != rhs.size()) return false;
58
59 Stack<unsigned> perm;
60 for (int i = 0; i<lhs.size(); i++) {
61 perm.push(i);
62 }
63 return permEq(lhs, rhs, perm, 0);
64
65 }
operator !=(const Clause & lhs,const Clause & rhs)66 bool operator!=(const Clause& lhs, const Clause& rhs) {
67 return !(lhs == rhs);
68 }
69
70
exhaustiveGve(Clause * in)71 Clause* exhaustiveGve(Clause* in) {
72
73 struct FakeOrdering : Kernel::Ordering {
74 virtual Result compare(Literal*, Literal*) const override { return Kernel::Ordering::LESS; }
75 virtual Result compare(TermList, TermList) const override {ASSERTION_VIOLATION}
76 virtual Comparison compareFunctors(unsigned, unsigned) const override {ASSERTION_VIOLATION}
77 };
78 static FakeOrdering ord;
79 static GaussianVariableElimination inf = GaussianVariableElimination();
80 static InterpretedEvaluation ev = InterpretedEvaluation(false, ord);
81 Clause* last = in;
82 Clause* latest = in;
83 do {
84 last = latest;
85 latest = ev.simplify(inf.simplify(last));
86 } while (latest != last);
87 return latest;
88 }
89
90
test_eliminate_na(Clause & toSimplify)91 void test_eliminate_na(Clause& toSimplify) {
92 auto res = exhaustiveGve(&toSimplify);
93 if (res != &toSimplify ) {
94 cout << endl;
95 cout << "[ case ]: " << toSimplify.toString() << endl;
96 cout << "[ is ]: " << res->toString() << endl;
97 cout << "[ expected ]: < nop >" << endl;
98 exit(-1);
99 }
100 }
101
test_eliminate(Clause & toSimplify,const Clause & expected)102 void test_eliminate(Clause& toSimplify, const Clause& expected) {
103 auto res = exhaustiveGve(&toSimplify);
104 if (!res || *res != expected) {
105 cout << endl;
106 cout << "[ case ]: " << toSimplify.toString() << endl;
107 cout << "[ is ]: " << res->toString() << endl;
108 cout << "[ expected ]: " << expected.toString() << endl;
109 exit(-1);
110 }
111 }
112
113 #define TEST_ELIMINATE(name, toSimplify, expected) \
114 TEST_FUN(name) { \
115 THEORY_SYNTAX_SUGAR(REAL) \
116 _Pragma("GCC diagnostic push") \
117 _Pragma("GCC diagnostic ignored \"-Wunused\"") \
118 THEORY_SYNTAX_SUGAR_FUN(f, 1) \
119 _Pragma("GCC diagnostic pop") \
120 test_eliminate((toSimplify),(expected)); \
121 }
122
123 #define TEST_ELIMINATE_NA(name, toSimplify) \
124 TEST_FUN(name) { \
125 THEORY_SYNTAX_SUGAR(REAL) \
126 _Pragma("GCC diagnostic push") \
127 _Pragma("GCC diagnostic ignored \"-Wunused\"") \
128 THEORY_SYNTAX_SUGAR_FUN(f, 1) \
129 _Pragma("GCC diagnostic pop") \
130 test_eliminate_na((toSimplify)); \
131 }
132
133 TEST_ELIMINATE(test_1
134 , clause({ neq(mul(3, x), 6), lt(x, y) })
135 , clause({ lt(2, y) })
136 )
137
138 TEST_ELIMINATE_NA(test_2
139 , clause({ eq(mul(3, x), 6), lt(x, y) })
140 )
141
142 TEST_ELIMINATE(test_3
143 , clause({ neq(mul(3, x), 6), lt(x, x) })
144 , clause({ /* lt(2, 2) */ })
145 )
146
147 TEST_ELIMINATE(test_uninterpreted
148 , clause({ neq(mul(3, f(x)), y), lt(x, y) })
149 , clause({ lt(x, mul(3, f(x))) })
150 )
151
152 // x!=4 \/ x+y != 5 \/ C[x]
153 // 4+y != 5 \/ C[4]
154 // C[4]
155 TEST_ELIMINATE(test_multiplesteps_1
156 , clause({ neq(x, 4), neq(add(x,y), 5), lt(x, f(x)) })
157 , clause({ lt(4, f(4)) })
158 )
159
160 // x!=4 \/ x+y != 5 \/ C[x,y]
161 // 4+y != 5 \/ C[4,y]
162 // C[4,1]
163 TEST_ELIMINATE(test_multiplesteps_2
164 , clause({ neq(x, 4), neq(add(x,y), 5), lt(x, f(y)) })
165 , clause({ lt(4, f(1)) })
166 )
167
168 // x !=4 \/ x+y != 5 \/ C[x]
169 // 5-y!=4 \/ C[5-y]
170 // \/ C[5]
171
172
173