#include <circuit.h>
Public Member Functions
- Circuit (SearchEngineFast *se, const Theorem &thm)
- bool propagate (SearchEngineFast *se)
Private Attributes
Detailed Description
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(), CVC3::Expr::isNot(), 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(), 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(), IFF_R, CVC3::Theorem::isNull(), 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:
