CVC3::Circuit Class Reference

#include <circuit.h>

Collaboration diagram for CVC3::Circuit:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Attributes


Detailed Description

Definition at line 31 of file circuit.h.


Constructor & Destructor Documentation

CVC3::Circuit::Circuit ( SearchEngineFast se,
const Theorem thm 
)

Definition at line 28 of file circuit.cpp.

References CVC3::Expr::arity(), CVC3::SearchEngineFast::d_circuitsByExpr, d_lits, d_thm, CVC3::SearchImplBase::d_vm, CVC3::Theorem::getExpr(), and CVC3::Expr::negate().


Member Function Documentation

bool CVC3::Circuit::propagate ( SearchEngineFast se  ) 

Definition at line 47 of file circuit.cpp.

References CVC3::TheoryCore::addFact(), CVC3::AND_R, CVC3::Expr::arity(), CVC3::SearchEngineRules::confAndrAF(), CVC3::SearchEngineRules::confAndrAT(), CVC3::SearchEngineRules::confIffr(), CVC3::SearchEngineRules::confIterIfThen(), CVC3::SearchEngineRules::confIterThenElse(), CVC3::SearchEngineFast::d_circuitPropCount, CVC3::SearchEngineFast::d_conflictTheorem, CVC3::SearchEngine::d_core, CVC3::SearchEngineFast::d_literals, d_lits, CVC3::SearchEngine::d_rules, d_thm, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Literal::getTheorem(), CVC3::Literal::getValue(), CVC3::IFF_R, CVC3::Theorem::isNull(), CVC3::ITE_R, CVC3::SearchImplBase::newLiteral(), CVC3::SearchEngineRules::propAndrAF(), CVC3::SearchEngineRules::propAndrAT(), CVC3::SearchEngineRules::propAndrLF(), CVC3::SearchEngineRules::propAndrLRT(), CVC3::SearchEngineRules::propAndrRF(), CVC3::SearchEngineRules::propIffr(), CVC3::SearchEngineRules::propIterIfThen(), CVC3::SearchEngineRules::propIterIte(), CVC3::SearchEngineRules::propIterThen(), CVC3::SearchEngineFast::recordFact(), vals3, and vals4.


Member Data Documentation

Theorem CVC3::Circuit::d_thm [private]

Definition at line 34 of file circuit.h.

Referenced by Circuit(), and propagate().

Literal CVC3::Circuit::d_lits[4] [private]

Definition at line 35 of file circuit.h.

Referenced by Circuit(), and propagate().


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