CVC3  2.4.1
Public Member Functions | List of all members
CVC3::SimulateTheoremProducer Class Reference

#include <simulate_theorem_producer.h>

Inheritance diagram for CVC3::SimulateTheoremProducer:
CVC3::SimulateProofRules CVC3::TheoremProducer

Public Member Functions

 SimulateTheoremProducer (TheoremManager *tm)
 Constructor.
virtual ~SimulateTheoremProducer ()
virtual Theorem expandSimulate (const Expr &e)
 SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k)
- Public Member Functions inherited from CVC3::SimulateProofRules
virtual ~SimulateProofRules ()
 Destructor.
- Public Member Functions inherited from CVC3::TheoremProducer
 TheoremProducer (TheoremManager *tm)
virtual ~TheoremProducer ()
bool withProof ()
 Testing whether to generate proofs.
bool withAssumptions ()
 Testing whether to generate assumptions.
Proof newLabel (const Expr &e)
 Create a new proof label (bound variable) for an assumption (formula)
Proof newPf (const std::string &name)
Proof newPf (const std::string &name, const Expr &e)
Proof newPf (const std::string &name, const Proof &pf)
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2)
Proof newPf (const std::string &name, const Expr &e, const Proof &pf)
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end)
Proof newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)
Proof newPf (const std::string &name, const std::vector< Expr > &args)
Proof newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args)
Proof newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs)
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)
Proof newPf (const std::string &name, const std::vector< Proof > &pfs)
Proof newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf)
Proof newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)
Proof newPf (const Proof &label, const Expr &frm, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label formula proof)
Proof newPf (const Proof &label, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label proof).
Proof newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)
 Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf)
Proof newPf (const std::vector< Proof > &labels, const Proof &pf)

Additional Inherited Members

- Protected Member Functions inherited from CVC3::TheoremProducer
Theorem newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf)
 Create a new theorem. See also newRWTheorem() and newReflTheorem()
Theorem newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 Create a rewrite theorem: lhs = rhs.
Theorem newReflTheorem (const Expr &e)
 Create a reflexivity theorem.
Theorem newAssumption (const Expr &thm, const Proof &pf, int scope=-1)
Theorem3 newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf)
Theorem3 newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
void soundError (const std::string &file, int line, const std::string &cond, const std::string &msg)
- Protected Attributes inherited from CVC3::TheoremProducer
TheoremManagerd_tm
ExprManagerd_em
const bool * d_checkProofs
Op d_pfOp
Expr d_hole

Detailed Description

Definition at line 30 of file simulate_theorem_producer.h.

Constructor & Destructor Documentation

CVC3::SimulateTheoremProducer::SimulateTheoremProducer ( TheoremManager tm)
inline

Constructor.

Definition at line 34 of file simulate_theorem_producer.h.

virtual CVC3::SimulateTheoremProducer::~SimulateTheoremProducer ( )
inlinevirtual

Definition at line 35 of file simulate_theorem_producer.h.

Member Function Documentation

Theorem SimulateTheoremProducer::expandSimulate ( const Expr e)
virtual

The documentation for this class was generated from the following files: