CVC3::Theorem3 Class Reference

Theorem3. More...

#include <theorem.h>

Collaboration diagram for CVC3::Theorem3:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Friends


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 
) [inline, private]

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 
) [inline, private]

Definition at line 332 of file theorem.h.

CVC3::Theorem3::Theorem3 (  )  [inline]

Definition at line 346 of file theorem.h.

virtual CVC3::Theorem3::~Theorem3 (  )  [inline, virtual]

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().

Referenced by CVC3::VCL::getAssumptionsTCC(), CVC3::VCL::getClosure(), CVC3::VCL::getProof(), CVC3::VCL::getProofClosure(), CVC3::VCL::getProofQuery(), and CVC3::VCL::incomplete().

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::VCL::getClosure(), CVC3::VCL::getProofQuery(), and 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]

Definition at line 365 of file theorem.h.

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

Referenced by CVC3::VCL::deriveClosure(), and CVC3::CommonTheoremProducer::implIntro3().

Proof CVC3::Theorem3::getProof (  )  const [inline]

Definition at line 370 of file theorem.h.

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

Referenced by CVC3::VCL::getProofClosure(), and 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]

Definition at line 314 of file theorem.h.

Referenced by getAssumptionsRef(), getExpr(), getLHS(), getProof(), getRHS(), getScope(), isAbsLiteral(), isAssump(), isNull(), isRewrite(), print(), printDebug(), printx(), withAssumptions(), and withProof().


The documentation for this class was generated from the following file:
Generated on Wed Nov 18 16:16:03 2009 for CVC3 by  doxygen 1.5.2