CVC3  2.4.1
Public Member Functions | Protected Attributes | Private Member Functions | Private Attributes | Friends
CVC3::Theory Class Reference

Base class for theories. More...

#include <theory.h>

Inheritance diagram for CVC3::Theory:
CVC3::TheoryArith CVC3::TheoryArray CVC3::TheoryBitvector CVC3::TheoryCore CVC3::TheoryDatatype CVC3::TheoryQuant CVC3::TheoryRecords CVC3::TheorySimulate CVC3::TheoryUF

List of all members.

Public Member Functions

 Theory (TheoryCore *theoryCore, const std::string &name)
 Whether theory has been used (for smtlib translator)
virtual ~Theory (void)
 Destructor.
ExprManagergetEM ()
 Access to ExprManager.
TheoryCoretheoryCore ()
 Get a pointer to theoryCore.
CommonProofRulesgetCommonRules ()
 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 ExprStreamprint (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.
TheorytheoryOf (int kind)
 Return the theory associated with a kind.
TheorytheoryOf (const Type &e)
 Return the theory associated with a type.
TheorytheoryOf (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 TheoremfindRef (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 ExprfalseExpr ()
 Return FALSE Expr.
const ExprtrueExpr ()
 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

ExprManagerd_em
TheoryCored_theoryCore
 Provides the core functionality.
CommonProofRulesd_commonRules
 Commonly used proof rules.
std::string d_name
 Name of the theory (for debugging)

Friends

class TheoryCore

Detailed Description

Base class for theories.

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.


Constructor & Destructor Documentation

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 
)

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.

Theory::~Theory ( void  )
virtual

Destructor.

Definition at line 44 of file theory.cpp.


Member Function Documentation

ExprManager* CVC3::Theory::getEM ( )
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().

TheoryCore* CVC3::Theory::theoryCore ( )
inline
CommonProofRules* CVC3::Theory::getCommonRules ( )
inline
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<<(), and CVC3::TheoryCore::refineCounterExample().

virtual void CVC3::Theory::setUsed ( )
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().

virtual bool CVC3::Theory::theoryUsed ( )
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().

bool Theory::inconsistent ( )
virtual
void Theory::setInconsistent ( const Theorem e)
virtual
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 112 of file theory.cpp.

References d_theoryCore, and CVC3::TheoryCore::setIncomplete().

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryQuant::naiveCheckSat(), and CVC3::TheoryQuant::synCheckSat().

Theorem Theory::simplify ( const Expr e)
virtual
Expr CVC3::Theory::simplifyExpr ( const Expr e)
inline
void Theory::enqueueFact ( const Theorem e)
virtual
void Theory::enqueueSE ( const Theorem e)
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().

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 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().

Expr Theory::parseExpr ( const Expr e)
virtual
void Theory::assignValue ( const Expr t,
const Expr val 
)
virtual
void Theory::assignValue ( const Theorem thm)
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 
)
void Theory::unregisterKinds ( Theory theory,
std::vector< int > &  kinds 
)
void Theory::registerTheory ( Theory theory,
std::vector< int > &  kinds,
bool  hasSolver = false 
)
void Theory::unregisterTheory ( Theory theory,
std::vector< int > &  kinds,
bool  hasSolver 
)
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)
Theory * Theory::theoryOf ( const Type e)
Theory * Theory::theoryOf ( const Expr e)
Theorem Theory::find ( const Expr e)

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().

const Theorem & Theory::findRef ( const Expr e)

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().

Theorem Theory::findReduce ( const Expr e)
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().

Expr CVC3::Theory::findExpr ( const Expr e)
inline

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().

Expr Theory::getTCC ( const Expr e)
Type Theory::getBaseType ( const Expr e)

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().

Type Theory::getBaseType ( const Type tp)

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().

Expr Theory::getTypePred ( const Type t,
const Expr e 
)
Theorem Theory::updateHelper ( const Expr e)

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'.

See also:
update

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)
void Theory::updateCC ( const Theorem e,
const Expr d 
)
Theorem Theory::rewriteCC ( const Expr e)

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().

void Theory::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.

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().

Theorem Theory::getModelValue ( const Expr e)

Fetch the concrete assignment to the variable during model generation.

Reimplemented in CVC3::TheoryCore.

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 
)
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.

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 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().

bool Theory::isLeafIn ( const Expr e1,
const Expr e2 
)
bool Theory::leavesAreSimp ( const Expr e)
Type CVC3::Theory::boolType ( )
inline
const Expr& CVC3::Theory::falseExpr ( )
inline
const Expr& CVC3::Theory::trueExpr ( )
inline
Expr Theory::newVar ( const std::string &  name,
const Type type 
)
Expr Theory::newVar ( const std::string &  name,
const Type type,
const Expr def 
)

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.

Op Theory::newFunction ( const std::string &  name,
const Type type,
bool  computeTransClosure 
)
Op Theory::lookupFunction ( const std::string &  name,
Type type 
)

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.

Op Theory::newFunction ( const std::string &  name,
const Type type,
const Expr def 
)

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().

Expr Theory::addBoundVar ( const std::string &  name,
const Type type 
)
Expr Theory::addBoundVar ( const std::string &  name,
const Type type,
const Expr def 
)

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.

Expr Theory::lookupVar ( const std::string &  name,
Type type 
)

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.

Type Theory::newTypeExpr ( const std::string &  name,
const Type def 
)

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().

Type Theory::newSubtypeExpr ( const Expr pred,
const Expr witness 
)
Expr Theory::resolveID ( const std::string &  name)
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().

Theorem Theory::typePred ( const Expr e)

Return BOOLEAN type.

Reimplemented in CVC3::TheoryCore.

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().

Theorem CVC3::Theory::reflexivityRule ( const Expr a)
inline

==> 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().

Theorem CVC3::Theory::symmetryRule ( const Theorem a1_eq_a2)
inline
Theorem CVC3::Theory::transitivityRule ( const Theorem a1_eq_a2,
const Theorem a2_eq_a3 
)
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().

Theorem CVC3::Theory::substitutivityRule ( const Op op,
const std::vector< Theorem > &  thms 
)
inline
Theorem CVC3::Theory::substitutivityRule ( const Expr e,
const Theorem t 
)
inline

Special case for unary operators.

Definition at line 691 of file theory.h.

References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().

Theorem CVC3::Theory::substitutivityRule ( const Expr e,
const Theorem t1,
const Theorem t2 
)
inline

Special case for binary operators.

Definition at line 696 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 702 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 708 of file theory.h.

References d_commonRules, and CVC3::CommonProofRules::substitutivityRule().

Theorem CVC3::Theory::iffMP ( const Theorem e1,
const Theorem e1_iff_e2 
)
inline
Theorem CVC3::Theory::rewriteAnd ( const Expr e)
inline
Theorem CVC3::Theory::rewriteOr ( const Expr e)
inline

==> 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().

Theorem Theory::rewriteIte ( const Expr e)
Theorem Theory::renameExpr ( const Expr e)

Friends And Related Function Documentation

friend class TheoryCore
friend

Definition at line 65 of file theory.h.


Member Data Documentation

ExprManager* CVC3::Theory::d_em
private
TheoryCore* CVC3::Theory::d_theoryCore
private
CommonProofRules* CVC3::Theory::d_commonRules
private
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

The documentation for this class was generated from the following files: