68 #ifndef _CVC3_TRUSTED_
69 #warning "This file should be included only by TRUSTED code. Define _CVC3_TRUSTED_ before including this file."
72 #ifndef _cvc3__theorem_producer_h_
73 #define _cvc3__theorem_producer_h_
83 #define CHECK_SOUND(cond, msg) { if(!(cond)) \
84 soundError(__FILE__, __LINE__, #cond, msg); }
87 #define CHECK_PROOFS *d_checkProofs
111 TRACE(
"newTheorem",
"newTheorem(", thm,
")");
112 debugger.counter(
"newTheorem() called on equality")++;
137 TRACE(
"newTheorem",
"newTheorem3(", thm,
")");
138 debugger.counter(
"newTheorem3() called on equality")++;
149 void soundError(
const std::string& file,
int line,
150 const std::string& cond,
const std::string& msg);
193 const std::vector<Proof>& pfs);
196 Proof newPf(
const std::string& name,
const std::vector<Expr>& args);
198 const std::vector<Expr>& args);
200 const std::vector<Proof>& pfs);
202 const std::vector<Proof>& pfs);
203 Proof newPf(
const std::string& name,
const std::vector<Proof>& pfs);
204 Proof newPf(
const std::string& name,
const std::vector<Expr>& args,
206 Proof newPf(
const std::string& name,
const std::vector<Expr>& args,
207 const std::vector<Proof>& pfs);
221 const std::vector<Expr>& frms,
virtual ~TheoremProducer()
Theorem newAssumption(const Expr &thm, const Proof &pf, int scope=-1)
Data structure of expressions in CVC3.
TheoremProducer(TheoremManager *tm)
Theorem newTheorem(const Expr &thm, const Assumptions &assump, const Proof &pf)
Create a new theorem. See also newRWTheorem() and newReflTheorem()
Theorem newReflTheorem(const Expr &e)
Create a reflexivity theorem.
bool withProof()
Testing whether to generate proofs.
bool withAssumptions()
Testing whether to generate assumptions.
const bool * d_checkProofs
Proof newLabel(const Expr &e)
Create a new proof label (bound variable) for an assumption (formula)
Theorem3 newTheorem3(const Expr &thm, const Assumptions &assump, const Proof &pf)
Theorem newRWTheorem(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
Create a rewrite theorem: lhs = rhs.
void soundError(const std::string &file, int line, const std::string &cond, const std::string &msg)
Theorem3 newRWTheorem3(const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
Proof newPf(const std::string &name)
static const Assumptions & emptyAssump()