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,