#include <common_proof_rules.h>
Inheritance diagram for CVC3::CommonProofRules:
Definition at line 46 of file common_proof_rules.h.
virtual CVC3::CommonProofRules::~CommonProofRules | ( | ) | [inline, virtual] |
virtual Theorem3 CVC3::CommonProofRules::queryTCC | ( | const Theorem & | phi, | |
const Theorem & | D_phi | |||
) | [pure virtual] |
Convert 2-valued formula to 3-valued by discharging its TCC ():
.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::VCL::query().
virtual Theorem3 CVC3::CommonProofRules::implIntro3 | ( | const Theorem3 & | phi, | |
const std::vector< Expr > & | assump, | |||
const std::vector< Theorem > & | tccs | |||
) | [pure virtual] |
3-valued implication introduction rule:
phi | is the formula | |
assump | is the vector of assumptions | |
tccs | is the vector of TCCs for assumptions |
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::VCL::deriveClosure().
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::CoreTheoremProducer::IffToIte(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::ExprTransform::preprocess(), CVC3::ExprTransform::pushNegation(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::Theory::reflexivityRule(), CVC3::SearchImplBase::replaceITE(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryCore::rewrite(), and CVC3::TheoryCore::setupTerm().
==> (a == a) IFF TRUE
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryCore::rewriteCore(), and CVC3::TheoryCore::rewriteLitCore().
(same for IFF)
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::enqueueCNFrec(), SAT::CNF_Manager::replaceITErec(), and CVC3::Theory::symmetryRule().
virtual Theorem CVC3::CommonProofRules::transitivityRule | ( | const Theorem & | a1_eq_a2, | |
const Theorem & | a2_eq_a3 | |||
) | [pure virtual] |
(same for IFF)
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::findInCNFCache(), CVC3::ExprTransform::preprocess(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::SearchImplBase::replaceITE(), and CVC3::Theory::transitivityRule().
virtual Theorem CVC3::CommonProofRules::substitutivityRule | ( | const Expr & | e, | |
const Theorem & | thm | |||
) | [pure virtual] |
Optimized case for expr with one child.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryArithOld::assertFact(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryCore::simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::Theory::substitutivityRule(), CVC3::TheoryCore::update(), and CVC3::Theory::updateHelper().
virtual Theorem CVC3::CommonProofRules::substitutivityRule | ( | const Expr & | e, | |
const std::vector< unsigned > & | changed, | |||
const std::vector< Theorem > & | thms | |||
) | [pure virtual] |
except that only those arguments are given that .
e | is the original expression . | |
changed | is the vector of indices of changed kids | |
thms | are the theorems for the changed kids. |
Implemented in CVC3::CommonTheoremProducer.
virtual Theorem CVC3::CommonProofRules::substitutivityRule | ( | const Expr & | e, | |
const int | changed, | |||
const Theorem & | thm | |||
) | [pure virtual] |
Implemented in CVC3::CommonTheoremProducer.
virtual Theorem CVC3::CommonProofRules::contradictionRule | ( | const Theorem & | e, | |
const Theorem & | not_e | |||
) | [pure virtual] |
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchEngineFast::addLiteralFact(), CVC3::TheoryCore::processEquality(), and CVC3::SearchEngineFast::recordFact().
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryCore::assertFormula(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::setFindLiteral(), and CVC3::TheoryCore::simplifyOp().
e1 <=> e2 ==> ~e1 <=> ~e2
Where ~e is the inverse of e (that is, ~(!e') = e').
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::findInCNFCache(), and CVC3::TheoryCore::rewriteLiteral().
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::enqueueCNFrec(), and CVC3::SearchEngineFast::split().
virtual Theorem CVC3::CommonProofRules::iffMP | ( | const Theorem & | e1, | |
const Theorem & | e1_iff_e2 | |||
) | [pure virtual] |
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::fixConflict(), CVC3::Theory::iffMP(), CVC3::ExprTransform::preprocess(), CVC3::SearchImplBase::replaceITE(), and SAT::CNF_Manager::replaceITErec().
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::processIntEq(), and CVC3::TheoryArithNew::processIntEq().
virtual Theorem CVC3::CommonProofRules::implIntro | ( | const Theorem & | phi, | |
const std::vector< Expr > & | assump | |||
) | [pure virtual] |
Implication introduction rule:
.
phi | is the formula | |
assump | is the vector of assumptions |
Implemented in CVC3::CommonTheoremProducer.
e1 => e2 ==> ~e2 => ~e1
Where ~e is the inverse of e (that is, ~(!e') = e').
Implemented in CVC3::CommonTheoremProducer.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryCore::assertFormula(), and CVC3::TheoryCore::setFindLiteral().
==> (e1 <=> e2) <=> [simplified expr]
Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite(), and CVC3::TheoryBitvector::rewriteBoolean().
==> AND(e1,e2) IFF [simplified expr]
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::Theory::computeTCC(), and CVC3::Theory::rewriteAnd().
==> OR(e1,...,en) IFF [simplified expr]
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchEngineFast::fixConflict(), and CVC3::Theory::rewriteOr().
==> NOT TRUE IFF FALSE
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::CoreTheoremProducer::NotToIte(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryBitvector::rewriteBoolean(), and CVC3::TheoryCore::rewriteLitCore().
==> NOT FALSE IFF TRUE
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::CoreTheoremProducer::NotToIte(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryBitvector::rewriteBoolean(), and CVC3::TheoryCore::rewriteLitCore().
==> NOT NOT e IFF e, takes !!e
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::findInCNFCache(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryCore::rewriteCore(), and CVC3::TheoryCore::rewriteLitCore().
skolem rewrite rule: Introduces axiom |- Exists(x) phi(x) <=> phi(c) where c is a constant defined by the expression Exists(x) phi(x)
Implemented in CVC3::CommonTheoremProducer.
Special version of skolemizeRewrite for "EXISTS x. t = x".
Implemented in CVC3::CommonTheoremProducer.
|- EXISTS x. e = x
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryArithNew::getVariableIntroThm().
If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm.
thm | is the Theorem(EXISTS x: phi(x)) |
Implemented in CVC3::CommonTheoremProducer.
Retrun a theorem "|- e = v" for a new Skolem constant v.
This is equivalent to skolemize(d_core->varIntroRule(e)), only more efficient.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryArray::renameExpr(), CVC3::SearchImplBase::replaceITE(), and SAT::CNF_Manager::replaceITErec().
virtual Theorem CVC3::CommonProofRules::trueTheorem | ( | ) | [pure virtual] |
==> TRUE
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchSat::check(), CVC3::VCL::query(), and CVC3::SearchSimple::SearchSimple().
virtual std::vector<Theorem>& CVC3::CommonProofRules::getSkolemAxioms | ( | ) | [pure virtual] |
virtual void CVC3::CommonProofRules::clearSkolemAxioms | ( | ) | [pure virtual] |
virtual Theorem CVC3::CommonProofRules::ackermann | ( | const Expr & | e1, | |
const Expr & | e2 | |||
) | [pure virtual] |
Implemented in CVC3::CommonTheoremProducer.