23 #define _CVC3_TRUSTED_
33 void TheoremProducer::soundError(
const std::string& file,
int line,
34 const std::string& cond,
35 const std::string& msg)
38 ss <<
"in " << file <<
":" << line <<
" (" << cond <<
")\n" << msg;
45 : d_tm(tm), d_em(tm->getEM()),
46 d_checkProofs(&(tm->getFlags()[
"check-proofs"].getBool())),
55 static int s_counter = 0;
56 static string s_prefix =
"assump";
61 return newPf(
"assumptions", e);
70 return newPf(
"assumptions", e);
124 kids.insert(kids.end(), begin, end);
134 kids.insert(kids.end(), begin, end);
141 const vector<Proof>& pfs) {
144 kids.insert(kids.end(), begin, end);
145 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
147 kids.push_back(i->getExpr());
153 const vector<Expr>& args) {
156 kids.insert(kids.end(), args.begin(), args.end());
163 const vector<Expr>& args) {
167 kids.insert(kids.end(), args.begin(), args.end());
174 const vector<Proof>& pfs) {
178 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
180 kids.push_back(i->getExpr());
187 const vector<Proof>& pfs) {
192 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
194 kids.push_back(i->getExpr());
200 const vector<Proof>& pfs) {
203 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
205 kids.push_back(i->getExpr());
211 const vector<Expr>& args,
215 kids.insert(kids.end(), args.begin(), args.end());
222 const vector<Expr>& args,
223 const vector<Proof>& pfs) {
226 kids.insert(kids.end(), args.begin(), args.end());
227 for(vector<Proof>::const_iterator i=pfs.begin(), iend=pfs.end();
229 kids.push_back(i->getExpr());
239 "TheoremProducer::newPf: bad variable in LAMBDA expression: "
250 "TheoremProducer::newPf: bad variable in LAMBDA expression: "
259 const std::vector<Expr>& frms,
262 for(
unsigned i=0; i<labels.size(); i++) {
263 const Expr& v = labels[i].getExpr();
266 "TheoremProducer::newPf: bad variable in LAMBDA expression: "
269 "TheoremProducer::newPf: wrong variable type in "
281 for(
unsigned i=0; i<labels.size(); i++) {
282 const Expr& v = labels[i].getExpr();
284 "TheoremProducer::newPf: bad variable in LAMBDA expression: "
Data structure of expressions in CVC3.
ExprManager * getEM() const
MS C++ specific settings.
#define DebugAssert(cond, str)
Expr newClosureExpr(int kind, const Expr &var, const Expr &body)
Expr newBoundVarExpr(const std::string &name, const std::string &uid)
const Expr & getExpr() const
std::string toString() const
Print the expression to a string.
Expr newLeafExpr(const Op &op)
Proof newLabel(const Expr &e)
Create a new proof label (bound variable) for an assumption (formula)
Expr newVarExpr(const std::string &s)
Proof newPf(const std::string &name)
const CLFlags & getFlags() const
An exception to be thrown when unsoundness is detected in a proof rule.
Type getType() const
Get the type. Recursively compute if necessary.