CVCL::Circuit Class Reference

#include <circuit.h>

Collaboration diagram for CVCL::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 14 of file circuit.h.

---

Constructor & Destructor Documentation

CVCL::Circuit::Circuit (  SearchEngineFast *  se, const Theorem &  thm )

Definition at line 10 of file circuit.cpp. References CVCL::Expr::arity(), CVCL::SearchEngineFast::d_circuitsByExpr, d_lits, d_thm, CVCL::SearchImplBase::d_vm, CVCL::Theorem::getExpr(), CVCL::Expr::isNot(), and CVCL::Expr::negate().

---

Member Function Documentation

bool CVCL::Circuit::propagate (  SearchEngineFast *  se  )

Definition at line 29 of file circuit.cpp. References CVCL::TheoryCore::addFact(), CVCL::AND_R, CVCL::Expr::arity(), CVCL::SearchEngineRules::confAndrAF(), CVCL::SearchEngineRules::confAndrAT(), CVCL::SearchEngineRules::confIffr(), CVCL::SearchEngineRules::confIterIfThen(), CVCL::SearchEngineRules::confIterThenElse(), CVCL::SearchEngineFast::d_circuitPropCount, CVCL::SearchEngineFast::d_conflictTheorem, CVCL::SearchEngine::d_core, CVCL::SearchEngineFast::d_literals, d_lits, CVCL::SearchEngine::d_rules, d_thm, CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Literal::getTheorem(), CVCL::Literal::getValue(), CVCL::IFF_R, CVCL::Theorem::isNull(), CVCL::ITE_R, CVCL::SearchImplBase::newLiteral(), CVCL::SearchEngineRules::propAndrAF(), CVCL::SearchEngineRules::propAndrAT(), CVCL::SearchEngineRules::propAndrLF(), CVCL::SearchEngineRules::propAndrLRT(), CVCL::SearchEngineRules::propAndrRF(), CVCL::SearchEngineRules::propIffr(), CVCL::SearchEngineRules::propIterIfThen(), CVCL::SearchEngineRules::propIterIte(), CVCL::SearchEngineRules::propIterThen(), and CVCL::SearchEngineFast::recordFact().

---

Member Data Documentation

Theorem CVCL::Circuit::d_thm [private]

Definition at line 17 of file circuit.h. Referenced by Circuit(), and propagate().

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

Definition at line 18 of file circuit.h. Referenced by Circuit(), and propagate().

---

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

• circuit.h
• circuit.cpp

---