1
2 /*
3 * File CheckedFwSimplifier.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file CheckedFwSimplifier.cpp
21 * Implements class CheckedFwSimplifier.
22 */
23
24 #include "Lib/DHSet.hpp"
25
26 #include "Kernel/Clause.hpp"
27
28 #include "CheckedFwSimplifier.hpp"
29
30 namespace Test
31 {
32
33 using namespace Lib;
34 using namespace Kernel;
35 using namespace Inferences;
36
37 struct CheckedFwSimplifier::CheckingPerformer
38 : public ForwardSimplificationPerformer
39 {
40 public:
CheckingPerformerTest::CheckedFwSimplifier::CheckingPerformer41 CheckingPerformer()
42 {
43 }
44
performTest::CheckedFwSimplifier::CheckingPerformer45 void perform(ClauseIterator premises, Clause* replacement)
46 {
47 CALL("CheckedFwSimplifier::CheckingPerformer::perform");
48 ASSERTION_VIOLATION;
49 INVALID_OPERATION("perform method of CheckingPerformer should never be called");
50 }
51
willPerformTest::CheckedFwSimplifier::CheckingPerformer52 bool willPerform(Clause* premise)
53 {
54 CALL("CheckedFwSimplifier::CheckingPerformer::willPerform");
55
56 if(_recording) {
57 _firstCnt++;
58 _resultSet.insert(premise);
59 _resultsOfFirst.push(premise);
60 }
61 else {
62 _secondCnt++;
63 _resultsOfSecond.push(premise);
64 if(!_resultSet.remove(premise)) {
65 if(_ok) { _ok=false; cout<<endl; }
66 cout<<"-the second inference yielded premise that the first one did not"<<endl;
67 cout<<"query: "<<_query->toString()<<endl;
68 cout<<"result: "<<premise->toString()<<endl;
69 // ASSERTION_VIOLATION;
70 }
71 }
72 return false;
73 }
74
clauseKeptTest::CheckedFwSimplifier::CheckingPerformer75 bool clauseKept()
76 {
77 CALL("CheckedFwSimplifier::CheckingPerformer::clauseKept");
78 return true;
79 }
80
resetAndStartRecordingTest::CheckedFwSimplifier::CheckingPerformer81 void resetAndStartRecording(Clause* query)
82 {
83 CALL("CheckedFwSimplifier::CheckingPerformer::resetAndStartRecording");
84
85 _query=query;
86 _firstCnt=0;
87 _secondCnt=0;
88 _ok=true;
89
90 _resultSet.reset();
91 _resultsOfFirst.reset();
92 _resultsOfSecond.reset();
93 _recording=true;
94 }
95
startCheckingTest::CheckedFwSimplifier::CheckingPerformer96 void startChecking()
97 {
98 CALL("CheckedFwSimplifier::CheckingPerformer::startChecking");
99
100 _recording=false;
101 }
102
doneCheckingTest::CheckedFwSimplifier::CheckingPerformer103 void doneChecking()
104 {
105 CALL("CheckedFwSimplifier::CheckingPerformer::doneChecking");
106
107 ClauseIterator it=_resultSet.iterator();
108
109 while(it.hasNext()) {
110 Clause* cl=it.next();
111 if(_ok) { _ok=false; cout<<endl; }
112 cout<<"+the first inference yielded premise that the second one did not"<<endl;
113 cout<<"query: "<<_query->toString()<<endl;
114 cout<<"result: "<<cl->toString()<<endl;
115 // ASSERTION_VIOLATION;
116 }
117
118
119 // ASS_EQ(_firstCnt,_secondCnt);
120 if(_firstCnt!=_secondCnt) {
121 if(_ok) { _ok=false; cout<<endl; }
122 cout<<"first and second inference didn't come up with the same number of premises"<<endl;
123 cout<<"first:second is "<<_firstCnt<<":"<<_secondCnt<<endl;
124 // INVALID_OPERATION("first and second inference didn't come up with the same premises");
125 }
126
127 if(!_ok) {
128 cout<<"All results given by first:"<<endl;
129 while(_resultsOfFirst.isNonEmpty()) {
130 cout<<_resultsOfFirst.pop()->toString()<<endl;
131 }
132 cout<<"All results given by second:"<<endl;
133 while(_resultsOfSecond.isNonEmpty()) {
134 cout<<_resultsOfSecond.pop()->toString()<<endl;
135 }
136 }
137 }
138
139 private:
140 Clause* _query;
141 bool _ok;
142 bool _recording;
143 DHSet<Clause*> _resultSet;
144 ClauseStack _resultsOfFirst;
145 ClauseStack _resultsOfSecond;
146 size_t _firstCnt;
147 size_t _secondCnt;
148 };
149
150
CheckedFwSimplifier(ForwardSimplificationEngine * fse1,ForwardSimplificationEngine * fse2)151 CheckedFwSimplifier::CheckedFwSimplifier(ForwardSimplificationEngine* fse1, ForwardSimplificationEngine* fse2)
152 : _fse1(fse1), _fse2(fse2)
153 {
154 CALL("CheckedFwSimplifier::CheckedFwSimplifier");
155 ASS(fse1);
156 ASS(fse2);
157
158 _chp=new CheckingPerformer();
159 }
160
~CheckedFwSimplifier()161 CheckedFwSimplifier::~CheckedFwSimplifier()
162 {
163 delete _chp;
164 }
165
attach(SaturationAlgorithm * salg)166 void CheckedFwSimplifier::attach(SaturationAlgorithm* salg)
167 {
168 CALL("CheckedFwSimplifier::attach");
169
170 _fse1->attach(salg);
171 _fse2->attach(salg);
172 }
173
detach()174 void CheckedFwSimplifier::detach()
175 {
176 CALL("CheckedFwSimplifier::detach");
177
178 _fse1->detach();
179 _fse2->detach();
180 }
181
perform(Clause * cl,ForwardSimplificationPerformer * simplPerformer)182 void CheckedFwSimplifier::perform(Clause *cl, ForwardSimplificationPerformer *simplPerformer)
183 {
184 CALL("CheckedFwSimplifier::perform");
185
186 _chp->resetAndStartRecording(cl);
187 _fse1->perform(cl, _chp);
188 _chp->startChecking();
189 _fse2->perform(cl, _chp);
190 _chp->doneChecking();
191
192 //perform the actual simplification
193 _fse1->perform(cl, simplPerformer);
194 }
195
196 }
197
198
199
200