CVC3::Circuit Class Reference

#include <circuit.h>

Collaboration diagram for CVC3::Circuit:

[legend]List of all members.

Public Member Functions

• Circuit (SearchEngineFast *se, const Theorem &thm)
• bool propagate (SearchEngineFast *se)

Private Attributes

• Theorem d_thm
• Literal d_lits [4]

---

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:

• circuit.h
• circuit.cpp

---