CVC3
|
#include <common_proof_rules.h>
Inherited by CVC3::CommonTheoremProducer.
Public Member Functions | |
virtual | ~CommonProofRules () |
Destructor. | |
virtual Theorem3 | queryTCC (const Theorem &phi, const Theorem &D_phi)=0 |
Convert 2-valued formula to 3-valued by discharging its TCC ( ![]()
| |
virtual Theorem3 | implIntro3 (const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)=0 |
3-valued implication introduction rule:
| |
virtual Theorem | assumpRule (const Expr &a, int scope=-1)=0 |
| |
virtual Theorem | reflexivityRule (const Expr &a)=0 |
| |
virtual Theorem | rewriteReflexivity (const Expr &a_eq_a)=0 |
==> (a == a) IFF TRUE | |
virtual Theorem | symmetryRule (const Theorem &a1_eq_a2)=0 |
| |
virtual Theorem | rewriteUsingSymmetry (const Expr &a1_eq_a2)=0 |
| |
virtual Theorem | transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)=0 |
| |
virtual Theorem | substitutivityRule (const Expr &e, const Theorem &thm)=0 |
Optimized case for expr with one child. | |
virtual Theorem | substitutivityRule (const Expr &e, const Theorem &thm1, const Theorem &thm2)=0 |
Optimized case for expr with two children. | |
virtual Theorem | substitutivityRule (const Op &op, const std::vector< Theorem > &thms)=0 |
| |
virtual Theorem | substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)=0 |
| |
virtual Theorem | substitutivityRule (const Expr &e, const int changed, const Theorem &thm)=0 |
virtual Theorem | contradictionRule (const Theorem &e, const Theorem ¬_e)=0 |
| |
virtual Theorem | excludedMiddle (const Expr &e)=0 |
virtual Theorem | iffTrue (const Theorem &e)=0 |
| |
virtual Theorem | iffNotFalse (const Theorem &e)=0 |
| |
virtual Theorem | iffTrueElim (const Theorem &e)=0 |
| |
virtual Theorem | iffFalseElim (const Theorem &e)=0 |
| |
virtual Theorem | iffContrapositive (const Theorem &thm)=0 |
e1 <=> e2 ==> ~e1 <=> ~e2 | |
virtual Theorem | notNotElim (const Theorem ¬_not_e)=0 |
| |
virtual Theorem | iffMP (const Theorem &e1, const Theorem &e1_iff_e2)=0 |
| |
virtual Theorem | implMP (const Theorem &e1, const Theorem &e1_impl_e2)=0 |
| |
virtual Theorem | andElim (const Theorem &e, int i)=0 |
| |
virtual Theorem | andIntro (const Theorem &e1, const Theorem &e2)=0 |
| |
virtual Theorem | andIntro (const std::vector< Theorem > &es)=0 |
| |
virtual Theorem | implIntro (const Theorem &phi, const std::vector< Expr > &assump)=0 |
Implication introduction rule:
| |
virtual Theorem | implContrapositive (const Theorem &thm)=0 |
e1 => e2 ==> ~e2 => ~e1 | |
virtual Theorem | rewriteIteTrue (const Expr &e)=0 |
==> ITE(TRUE, e1, e2) == e1 | |
virtual Theorem | rewriteIteFalse (const Expr &e)=0 |
==> ITE(FALSE, e1, e2) == e2 | |
virtual Theorem | rewriteIteSame (const Expr &e)=0 |
==> ITE(c, e, e) == e | |
virtual Theorem | notToIff (const Theorem ¬_e)=0 |
| |
virtual Theorem | xorToIff (const Expr &e)=0 |
| |
virtual Theorem | rewriteIff (const Expr &e)=0 |
==> (e1 <=> e2) <=> [simplified expr] | |
virtual Theorem | rewriteAnd (const Expr &e)=0 |
==> AND(e1,e2) IFF [simplified expr] | |
virtual Theorem | rewriteOr (const Expr &e)=0 |
==> OR(e1,...,en) IFF [simplified expr] | |
virtual Theorem | rewriteNotTrue (const Expr &e)=0 |
==> NOT TRUE IFF FALSE | |
virtual Theorem | rewriteNotFalse (const Expr &e)=0 |
==> NOT FALSE IFF TRUE | |
virtual Theorem | rewriteNotNot (const Expr &e)=0 |
==> NOT NOT e IFF e, takes !!e | |
virtual Theorem | rewriteNotForall (const Expr &forallExpr)=0 |
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e | |
virtual Theorem | rewriteNotExists (const Expr &existsExpr)=0 |
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e | |
virtual Expr | skolemize (const Expr &e)=0 |
virtual Theorem | skolemizeRewrite (const Expr &e)=0 |
virtual Theorem | skolemizeRewriteVar (const Expr &e)=0 |
Special version of skolemizeRewrite for "EXISTS x. t = x". | |
virtual Theorem | varIntroRule (const Expr &e)=0 |
|- EXISTS x. e = x | |
virtual Theorem | skolemize (const Theorem &thm)=0 |
If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm. | |
virtual Theorem | varIntroSkolem (const Expr &e)=0 |
Retrun a theorem "|- e = v" for a new Skolem constant v. | |
virtual Theorem | trueTheorem ()=0 |
==> TRUE | |
virtual Theorem | rewriteAnd (const Theorem &e)=0 |
AND(e1,e2) ==> [simplified expr]. | |
virtual Theorem | rewriteOr (const Theorem &e)=0 |
OR(e1,...,en) ==> [simplified expr]. | |
virtual std::vector< Theorem > & | getSkolemAxioms ()=0 |
virtual void | clearSkolemAxioms ()=0 |
virtual Theorem | ackermann (const Expr &e1, const Expr &e2)=0 |
virtual Theorem | liftOneITE (const Expr &e)=0 |
Definition at line 46 of file common_proof_rules.h.
|
inlinevirtual |
Destructor.
Definition at line 49 of file common_proof_rules.h.
|
pure virtual |
Convert 2-valued formula to 3-valued by discharging its TCC ( ):
.
Implemented in CVC3::CommonTheoremProducer.
|
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.
Implemented in CVC3::CommonTheoremProducer.
Referenced by SAT::CNF_Manager::concreteThm(), CVC3::ExprTransform::newPP(), CVC3::ExprTransform::newPPrec(), 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(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::substitute(), and SAT::CNF_Manager::translateExprRec().
==> (a == a) IFF TRUE
Implemented in CVC3::CommonTheoremProducer.
(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().
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), and CVC3::TheoryCore::update().
|
pure virtual |
(same for IFF)
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::findInCNFCache(), CVC3::ExprTransform::newPPrec(), CVC3::ExprTransform::preprocess(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::SearchImplBase::replaceITE(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::substitute(), and CVC3::Theory::transitivityRule().
|
pure virtual |
Optimized case for expr with one child.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryArith3::assertFact(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::Theory::findReduce(), CVC3::ExprTransform::newPPrec(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), SAT::CNF_Manager::replaceITErec(), CVC3::Theory::simplifyOp(), CVC3::TheoryCore::simplifyOp(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::substitute(), CVC3::Theory::substitutivityRule(), CVC3::TheoryCore::update(), and CVC3::Theory::updateHelper().
|
pure virtual |
Optimized case for expr with two children.
Implemented in CVC3::CommonTheoremProducer.
|
pure virtual |
Implemented in CVC3::CommonTheoremProducer.
|
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 ![]() |
Implemented in CVC3::CommonTheoremProducer.
|
pure virtual |
Implemented in CVC3::CommonTheoremProducer.
|
pure virtual |
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchEngineFast::addLiteralFact(), and CVC3::SearchEngineFast::recordFact().
Implemented in CVC3::CommonTheoremProducer.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), and CVC3::TheoryCore::simplifyOp().
Implemented in CVC3::CommonTheoremProducer.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryCore::registerAtom(), CVC3::SearchEngineFast::split(), CVC3::TheoryUF::update(), and CVC3::TheoryCore::update().
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryCore::registerAtom(), CVC3::SearchEngineFast::split(), and CVC3::TheoryCore::update().
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().
|
pure virtual |
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchEngineFast::fixConflict(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::Theory::iffMP(), CVC3::ExprTransform::preprocess(), CVC3::SearchImplBase::replaceITE(), and SAT::CNF_Manager::replaceITErec().
|
pure virtual |
Implemented in CVC3::CommonTheoremProducer.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryCore::checkSolved(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchSat::newUserAssumptionIntHelper(), and CVC3::TheoryBitvector::solve().
Implemented in CVC3::CommonTheoremProducer.
|
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.
==> ITE(TRUE, e1, e2) == e1
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::Theory::rewriteIte().
==> ITE(FALSE, e1, e2) == e2
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::Theory::rewriteIte().
==> ITE(c, e, e) == e
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::Theory::rewriteIte(), and CVC3::TheoryCore::simplifyOp().
Implemented in CVC3::CommonTheoremProducer.
==> (e1 <=> e2) <=> [simplified expr]
Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::TheoryCore::rewrite().
==> AND(e1,e2) IFF [simplified expr]
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::Theory::computeTCC(), CVC3::TheoryBitvector::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::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().
==> NOT FALSE IFF TRUE
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().
==> NOT NOT e IFF e, takes !!e
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::findInCNFCache(), CVC3::ExprTransform::pushNegation1(), and CVC3::ExprTransform::pushNegationRec().
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
Implemented in CVC3::CommonTheoremProducer.
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Implemented in CVC3::CommonTheoremProducer.
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.
Referenced by CVC3::TheoryArithNew::getVariableIntroThm().
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::Theory::renameExpr(), CVC3::SearchImplBase::replaceITE(), SAT::CNF_Manager::replaceITErec(), and CVC3::TheoryArithOld::TheoryArithOld().
|
pure virtual |
==> TRUE
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchSimple::SearchSimple().
AND(e1,e2) ==> [simplified expr].
Implemented in CVC3::CommonTheoremProducer.
OR(e1,...,en) ==> [simplified expr].
Implemented in CVC3::CommonTheoremProducer.
|
pure virtual |
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::processResult().
|
pure virtual |
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::SearchImplBase::checkValid().
Implemented in CVC3::CommonTheoremProducer.
Implemented in CVC3::CommonTheoremProducer.
Referenced by CVC3::ExprTransform::newPPrec(), and CVC3::ExprTransform::simplifyWithCare().