CVC3
|
Base class for theories. More...
#include <theory.h>
Inherited by CVC3::TheoryArith, CVC3::TheoryArray, CVC3::TheoryBitvector, CVC3::TheoryCore, CVC3::TheoryDatatype, CVC3::TheoryQuant, CVC3::TheoryRecords, CVC3::TheorySimulate, and CVC3::TheoryUF.
Public Member Functions | |
Theory (TheoryCore *theoryCore, const std::string &name) | |
Whether theory has been used (for smtlib translator) | |
virtual | ~Theory (void) |
Destructor. | |
ExprManager * | getEM () |
Access to ExprManager. | |
TheoryCore * | theoryCore () |
Get a pointer to theoryCore. | |
CommonProofRules * | getCommonRules () |
Get a pointer to common proof rules. | |
const std::string & | getName () const |
Get the name of the theory (for debugging purposes) | |
virtual void | setUsed () |
Set the "used" flag on this theory (for smtlib translator) | |
virtual bool | theoryUsed () |
Get whether theory has been used (for smtlib translator) | |
virtual void | addSharedTerm (const Expr &e) |
Notify theory of a new shared term. | |
virtual void | assertFact (const Theorem &e)=0 |
Assert a new fact to the decision procedure. | |
virtual void | checkSat (bool fullEffort)=0 |
Check for satisfiability in the theory. | |
virtual Theorem | rewrite (const Expr &e) |
Theory-specific rewrite rules. | |
virtual Theorem | theoryPreprocess (const Expr &e) |
Theory-specific preprocessing. | |
virtual void | setup (const Expr &e) |
Set up the term e for call-backs when e or its children change. | |
virtual void | update (const Theorem &e, const Expr &d) |
Notify a theory of a new equality. | |
virtual Theorem | solve (const Theorem &e) |
An optional solver. | |
virtual void | checkAssertEqInvariant (const Theorem &e) |
A debug check used by the primary solver. | |
virtual Theorem | simplifyOp (const Expr &e) |
Recursive simplification step. | |
virtual void | checkType (const Expr &e) |
Check that e is a valid Type expr. | |
virtual Cardinality | finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize) |
Compute information related to finiteness of types. | |
virtual void | computeType (const Expr &e) |
Compute and store the type of e. | |
virtual Type | computeBaseType (const Type &tp) |
Compute the base type of the top-level operator of an arbitrary type. | |
virtual Expr | computeTypePred (const Type &t, const Expr &e) |
Theory specific computation of the subtyping predicate for type t applied to the expression e. | |
virtual Expr | computeTCC (const Expr &e) |
Compute and cache the TCC of e. | |
virtual Expr | parseExprOp (const Expr &e) |
Theory-specific parsing implemented by the DP. | |
virtual ExprStream & | print (ExprStream &os, const Expr &e) |
Theory-specific pretty-printing. | |
virtual void | computeModelTerm (const Expr &e, std::vector< Expr > &v) |
Add variables from 'e' to 'v' for constructing a concrete model. | |
virtual void | refineCounterExample () |
Process disequalities from the arrangement for model generation. | |
virtual void | computeModelBasic (const std::vector< Expr > &v) |
Assign concrete values to basic-type variables in v. | |
virtual void | computeModel (const Expr &e, std::vector< Expr > &vars) |
Compute the value of a compound variable from the more primitive ones. | |
virtual void | assertTypePred (const Expr &e, const Theorem &pred) |
Receives all the type predicates for the types of the given theory. | |
virtual Theorem | rewriteAtomic (const Expr &e) |
Theory-specific rewrites for atomic formulas. | |
virtual void | notifyInconsistent (const Theorem &thm) |
Notification of conflict. | |
virtual void | registerAtom (const Expr &e, const Theorem &thm) |
virtual void | registerAtom (const Expr &e) |
Theory-specific registration of atoms. | |
Core Framework Functionality | |
These methods provide convenient access to core functionality for the benefit of decision procedures. | |
virtual bool | inconsistent () |
Check if the current context is inconsistent. | |
virtual void | setInconsistent (const Theorem &e) |
Make the context inconsistent; The formula proved by e must FALSE. | |
virtual void | setIncomplete (const std::string &reason) |
Mark the current decision branch as possibly incomplete. | |
virtual Theorem | simplify (const Expr &e) |
Simplify a term e and return a Theorem(e==e') | |
Expr | simplifyExpr (const Expr &e) |
Simplify a term e w.r.t. the current context. | |
virtual void | enqueueFact (const Theorem &e) |
Submit a derived fact to the core from a decision procedure. | |
virtual void | enqueueSE (const Theorem &e) |
Check if the current context is inconsistent. | |
virtual void | assertEqualities (const Theorem &e) |
Handle new equalities (usually asserted through addFact) | |
virtual Expr | parseExpr (const Expr &e) |
Parse the generic expression. | |
virtual void | assignValue (const Expr &t, const Expr &val) |
Assigns t a concrete value val. Used in model generation. | |
virtual void | assignValue (const Theorem &thm) |
Record a derived assignment to a variable (LHS). | |
Theory Helper Methods | |
These methods provide basic functionality needed by all theories. | |
void | registerKinds (Theory *theory, std::vector< int > &kinds) |
Register new kinds with the given theory. | |
void | unregisterKinds (Theory *theory, std::vector< int > &kinds) |
Unregister kinds for a theory. | |
void | registerTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver=false) |
Register a new theory. | |
void | unregisterTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver) |
Unregister a theory. | |
int | getNumTheories () |
Return the number of registered theories. | |
bool | hasTheory (int kind) |
Test whether a kind maps to any theory. | |
Theory * | theoryOf (int kind) |
Return the theory associated with a kind. | |
Theory * | theoryOf (const Type &e) |
Return the theory associated with a type. | |
Theory * | theoryOf (const Expr &e) |
Return the theory associated with an Expr. | |
Theorem | find (const Expr &e) |
Return the theorem that e is equal to its find. | |
const Theorem & | findRef (const Expr &e) |
Return the find as a reference: expr must have a find. | |
Theorem | findReduce (const Expr &e) |
Return find-reduced version of e. | |
bool | findReduced (const Expr &e) |
Return true iff e is find-reduced. | |
Expr | findExpr (const Expr &e) |
Return the find of e, or e if it has no find. | |
Expr | getTCC (const Expr &e) |
Compute the TCC of e, or the subtyping predicate, if e is a type. | |
Type | getBaseType (const Expr &e) |
Compute (or look up in cache) the base type of e and return the result. | |
Type | getBaseType (const Type &tp) |
Compute the base type from an arbitrary type. | |
Expr | getTypePred (const Type &t, const Expr &e) |
Calls the correct theory to compute a type predicate. | |
Theorem | updateHelper (const Expr &e) |
Update the children of the term e. | |
void | setupCC (const Expr &e) |
Setup a term for congruence closure (must have sig and rep attributes) | |
void | updateCC (const Theorem &e, const Expr &d) |
Update a term w.r.t. congruence closure (must be setup with setupCC()) | |
Theorem | rewriteCC (const Expr &e) |
Rewrite a term w.r.t. congruence closure (must be setup with setupCC()) | |
void | getModelTerm (const Expr &e, std::vector< Expr > &v) |
Calls the correct theory to get all of the terms that need to be assigned values in the concrete model. | |
Theorem | getModelValue (const Expr &e) |
Fetch the concrete assignment to the variable during model generation. | |
void | addSplitter (const Expr &e, int priority=0) |
Suggest a splitter to the SearchEngine. | |
void | addGlobalLemma (const Theorem &thm, int priority=0) |
Add a global lemma. | |
Core Testers | |
bool | isLeaf (const Expr &e) |
Test if e is an i-leaf term for the current theory. | |
bool | isLeafIn (const Expr &e1, const Expr &e2) |
Test if e1 is an i-leaf in e2. | |
bool | leavesAreSimp (const Expr &e) |
Test if all i-leaves of e are simplified. | |
Common Type and Expr Methods | |
Type | boolType () |
Return BOOLEAN type. | |
const Expr & | falseExpr () |
Return FALSE Expr. | |
const Expr & | trueExpr () |
Return TRUE Expr. | |
Expr | newVar (const std::string &name, const Type &type) |
Create a new variable given its name and type. | |
Expr | newVar (const std::string &name, const Type &type, const Expr &def) |
Create a new named expression given its name, type, and definition. | |
Op | newFunction (const std::string &name, const Type &type, bool computeTransClosure) |
Create a new uninterpreted function. | |
Op | lookupFunction (const std::string &name, Type *type) |
Look up a function by name. | |
Op | newFunction (const std::string &name, const Type &type, const Expr &def) |
Create a new defined function. | |
Expr | addBoundVar (const std::string &name, const Type &type) |
Create and add a new bound variable to the stack, for parseExprOp(). | |
Expr | addBoundVar (const std::string &name, const Type &type, const Expr &def) |
Create and add a new bound named def to the stack, for parseExprOp(). | |
Expr | lookupVar (const std::string &name, Type *type) |
Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet. | |
Type | newTypeExpr (const std::string &name) |
Create a new uninterpreted type with the given name. | |
Type | lookupTypeExpr (const std::string &name) |
Lookup type by name. Return Null if no such type exists. | |
Type | newTypeExpr (const std::string &name, const Type &def) |
Create a new type abbreviation with the given name. | |
Type | newSubtypeExpr (const Expr &pred, const Expr &witness) |
Create a new subtype expression. | |
Expr | resolveID (const std::string &name) |
Resolve an identifier, for use in parseExprOp() | |
void | installID (const std::string &name, const Expr &e) |
Install name as a new identifier associated with Expr e. | |
Theorem | typePred (const Expr &e) |
Return BOOLEAN type. | |
Commonly Used Proof Rules | |
Theorem | reflexivityRule (const Expr &a) |
==> a == a | |
Theorem | symmetryRule (const Theorem &a1_eq_a2) |
a1 == a2 ==> a2 == a1 | |
Theorem | transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) |
(a1 == a2) & (a2 == a3) ==> (a1 == a3) | |
Theorem | substitutivityRule (const Op &op, const std::vector< Theorem > &thms) |
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n) | |
Theorem | substitutivityRule (const Expr &e, const Theorem &t) |
Special case for unary operators. | |
Theorem | substitutivityRule (const Expr &e, const Theorem &t1, const Theorem &t2) |
Special case for binary operators. | |
Theorem | substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms) |
Optimized: only positions which changed are included. | |
Theorem | substitutivityRule (const Expr &e, int changed, const Theorem &thm) |
Optimized: only a single position changed. | |
Theorem | iffMP (const Theorem &e1, const Theorem &e1_iff_e2) |
e1 AND (e1 IFF e2) ==> e2 | |
Theorem | rewriteAnd (const Expr &e) |
==> AND(e1,e2) IFF [simplified expr] | |
Theorem | rewriteOr (const Expr &e) |
==> OR(e1,...,en) IFF [simplified expr] | |
Theorem | rewriteIte (const Expr &e) |
Derived rule for rewriting ITE. | |
Theorem | renameExpr (const Expr &e) |
Derived rule to create a new name for an expression. | |
Protected Attributes | |
bool | d_theoryUsed |
Private Member Functions | |
Theory (void) | |
Private default constructor. | |
Private Attributes | |
ExprManager * | d_em |
TheoryCore * | d_theoryCore |
Provides the core functionality. | |
CommonProofRules * | d_commonRules |
Commonly used proof rules. | |
std::string | d_name |
Name of the theory (for debugging) | |
Friends | |
class | TheoryCore |
Base class for theories.
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.
|
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 | ||
) |
Whether theory has been used (for smtlib translator)
Exposed constructor.
Note that each instance of Theory must have a name (mostly for debugging purposes).
Definition at line 36 of file theory.cpp.
|
virtual |
Destructor.
Definition at line 44 of file theory.cpp.
|
inline |
Access to ExprManager.
Definition at line 90 of file theory.h.
References d_em.
Referenced by addBoundVar(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryRecords::checkType(), CVC3::TheoryUF::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryBitvector::checkType(), CVC3::TheoryArith3::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryCore::checkType(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryRecords::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryQuant::enqueueInst(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::TheoryArray::finiteTypeInfo(), CVC3::TheoryCore::finiteTypeInfo(), CVC3::TheoryCore::getAssignment(), CVC3::SearchEngine::getConcreteModel(), CVC3::CompleteInstPreProcessor::inst(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoryUF::lambdaExpr(), lookupFunction(), lookupVar(), CVC3::CompleteInstPreProcessor::minusOne(), 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::TheoryCore::parseExpr(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::CompleteInstPreProcessor::plusOne(), CVC3::ExprTransform::preprocess(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryQuant::print(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryCore::printSmtLibShared(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::TheoryArith::rat(), CVC3::TheoryBitvector::rat(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::TheoryRecords::recordExpr(), CVC3::TheoryRecords::recordSelect(), CVC3::TheoryRecords::recordType(), CVC3::TheoryRecords::recordUpdate(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), registerKinds(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::ExprTransform::simplifyWithCare(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::TheoryArith3::TheoryArith3(), 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(), CVC3::TheoryRecords::tupleUpdate(), unregisterKinds(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and updateCC().
|
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::TheoryArray::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryQuant::debug(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryQuant::getExprScore(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryArray::print(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryQuant::pushBackList(), CVC3::TheoryQuant::pushForwList(), CVC3::TheoryQuant::recursiveMap(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryQuant::saveContext(), CVC3::TheoryRecords::setup(), CVC3::TheoryArray::setup(), CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryQuant::synCheckSat(), CVC3::TheoryQuant::synNewInst(), CVC3::TheoryQuant::theoryPreprocess(), and CVC3::TheoryQuant::TheoryQuant().
|
inline |
Get a pointer to common proof rules.
Definition at line 96 of file theory.h.
References d_commonRules.
Referenced by CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryBitvector::checkSat(), CVC3::CompleteInstPreProcessor::collectIndex(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryBitvector::computeTCC(), CVC3::ExprTransform::ExprTransform(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::CompleteInstPreProcessor::simplifyQuant(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::TheoryArithOld(), CVC3::TheoryUF::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), and CVC3::TheoryArithOld::update().
|
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<<(), and CVC3::TheoryCore::refineCounterExample().
|
inlinevirtual |
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::processType().
|
inlinevirtual |
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().
|
virtual |
Check if the current context is inconsistent.
Reimplemented in CVC3::TheoryCore.
Definition at line 97 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::inconsistent().
Referenced by CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArith3::assignVariables(), CVC3::TheoryArithOld::assignVariables(), CVC3::TheoryArith3::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryRecords::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), and CVC3::TheoryArithOld::update().
|
virtual |
Make the context inconsistent; The formula proved by e must FALSE.
Reimplemented in CVC3::TheoryCore.
Definition at line 103 of file theory.cpp.
References d_theoryCore, IF_DEBUG, and CVC3::TheoryCore::setInconsistent().
Referenced by CVC3::TheoryArithNew::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::checkSat(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), and CVC3::TheoryArithOld::update().
|
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 112 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::setIncomplete().
Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryQuant::naiveCheckSat(), and CVC3::TheoryQuant::synCheckSat().
Simplify a term e and return a Theorem(e==e')
Reimplemented in CVC3::TheoryCore.
Definition at line 119 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::simplify().
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArith3::computeModel(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryUF::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArithOld::rewrite(), simplifyExpr(), CVC3::TheoryArray::update(), CVC3::TheoryBitvector::update(), and CVC3::TheoryArithOld::update().
Simplify a term e w.r.t. the current context.
Definition at line 430 of file theory.h.
References CVC3::Theorem::getRHS(), and simplify().
Referenced by CVC3::CompleteInstPreProcessor::addIndex(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::enqueueInst(), CVC3::SearchEngineFast::findSplitter(), CVC3::TheoryQuant::multMatchChild(), newSubtypeExpr(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArray::setup(), CVC3::TheoryQuant::simplifyExprMap(), CVC3::TheoryQuant::simpRAWList(), and CVC3::TheoryQuant::synNewInst().
|
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 128 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::enqueueFact().
Referenced by CVC3::TheoryRecords::assertFact(), CVC3::TheoryUF::assertFact(), CVC3::TheoryArray::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryQuant::assertFact(), assertTypePred(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryArith3::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryArithNew::checkSatInteger(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryDatatype::instantiate(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryQuant::sendInstNew(), CVC3::TheoryRecords::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), and updateCC().
|
virtual |
Check if the current context is inconsistent.
Reimplemented in CVC3::TheoryCore.
Definition at line 134 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::enqueueSE().
|
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 142 of file theory.cpp.
References CVC3::TheoryCore::assertEqualities(), and d_theoryCore.
Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryRecords::setup(), CVC3::TheoryRecords::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), and CVC3::TheoryArithOld::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 519 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::parseExpr().
Referenced by CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), and CVC3::TheoryQuant::parseExprOp().
Assigns t a concrete value val. Used in model generation.
Reimplemented in CVC3::TheoryCore.
Definition at line 162 of file theory.cpp.
References CVC3::TheoryCore::assignValue(), d_theoryCore, getName(), CVC3::Expr::toString(), and TRACE.
Referenced by CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArith3::assignVariables(), CVC3::TheoryArithOld::assignVariables(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArith3::computeModel(), CVC3::TheoryArithOld::computeModel(), and computeModel().
|
virtual |
Record a derived assignment to a variable (LHS).
Reimplemented in CVC3::TheoryCore.
Definition at line 170 of file theory.cpp.
References CVC3::TheoryCore::assignValue(), d_theoryCore, getName(), and TRACE.
void Theory::registerKinds | ( | Theory * | theory, |
std::vector< int > & | kinds | ||
) |
Register new kinds with the given theory.
Definition at line 177 of file theory.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), d_theoryCore, CVC3::TheoryCore::d_theoryMap, DebugAssert, getEM(), CVC3::ExprManager::getKindName(), and CVC3::int2string().
Referenced by registerTheory().
void Theory::unregisterKinds | ( | Theory * | theory, |
std::vector< int > & | kinds | ||
) |
Unregister kinds for a theory.
Definition at line 190 of file theory.cpp.
References d_theoryCore, CVC3::TheoryCore::d_theoryMap, DebugAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::erase(), getEM(), and CVC3::int2string().
Referenced by unregisterTheory().
void Theory::registerTheory | ( | Theory * | theory, |
std::vector< int > & | kinds, | ||
bool | hasSolver = false |
||
) |
Register a new theory.
Definition at line 203 of file theory.cpp.
References CVC3::TheoryCore::d_solver, CVC3::TheoryCore::d_theories, d_theoryCore, DebugAssert, and registerKinds().
Referenced by CVC3::TheoryArith3::TheoryArith3(), 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().
void Theory::unregisterTheory | ( | Theory * | theory, |
std::vector< int > & | kinds, | ||
bool | hasSolver | ||
) |
Unregister a theory.
Definition at line 224 of file theory.cpp.
References CVC3::TheoryCore::d_solver, CVC3::TheoryCore::d_theories, d_theoryCore, DebugAssert, and unregisterKinds().
Referenced by CVC3::TheoryArithOld::~TheoryArithOld().
int Theory::getNumTheories | ( | ) |
Return the number of registered theories.
Definition at line 241 of file theory.cpp.
References CVC3::TheoryCore::d_theories, and d_theoryCore.
Referenced by CVC3::TheoryCore::buildModel(), and CVC3::TheoryCore::refineCounterExample().
bool Theory::hasTheory | ( | int | kind | ) |
Test whether a kind maps to any theory.
Definition at line 247 of file theory.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), d_theoryCore, and CVC3::TheoryCore::d_theoryMap.
Referenced by CVC3::TheoryCore::parseExpr().
Theory * Theory::theoryOf | ( | int | kind | ) |
Return the theory associated with a kind.
Definition at line 252 of file theory.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), d_theoryCore, CVC3::TheoryCore::d_theoryMap, DebugAssert, getEM(), and CVC3::ExprManager::getKindName().
Referenced by CVC3::TheoryBitvector::assertTypePred(), CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::checkEquation(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryUF::computeType(), CVC3::TheoryCore::computeTypePred(), CVC3::TheoryUF::finiteTypeInfo(), CVC3::TheoryDatatype::finiteTypeInfo(), getBaseType(), getModelTerm(), getTCC(), getTypePred(), isLeaf(), isLeafIn(), CVC3::TheoryBitvector::isTermIn(), CVC3::TheoryCore::parseExpr(), CVC3::Translator::processType(), CVC3::SearchImplBase::registerAtom(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryCore::rewriteLiteral(), CVC3::TheoryUF::setup(), CVC3::TheoryArray::setup(), CVC3::TheoryCore::setupTerm(), CVC3::ExprTransform::simplifyWithCare(), and CVC3::TheoryCore::solve().
Return the theory associated with a type.
Definition at line 260 of file theory.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), d_theoryCore, CVC3::TheoryCore::d_theoryMap, DebugAssert, getBaseType(), getEM(), CVC3::Type::getExpr(), CVC3::ExprManager::getKindName(), CVC3::Expr::getOpKind(), and CVC3::Expr::isNull().
Return the theory associated with an Expr.
Definition at line 271 of file theory.cpp.
References Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::count(), 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 310 of file theory.cpp.
References DebugAssert, CVC3::Expr::getFind(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::Theorem::isRefl(), reflexivityRule(), CVC3::Expr::setFind(), and transitivityRule().
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::buildModel(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryCore::collectBasicVars(), computeModel(), CVC3::TheoryCore::computeModelBasic(), CVC3::TheoryArithOld::computeTermBounds(), findExpr(), findReduce(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryArithNew::getBeta(), CVC3::TheoryArithNew::getLowerBound(), CVC3::TheoryArithNew::getLowerBoundThm(), CVC3::TheoryArithNew::getUpperBound(), CVC3::TheoryArithNew::getUpperBoundThm(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryCore::rewrite(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryCore::update(), and CVC3::TheoryBitvector::updateSubterms().
Return the find as a reference: expr must have a find.
Definition at line 295 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 CVC3::TheoryArray::update(), and updateHelper().
Return find-reduced version of e.
Definition at line 327 of file theory.cpp.
References CVC3::Expr::arity(), d_commonRules, find(), CVC3::Expr::hasFind(), CVC3::Theorem::isRefl(), reflexivityRule(), and CVC3::CommonProofRules::substitutivityRule().
bool Theory::findReduced | ( | const Expr & | e | ) |
Return true iff e is find-reduced.
Definition at line 357 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 503 of file theory.h.
References find(), CVC3::Theorem::getRHS(), and CVC3::Expr::hasFind().
Referenced by CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArith3::assignVariables(), CVC3::TheoryArithOld::assignVariables(), CVC3::TheoryDatatype::canCollapse(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryArith3::computeModel(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithNew::computeModelBasic(), CVC3::TheoryArith3::computeModelBasic(), CVC3::TheoryArithOld::computeModelBasic(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryArith3::computeModelTerm(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::TheoryArithNew::findRationalBound(), CVC3::TheoryArith3::findRationalBound(), CVC3::TheoryArithOld::findRationalBound(), CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArray::setup(), CVC3::TheoryUF::update(), and CVC3::TheoryArithOld::update().
Compute the TCC of e, or the subtyping predicate, if e is a type.
Definition at line 367 of file theory.cpp.
References computeTCC(), CVC3::TheoryCore::d_tccCache, d_theoryCore, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getKind(), getName(), CVC3::Expr::isVar(), theoryOf(), TRACE, and trueExpr().
Referenced by CVC3::TheoryUF::computeTCC(), computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryQuant::computeTCC(), and newSubtypeExpr().
Compute (or look up in cache) the base type of e and return the result.
Definition at line 383 of file theory.cpp.
References CVC3::Expr::getType().
Referenced by CVC3::TheoryDatatype::addSharedTerm(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryArray::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::TheoryCore::buildModel(), CVC3::TheoryQuant::canMatch(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryCore::collectBasicVars(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheorySimulate::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::TheoryQuant::findInstAssumptions(), CVC3::Translator::finish(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), getModelTerm(), CVC3::TheoryDatatype::instantiate(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), newVar(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryCore::print(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::TheoryQuant::recInstantiate(), CVC3::TheoryQuant::recursiveMap(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArray::rewrite(), CVC3::TheoryCore::rewriteLiteral(), CVC3::TheoryRecords::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryCore::solve(), theoryOf(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::TheoryDatatype::update(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().
Compute the base type from an arbitrary type.
Definition at line 389 of file theory.cpp.
References computeBaseType(), DebugAssert, CVC3::Type::getExpr(), CVC3::Expr::isNull(), CVC3::Expr::lookupType(), CVC3::Expr::setType(), theoryOf(), and CVC3::Type::toString().
Calls the correct theory to compute a type predicate.
Definition at line 406 of file theory.cpp.
References computeTypePred(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), and theoryOf().
Referenced by CVC3::TheorySimulate::computeTCC(), CVC3::TheoryRecords::computeTCC(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryRecords::computeTypePred(), and CVC3::TheoryCore::computeTypePred().
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 417 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::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and updateCC().
void Theory::setupCC | ( | const Expr & | e | ) |
Setup a term for congruence closure (must have sig and rep attributes)
Definition at line 459 of file theory.cpp.
References CVC3::Expr::addToNotify(), CVC3::Expr::arity(), reflexivityRule(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), and CVC3::Expr::setUsesCC().
Referenced by CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryUF::setup(), CVC3::TheoryRecords::setup(), and CVC3::TheoryDatatype::setup().
Update a term w.r.t. congruence closure (must be setup with setupCC())
Definition at line 473 of file theory.cpp.
References CVC3::Expr::addToNotify(), CVC3::Expr::arity(), enqueueFact(), getEM(), CVC3::Expr::getRep(), CVC3::Theorem::getRHS(), CVC3::Expr::getSig(), CVC3::Expr::getType(), CVC3::ExprManager::invalidateSimpCache(), 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 512 of file theory.cpp.
References CVC3::Expr::getRep(), CVC3::Theorem::isNull(), reflexivityRule(), and symmetryRule().
Referenced by CVC3::TheoryRecords::rewrite(), and CVC3::TheoryUF::rewrite().
Calls the correct theory to get all of the terms that need to be assigned values in the concrete model.
Definition at line 527 of file theory.cpp.
References computeModelTerm(), DebugAssert, getBaseType(), getName(), IF_DEBUG, theoryOf(), CVC3::Expr::toString(), and TRACE.
Referenced by CVC3::TheoryCore::collectBasicVars().
Fetch the concrete assignment to the variable during model generation.
Definition at line 541 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::getModelValue().
Referenced by CVC3::TheoryRecords::computeModel(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), and CVC3::TheoryBitvector::computeModel().
void Theory::addSplitter | ( | const Expr & | e, |
int | priority = 0 |
||
) |
Suggest a splitter to the SearchEngine.
Definition at line 148 of file theory.cpp.
References CVC3::TheoryCore::CoreSatAPI::addSplitter(), CVC3::TheoryCore::d_coreSatAPI, d_theoryCore, DebugAssert, getName(), CVC3::int2string(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isBoolConst(), and TRACE.
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), and CVC3::TheoryArithOld::refineCounterExample().
void Theory::addGlobalLemma | ( | const Theorem & | thm, |
int | priority = 0 |
||
) |
Add a global lemma.
Definition at line 157 of file theory.cpp.
References CVC3::TheoryCore::CoreSatAPI::addLemma(), CVC3::TheoryCore::d_coreSatAPI, and d_theoryCore.
|
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 556 of file theory.h.
References CVC3::Expr::isVar(), and theoryOf().
Referenced by CVC3::TheoryArithNew::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArithNew::assertLower(), CVC3::TheoryArithNew::assertUpper(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::TheoryBitvector::canSolveFor(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithNew::collectVars(), CVC3::TheoryArith3::collectVars(), CVC3::TheoryArithOld::collectVars(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithOld::getUpperBound(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), isLeafIn(), CVC3::TheoryBitvector::isLinearTerm(), CVC3::TheoryArithOld::isNonlinearSumTerm(), CVC3::BitvectorTheoremProducer::isolate_var(), leavesAreSimp(), CVC3::TheoryBitvector::multiply_coeff(), CVC3::TheoryBitvector::Odd_coeff(), CVC3::BitvectorTheoremProducer::okToSplit(), CVC3::TheoryArithNew::pivotRule(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryArithNew::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryArithOld::termDegree(), and CVC3::TheoryBitvector::updateSubterms().
Test if e1 is an i-leaf in e2.
Definition at line 546 of file theory.cpp.
References CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), isLeaf(), and theoryOf().
Referenced by CVC3::TheoryBitvector::assertFact(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::TheoryBitvector::Odd_coeff(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::TheoryArithNew::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArith3::solve(), and CVC3::TheoryArithOld::solve().
bool Theory::leavesAreSimp | ( | const Expr & | e | ) |
Test if all i-leaves of e are simplified.
Definition at line 557 of file theory.cpp.
References CVC3::Expr::arity(), CVC3::Expr::getFind(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), and isLeaf().
Referenced by CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::update(), and CVC3::TheoryArith3::update().
|
inline |
Return BOOLEAN type.
Definition at line 576 of file theory.h.
References d_em, and CVC3::Type::typeBool().
Referenced by CVC3::TheoryArithNew::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryCore::parseExprOp(), and CVC3::TheoryQuant::parseExprOp().
|
inline |
Return FALSE Expr.
Definition at line 579 of file theory.h.
References d_em, and CVC3::ExprManager::falseExpr().
Referenced by CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::constEq(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::TheoryCore::finiteTypeInfo(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::SearchEngine::getConcreteModel(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryCore::print(), CVC3::SearchImplBase::returnFromCheck(), CVC3::TheoryCore::setInconsistent(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::SearchEngine::tryModelGeneration(), CVC3::TheoryArithOld::update(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().
|
inline |
Return TRUE Expr.
Definition at line 582 of file theory.h.
References d_em, and CVC3::ExprManager::trueExpr().
Referenced by CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryDatatype::computeTCC(), computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::BitvectorTheoremProducer::constEq(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::TheoryCore::finiteTypeInfo(), CVC3::BitvectorTheoremProducer::generalIneqn(), getTCC(), CVC3::CompleteInstPreProcessor::inst(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::TheoryQuant::mapTermsByType(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryCore::print(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::TheoryQuant::theoryPreprocess(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::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 569 of file theory.cpp.
References CVC3::TheoryCore::addToVarDB(), CVC3::Type::arity(), d_em, d_theoryCore, DebugAssert, getEM(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), installID(), CVC3::Type::isBool(), CVC3::Type::isFunction(), CVC3::Type::isNull(), CVC3::ExprManager::newSymbolExpr(), CVC3::ExprManager::newVarExpr(), resolveID(), CVC3::Type::toString(), TYPEDEF, and UCONST.
Referenced by CVC3::BitvectorTheoremProducer::bvUDivConst(), CVC3::BitvectorTheoremProducer::bvURemConst(), 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 610 of file theory.cpp.
References ARROW, DebugAssert, getBaseType(), CVC3::Expr::getType(), installID(), CVC3::Type::isNull(), CVC3::Expr::isNull(), resolveID(), CVC3::Type::toString(), and TYPEDEF.
Create a new uninterpreted function.
Add the definition to the database for resolving IDs in parseExpr
Definition at line 647 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(), TYPEDEF, and UFUNC.
Referenced by CVC3::TheoryDatatype::dataType().
Look up a function by name.
Returns the function and sets type to the type of the function if it exists. If not, returns a NULL Op object.
Definition at line 697 of file theory.cpp.
References getEM(), CVC3::Expr::lookupType(), CVC3::Expr::mkOp(), CVC3::ExprManager::newSymbolExpr(), and UFUNC.
Create a new defined function.
Add the definition to the database for resolving IDs in parseExpr
Definition at line 678 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 709 of file theory.cpp.
References boundVarCount, CVC3::ExprMap< Data >::clear(), CVC3::TheoryCore::d_boundVarMap, CVC3::TheoryCore::d_boundVarStack, CVC3::TheoryCore::d_parseCache, CVC3::TheoryCore::d_parseCacheOther, CVC3::TheoryCore::d_parseCacheTop, d_theoryCore, DebugAssert, CVC3::ExprMap< Data >::empty(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), getEM(), CVC3::Expr::getKind(), RAW_LIST, CVC3::Expr::toString(), and TRACE.
Referenced by CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryCore::parseExprOp(), and CVC3::TheoryQuant::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 738 of file theory.cpp.
References boundVarCount, CVC3::ExprMap< Data >::clear(), CVC3::TheoryCore::d_boundVarMap, CVC3::TheoryCore::d_boundVarStack, CVC3::TheoryCore::d_parseCache, CVC3::TheoryCore::d_parseCacheOther, CVC3::TheoryCore::d_parseCacheTop, d_theoryCore, DebugAssert, CVC3::ExprMap< Data >::empty(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), getEM(), CVC3::Expr::getKind(), CVC3::Type::isNull(), LETDECL, RAW_LIST, CVC3::Type::toString(), CVC3::Expr::toString(), and TRACE.
Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Definition at line 776 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 790 of file theory.cpp.
References getEM(), installID(), CVC3::Expr::isNull(), resolveID(), and TYPEDECL.
Referenced by CVC3::Translator::finish().
Type Theory::lookupTypeExpr | ( | const std::string & | name | ) |
Lookup type by name. Return Null if no such type exists.
Definition at line 805 of file theory.cpp.
References CVC3::Expr::getKind(), CVC3::Expr::isNull(), CVC3::Expr::isType(), resolveID(), and TYPEDECL.
Create a new type abbreviation with the given name.
Definition at line 872 of file theory.cpp.
References CVC3::Type::getExpr(), installID(), CVC3::Expr::isNull(), and resolveID().
Create a new subtype expression.
Definition at line 816 of file theory.cpp.
References CVC3::TheoryCore::CoreSatAPI::check(), CVC3::TheoryCore::d_coreSatAPI, d_em, d_theoryCore, EXISTS, FORALL, CVC3::Expr::getBody(), CVC3::TheoryCore::getFlags(), getTCC(), CVC3::Expr::getType(), CVC3::Expr::getVars(), CVC3::Expr::isLambda(), CVC3::Expr::isNull(), CVC3::Expr::mkOp(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), simplifyExpr(), 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 887 of file theory.cpp.
References CVC3::TheoryCore::d_boundVarMap, CVC3::TheoryCore::d_globals, d_theoryCore, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::Expr::getKind(), and 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(), lookupTypeExpr(), 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 910 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.
Definition at line 918 of file theory.cpp.
References d_theoryCore, and CVC3::TheoryCore::typePred().
Referenced by CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArith3::rewrite(), and CVC3::TheoryArithOld::rewrite().
==> a == a
Definition at line 673 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::reflexivityRule().
Referenced by CVC3::TheoryArithNew::assertFact(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::TheoryCore::callTheoryPreprocess(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::BitvectorTheoremProducer::extractBVPlus(), find(), findReduce(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::BitvectorTheoremProducer::MarkNonSolvableEq(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArray::pullIndex(), CVC3::ExprTransform::pushNegationRec(), CVC3::TheorySimulate::rewrite(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryUF::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryDatatype::rewrite(), rewrite(), CVC3::TheoryQuant::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewriteAtomic(), rewriteAtomic(), rewriteCC(), rewriteIte(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryArray::setup(), setupCC(), CVC3::TheoryArithNew::setupRec(), CVC3::TheoryArith3::setupRec(), CVC3::TheoryArithOld::setupRec(), CVC3::TheoryCore::setupTerm(), simplifyOp(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), theoryPreprocess(), CVC3::TheoryQuant::theoryPreprocess(), and updateHelper().
a1 == a2 ==> a2 == a1
Definition at line 677 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::symmetryRule().
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assignValue(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithNew::getVariableIntroThm(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArray::rewrite(), rewriteCC(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryArray::solve(), CVC3::TheoryDatatype::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryCore::update(), and updateCC().
|
inline |
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition at line 681 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::transitivityRule().
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assignValue(), CVC3::TheoryCore::buildModel(), CVC3::TheoryCore::callTheoryPreprocess(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith3::canonSimplify(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArith::canonThm(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArray::checkSat(), CVC3::TheoryCore::collectModelValues(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), find(), findRef(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryUF::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryDatatype::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryRecords::setup(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryCore::update(), updateCC(), and CVC3::TheoryBitvector::updateSubterms().
|
inline |
(c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Definition at line 686 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
Referenced by CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArray::checkSat(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryRecords::setup(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryArray::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryBitvector::updateSubterms().
Special case for unary operators.
Definition at line 691 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
|
inline |
Special case for binary operators.
Definition at line 696 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
|
inline |
Optimized: only positions which changed are included.
Definition at line 702 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
|
inline |
Optimized: only a single position changed.
Definition at line 708 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().
e1 AND (e1 IFF e2) ==> e2
Definition at line 714 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::iffMP().
Referenced by CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArray::checkSat(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryCore::setupTerm(), CVC3::SearchImplBase::simplify(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryCore::update().
==> AND(e1,e2) IFF [simplified expr]
Definition at line 719 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::rewriteAnd().
Referenced by CVC3::TheorySimulate::computeTCC(), CVC3::TheoryRecords::computeTCC(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryCore::rewrite(), and CVC3::TheoryCore::simplifyOp().
==> OR(e1,...,en) IFF [simplified expr]
Definition at line 724 of file theory.h.
References d_commonRules, and CVC3::CommonProofRules::rewriteOr().
Referenced by CVC3::TheoryCore::computeTCC(), CVC3::TheoryCore::rewrite(), and CVC3::TheoryCore::simplifyOp().
Derived rule for rewriting ITE.
Definition at line 923 of file theory.cpp.
References d_commonRules, reflexivityRule(), CVC3::CommonProofRules::rewriteIteFalse(), CVC3::CommonProofRules::rewriteIteSame(), and CVC3::CommonProofRules::rewriteIteTrue().
Referenced by CVC3::TheoryArray::checkSat(), and CVC3::TheoryCore::rewrite().
Derived rule to create a new name for an expression.
Definition at line 935 of file theory.cpp.
References CVC3::TheoryCore::addToVarDB(), d_commonRules, d_theoryCore, DebugAssert, CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::Expr::isSkolem(), CVC3::Theorem::toString(), and CVC3::CommonProofRules::varIntroSkolem().
Referenced by CVC3::TheoryArray::update(), and CVC3::TheoryBitvector::update().
|
friend |
|
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::print(), CVC3::TheoryCore::refineCounterExample(), CVC3::TheoryCore::TheoryCore(), trueExpr(), and CVC3::TheoryCore::~TheoryCore().
|
private |
Provides the core functionality.
Definition at line 68 of file theory.h.
Referenced by addBoundVar(), addGlobalLemma(), addSplitter(), assertEqualities(), assignValue(), enqueueFact(), enqueueSE(), CVC3::TheoryCore::getAssignment(), getModelValue(), getNumTheories(), getTCC(), CVC3::TheoryCore::getValue(), hasTheory(), inconsistent(), installID(), newFunction(), newSubtypeExpr(), newVar(), parseExpr(), registerAtom(), registerKinds(), registerTheory(), renameExpr(), resolveID(), setIncomplete(), setInconsistent(), simplify(), simplifyOp(), theoryCore(), CVC3::TheoryCore::TheoryCore(), theoryOf(), typePred(), unregisterKinds(), and unregisterTheory().
|
private |
Commonly used proof rules.
Definition at line 69 of file theory.h.
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::checkSolved(), computeTCC(), findReduce(), getCommonRules(), iffMP(), reflexivityRule(), CVC3::TheoryCore::registerAtom(), renameExpr(), CVC3::TheoryCore::rewrite(), rewriteAnd(), rewriteIte(), CVC3::TheoryCore::rewriteLiteral(), rewriteOr(), simplifyOp(), CVC3::TheoryCore::simplifyOp(), substitutivityRule(), symmetryRule(), CVC3::TheoryCore::TheoryCore(), transitivityRule(), CVC3::TheoryCore::update(), and updateHelper().
|
private |
Name of the theory (for debugging)
Definition at line 70 of file theory.h.
Referenced by getName(), and CVC3::TheoryCore::TheoryCore().
|
protected |
Definition at line 79 of file theory.h.
Referenced by CVC3::TheoryBitvector::parseExprOp(), CVC3::TheorySimulate::print(), CVC3::TheoryRecords::print(), CVC3::TheoryUF::print(), CVC3::TheoryArray::print(), CVC3::TheoryQuant::print(), CVC3::TheoryBitvector::printSmtLibShared(), setUsed(), CVC3::TheoryCore::TheoryCore(), and theoryUsed().