00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
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
00044 TheoremProducer::TheoremProducer(TheoremManager *tm)
00045 : d_tm(tm), d_em(tm->getEM()),
00046 d_checkProofs(&(tm->getFlags()["check-proofs"].getBool())),
00047
00048 d_pfOp(PF_APPLY)
00049 { d_hole = d_em->newLeafExpr(PF_HOLE); }
00050
00051
00052 Proof TheoremProducer::newLabel(const Expr& e)
00053 {
00054
00055 static int s_counter = 0;
00056 static string s_prefix = "assump";
00057 ostringstream ss;
00058 ss << s_counter++;
00059
00060
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 }