1 /*****************************************************************************/
2 /*!
3 *\file cnf_theorem_producer.cpp
4 *\brief Implementation of CNF_TheoremProducer
5 *
6 * Author: Clark Barrett
7 *
8 * Created: Thu Jan 5 05:49:24 2006
9 *
10 * <hr>
11 *
12 * License to use, copy, modify, sell and/or distribute this software
13 * and its documentation for any purpose is hereby granted without
14 * royalty, subject to the terms and conditions defined in the \ref
15 * LICENSE file provided with this distribution.
16 *
17 * <hr>
18 *
19 */
20 /*****************************************************************************/
21
22 #include "cnf_manager.h"
23
24 #define _CVC3_TRUSTED_
25 #include "cnf_theorem_producer.h"
26
27
28 using namespace std;
29 using namespace CVC3;
30 using namespace SAT;
31
32
33 /////////////////////////////////////////////////////////////////////////////
34 // class CNF_Manager trusted methods
35 /////////////////////////////////////////////////////////////////////////////
36
37
createProofRules(TheoremManager * tm,const CLFlags & flags)38 CNF_Rules* CNF_Manager::createProofRules(TheoremManager* tm, const CLFlags& flags) {
39 return new CNF_TheoremProducer(tm, flags);
40 }
41
42
43 /////////////////////////////////////////////////////////////////////////////
44 // Proof rules
45 /////////////////////////////////////////////////////////////////////////////
46
47
48
getSmartClauses(const Theorem & thm,vector<Theorem> & clauses)49 void CNF_TheoremProducer::getSmartClauses(const Theorem& thm, vector<Theorem>& clauses)
50 {
51 // DebugAssert(!thm.getExpr().isDeductionLiteral(), "Expected unproved expr");
52 vector<Theorem> assumptions;
53 thm.clearAllFlags();
54 thm.GetSatAssumptions(assumptions);
55 // Proof pf;
56 // if (withProof()) {
57 // pf = newPf("learned_clause_smart", thm.getProof());
58 // }
59 Theorem thm2;
60 vector<Expr> TempVec;
61 vector<Proof> pfs;
62 if (!thm.getExpr().isFalse()) {
63 TempVec.push_back(thm.getExpr());
64 pfs.push_back(thm.getProof());
65 }
66 for (vector<Theorem>::size_type i = 0; i < assumptions.size(); i++) {
67 if (thm.getExpr() == assumptions[i].getExpr()) {
68 // skip this clause as it is trivial
69 if (!(assumptions[i].isAssump())) {
70 getSmartClauses(assumptions[i], clauses);
71 }
72 return;
73 }
74 TempVec.push_back(assumptions[i].getExpr().negate());
75 pfs.push_back(assumptions[i].getProof());
76 }
77
78 Proof pf;
79 if (TempVec.size() == 1){
80 if (withProof()) {
81 pf = newPf("learned_clause_smart", TempVec[0], pfs);
82 }
83 thm2 = newTheorem(TempVec[0], Assumptions::emptyAssump(), pf);
84 }
85 else if (TempVec.size() > 1) {
86 if (withProof()) {
87 pf = newPf("learned_clause_smart", Expr(OR, TempVec), pfs);
88 }
89 thm2 = newTheorem(Expr(OR, TempVec), Assumptions::emptyAssump(), pf);
90 }
91 else {
92 FatalAssert(false, "Should be unreachable");
93 }
94 thm2.setQuantLevel(thm.getQuantLevel());
95 clauses.push_back(thm2);
96 // thm.getExpr().setDeductionLiteral();
97
98 for (vector<Theorem>::iterator itr = assumptions.begin(); itr != assumptions.end(); itr++) {
99 if (!((*itr).isAssump())) {// && !(*itr).getExpr().isDeductionLiteral()) {
100 getSmartClauses((*itr), clauses);
101 }
102 }
103 }
104
105
learnedClauses(const Theorem & thm,vector<Theorem> & clauses,bool newLemma)106 void CNF_TheoremProducer::learnedClauses(const Theorem& thm,
107 vector<Theorem>& clauses,
108 bool newLemma)
109 {
110 IF_DEBUG(if(debugger.trace("cnf proofs")) {
111 ostream& os = debugger.getOS();
112 os << "learnedClause {" << endl;
113 os << thm;
114 })
115
116 if (!newLemma && d_smartClauses) {
117 getSmartClauses(thm, clauses);
118 return;
119 }
120
121 // if (newLemma || d_flags["dynack"].getInt() <= 0) {
122 // if (NewClausel == true) {
123 // return;
124 // }
125
126 vector<Expr> assumptions;
127 Proof pf;
128 thm.getLeafAssumptions(assumptions, true /*negate*/);
129
130 vector<Expr>::iterator iend = assumptions.end();
131 for (vector<Expr>::iterator i = assumptions.begin();
132 i != iend; ++i) {
133 DebugAssert(i->isAbsLiteral(), "Expected only literal assumptions");
134 }
135
136 if (!thm.getExpr().isFalse())
137 assumptions.push_back(thm.getExpr());
138
139 DebugAssert(assumptions.size() > 0, "Expected at least one entry");
140
141 Theorem thm2;
142 if (assumptions.size() == 1) {
143 if(withProof()) {
144 pf = newPf("learned_clause", thm.getProof());
145 }
146 thm2 = newTheorem(assumptions[0], Assumptions::emptyAssump(), pf);
147 }
148 else {
149 Expr clauseExpr = Expr(OR, assumptions);
150 if(withProof()) {
151 pf = newPf("learned_clause", thm.getProof());
152 }
153 thm2 = newTheorem(clauseExpr, Assumptions::emptyAssump(), pf);
154 }
155 thm2.setQuantLevel(thm.getQuantLevel());
156 clauses.push_back(thm2);
157 // }
158 // else {
159
160 // vector<Expr> congruences;
161
162 // thm.getAssumptionsAndCong(assumptions, congruences, true /*negate*/);
163
164 // vector<Expr>::iterator i = assumptions.begin(), iend = assumptions.end();
165 // for (; i != iend; ++i) {
166 // DebugAssert(i->isAbsLiteral(), "Expected only literal assumptions");
167 // }
168
169 // if (!thm.getExpr().isFalse())
170 // assumptions.push_back(thm.getExpr());
171
172 // if(withProof()) {
173 // pf = newPf("learned_clause", thm.getProof());
174 // }
175
176 // DebugAssert(assumptions.size() > 0, "Expected at least one entry");
177
178 // Theorem thm2;
179 // if (assumptions.size() == 1) {
180 // Expr clauseExpr = assumptions[0];
181 // if(withProof()) {
182 // pf = newPf("learned_clause", clauseExpr, thm.getProof());
183 // }
184 // thm2 = newTheorem(clauseExpr, Assumptions::emptyAssump(), pf);
185 // }
186 // else {
187 // Expr clauseExpr = Expr(OR, assumptions);
188 // if(withProof()) {
189 // pf = newPf("learned_clause", clauseExpr, thm.getProof());
190 // }
191 // thm2 = newTheorem(clauseExpr, Assumptions::emptyAssump(), pf);
192 // }
193 // thm2.setQuantLevel(thm.getQuantLevel());
194 // clauses.push_back(thm2);
195
196 // for (i = congruences.begin(), iend = congruences.end(); i != iend; ++i) {
197 // if (withProof()) {
198 // pf = newPf("congruence", *i);
199 // }
200 // thm2 = newTheorem(*i, Assumptions::emptyAssump(), pf);
201 // thm2.setQuantLevel(thm.getQuantLevel());
202 // clauses.push_back(thm2);
203 // }
204 // }
205 }
206
207
ifLiftRule(const Expr & e,int itePos)208 Theorem CNF_TheoremProducer::ifLiftRule(const Expr& e, int itePos) {
209 if(CHECK_PROOFS) {
210 CHECK_SOUND(e.getType().isBool(),
211 "CNF_TheoremProducer::ifLiftRule("
212 "input must be a Predicate: e = " + e.toString()+")");
213 CHECK_SOUND(itePos >= 0, "itePos negative"+int2string(itePos));
214 CHECK_SOUND(e.arity() > itePos && e[itePos].isITE(),
215 "CNF_TheoremProducer::ifLiftRule("
216 "input does not have an ITE: e = " + e.toString()+")");
217 }
218 const Expr& ite = e[itePos];
219 const Expr& cond = ite[0];
220 const Expr& t1 = ite[1];
221 const Expr& t2 = ite[2];
222
223 if(CHECK_PROOFS) {
224 CHECK_SOUND(cond.getType().isBool(),
225 "CNF_TheoremProducer::ifLiftRule("
226 "input does not have an ITE: e = " + e.toString()+")");
227 }
228
229 vector<Expr> k1 = e.getKids();
230 Op op(e.getOp());
231
232 k1[itePos] = t1;
233 Expr pred1 = Expr(op, k1);
234
235 k1[itePos] = t2;
236 Expr pred2 = Expr(op, k1);
237
238 Expr resultITE = cond.iteExpr(pred1, pred2);
239
240 Proof pf;
241 if (withProof())
242 pf = newPf("if_lift_rule", e, resultITE, d_em->newRatExpr(itePos));
243 return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf);
244 }
245
CNFtranslate(const Expr & before,const Expr & after,std::string reason,int pos,const vector<Theorem> & thms)246 Theorem CNF_TheoremProducer::CNFtranslate(const Expr& before,
247 const Expr& after,
248 std::string reason,
249 int pos,
250 const vector<Theorem>& thms) {
251 //well, this is assert the e as a theorem without any justification.
252 //change this as soon as possible
253 // cout << "###" << before;
254 Proof pf;
255 if (withProof()){
256 vector<Expr> chs ;
257 chs.push_back(d_em->newStringExpr(reason));
258 chs.push_back(before);
259 chs.push_back(after);
260 chs.push_back(d_em->newRatExpr(pos));
261 vector<Proof> pfs;
262 for(vector<Theorem>::const_iterator i = thms.begin(), iend= thms.end();
263 i != iend; i++){
264 pfs.push_back((*i).getProof());
265 }
266 pf = newPf("CNF", chs, pfs );
267 }
268 return newTheorem(after, Assumptions(thms), pf);
269 }
270
CNFITEtranslate(const Expr & before,const vector<Expr> & after,const vector<Theorem> & thms,int pos)271 Theorem CNF_TheoremProducer::CNFITEtranslate(const Expr& before,
272 const vector<Expr>& after,
273 const vector<Theorem>& thms,
274 int pos){
275 DebugAssert(3 == after.size(), "why this happens");
276 DebugAssert(3 == thms.size(), "why this happens");
277
278 Proof pf;
279 if (withProof()){
280 DebugAssert(thms[0].getRHS() == after[0] , "this never happens");
281 DebugAssert(thms[1].getRHS() == after[1] , "this never happens");
282 DebugAssert(thms[2].getRHS() == after[2] , "this never happens");
283 DebugAssert(thms[0].getLHS() == before[0] , "this never happens");
284 DebugAssert(thms[1].getLHS() == before[1] , "this never happens");
285 DebugAssert(thms[2].getLHS() == before[2] , "this never happens");
286
287 vector<Expr> chs ;
288 chs.push_back(before);
289 chs.push_back(after[0]);
290 chs.push_back(after[1]);
291 chs.push_back(after[2]);
292 chs.push_back(d_em->newRatExpr(pos));
293 vector<Proof> pfs;
294 pfs.push_back(thms[0].getProof());
295 pfs.push_back(thms[1].getProof());
296 pfs.push_back(thms[2].getProof());
297 pf = newPf("CNFITE", chs, pfs );
298 }
299
300 Expr newe0 = after[0];
301 Expr afterExpr = newe0.iteExpr(after[1],after[2]);
302 //we should produce a newRWTheorm whenever possible and then use iffmp rule to get the desired result
303 return newTheorem(afterExpr, Assumptions(thms), pf);
304 }
305
306
307
308
309
310 // because the way of cnf translation, add unit means the theorem from other parts of cvc3, not from cnf translation
CNFAddUnit(const Theorem & thm)311 Theorem CNF_TheoremProducer::CNFAddUnit(const Theorem& thm){
312
313 //wrap the thm so the hol light translator know this
314 Proof pf;
315 if (withProof()){
316 pf = newPf("cnf_add_unit", thm.getExpr(), thm.getProof() );
317 }
318 return newTheorem(thm.getExpr(), thm.getAssumptionsRef(), pf);
319 }
320
CNFConvert(const Expr & e,const Theorem & thm)321 Theorem CNF_TheoremProducer::CNFConvert(const Expr& e, const Theorem& thm){
322
323 //wrap the thm so the hol light translator know this
324 Proof pf;
325 if (withProof()){
326 pf = newPf("cnf_convert", e, thm.getExpr(), thm.getProof() );
327 }
328 DebugAssert(thm.getExpr().isOr(),"convert is not or exprs");
329 return newTheorem(thm.getExpr(), thm.getAssumptionsRef(), pf);
330 }
331
332
333