CVC3
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::Theorem3 Class Reference

Theorem3. More...

#include <theorem.h>

Collaboration diagram for CVC3::Theorem3:
Collaboration graph

Public Member Functions

void printDebug () const
 
 Theorem3 ()
 
virtual ~Theorem3 ()
 
bool isNull () const
 
bool isRewrite () const
 
bool isAssump () const
 
Expr getExpr () const
 
const ExprgetLHS () const
 
const ExprgetRHS () const
 
const AssumptionsgetAssumptionsRef () const
 
Proof getProof () const
 
int getScope () const
 
bool withProof () const
 
bool withAssumptions () const
 
std::string toString () const
 
void printx () const
 
void print () const
 
bool isAbsLiteral () const
 Check if the theorem is a literal.
 

Private Member Functions

 Theorem3 (TheoremManager *tm, const Expr &thm, const Assumptions &assump, const Proof &pf, bool isAssump=false, int scope=-1)
 
 Theorem3 (TheoremManager *tm, const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 

Private Attributes

Theorem d_thm
 

Friends

class TheoremProducer
 
bool operator== (const Theorem3 &t1, const Theorem3 &t2)
 
bool operator!= (const Theorem3 &t1, const Theorem3 &t2)
 
std::ostream & operator<< (std::ostream &os, const Theorem3 &t)
 

Detailed Description

Theorem3.

Author: Sergey Berezin

Created: Tue Nov 4 17:57:07 2003

Implements the 3-valued theorem used for the user assertions and the result of query. It is simply a wrapper around class Theorem, but has a different semantic meaning: the formula may have partial functions and has the Kleene's 3-valued interpretation. The fact that a Theorem3 value is derived means that the TCCs for the formula and all of its assumptions are valid in the current context, and the proofs of TCCs contribute to the set of assumptions.

Definition at line 308 of file theorem.h.

Constructor & Destructor Documentation

CVC3::Theorem3::Theorem3 ( TheoremManager tm,
const Expr thm,
const Assumptions assump,
const Proof pf,
bool  isAssump = false,
int  scope = -1 
)
inlineprivate

Definition at line 325 of file theorem.h.

CVC3::Theorem3::Theorem3 ( TheoremManager tm,
const Expr lhs,
const Expr rhs,
const Assumptions assump,
const Proof pf 
)
inlineprivate

Definition at line 332 of file theorem.h.

CVC3::Theorem3::Theorem3 ( )
inline

Definition at line 346 of file theorem.h.

virtual CVC3::Theorem3::~Theorem3 ( )
inlinevirtual

Definition at line 349 of file theorem.h.

Member Function Documentation

void CVC3::Theorem3::printDebug ( ) const
inline

Definition at line 341 of file theorem.h.

References d_thm, and CVC3::Theorem::printDebug().

bool CVC3::Theorem3::isNull ( ) const
inline

Definition at line 351 of file theorem.h.

References d_thm, and CVC3::Theorem::isNull().

bool CVC3::Theorem3::isRewrite ( ) const
inline

Definition at line 354 of file theorem.h.

References d_thm, and CVC3::Theorem::isRewrite().

bool CVC3::Theorem3::isAssump ( ) const
inline

Definition at line 355 of file theorem.h.

References d_thm, and CVC3::Theorem::isAssump().

Expr CVC3::Theorem3::getExpr ( ) const
inline

Definition at line 358 of file theorem.h.

References d_thm, and CVC3::Theorem::getExpr().

Referenced by CVC3::CommonTheoremProducer::implIntro3().

const Expr& CVC3::Theorem3::getLHS ( ) const
inline

Definition at line 359 of file theorem.h.

References d_thm, and CVC3::Theorem::getLHS().

const Expr& CVC3::Theorem3::getRHS ( ) const
inline

Definition at line 360 of file theorem.h.

References d_thm, and CVC3::Theorem::getRHS().

const Assumptions& CVC3::Theorem3::getAssumptionsRef ( ) const
inline
Proof CVC3::Theorem3::getProof ( ) const
inline

Definition at line 370 of file theorem.h.

References d_thm, and CVC3::Theorem::getProof().

Referenced by CVC3::CommonTheoremProducer::implIntro3().

int CVC3::Theorem3::getScope ( ) const
inline

Definition at line 374 of file theorem.h.

References d_thm, and CVC3::Theorem::getScope().

bool CVC3::Theorem3::withProof ( ) const
inline

Definition at line 377 of file theorem.h.

References d_thm, and CVC3::Theorem::withProof().

bool CVC3::Theorem3::withAssumptions ( ) const
inline

Definition at line 378 of file theorem.h.

References d_thm, and CVC3::Theorem::withAssumptions().

std::string CVC3::Theorem3::toString ( ) const
inline

Definition at line 410 of file theorem.h.

void CVC3::Theorem3::printx ( ) const
inline

Definition at line 384 of file theorem.h.

References d_thm, and CVC3::Theorem::printx().

void CVC3::Theorem3::print ( ) const
inline

Definition at line 385 of file theorem.h.

References d_thm, and CVC3::Theorem::print().

bool CVC3::Theorem3::isAbsLiteral ( ) const
inline

Check if the theorem is a literal.

Definition at line 388 of file theorem.h.

References d_thm, and CVC3::Theorem::isAbsLiteral().

Friends And Related Function Documentation

friend class TheoremProducer
friend

Definition at line 312 of file theorem.h.

bool operator== ( const Theorem3 t1,
const Theorem3 t2 
)
friend

Definition at line 316 of file theorem.h.

bool operator!= ( const Theorem3 t1,
const Theorem3 t2 
)
friend

Definition at line 319 of file theorem.h.

std::ostream& operator<< ( std::ostream &  os,
const Theorem3 t 
)
friend

Definition at line 390 of file theorem.h.

Member Data Documentation

Theorem CVC3::Theorem3::d_thm
private

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