CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file theorem_producer.cpp 00004 * \brief See theorem_producer.h file for more information. 00005 * 00006 * Author: Sergey Berezin 00007 * 00008 * Created: Thu Feb 20 16:22:31 2003 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 00023 #define _CVC3_TRUSTED_ 00024 #include "theorem_producer.h" 00025 #include "sound_exception.h" 00026 #include "command_line_flags.h" 00027 00028 00029 using namespace std; 00030 using namespace CVC3; 00031 00032 00033 void TheoremProducer::soundError(const std::string& file, int line, 00034 const std::string& cond, 00035 const std::string& msg) 00036 { 00037 ostringstream ss; 00038 ss << "in " << file << ":" << line << " (" << cond << ")\n" << msg; 00039 throw SoundException(ss.str()); 00040 } 00041 00042 00043 // Constructor 00044 TheoremProducer::TheoremProducer(TheoremManager *tm) 00045 : d_tm(tm), d_em(tm->getEM()), 00046 d_checkProofs(&(tm->getFlags()["check-proofs"].getBool())), 00047 // Proof rule application: will have kids 00048 d_pfOp(PF_APPLY) 00049 { d_hole = d_em->newLeafExpr(PF_HOLE); } 00050 00051 00052 Proof TheoremProducer::newLabel(const Expr& e) 00053 { 00054 // Counter to generate unique proof labels ('u') 00055 static int s_counter = 0; 00056 static string s_prefix = "assump"; 00057 ostringstream ss; 00058 ss << s_counter++; 00059 00060 //TODO: Get rid of hack storing expr in Type field 00061 Expr var = d_tm->getEM()->newBoundVarExpr(s_prefix, ss.str(), Type(e, true)); 00062 return Proof(var); 00063 //return newPf("assumptions", var , e); 00064 } 00065 00066 00067 Proof TheoremProducer::newPf(const string& name) 00068 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name))); } 00069 00070 00071 Proof TheoremProducer::newPf(const string& name, const Expr& e) 00072 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e)); } 00073 00074 00075 Proof TheoremProducer::newPf(const string& name, const Proof& pf) 00076 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), pf.getExpr())); } 00077 00078 00079 Proof TheoremProducer::newPf(const string& name, 00080 const Expr& e1, const Expr& e2) 00081 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e1, e2)); } 00082 00083 00084 Proof TheoremProducer::newPf(const string& name, const Expr& e, 00085 const Proof& pf) 00086 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e, pf.getExpr())); } 00087 00088 00089 Proof TheoremProducer::newPf(const string& name, const Expr& e1, 00090 const Expr& e2, const Expr& e3) { 00091 vector<Expr> kids; 00092 kids.push_back(d_em->newVarExpr(name)); 00093 kids.push_back(e1); 00094 kids.push_back(e2); 00095 kids.push_back(e3); 00096 return Proof(Expr(d_pfOp, kids)); 00097 } 00098 00099 00100 Proof TheoremProducer::newPf(const string& name, const Expr& e1, 00101 const Expr& e2, const Proof& pf) { 00102 vector<Expr> kids; 00103 kids.push_back(d_em->newVarExpr(name)); 00104 kids.push_back(e1); 00105 kids.push_back(e2); 00106 kids.push_back(pf.getExpr()); 00107 return Proof(Expr(d_pfOp, kids)); 00108 } 00109 00110 00111 Proof TheoremProducer::newPf(const string& name, 00112 Expr::iterator begin, 00113 const Expr::iterator &end) { 00114 vector<Expr> kids; 00115 kids.push_back(d_em->newVarExpr(name)); 00116 kids.insert(kids.end(), begin, end); 00117 return Proof(Expr(d_pfOp, kids)); 00118 } 00119 00120 00121 Proof TheoremProducer::newPf(const string& name, const Expr& e, 00122 Expr::iterator begin, const Expr::iterator &end) { 00123 vector<Expr> kids; 00124 kids.push_back(d_em->newVarExpr(name)); 00125 kids.push_back(e); 00126 kids.insert(kids.end(), begin, end); 00127 return Proof(Expr(d_pfOp, kids)); 00128 } 00129 00130 00131 Proof TheoremProducer::newPf(const string& name, 00132 Expr::iterator begin, const Expr::iterator &end, 00133 const vector<Proof>& pfs) { 00134 vector<Expr> kids; 00135 kids.push_back(d_em->newVarExpr(name)); 00136 kids.insert(kids.end(), begin, end); 00137 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end(); 00138 i != iend; ++i) 00139 kids.push_back(i->getExpr()); 00140 return Proof(Expr(d_pfOp, kids)); 00141 } 00142 00143 00144 Proof TheoremProducer::newPf(const string& name, 00145 const vector<Expr>& args) { 00146 vector<Expr> kids; 00147 kids.push_back(d_em->newVarExpr(name)); 00148 kids.insert(kids.end(), args.begin(), args.end()); 00149 return Proof(Expr(d_pfOp, kids)); 00150 } 00151 00152 00153 Proof TheoremProducer::newPf(const string& name, 00154 const Expr& e, 00155 const vector<Expr>& args) { 00156 vector<Expr> kids; 00157 kids.push_back(d_em->newVarExpr(name)); 00158 kids.push_back(e); 00159 kids.insert(kids.end(), args.begin(), args.end()); 00160 return Proof(Expr(d_pfOp, kids)); 00161 } 00162 00163 00164 Proof TheoremProducer::newPf(const string& name, 00165 const Expr& e, 00166 const vector<Proof>& pfs) { 00167 vector<Expr> kids; 00168 kids.push_back(d_em->newVarExpr(name)); 00169 kids.push_back(e); 00170 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end(); 00171 i != iend; ++i) 00172 kids.push_back(i->getExpr()); 00173 return Proof(Expr(d_pfOp, kids)); 00174 } 00175 00176 00177 Proof TheoremProducer::newPf(const string& name, 00178 const Expr& e1, const Expr& e2, 00179 const vector<Proof>& pfs) { 00180 vector<Expr> kids; 00181 kids.push_back(d_em->newVarExpr(name)); 00182 kids.push_back(e1); 00183 kids.push_back(e2); 00184 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end(); 00185 i != iend; ++i) 00186 kids.push_back(i->getExpr()); 00187 return Proof(Expr(d_pfOp, kids)); 00188 } 00189 00190 00191 Proof TheoremProducer::newPf(const string& name, 00192 const vector<Proof>& pfs) { 00193 vector<Expr> kids; 00194 kids.push_back(d_em->newVarExpr(name)); 00195 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end(); 00196 i != iend; ++i) 00197 kids.push_back(i->getExpr()); 00198 return Proof(Expr(d_pfOp, kids)); 00199 } 00200 00201 00202 Proof TheoremProducer::newPf(const string& name, 00203 const vector<Expr>& args, 00204 const Proof& pf) { 00205 vector<Expr> kids; 00206 kids.push_back(d_em->newVarExpr(name)); 00207 kids.insert(kids.end(), args.begin(), args.end()); 00208 kids.push_back(pf.getExpr()); 00209 return Proof(Expr(d_pfOp, kids)); 00210 } 00211 00212 00213 Proof TheoremProducer::newPf(const string& name, 00214 const vector<Expr>& args, 00215 const vector<Proof>& pfs) { 00216 vector<Expr> kids; 00217 kids.push_back(d_em->newVarExpr(name)); 00218 kids.insert(kids.end(), args.begin(), args.end()); 00219 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end(); 00220 i != iend; ++i) 00221 kids.push_back(i->getExpr()); 00222 return Proof(Expr(d_pfOp, kids)); 00223 } 00224 00225 00226 Proof TheoremProducer::newPf(const Proof& label, const Expr& frm, 00227 const Proof& pf) { 00228 Expr v(label.getExpr()); 00229 IF_DEBUG(Type tp(frm, true);) 00230 DebugAssert(v.isVar() && v.getType() == tp, 00231 "TheoremProducer::newPf: bad variable in LAMBDA expression: " 00232 +v.toString()); 00233 vector<Expr> u; 00234 u.push_back(v); 00235 return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr())); 00236 } 00237 00238 00239 Proof TheoremProducer::newPf(const Proof& label, const Proof& pf) { 00240 Expr v(label.getExpr()); 00241 DebugAssert(v.isVar(), 00242 "TheoremProducer::newPf: bad variable in LAMBDA expression: " 00243 +v.toString()); 00244 vector<Expr> u; 00245 u.push_back(v); 00246 return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr())); 00247 } 00248 00249 00250 Proof TheoremProducer::newPf(const std::vector<Proof>& labels, 00251 const std::vector<Expr>& frms, 00252 const Proof& pf) { 00253 std::vector<Expr> u; 00254 for(unsigned i=0; i<labels.size(); i++) { 00255 const Expr& v = labels[i].getExpr(); 00256 IF_DEBUG(Type tp(frms[i], true);) 00257 DebugAssert(v.isVar(), 00258 "TheoremProducer::newPf: bad variable in LAMBDA expression: " 00259 +v.toString()); 00260 DebugAssert(v.getType() == tp, 00261 "TheoremProducer::newPf: wrong variable type in " 00262 "LAMBDA expression.\nExpected: "+tp.getExpr().toString() 00263 +"\nFound: "+v.getType().getExpr().toString()); 00264 u.push_back(v); 00265 } 00266 return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr())); 00267 } 00268 00269 00270 Proof TheoremProducer::newPf(const std::vector<Proof>& labels, 00271 const Proof& pf) { 00272 std::vector<Expr> u; 00273 for(unsigned i=0; i<labels.size(); i++) { 00274 const Expr& v = labels[i].getExpr(); 00275 DebugAssert(v.isVar(), 00276 "TheoremProducer::newPf: bad variable in LAMBDA expression: " 00277 +v.toString()); 00278 u.push_back(v); 00279 } 00280 return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr())); 00281 }