cnf_theorem_producer.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file cnf_theorem_producer.cpp
00004  *\brief Implementation of CNF_TheoremProducer
00005  *
00006  * Author: Clark Barrett
00007  *
00008  * Created: Thu Jan  5 05:49:24 2006
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #include "cnf_manager.h"
00023 
00024 #define _CVC3_TRUSTED_
00025 #include "cnf_theorem_producer.h"
00026 
00027 
00028 using namespace std;
00029 using namespace CVC3;
00030 using namespace SAT;
00031 
00032 
00033 /////////////////////////////////////////////////////////////////////////////
00034 // class CNF_Manager trusted methods
00035 /////////////////////////////////////////////////////////////////////////////
00036 
00037 
00038 CNF_Rules* CNF_Manager::createProofRules(TheoremManager* tm) {
00039   return new CNF_TheoremProducer(tm);
00040 }
00041 
00042 
00043 /////////////////////////////////////////////////////////////////////////////
00044 // Proof rules
00045 /////////////////////////////////////////////////////////////////////////////
00046 
00047 
00048 Theorem CNF_TheoremProducer::learnedClause(const Theorem& thm)
00049 {
00050   IF_DEBUG(if(debugger.trace("cnf proofs")) {
00051     ostream& os = debugger.getOS();
00052     os << "learnedClause {" << endl;
00053     os << thm;
00054   });
00055 
00056   if(CHECK_PROOFS) {
00057     CHECK_SOUND(withAssumptions(),
00058     "learnedClause: called while running without assumptions");
00059   }
00060 
00061   vector<Expr> assumptions;
00062 
00063   thm.getLeafAssumptions(assumptions, true /*negate*/);
00064 
00065   vector<Expr>::iterator iend = assumptions.end();
00066   for (vector<Expr>::iterator i = assumptions.begin();
00067        i != iend; ++i) {
00068     DebugAssert(i->isAbsLiteral(), "Expected only literal assumptions");
00069   }
00070 
00071   if (!thm.getExpr().isFalse())
00072     assumptions.push_back(thm.getExpr());
00073 
00074   Proof pf;
00075 
00076   if(withProof()) {
00077     pf = newPf("learned_clause", thm.getProof());
00078   }
00079 
00080   // Use ExprManager in newExpr, since assumptions may be empty
00081   DebugAssert(assumptions.size() > 0, "Expected at least one entry");
00082 
00083   Theorem thm2;
00084   if (assumptions.size() == 1) {
00085     thm2 = newTheorem(assumptions[0], Assumptions::emptyAssump(), pf);
00086   }
00087   else {
00088     thm2 = newTheorem(Expr(OR, assumptions), Assumptions::emptyAssump(), pf);
00089   }
00090   thm2.setQuantLevel(thm.getQuantLevel());
00091   return thm2;
00092 }
00093 
00094 
00095 Theorem CNF_TheoremProducer::ifLiftRule(const Expr& e, int itePos) {
00096   if(CHECK_PROOFS) {
00097     CHECK_SOUND(e.getType().isBool(),
00098     "CNF_TheoremProducer::ifLiftRule("
00099     "input must be a Predicate: e = " + e.toString()+")");
00100     CHECK_SOUND(itePos >= 0, "itePos negative"+int2string(itePos));
00101     CHECK_SOUND(e.arity() > itePos && e[itePos].isITE(),
00102     "CNF_TheoremProducer::ifLiftRule("
00103     "input does not have an ITE: e = " + e.toString()+")");
00104   }
00105   const Expr& ite = e[itePos];
00106   const Expr& cond = ite[0];
00107   const Expr& t1 = ite[1];
00108   const Expr& t2 = ite[2];
00109 
00110   if(CHECK_PROOFS) {
00111     CHECK_SOUND(cond.getType().isBool(),
00112     "CNF_TheoremProducer::ifLiftRule("
00113     "input does not have an ITE: e = " + e.toString()+")");
00114   }    
00115 
00116   vector<Expr> k1 = e.getKids();
00117   Op op(e.getOp());
00118 
00119   k1[itePos] = t1;
00120   Expr pred1 =  Expr(op, k1);
00121 
00122   k1[itePos] = t2;
00123   Expr pred2 =  Expr(op, k1);
00124 
00125   Expr resultITE = cond.iteExpr(pred1, pred2);
00126 
00127   Proof pf;
00128   if (withProof())
00129     pf = newPf("if_lift_rule", e, d_em->newRatExpr(itePos));
00130   return newRWTheorem(e, resultITE, Assumptions::emptyAssump(), pf);
00131 }

Generated on Tue Jul 3 14:33:35 2007 for CVC3 by  doxygen 1.5.1