#include <theory.h>
Inheritance diagram for CVC3::Theory:
Author: Clark Barrett
Created: Thu Jan 30 16:37:56 2003
This is an abstract class which all theories should inherit from. In addition to providing an abstract theory interface, it provides access functions to core functionality. However, in order to avoid duplicating the data structures which implement this functionality, all the functionality is stored in a separate class (which actually derives from this one) called TheoryCore. These two classes work closely together to provide the core functionality.
Definition at line 64 of file theory.h.
Theory::Theory | ( | void | ) | [private] |
Private default constructor.
Everyone besides TheoryCore has to use the public constructor which sets up all the provided functionality automatically.
Definition at line 33 of file theory.cpp.
Theory::Theory | ( | TheoryCore * | theoryCore, | |
const std::string & | name | |||
) |
Exposed constructor.
Note that each instance of Theory must have a name (mostly for debugging purposes).
Definition at line 36 of file theory.cpp.
Theory::~Theory | ( | void | ) | [virtual] |
ExprManager* CVC3::Theory::getEM | ( | ) | [inline] |
Access to ExprManager.
Definition at line 90 of file theory.h.
References d_em.
Referenced by addBoundVar(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryUF::checkType(), CVC3::TheoryRecords::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryCore::checkType(), CVC3::TheoryBitvector::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryRecords::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryQuant::enqueueInst(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::SearchEngine::getConcreteModel(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::TheoryUF::lambdaExpr(), lookupVar(), CVC3::TheoryBitvector::newBitvectorTypeExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVIndexExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), newFunction(), CVC3::TheoryBitvector::newSXExpr(), newTypeExpr(), newVar(), CVC3::TheoryCore::CoreNotifyObj::notify(), CVC3::QuantTheoremProducer::packVar(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryUF::parseExprOp(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryUF::print(), CVC3::TheoryQuant::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::TheoryBitvector::rat(), CVC3::TheoryArith::rat(), CVC3::TheoryRecords::recordExpr(), CVC3::TheoryRecords::recordSelect(), CVC3::TheoryRecords::recordType(), CVC3::TheoryRecords::recordUpdate(), registerKinds(), CVC3::TheoryArith::rewriteToDiff(), CVC3::TheoryArithNew::TheoryArithNew(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::TheoryArray::TheoryArray(), CVC3::TheoryBitvector::TheoryBitvector(), CVC3::TheoryDatatype::TheoryDatatype(), theoryOf(), CVC3::TheoryQuant::TheoryQuant(), CVC3::TheoryRecords::TheoryRecords(), CVC3::TheoryUF::TheoryUF(), CVC3::TheoryUF::transClosureExpr(), CVC3::TheoryRecords::tupleExpr(), CVC3::TheoryRecords::tupleSelect(), CVC3::TheoryRecords::tupleType(), and CVC3::TheoryRecords::tupleUpdate().
TheoryCore* CVC3::Theory::theoryCore | ( | ) | [inline] |
Get a pointer to theoryCore.
Definition at line 93 of file theory.h.
References d_theoryCore.
Referenced by CVC3::TheoryQuant::add_parent(), CVC3::TheoryUF::assertFact(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::TheoryUF::createProofRules(), CVC3::TheorySimulate::createProofRules(), CVC3::TheoryRecords::createProofRules(), CVC3::TheoryQuant::createProofRules(), CVC3::TheoryArray::createProofRules(), CVC3::TheoryArithNew::createProofRules(), CVC3::TheoryArithOld::createProofRulesOld(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryQuant::getExprScore(), CVC3::TheoryQuant::hasGoodSynMultiInst(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArray::print(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryQuant::pushBackList(), CVC3::TheoryQuant::pushForwList(), CVC3::TheoryQuant::recursiveMap(), CVC3::TheoryArray::renameExpr(), CVC3::TheoryArith::rewriteToDiff(), CVC3::TheoryQuant::saveContext(), CVC3::TheoryArray::setup(), CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryQuant::synCheckSat(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoryQuant::TheoryQuant(), and CVC3::QuantTheoremProducer::universalInst().
CommonProofRules* CVC3::Theory::getCommonRules | ( | ) | [inline] |
Get a pointer to common proof rules.
Definition at line 96 of file theory.h.
References d_commonRules.
Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::ExprTransform::ExprTransform(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArray::renameExpr(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryUF::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().
const std::string& CVC3::Theory::getName | ( | ) | const [inline] |
Get the name of the theory (for debugging purposes).
Definition at line 99 of file theory.h.
References d_name.
Referenced by addSplitter(), assignValue(), CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::collectModelValues(), getModelTerm(), getTCC(), CVC3::operator<<(), CVC3::TheoryCore::refineCounterExample(), and CVC3::VCL::reprocessFlags().
virtual void CVC3::Theory::setUsed | ( | ) | [inline, virtual] |
Set the "used" flag on this theory (for smtlib translator).
Definition at line 102 of file theory.h.
References d_theoryUsed.
Referenced by CVC3::Translator::preprocessRec(), and CVC3::Translator::processType().
virtual bool CVC3::Theory::theoryUsed | ( | ) | [inline, virtual] |
Get whether theory has been used (for smtlib translator).
Definition at line 104 of file theory.h.
References d_theoryUsed.
Referenced by CVC3::Translator::finish().
bool Theory::inconsistent | ( | ) | [virtual] |
Check if the current context is inconsistent.
Reimplemented in CVC3::TheoryCore.
Definition at line 90 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::inconsistent().
Referenced by CVC3::TheoryArithOld::assignVariables(), CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryRecords::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().
void Theory::setInconsistent | ( | const Theorem & | e | ) | [virtual] |
Make the context inconsistent; The formula proved by e must FALSE.
Reimplemented in CVC3::TheoryCore.
Definition at line 96 of file theory.cpp.
References CVC3::Debug::counter(), d_theoryCore, CVC3::debugger, IF_DEBUG, and CVC3::TheoryCore::setInconsistent().
Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithNew::checkSat(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryArithOld::processBuffer(), and CVC3::TheoryArithOld::projectInequalities().
void Theory::setIncomplete | ( | const std::string & | reason | ) | [virtual] |
Mark the current decision branch as possibly incomplete.
This should be set when a decision procedure uses an incomplete algorithm, and cannot guarantee satisfiability after the final checkSat() call with full effort. An example would be instantiation of universal quantifiers.
A decision procedure can provide a reason for incompleteness, which will be reported back to the user.
Reimplemented in CVC3::TheoryCore.
Definition at line 105 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::setIncomplete().
Referenced by CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoryArithOld::projectInequalities(), and CVC3::TheoryQuant::synCheckSat().
Simplify a term e and return a Theorem(e==e').
Reimplemented in CVC3::TheoryCore.
Definition at line 112 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::simplify().
Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryUF::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryBitvector::rewriteAtomic(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryBitvector::setup(), simplifyExpr(), CVC3::TheoryBitvector::simplifyOp(), and CVC3::TheoryArray::update().
Simplify a term e w.r.t. the current context.
Definition at line 398 of file theory.h.
References CVC3::Theorem::getRHS(), and simplify().
Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::SearchSat::check(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryQuant::enqueueInst(), CVC3::SearchEngineFast::findSplitter(), CVC3::TheoryQuant::goodSynMatch(), CVC3::TheoryQuant::matchChild(), newSubtypeExpr(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::TheoryQuant::recSynMatch(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArray::setup(), and CVC3::TheoryQuant::synNewInst().
void Theory::enqueueFact | ( | const Theorem & | e | ) | [virtual] |
Submit a derived fact to the core from a decision procedure.
e | is the Theorem for the new fact |
Reimplemented in CVC3::TheoryCore.
Definition at line 121 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::enqueueFact().
Referenced by CVC3::TheoryUF::assertFact(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryArithOld::assertFact(), assertTypePred(), CVC3::TheoryUF::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryArithNew::checkSatInteger(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryDatatype::instantiate(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryQuant::sendInstNew(), CVC3::TheoryRecords::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryBitvector::setup(), CVC3::TheoryUF::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), and updateCC().
void Theory::assertEqualities | ( | const Theorem & | e | ) | [virtual] |
Handle new equalities (usually asserted through addFact).
INVARIANT: the Theorem 'e' is an equality e1==e2, where e2 is i-leaf simplified in the current context, or a conjunction of such equalities.
Reimplemented in CVC3::TheoryCore.
Definition at line 128 of file theory.cpp.
References CVC3::TheoryCore::assertEqualities(), and d_theoryCore.
Referenced by CVC3::TheoryRecords::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().
Parse the generic expression.
This method should be used in parseExprOp() for recursive calls to subexpressions, and is the method called by the command processor.
Reimplemented in CVC3::TheoryCore.
Definition at line 419 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::parseExpr().
Referenced by CVC3::TheoryUF::parseExprOp(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), and CVC3::TheoryArithNew::parseExprOp().
Assigns t a concrete value val. Used in model generation.
Reimplemented in CVC3::TheoryCore.
Definition at line 143 of file theory.cpp.
References CVC3::TheoryCore::assignValue(), d_theoryCore, getName(), CVC3::Expr::toString(), and CVC3::TRACE.
Referenced by CVC3::TheoryArithOld::assignVariables(), CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithNew::computeModel(), and computeModel().
void Theory::assignValue | ( | const Theorem & | thm | ) | [virtual] |
Record a derived assignment to a variable (LHS).
Reimplemented in CVC3::TheoryCore.
Definition at line 151 of file theory.cpp.
References CVC3::TheoryCore::assignValue(), d_theoryCore, getName(), and CVC3::TRACE.
void Theory::registerKinds | ( | Theory * | theory, | |
std::vector< int > & | kinds | |||
) |
Register new kinds with the given theory.
Definition at line 158 of file theory.cpp.
References d_theoryCore, CVC3::TheoryCore::d_theoryMap, DebugAssert, getEM(), and CVC3::ExprManager::getKindName().
Referenced by registerTheory().
void Theory::registerTheory | ( | Theory * | theory, | |
std::vector< int > & | kinds, | |||
bool | hasSolver = false | |||
) |
Register a new theory.
Definition at line 171 of file theory.cpp.
References CVC3::TheoryCore::d_solver, CVC3::TheoryCore::d_theories, d_theoryCore, DebugAssert, and registerKinds().
Referenced by CVC3::TheoryArithNew::TheoryArithNew(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::TheoryArray::TheoryArray(), CVC3::TheoryBitvector::TheoryBitvector(), CVC3::TheoryCore::TheoryCore(), CVC3::TheoryDatatype::TheoryDatatype(), CVC3::TheoryQuant::TheoryQuant(), CVC3::TheoryRecords::TheoryRecords(), CVC3::TheorySimulate::TheorySimulate(), and CVC3::TheoryUF::TheoryUF().
int Theory::getNumTheories | ( | ) |
Return the number of registered theories.
Definition at line 183 of file theory.cpp.
References CVC3::TheoryCore::d_theories, and d_theoryCore.
Referenced by CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::processFactQueue(), CVC3::TheoryCore::refineCounterExample(), and CVC3::TheoryCore::setInconsistent().
bool Theory::hasTheory | ( | int | kind | ) |
Test whether a kind maps to any theory.
Definition at line 189 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::d_theoryMap.
Referenced by CVC3::TheoryCore::parseExpr(), and CVC3::PrettyPrinterCore::print().
Theory * Theory::theoryOf | ( | int | kind | ) |
Return the theory associated with a kind.
Definition at line 194 of file theory.cpp.
References d_theoryCore, CVC3::TheoryCore::d_theoryMap, DebugAssert, getEM(), and CVC3::ExprManager::getKindName().
Referenced by CVC3::TheoryCore::assertFormula(), CVC3::TheoryBitvector::assertTypePred(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryCore::buildModel(), CVC3::TypeComputerCore::checkType(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryCore::computeTypePred(), getBaseType(), getModelTerm(), getTCC(), getTypePred(), isLeaf(), isLeafIn(), CVC3::TheoryCore::parseExpr(), CVC3::Translator::preprocessRec(), CVC3::PrettyPrinterCore::print(), CVC3::Translator::processType(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::rewriteLiteral(), CVC3::TheoryCore::rewriteN(), CVC3::TheoryCore::setupSubFormulas(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplify(), and CVC3::TheoryCore::solve().
Return the theory associated with an Expr.
Definition at line 202 of file theory.cpp.
References d_theoryCore, CVC3::TheoryCore::d_theoryMap, DebugAssert, getBaseType(), getEM(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::ExprManager::getKindName(), CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), CVC3::Expr::isEq(), CVC3::Expr::isNot(), CVC3::Expr::isNull(), and CVC3::Expr::isVar().
Return the theorem that e is equal to its find.
Definition at line 242 of file theory.cpp.
References DebugAssert, CVC3::Expr::getFind(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::Theorem::isRefl(), reflexivityRule(), and transitivityRule().
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::buildModel(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryBitvector::checkSat(), CVC3::SearchSimple::checkValidRec(), CVC3::TheoryCore::collectBasicVars(), computeModel(), CVC3::TheoryCore::computeModelBasic(), findExpr(), CVC3::TheoryArithNew::getBeta(), CVC3::TheoryArithNew::getLowerBound(), CVC3::TheoryArithNew::getLowerBoundThm(), CVC3::TheoryCore::getModelValue(), CVC3::TheoryArithNew::getUpperBound(), CVC3::TheoryArithNew::getUpperBoundThm(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryCore::processEquality(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryRecords::setup(), CVC3::TheoryCore::simplify(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().
Return the find as a reference: expr must have a find.
Definition at line 227 of file theory.cpp.
References DebugAssert, CVC3::Expr::getFind(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::Expr::setFind(), and transitivityRule().
Referenced by updateHelper().
bool Theory::findReduced | ( | const Expr & | e | ) |
Return true iff e is find-reduced.
Definition at line 259 of file theory.cpp.
References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::getFind(), CVC3::Theorem::getRHS(), and CVC3::Expr::hasFind().
Referenced by CVC3::TheoryCore::assertEqualities().
Return the find of e, or e if it has no find.
Definition at line 461 of file theory.h.
References find(), CVC3::Theorem::getRHS(), and CVC3::Expr::hasFind().
Referenced by CVC3::TheoryArithOld::assignVariables(), CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryDatatype::canCollapse(), CVC3::SearchSat::check(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryArithOld::computeModelBasic(), CVC3::TheoryArithNew::computeModelBasic(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryArithOld::findRationalBound(), CVC3::TheoryArithNew::findRationalBound(), CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArray::rewrite(), CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryUF::update(), and CVC3::TheoryBitvector::update().
Compute the TCC of e, or the subtyping predicate, if e is a type.
Definition at line 269 of file theory.cpp.
References computeTCC(), CVC3::TheoryCore::d_tccCache, d_theoryCore, CVC3::Expr::getKind(), getName(), CVC3::Expr::isVar(), theoryOf(), CVC3::TRACE, and trueExpr().
Referenced by CVC3::TheoryUF::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryCore::computeTCC(), computeTCC(), and newSubtypeExpr().
Compute (or look up in cache) the base type of e and return the result.
Definition at line 285 of file theory.cpp.
References CVC3::Expr::getType().
Referenced by CVC3::TheoryDatatype::addSharedTerm(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::TheoryCore::buildModel(), CVC3::TheoryBitvector::BVSize(), CVC3::TheoryQuant::canMatch(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheorySimulate::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandRecord(), CVC3::RecordsTheoremProducer::expandTuple(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), getModelTerm(), CVC3::TheoryDatatype::instantiate(), CVC3::TheoryDatatype::mergeLabels(), newVar(), CVC3::TheoryBitvector::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryQuant::recursiveMap(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryCore::rewriteLiteral(), CVC3::TheoryRecords::setup(), CVC3::TheoryDatatype::setup(), theoryOf(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::QuantTheoremProducer::universalInst(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().
Compute the base type from an arbitrary type.
Definition at line 291 of file theory.cpp.
References computeBaseType(), DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::isNull(), CVC3::Expr::lookupType(), theoryOf(), and CVC3::Type::toString().
Calls the correct theory to compute a type predicate.
Definition at line 308 of file theory.cpp.
References computeTypePred(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), and theoryOf().
Referenced by CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryRecords::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryRecords::computeTypePred(), CVC3::TheoryCore::computeTypePred(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::CoreTheoremProducer::typePred(), and CVC3::QuantTheoremProducer::universalInst().
Update the children of the term e.
When a decision procedure receives a call to update() because a child of a term 'e' has changed, this method can be called to compute the new value of 'e'.
Definition at line 319 of file theory.cpp.
References CVC3::Expr::arity(), d_commonRules, findRef(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), reflexivityRule(), and CVC3::CommonProofRules::substitutivityRule().
Referenced by CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), and updateCC().
void Theory::setupCC | ( | const Expr & | e | ) |
Setup a term for congruence closure (must have sig and rep attributes).
Definition at line 361 of file theory.cpp.
References CVC3::Expr::arity(), reflexivityRule(), CVC3::Expr::setRep(), and CVC3::Expr::setSig().
Referenced by CVC3::TheoryUF::setup(), CVC3::TheoryRecords::setup(), CVC3::TheoryDatatypeLazy::setup(), and CVC3::TheoryDatatype::setup().
Update a term w.r.t. congruence closure (must be setup with setupCC()).
Definition at line 374 of file theory.cpp.
References CVC3::Expr::arity(), enqueueFact(), CVC3::Expr::getRep(), CVC3::Theorem::getRHS(), CVC3::Expr::getSig(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Theorem::isNull(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), symmetryRule(), transitivityRule(), and updateHelper().
Referenced by CVC3::TheoryRecords::update().
Rewrite a term w.r.t. congruence closure (must be setup with setupCC()).
Definition at line 412 of file theory.cpp.
References CVC3::Expr::getRep(), CVC3::Theorem::isNull(), reflexivityRule(), and symmetryRule().
Referenced by CVC3::TheoryUF::rewrite(), and CVC3::TheoryRecords::rewrite().
Calls the correct theory to get all of the terms that need to be assigned values in the concrete model.
Definition at line 427 of file theory.cpp.
References computeModelTerm(), DebugAssert, getBaseType(), getName(), IF_DEBUG, theoryOf(), CVC3::Expr::toString(), and CVC3::TRACE.
Referenced by CVC3::TheoryCore::collectBasicVars().
Fetch the concrete assignment to the variable during model generation.
Reimplemented in CVC3::TheoryCore.
Definition at line 441 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::getModelValue().
Referenced by CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), and CVC3::TheoryArray::computeModel().
void Theory::addSplitter | ( | const Expr & | e, | |
int | priority = 0 | |||
) |
Suggest a splitter to the SearchEngine.
Definition at line 134 of file theory.cpp.
References CVC3::TheoryCore::d_coreSatAPI, d_theoryCore, DebugAssert, getName(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isBoolConst(), and CVC3::TRACE.
Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::refineCounterExample(), and CVC3::TheoryArithNew::refineCounterExample().
bool CVC3::Theory::isLeaf | ( | const Expr & | e | ) | [inline] |
Test if e is an i-leaf term for the current theory.
A term 'e' is an i-leaf for a theory 'i', if it is a variable, or 'e' belongs to a different theory. This definition makes sense for a larger term which by itself belongs to the current theory 'i', but (some of) its children are variables or belong to different theories.
Definition at line 511 of file theory.h.
References CVC3::Expr::isVar(), and theoryOf().
Referenced by CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithNew::assertLower(), CVC3::TheoryArithNew::assertUpper(), CVC3::ArithTheoremProducer::canonMultOne(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithOld::collectVars(), CVC3::TheoryArithNew::collectVars(), isLeafIn(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::TheoryArithNew::kidsCanonical(), leavesAreSimp(), CVC3::TheoryArithNew::pivotRule(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArithOld::substAndCanonize(), and CVC3::TheoryArithNew::substAndCanonize().
Test if e1 is an i-leaf in e2.
Definition at line 446 of file theory.cpp.
References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), isLeaf(), and theoryOf().
Referenced by CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::solve(), and CVC3::TheoryArithNew::solve().
bool Theory::leavesAreSimp | ( | const Expr & | e | ) |
Test if all i-leaves of e are simplified.
Definition at line 457 of file theory.cpp.
References CVC3::Expr::arity(), CVC3::Expr::getFind(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), and isLeaf().
Referenced by CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().
Type CVC3::Theory::boolType | ( | ) | [inline] |
Return BOOLEAN type.
Definition at line 531 of file theory.h.
References d_em, and CVC3::Type::typeBool().
Referenced by CVC3::TheoryCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryQuant::mapTermsByType(), and CVC3::TheoryQuant::parseExprOp().
const Expr& CVC3::Theory::falseExpr | ( | ) | [inline] |
Return FALSE Expr.
Definition at line 534 of file theory.h.
References d_em, and CVC3::ExprManager::falseExpr().
Referenced by CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::SearchEngine::getConcreteModel(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryQuant::newTopMatch(), CVC3::SearchImplBase::returnFromCheck(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::TheoryArith::rewriteToDiff(), CVC3::BitvectorTheoremProducer::signBVLTRule(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().
const Expr& CVC3::Theory::trueExpr | ( | ) | [inline] |
Return TRUE Expr.
Definition at line 537 of file theory.h.
References d_em, and CVC3::ExprManager::trueExpr().
Referenced by CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryDatatype::computeTCC(), computeTCC(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::BitvectorTheoremProducer::generalIneqn(), getTCC(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryQuant::newTopMatch(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::TheoryArith::rewriteToDiff(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), and CVC3::BitvectorTheoremProducer::zeroLeq().
Create a new variable given its name and type.
Add the variable to the database for resolving IDs in parseExpr
Definition at line 469 of file theory.cpp.
References CVC3::TheoryCore::addToVarDB(), CVC3::Type::arity(), CVC3::ARROW, d_em, d_theoryCore, DebugAssert, getEM(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), installID(), CVC3::Type::isBool(), CVC3::Type::isNull(), CVC3::ExprManager::newSymbolExpr(), CVC3::ExprManager::newVarExpr(), resolveID(), CVC3::Type::toString(), CVC3::TYPEDEF, and CVC3::UCONST.
Referenced by CVC3::TheoryDatatype::getConstant(), CVC3::TheoryArithNew::updateDependencies(), and CVC3::Translator::zeroVar().
Create a new named expression given its name, type, and definition.
Add the definition to the database for resolving IDs in parseExpr
Definition at line 508 of file theory.cpp.
References CVC3::ARROW, DebugAssert, getBaseType(), CVC3::Expr::getType(), installID(), CVC3::Expr::isNull(), CVC3::Type::isNull(), resolveID(), CVC3::Type::toString(), and CVC3::TYPEDEF.
Create a new uninterpreted function.
Add the definition to the database for resolving IDs in parseExpr
Definition at line 545 of file theory.cpp.
References CVC3::TheoryCore::addToVarDB(), CVC3::Type::arity(), d_theoryCore, DebugAssert, getEM(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), installID(), CVC3::Type::isBool(), CVC3::Type::isFunction(), CVC3::Type::isNull(), CVC3::ExprManager::newSymbolExpr(), resolveID(), CVC3::Type::toString(), CVC3::TYPEDEF, and CVC3::UFUNC.
Referenced by CVC3::TheoryDatatype::dataType().
Create a new defined function.
Add the definition to the database for resolving IDs in parseExpr
Definition at line 576 of file theory.cpp.
References DebugAssert, installID(), CVC3::Type::isNull(), CVC3::Expr::mkOp(), resolveID(), and CVC3::Type::toString().
Create and add a new bound variable to the stack, for parseExprOp().
The stack is popped automatically upon return from the parseExprOp() which used this method.
Bound variable names may repeat, in which case the latest declaration takes precedence.
Definition at line 598 of file theory.cpp.
References boundVarCount, CVC3::TheoryCore::d_boundVarMap, CVC3::TheoryCore::d_boundVarStack, CVC3::TheoryCore::d_parseCache, d_theoryCore, DebugAssert, getEM(), CVC3::Expr::getKind(), CVC3::RAW_LIST, CVC3::Expr::toString(), and CVC3::TRACE.
Referenced by CVC3::TheoryUF::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryCore::parseExprOp(), and CVC3::TheoryArray::parseExprOp().
Create and add a new bound named def to the stack, for parseExprOp().
The stack is popped automatically upon return from the parseExprOp() which used this method.
Bound variable names may repeat, in which case the latest declaration takes precedence.
The type may be Null, but 'def' must always be a valid Expr
Definition at line 615 of file theory.cpp.
References boundVarCount, CVC3::TheoryCore::d_boundVarMap, CVC3::TheoryCore::d_boundVarStack, d_theoryCore, DebugAssert, getEM(), CVC3::Expr::getKind(), CVC3::Type::isNull(), CVC3::LETDECL, CVC3::RAW_LIST, CVC3::Expr::toString(), CVC3::Type::toString(), and CVC3::TRACE.
Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Definition at line 641 of file theory.cpp.
References getEM(), CVC3::Expr::lookupType(), and CVC3::ExprManager::newVarExpr().
Type Theory::newTypeExpr | ( | const std::string & | name | ) |
Create a new uninterpreted type with the given name.
Add the name to the global variable database d_globals
Definition at line 655 of file theory.cpp.
References getEM(), installID(), CVC3::Expr::isNull(), resolveID(), and CVC3::TYPEDECL.
Create a new type abbreviation with the given name.
Definition at line 726 of file theory.cpp.
References CVC3::Type::getExpr(), installID(), CVC3::Expr::isNull(), and resolveID().
Create a new subtype expression.
Definition at line 670 of file theory.cpp.
References CVC3::TheoryCore::d_coreSatAPI, d_em, d_theoryCore, CVC3::EXISTS, CVC3::FORALL, CVC3::TheoryCore::getFlags(), getTCC(), CVC3::Expr::getType(), CVC3::Expr::isLambda(), CVC3::Expr::isNull(), CVC3::Expr::mkOp(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), simplifyExpr(), CVC3::SUBTYPE, and CVC3::Expr::toString().
Referenced by CVC3::TheoryCore::parseExprOp().
Expr Theory::resolveID | ( | const std::string & | name | ) |
Resolve an identifier, for use in parseExprOp().
First, search the bound variable stack, and if the name is not found, search the global constant and type declarations.
Definition at line 741 of file theory.cpp.
References CVC3::TheoryCore::d_boundVarMap, CVC3::TheoryCore::d_globals, d_theoryCore, CVC3::Expr::getKind(), and CVC3::RAW_LIST.
Referenced by CVC3::TheoryUF::assertFact(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryUF::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::TheoryDatatype::getConstant(), installID(), newFunction(), newTypeExpr(), newVar(), CVC3::TheoryCore::parseExpr(), and CVC3::TheoryUF::parseExprOp().
void Theory::installID | ( | const std::string & | name, | |
const Expr & | e | |||
) |
Install name as a new identifier associated with Expr e.
Definition at line 764 of file theory.cpp.
References CVC3::TheoryCore::d_globals, d_theoryCore, DebugAssert, and resolveID().
Referenced by CVC3::TheoryDatatype::dataType(), newFunction(), newTypeExpr(), and newVar().
Return BOOLEAN type.
Reimplemented in CVC3::TheoryCore.
Definition at line 772 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::typePred().
Referenced by CVC3::TheoryArithOld::isIntegerThm(), CVC3::TheoryArithNew::isIntegerThm(), and CVC3::TheoryArithOld::rewrite().
==> a == a
Definition at line 619 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::reflexivityRule().
Referenced by CVC3::TheoryArithNew::assertFact(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultOne(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::BitvectorTheoremProducer::extractBVPlus(), find(), CVC3::TheoryBitvector::flattenBVPlus(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryBitvector::pushNegation(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheoryUF::rewrite(), CVC3::TheorySimulate::rewrite(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), rewrite(), CVC3::TheoryBitvector::rewriteAtomic(), rewriteAtomic(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), rewriteCC(), CVC3::TheoryBitvector::rewriteConst(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::rewriteIte(), CVC3::TheoryCore::rewriteLitCore(), CVC3::TheoryCore::rewriteN(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryArray::setup(), setupCC(), CVC3::TheoryArithOld::setupRec(), CVC3::TheoryArithNew::setupRec(), CVC3::TheoryBitvector::signExtendBVLT(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), simplifyOp(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), and updateHelper().
a1 == a2 ==> a2 == a1
Definition at line 623 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::symmetryRule().
Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryCore::assignValue(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArray::rewrite(), CVC3::TheoryBitvector::rewriteBV(), rewriteCC(), CVC3::TheoryRecords::setup(), CVC3::TheoryDatatype::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArray::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), and updateCC().
Theorem CVC3::Theory::transitivityRule | ( | const Theorem & | a1_eq_a2, | |
const Theorem & | a2_eq_a3 | |||
) | [inline] |
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition at line 627 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::transitivityRule().
Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryCore::buildModel(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith::canonThm(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryArray::computeModel(), find(), findRef(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::TheoryUF::rewrite(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryBitvector::rewriteAtomic(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::rewriteN(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::setup(), CVC3::TheoryBitvector::signExtendBVLT(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), and updateCC().
Theorem CVC3::Theory::substitutivityRule | ( | const Op & | op, | |
const std::vector< Theorem > & | thms | |||
) | [inline] |
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Definition at line 632 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
Referenced by CVC3::TheoryArithNew::assertFact(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteN(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::signExtendBVLT(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().
Theorem CVC3::Theory::substitutivityRule | ( | const Expr & | e, | |
const Theorem & | t1, | |||
const Theorem & | t2 | |||
) | [inline] |
Special case for binary operators.
Definition at line 637 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
Theorem CVC3::Theory::substitutivityRule | ( | const Expr & | e, | |
const std::vector< unsigned > & | changed, | |||
const std::vector< Theorem > & | thms | |||
) | [inline] |
Optimized: only positions which changed are included.
Definition at line 643 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
Theorem CVC3::Theory::substitutivityRule | ( | const Expr & | e, | |
int | changed, | |||
const Theorem & | thm | |||
) | [inline] |
Optimized: only a single position changed.
Definition at line 649 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
e1 AND (e1 IFF e2) ==> e2
Definition at line 655 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::iffMP().
Referenced by CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryCore::setFindLiteral(), CVC3::SearchImplBase::simplify(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryCore::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().
==> AND(e1,e2) IFF [simplified expr]
Definition at line 660 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::rewriteAnd().
Referenced by CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryRecords::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewriteBoolean(), and CVC3::TheoryCore::simplifyOp().
==> OR(e1,...,en) IFF [simplified expr]
Definition at line 665 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::rewriteOr().
Referenced by CVC3::TheoryCore::computeTCC(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewriteBoolean(), and CVC3::TheoryCore::simplifyOp().
friend class TheoryCore [friend] |
ExprManager* CVC3::Theory::d_em [private] |
Definition at line 67 of file theory.h.
Referenced by CVC3::TheoryCore::assertEqualities(), boolType(), CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryCore::computeType(), falseExpr(), getEM(), newSubtypeExpr(), newVar(), CVC3::TheoryCore::refineCounterExample(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::TheoryCore(), trueExpr(), and CVC3::TheoryCore::~TheoryCore().
TheoryCore* CVC3::Theory::d_theoryCore [private] |
Provides the core functionality.
Definition at line 68 of file theory.h.
Referenced by addBoundVar(), addSplitter(), assertEqualities(), assignValue(), enqueueFact(), getModelValue(), getNumTheories(), getTCC(), hasTheory(), inconsistent(), installID(), newFunction(), newSubtypeExpr(), newVar(), parseExpr(), registerKinds(), registerTheory(), resolveID(), setIncomplete(), setInconsistent(), simplify(), simplifyOp(), CVC3::TheoryCore::TheoryCore(), theoryCore(), theoryOf(), and typePred().
CommonProofRules* CVC3::Theory::d_commonRules [private] |
Commonly used proof rules.
Definition at line 69 of file theory.h.
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), computeTCC(), getCommonRules(), iffMP(), CVC3::TheoryCore::processEquality(), CVC3::TheoryCore::processUpdates(), reflexivityRule(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryCore::rewrite(), rewriteAnd(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::rewriteLitCore(), CVC3::TheoryCore::rewriteLiteral(), rewriteOr(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplifyOp(), simplifyOp(), substitutivityRule(), symmetryRule(), CVC3::TheoryCore::TheoryCore(), transitivityRule(), CVC3::TheoryCore::update(), and updateHelper().
std::string CVC3::Theory::d_name [private] |
Name of the theory (for debugging).
Definition at line 70 of file theory.h.
Referenced by getName(), and CVC3::TheoryCore::TheoryCore().
bool CVC3::Theory::d_theoryUsed [protected] |
Definition at line 79 of file theory.h.
Referenced by CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryUF::print(), CVC3::TheorySimulate::print(), CVC3::TheoryRecords::print(), CVC3::TheoryQuant::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryArray::print(), setUsed(), CVC3::TheoryCore::TheoryCore(), and theoryUsed().