theorem_producer.cpp

Go to the documentation of this file.
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 }
00064 
00065 
00066 Proof TheoremProducer::newPf(const string& name)
00067 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name))); }
00068 
00069 
00070 Proof TheoremProducer::newPf(const string& name, const Expr& e)
00071 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e)); }
00072 
00073 
00074 Proof TheoremProducer::newPf(const string& name, const Proof& pf)
00075 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), pf.getExpr())); }
00076 
00077     
00078 Proof TheoremProducer::newPf(const string& name,
00079            const Expr& e1, const Expr& e2)
00080 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e1, e2)); }
00081 
00082 
00083 Proof TheoremProducer::newPf(const string& name, const Expr& e,
00084            const Proof& pf)
00085 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e, pf.getExpr())); }
00086 
00087 
00088 Proof TheoremProducer::newPf(const string& name, const Expr& e1,
00089            const Expr& e2, const Expr& e3) {
00090   vector<Expr> kids;
00091   kids.push_back(d_em->newVarExpr(name));
00092   kids.push_back(e1);
00093   kids.push_back(e2);
00094   kids.push_back(e3);
00095   return Proof(Expr(d_pfOp, kids));
00096 }
00097 
00098 
00099 Proof TheoremProducer::newPf(const string& name, const Expr& e1,
00100            const Expr& e2, const Proof& pf) {
00101   vector<Expr> kids;
00102   kids.push_back(d_em->newVarExpr(name));
00103   kids.push_back(e1);
00104   kids.push_back(e2);
00105   kids.push_back(pf.getExpr());
00106   return Proof(Expr(d_pfOp, kids));
00107 }
00108 
00109 
00110 Proof TheoremProducer::newPf(const string& name,
00111            Expr::iterator begin,
00112            const Expr::iterator &end) {
00113   vector<Expr> kids;
00114   kids.push_back(d_em->newVarExpr(name));
00115   kids.insert(kids.end(), begin, end);
00116   return Proof(Expr(d_pfOp, kids));
00117 }
00118 
00119 
00120 Proof TheoremProducer::newPf(const string& name, const Expr& e,
00121            Expr::iterator begin, const Expr::iterator &end) {
00122   vector<Expr> kids;
00123   kids.push_back(d_em->newVarExpr(name));
00124   kids.push_back(e);
00125   kids.insert(kids.end(), begin, end);
00126   return Proof(Expr(d_pfOp, kids));
00127 }
00128 
00129 
00130 Proof TheoremProducer::newPf(const string& name,
00131            Expr::iterator begin, const Expr::iterator &end,
00132            const vector<Proof>& pfs) {
00133   vector<Expr> kids;
00134   kids.push_back(d_em->newVarExpr(name));
00135   kids.insert(kids.end(), begin, end);
00136   for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
00137       i != iend; ++i)
00138     kids.push_back(i->getExpr());
00139   return Proof(Expr(d_pfOp, kids));
00140 }
00141 
00142 
00143 Proof TheoremProducer::newPf(const string& name,
00144            const vector<Expr>& args) {
00145   vector<Expr> kids;
00146   kids.push_back(d_em->newVarExpr(name));
00147   kids.insert(kids.end(), args.begin(), args.end());
00148   return Proof(Expr(d_pfOp, kids));
00149 }
00150 
00151 
00152 Proof TheoremProducer::newPf(const string& name,
00153            const Expr& e,
00154            const vector<Expr>& args) {
00155   vector<Expr> kids;
00156   kids.push_back(d_em->newVarExpr(name));
00157   kids.push_back(e);
00158   kids.insert(kids.end(), args.begin(), args.end());
00159   return Proof(Expr(d_pfOp, kids));
00160 }
00161 
00162 
00163 Proof TheoremProducer::newPf(const string& name,
00164            const Expr& e,
00165            const vector<Proof>& pfs) {
00166   vector<Expr> kids;
00167   kids.push_back(d_em->newVarExpr(name));
00168   kids.push_back(e);
00169   for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
00170       i != iend; ++i)
00171     kids.push_back(i->getExpr());
00172   return Proof(Expr(d_pfOp, kids));
00173 }
00174 
00175 
00176 Proof TheoremProducer::newPf(const string& name,
00177            const Expr& e1, const Expr& e2,
00178            const vector<Proof>& pfs) {
00179   vector<Expr> kids;
00180   kids.push_back(d_em->newVarExpr(name));
00181   kids.push_back(e1);
00182   kids.push_back(e2);
00183   for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
00184       i != iend; ++i)
00185     kids.push_back(i->getExpr());
00186   return Proof(Expr(d_pfOp, kids));
00187 }
00188 
00189 
00190 Proof TheoremProducer::newPf(const string& name,
00191            const vector<Proof>& pfs) {
00192   vector<Expr> kids;
00193   kids.push_back(d_em->newVarExpr(name));
00194   for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
00195       i != iend; ++i)
00196     kids.push_back(i->getExpr());
00197   return Proof(Expr(d_pfOp, kids));
00198 }
00199 
00200 
00201 Proof TheoremProducer::newPf(const string& name,
00202            const vector<Expr>& args,
00203            const Proof& pf) {
00204   vector<Expr> kids;
00205   kids.push_back(d_em->newVarExpr(name));
00206   kids.insert(kids.end(), args.begin(), args.end());
00207   kids.push_back(pf.getExpr());
00208   return Proof(Expr(d_pfOp, kids));
00209 }
00210 
00211 
00212 Proof TheoremProducer::newPf(const string& name,
00213            const vector<Expr>& args,
00214            const vector<Proof>& pfs) {
00215   vector<Expr> kids;
00216   kids.push_back(d_em->newVarExpr(name));
00217   kids.insert(kids.end(), args.begin(), args.end());
00218   for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
00219       i != iend; ++i)
00220     kids.push_back(i->getExpr());
00221   return Proof(Expr(d_pfOp, kids));
00222 }
00223 
00224 
00225 Proof TheoremProducer::newPf(const Proof& label, const Expr& frm,
00226            const Proof& pf) {
00227   Expr v(label.getExpr());
00228   IF_DEBUG(Type tp(frm, true));
00229   DebugAssert(v.isVar() && v.getType() == tp,
00230         "TheoremProducer::newPf: bad variable in LAMBDA expression: "
00231         +v.toString());
00232   vector<Expr> u;
00233   u.push_back(v);
00234   return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));
00235 }
00236 
00237 
00238 Proof TheoremProducer::newPf(const Proof& label, const Proof& pf) {
00239   Expr v(label.getExpr());
00240   DebugAssert(v.isVar(),
00241         "TheoremProducer::newPf: bad variable in LAMBDA expression: "
00242         +v.toString());
00243   vector<Expr> u;
00244   u.push_back(v);
00245   return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));
00246 }
00247 
00248 
00249 Proof TheoremProducer::newPf(const std::vector<Proof>& labels,
00250            const std::vector<Expr>& frms,
00251            const Proof& pf) {
00252   std::vector<Expr> u;
00253   for(unsigned i=0; i<labels.size(); i++) {
00254     const Expr& v = labels[i].getExpr();
00255     IF_DEBUG(Type tp(frms[i], true));
00256     DebugAssert(v.isVar(),
00257     "TheoremProducer::newPf: bad variable in LAMBDA expression: "
00258     +v.toString());
00259     DebugAssert(v.getType() == tp,
00260     "TheoremProducer::newPf: wrong variable type in "
00261     "LAMBDA expression.\nExpected: "+tp.getExpr().toString()
00262     +"\nFound: "+v.getType().getExpr().toString());
00263     u.push_back(v);
00264   }
00265   return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));
00266 }
00267 
00268 
00269 Proof TheoremProducer::newPf(const std::vector<Proof>& labels,
00270            const Proof& pf) {
00271   std::vector<Expr> u;
00272   for(unsigned i=0; i<labels.size(); i++) {
00273     const Expr& v = labels[i].getExpr();
00274     DebugAssert(v.isVar(),
00275     "TheoremProducer::newPf: bad variable in LAMBDA expression: "
00276     +v.toString());
00277     u.push_back(v);
00278   }
00279   return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));
00280 }

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