CVC3  2.4.1
theorem_producer.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theorem_producer.cpp
4  * \brief See theorem_producer.h file for more information.
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Thu Feb 20 16:22:31 2003
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 
23 #define _CVC3_TRUSTED_
24 #include "theorem_producer.h"
25 #include "sound_exception.h"
26 #include "command_line_flags.h"
27 
28 
29 using namespace std;
30 using namespace CVC3;
31 
32 
33 void TheoremProducer::soundError(const std::string& file, int line,
34  const std::string& cond,
35  const std::string& msg)
36 {
37  ostringstream ss;
38  ss << "in " << file << ":" << line << " (" << cond << ")\n" << msg;
39  throw SoundException(ss.str());
40 }
41 
42 
43 // Constructor
44 TheoremProducer::TheoremProducer(TheoremManager *tm)
45  : d_tm(tm), d_em(tm->getEM()),
46  d_checkProofs(&(tm->getFlags()["check-proofs"].getBool())),
47  // Proof rule application: will have kids
48  d_pfOp(PF_APPLY)
50 
51 
53 {
54  // Counter to generate unique proof labels ('u')
55  static int s_counter = 0;
56  static string s_prefix = "assump";
57  ostringstream ss;
58  ss << s_counter++;
59 
60  if ((d_tm->getFlags()["lfsc-mode"]).getInt()!= 0 ) {
61  return newPf("assumptions", e);
62  }
63  else {
64  //TODO: Get rid of hack storing expr in Type field
65  // the following lines are commented by Yeting, for neat proofs
66  Expr var = d_tm->getEM()->newBoundVarExpr(s_prefix, ss.str(), Type(e, true));
67  return Proof(var); //by Yeting.
68  }
69 
70  return newPf("assumptions", e);
71  //return newPf("assumptions", var , e);
72 }
73 
74 
75 Proof TheoremProducer::newPf(const string& name)
76 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name))); }
77 
78 
79 Proof TheoremProducer::newPf(const string& name, const Expr& e)
80 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e)); }
81 
82 
83 Proof TheoremProducer::newPf(const string& name, const Proof& pf)
84 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), pf.getExpr())); }
85 
86 
87 Proof TheoremProducer::newPf(const string& name,
88  const Expr& e1, const Expr& e2)
89 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e1, e2)); }
90 
91 
92 Proof TheoremProducer::newPf(const string& name, const Expr& e,
93  const Proof& pf)
94 { return Proof(Expr(d_pfOp, d_em->newVarExpr(name), e, pf.getExpr())); }
95 
96 
97 Proof TheoremProducer::newPf(const string& name, const Expr& e1,
98  const Expr& e2, const Expr& e3) {
99  vector<Expr> kids;
100  kids.push_back(d_em->newVarExpr(name));
101  kids.push_back(e1);
102  kids.push_back(e2);
103  kids.push_back(e3);
104  return Proof(Expr(d_pfOp, kids));
105 }
106 
107 
108 Proof TheoremProducer::newPf(const string& name, const Expr& e1,
109  const Expr& e2, const Proof& pf) {
110  vector<Expr> kids;
111  kids.push_back(d_em->newVarExpr(name));
112  kids.push_back(e1);
113  kids.push_back(e2);
114  kids.push_back(pf.getExpr());
115  return Proof(Expr(d_pfOp, kids));
116 }
117 
118 
119 Proof TheoremProducer::newPf(const string& name,
120  Expr::iterator begin,
121  const Expr::iterator &end) {
122  vector<Expr> kids;
123  kids.push_back(d_em->newVarExpr(name));
124  kids.insert(kids.end(), begin, end);
125  return Proof(Expr(d_pfOp, kids));
126 }
127 
128 
129 Proof TheoremProducer::newPf(const string& name, const Expr& e,
130  Expr::iterator begin, const Expr::iterator &end) {
131  vector<Expr> kids;
132  kids.push_back(d_em->newVarExpr(name));
133  kids.push_back(e);
134  kids.insert(kids.end(), begin, end);
135  return Proof(Expr(d_pfOp, kids));
136 }
137 
138 
139 Proof TheoremProducer::newPf(const string& name,
140  Expr::iterator begin, const Expr::iterator &end,
141  const vector<Proof>& pfs) {
142  vector<Expr> kids;
143  kids.push_back(d_em->newVarExpr(name));
144  kids.insert(kids.end(), begin, end);
145  for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
146  i != iend; ++i)
147  kids.push_back(i->getExpr());
148  return Proof(Expr(d_pfOp, kids));
149 }
150 
151 
152 Proof TheoremProducer::newPf(const string& name,
153  const vector<Expr>& args) {
154  vector<Expr> kids;
155  kids.push_back(d_em->newVarExpr(name));
156  kids.insert(kids.end(), args.begin(), args.end());
157  return Proof(Expr(d_pfOp, kids));
158 }
159 
160 
161 Proof TheoremProducer::newPf(const string& name,
162  const Expr& e,
163  const vector<Expr>& args) {
164  vector<Expr> kids;
165  kids.push_back(d_em->newVarExpr(name));
166  kids.push_back(e);
167  kids.insert(kids.end(), args.begin(), args.end());
168  return Proof(Expr(d_pfOp, kids));
169 }
170 
171 
172 Proof TheoremProducer::newPf(const string& name,
173  const Expr& e,
174  const vector<Proof>& pfs) {
175  vector<Expr> kids;
176  kids.push_back(d_em->newVarExpr(name));
177  kids.push_back(e);
178  for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
179  i != iend; ++i)
180  kids.push_back(i->getExpr());
181  return Proof(Expr(d_pfOp, kids));
182 }
183 
184 
185 Proof TheoremProducer::newPf(const string& name,
186  const Expr& e1, const Expr& e2,
187  const vector<Proof>& pfs) {
188  vector<Expr> kids;
189  kids.push_back(d_em->newVarExpr(name));
190  kids.push_back(e1);
191  kids.push_back(e2);
192  for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
193  i != iend; ++i)
194  kids.push_back(i->getExpr());
195  return Proof(Expr(d_pfOp, kids));
196 }
197 
198 
199 Proof TheoremProducer::newPf(const string& name,
200  const vector<Proof>& pfs) {
201  vector<Expr> kids;
202  kids.push_back(d_em->newVarExpr(name));
203  for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
204  i != iend; ++i)
205  kids.push_back(i->getExpr());
206  return Proof(Expr(d_pfOp, kids));
207 }
208 
209 
210 Proof TheoremProducer::newPf(const string& name,
211  const vector<Expr>& args,
212  const Proof& pf) {
213  vector<Expr> kids;
214  kids.push_back(d_em->newVarExpr(name));
215  kids.insert(kids.end(), args.begin(), args.end());
216  kids.push_back(pf.getExpr());
217  return Proof(Expr(d_pfOp, kids));
218 }
219 
220 
221 Proof TheoremProducer::newPf(const string& name,
222  const vector<Expr>& args,
223  const vector<Proof>& pfs) {
224  vector<Expr> kids;
225  kids.push_back(d_em->newVarExpr(name));
226  kids.insert(kids.end(), args.begin(), args.end());
227  for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
228  i != iend; ++i)
229  kids.push_back(i->getExpr());
230  return Proof(Expr(d_pfOp, kids));
231 }
232 
233 
234 Proof TheoremProducer::newPf(const Proof& label, const Expr& frm,
235  const Proof& pf) {
236  Expr v(label.getExpr());
237  IF_DEBUG(Type tp(frm, true);)
238  DebugAssert(v.isVar() && v.getType() == tp,
239  "TheoremProducer::newPf: bad variable in LAMBDA expression: "
240  +v.toString());
241  vector<Expr> u;
242  u.push_back(v);
243  return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));
244 }
245 
246 
247 Proof TheoremProducer::newPf(const Proof& label, const Proof& pf) {
248  Expr v(label.getExpr());
249  DebugAssert(v.isVar(),
250  "TheoremProducer::newPf: bad variable in LAMBDA expression: "
251  +v.toString());
252  vector<Expr> u;
253  u.push_back(v);
254  return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));
255 }
256 
257 
258 Proof TheoremProducer::newPf(const std::vector<Proof>& labels,
259  const std::vector<Expr>& frms,
260  const Proof& pf) {
261  std::vector<Expr> u;
262  for(unsigned i=0; i<labels.size(); i++) {
263  const Expr& v = labels[i].getExpr();
264  IF_DEBUG(Type tp(frms[i], true);)
265  DebugAssert(v.isVar(),
266  "TheoremProducer::newPf: bad variable in LAMBDA expression: "
267  +v.toString());
268  DebugAssert(v.getType() == tp,
269  "TheoremProducer::newPf: wrong variable type in "
270  "LAMBDA expression.\nExpected: "+tp.getExpr().toString()
271  +"\nFound: "+v.getType().getExpr().toString());
272  u.push_back(v);
273  }
274  return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));
275 }
276 
277 
278 Proof TheoremProducer::newPf(const std::vector<Proof>& labels,
279  const Proof& pf) {
280  std::vector<Expr> u;
281  for(unsigned i=0; i<labels.size(); i++) {
282  const Expr& v = labels[i].getExpr();
283  DebugAssert(v.isVar(),
284  "TheoremProducer::newPf: bad variable in LAMBDA expression: "
285  +v.toString());
286  u.push_back(v);
287  }
288  return Proof(d_tm->getEM()->newClosureExpr(LAMBDA, u, pf.getExpr()));
289 }