CVC3
cnf_theorem_producer.cpp
Go to the documentation of this file.
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 
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 
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 
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 
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 
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 
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
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 
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