CVCL::Theory

CVCL::Theory Class Reference
[Theories, Theories]

Base class for theories. More...

#include <theory.h>

Inheritance diagram for CVCL::Theory:

[legend]Collaboration diagram for CVCL::Theory:

[legend]List of all members.

Public Member Functions

Theory (TheoryCore *theoryCore, const std::string &name)
Exposed constructor.
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 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 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 Theorem simplifyOp (const Expr &e)
Recursive simplification step.
virtual void checkType (const Expr &e)
Check that e is a valid Type expr.
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.

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, bool forceRebuild=true)
Simplify a term e and return a Theorem(e==e').
Expr simplifyExpr (const Expr &e, bool forceRebuild=true)
Simplify a term e w.r.t. the current context.
virtual Theorem simplifyRec (const Expr &e)
Recursive call of the simplifier. Should only be called from simplifyOp().
virtual void enqueueFact (const Theorem &e)
Submit a derived fact to the core from a decision procedure.
virtual void enqueueEquality (const Theorem &e)
Enqueue a new equality e: e1==e2, where e2 is i-leaf simplified.
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 registerTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
Register a new 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 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 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.

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 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 newTypeExpr (const std::string &name, const Type &def)
Create a new type abbreviation with the given name.
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.
Theorem subtypePredicate (const Expr &e)
e: T ==> |- [all the subtype-related facts for e and its subterms]

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 std::vector< unsigned > &changed, const std::vector< Theorem > &thms)
Optimized: only positions which changed are included.
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]

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

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 72 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 40 of file theory.cpp.

CVCL::Theory::Theory ( TheoryCore * theoryCore,

const std::string & name

)

Exposed constructor.
Note that each instance of Theory must have a name (mostly for debugging purposes).

Theory::~Theory ( void ) [virtual]

Destructor.

Definition at line 51 of file theory.cpp.

Member Function Documentation

TheoryCore* CVCL::Theory::theoryCore ( ) [inline]

Get a pointer to theoryCore.

Definition at line 101 of file theory.h.
References d_theoryCore.
Referenced by CVCL::TheoryUF::assertFact(), CVCL::TheoryBitvector::assertFact(), CVCL::TheoryBitvector::assertTypePred(), CVCL::TheoryUF::createProofRules(), CVCL::TheorySimulate::createProofRules(), CVCL::TheoryRecords::createProofRules(), CVCL::TheoryQuant::createProofRules(), CVCL::TheoryArray::createProofRules(), CVCL::TheoryArith::createProofRules(), CVCL::TheoryQuant::goodSynMatch(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryQuant::mapTermsByType(), CVCL::TheoryQuant::naiveCheckSat(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryArith::pickMonomial(), CVCL::TheoryArith::print(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryQuant::recursiveMap(), CVCL::TheoryArray::renameExpr(), CVCL::TheoryQuant::semCheckSat(), CVCL::TheoryArray::setup(), CVCL::TheoryBitvector::setupExpr(), CVCL::TheoryQuant::synCheckSat(), and CVCL::TheoryBitvector::update().

CommonProofRules* CVCL::Theory::getCommonRules ( ) [inline]

Get a pointer to common proof rules.

Definition at line 104 of file theory.h.
References d_commonRules.
Referenced by CVCL::TheoryBitvector::assertFact(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::ExprTransform::ExprTransform(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::CoreTheoremProducer::ImpToIte(), CVCL::TheoryArith::isIntegerDerive(), CVCL::CoreTheoremProducer::NotToIte(), CVCL::TheoryArith::processIntEq(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArray::renameExpr(), CVCL::TheoryArith::rewrite(), CVCL::TheoryBitvector::rewriteBoolean(), CVCL::TheoryUF::update(), and CVCL::TheoryArith::update().

const std::string& CVCL::Theory::getName ( ) const [inline]

Get the name of the theory (for debugging purposes).

Definition at line 107 of file theory.h.
References d_name.
Referenced by addSplitter(), TheoryCore::assertFormula(), assignValue(), TheoryCore::buildModel(), TheoryCore::checkSATCore(), TheoryCore::collectModelValues(), CVCL::TypeComputerCore::computeType(), TheoryCore::enqueueEquality(), enqueueEquality(), enqueueFact(), getBaseType(), getTCC(), getTypePred(), CVCL::operator<<(), TheoryCore::parseExpr(), TheoryCore::processFactQueue(), TheoryCore::processNotify(), TheoryCore::refineCounterExample(), TheoryCore::rewriteCore(), TheoryCore::rewriteLiteral(), TheoryCore::setInconsistent(), setInconsistent(), setupCC(), TheoryCore::setupTerm(), simplify(), TheoryCore::simplifyFullRec(), simplifyRec(), TheoryCore::solve(), and updateCC().

virtual bool CVCL::Theory::theoryUsed ( ) [inline, virtual]

Get whether theory has been used (for smtlib translator).

Reimplemented in CVCL::TheoryArith.
Definition at line 110 of file theory.h.
References d_theoryUsed.

bool Theory::inconsistent ( ) [virtual]

Check if the current context is inconsistent.

Reimplemented in CVCL::TheoryCore.
Definition at line 89 of file theory.cpp.
References d_theoryCore, and CVCL::TheoryCore::inconsistent().
Referenced by CVCL::TheoryArith::assignVariables(), CVCL::TheoryArith::checkSat(), CVCL::TheoryArith::processBuffer(), CVCL::TheoryRecords::update(), and CVCL::TheoryArith::update().

void Theory::setInconsistent ( const Theorem & e ) [virtual]

Make the context inconsistent; The formula proved by e must FALSE.

Reimplemented in CVCL::TheoryCore.
Definition at line 95 of file theory.cpp.
References CVCL::Debug::counter(), d_theoryCore, CVCL::debugger, getName(), IF_DEBUG(), CVCL::TheoryCore::setInconsistent(), and CVCL::TRACE.
Referenced by CVCL::TheoryArith::assertFact(), CVCL::TheoryBitvector::collectSharedSubterms(), CVCL::TheoryDatatypeLazy::mergeLabels(), CVCL::TheoryDatatype::mergeLabels(), CVCL::TheoryArith::processBuffer(), and CVCL::TheoryArith::projectInequalities().

virtual void CVCL::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 CVCL::TheoryCore.
Referenced by CVCL::TheoryArith::doSolve(), CVCL::TheoryQuant::naiveCheckSat(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryQuant::semCheckSat(), and CVCL::TheoryQuant::synCheckSat().

Theorem Theory::simplify ( const Expr & e,

bool forceRebuild = true

) [virtual]

Simplify a term e and return a Theorem(e==e').

See also:
simplifyExpr()

Reimplemented in CVCL::TheoryCore.
Definition at line 111 of file theory.cpp.
References d_theoryCore, getName(), CVCL::TheoryCore::simplify(), and CVCL::TRACE.
Referenced by CVCL::TheoryBitvector::assertFact(), CVCL::TheoryBitvector::checkSat(), CVCL::TheoryBitvector::computeModel(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryUF::rewrite(), CVCL::TheoryDatatype::rewrite(), CVCL::TheoryBitvector::rewriteAtomic(), CVCL::TheoryBitvector::rewriteBV(), and simplifyExpr().

Expr CVCL::Theory::simplifyExpr ( const Expr & e,

bool forceRebuild = true

) [inline]

Simplify a term e w.r.t. the current context.

See also:
simplify

Definition at line 393 of file theory.h.
References CVCL::Theorem::getRHS(), and simplify().
Referenced by CVCL::TheoryArith::canonSimplify(), CVCL::SearchEngineFast::findSplitter(), CVCL::TheoryQuant::recGoodSemMatch(), CVCL::TheoryQuant::recSynMatch(), and CVCL::TheoryArray::setup().

Theorem Theory::simplifyRec ( const Expr & e ) [virtual]

Recursive call of the simplifier. Should only be called from simplifyOp().

Reimplemented in CVCL::TheoryCore.
Definition at line 120 of file theory.cpp.
References d_theoryCore, getName(), CVCL::TheoryCore::simplifyRec(), and CVCL::TRACE.
Referenced by CVCL::TheoryBitvector::simplifyOp(), and simplifyOp().

void Theory::enqueueFact ( const Theorem & e ) [virtual]

Submit a derived fact to the core from a decision procedure.

Parameters:

e is the Theorem for the new fact

Reimplemented in CVCL::TheoryCore.
Definition at line 129 of file theory.cpp.
References d_theoryCore, CVCL::TheoryCore::enqueueFact(), getName(), and CVCL::TRACE.
Referenced by CVCL::TheoryUF::assertFact(), CVCL::TheoryRecords::assertFact(), CVCL::TheoryQuant::assertFact(), CVCL::TheoryBitvector::assertFact(), CVCL::TheoryArith::assertFact(), CVCL::TheoryBitvector::assertTypePred(), assertTypePred(), CVCL::TheoryUF::checkSat(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryBitvector::checkSat(), CVCL::TheoryArith::checkSat(), CVCL::TheoryQuant::enqueueInst(), CVCL::TheoryDatatype::instantiate(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryRecords::setup(), CVCL::TheoryDatatype::setup(), CVCL::TheoryBitvector::setupExpr(), CVCL::TheoryUF::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryBitvector::update(), CVCL::TheoryArray::update(), CVCL::TheoryArith::update(), and updateCC().

void Theory::enqueueEquality ( const Theorem & e ) [virtual]

Enqueue a new equality e: e1==e2, where e2 is i-leaf simplified.

Reimplemented in CVCL::TheoryCore.
Definition at line 136 of file theory.cpp.
References d_theoryCore, CVCL::TheoryCore::enqueueEquality(), getName(), CVCL::Theorem::isRewrite(), CVCL::Theorem::toString(), and CVCL::TRACE.
Referenced by CVCL::TheoryRecords::update(), CVCL::TheoryBitvector::update(), CVCL::TheoryArray::update(), and CVCL::TheoryArith::update().

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.
IMPORTANT: decision procedures should NOT use this function in update(); use enqueueEquality() instead.
Reimplemented in CVCL::TheoryCore.
Definition at line 146 of file theory.cpp.
References CVCL::TheoryCore::assertEqualities(), and d_theoryCore.

Expr Theory::parseExpr ( const Expr & e ) [virtual]

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 CVCL::TheoryCore.
Definition at line 383 of file theory.cpp.
References d_theoryCore, CVCL::TheoryCore::parseExpr(), and CVCL::TRACE.
Referenced by CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), CVCL::TheoryDatatype::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArray::parseExprOp(), and CVCL::TheoryArith::parseExprOp().

void Theory::assignValue ( const Expr & t,

const Expr & val

) [virtual]

Assigns t a concrete value val. Used in model generation.

Reimplemented in CVCL::TheoryCore.
Definition at line 159 of file theory.cpp.
References CVCL::TheoryCore::assignValue(), d_theoryCore, getName(), CVCL::Expr::toString(), and CVCL::TRACE.
Referenced by CVCL::TheoryArith::assignVariables(), CVCL::TheoryUF::computeModel(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryBitvector::computeModel(), CVCL::TheoryArray::computeModel(), and computeModel().

void Theory::assignValue ( const Theorem & thm ) [virtual]

Record a derived assignment to a variable (LHS).

Reimplemented in CVCL::TheoryCore.
Definition at line 167 of file theory.cpp.
References CVCL::TheoryCore::assignValue(), d_theoryCore, getName(), and CVCL::TRACE.

void CVCL::Theory::registerKinds ( Theory * theory,

std::vector< int > & kinds

)

Register new kinds with the given theory.

void CVCL::Theory::registerTheory ( Theory * theory,

std::vector< int > & kinds,

bool hasSolver = false

)

Register a new theory.

Referenced by CVCL::TheoryArith::TheoryArith(), CVCL::TheoryArray::TheoryArray(), CVCL::TheoryBitvector::TheoryBitvector(), CVCL::TheoryDatatype::TheoryDatatype(), CVCL::TheoryQuant::TheoryQuant(), CVCL::TheoryRecords::TheoryRecords(), CVCL::TheorySimulate::TheorySimulate(), and CVCL::TheoryUF::TheoryUF().

int Theory::getNumTheories ( )

Return the number of registered theories.

Definition at line 199 of file theory.cpp.
References CVCL::TheoryCore::d_theories, and d_theoryCore.
Referenced by TheoryCore::buildModel(), TheoryCore::checkSATCore(), TheoryCore::processFactQueue(), TheoryCore::refineCounterExample(), and TheoryCore::setInconsistent().

bool Theory::hasTheory ( int kind )

Test whether a kind maps to any theory.

Definition at line 205 of file theory.cpp.
References d_theoryCore, and CVCL::TheoryCore::d_theoryMap.
Referenced by TheoryCore::parseExpr(), and CVCL::PrettyPrinterCore::print().

Theory * Theory::theoryOf ( int kind )

Return the theory associated with a kind.

Definition at line 210 of file theory.cpp.
References d_theoryCore, CVCL::TheoryCore::d_theoryMap, getEM(), and CVCL::ExprManager::getKindName().
Referenced by TheoryCore::assertFormula(), TheoryCore::buildModel(), CVCL::TypeComputerCore::checkType(), TheoryCore::collectBasicVars(), TheoryCore::collectModelValues(), TheoryCore::computeTCC(), CVCL::TypeComputerCore::computeType(), TheoryCore::computeTypePred(), getBaseType(), getTCC(), getTypePred(), isLeaf(), isLeafIn(), TheoryCore::parseExpr(), CVCL::PrettyPrinterCore::print(), TheoryCore::rewrite(), TheoryCore::rewriteCore(), TheoryCore::rewriteLiteral(), TheoryCore::rewriteN(), TheoryCore::setupSubFormulas(), TheoryCore::setupTerm(), TheoryCore::simplifyFullRec(), TheoryCore::solve(), and theoryOf().

Theory * Theory::theoryOf ( const Expr & e )

Return the theory associated with an Expr.

Definition at line 218 of file theory.cpp.
References d_theoryCore, CVCL::TheoryCore::d_theoryMap, getBaseType(), getEM(), CVCL::Type::getExpr(), CVCL::Expr::getKind(), CVCL::ExprManager::getKindName(), CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), CVCL::Expr::isEq(), CVCL::Expr::isNot(), CVCL::Expr::isNull(), CVCL::Expr::isVar(), and theoryOf().

Theorem Theory::find ( const Expr & e )

Return the theorem that e is equal to its find.

Definition at line 242 of file theory.cpp.
References CVCL::Expr::getFind(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Expr::hasFind(), reflexivityRule(), CVCL::Expr::setFind(), and transitivityRule().
Referenced by TheoryCore::assertEqualities(), TheoryCore::assertFormula(), TheoryCore::assignValue(), TheoryCore::buildModel(), CVCL::TheoryArith::canonSimplify(), TheoryCore::checkSat(), CVCL::TheoryBitvector::checkSat(), CVCL::SearchSimple::checkValidRec(), TheoryCore::collectBasicVars(), computeModel(), TheoryCore::computeModelBasic(), findExpr(), CVCL::TheoryArith::isStale(), CVCL::TheoryDatatypeLazy::mergeLabels(), TheoryCore::processEquality(), TheoryCore::processUpdates(), TheoryCore::rewrite(), CVCL::TheoryBitvector::rewriteAux(), CVCL::TheoryBitvector::rewriteBV(), TheoryCore::rewriteCore(), CVCL::TheoryRecords::setup(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), CVCL::TheoryUF::update(), CVCL::TheoryRecords::update(), CVCL::TheoryBitvector::update(), CVCL::TheoryArray::update(), CVCL::TheoryArith::update(), and updateHelper().

Expr Theory::getTCC ( const Expr & e )

Compute the TCC of e, or the subtyping predicate, if e is a type.

Definition at line 257 of file theory.cpp.
References computeTCC(), CVCL::Expr::getKind(), getName(), CVCL::Expr::isNull(), CVCL::Expr::isVar(), CVCL::Expr::lookupTCC(), CVCL::Expr::setTCC(), theoryOf(), CVCL::TRACE, and trueExpr().
Referenced by CVCL::TheoryUF::computeTCC(), CVCL::TheoryQuant::computeTCC(), TheoryCore::computeTCC(), computeTCC(), and CVCL::CoreTheoremProducer::queryTCC().

Type Theory::getBaseType ( const Expr & e )

Compute (or look up in cache) the base type of e and return the result.

Definition at line 273 of file theory.cpp.
References CVCL::Expr::getType().
Referenced by CVCL::TheoryRecords::assertFact(), TheoryCore::assertFormula(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), TheoryCore::buildModel(), CVCL::TheoryBitvector::BVSize(), checkRewriteType(), TheoryCore::collectBasicVars(), TheoryCore::collectModelValues(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), TheoryCore::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), CVCL::TheoryRecords::computeType(), CVCL::TheoryDatatype::computeType(), TheoryCore::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::TheoryArray::computeType(), CVCL::TheoryArith::computeType(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::RecordsTheoremProducer::expandRecord(), CVCL::RecordsTheoremProducer::expandTuple(), CVCL::TheoryQuant::findInstAssumptions(), CVCL::Translator::preprocessRec(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryQuant::recGoodSemMatch(), CVCL::TheoryQuant::recInstantiate(), CVCL::TheoryQuant::recursiveMap(), CVCL::TheoryArith::refineCounterExample(), TheoryCore::rewriteLiteral(), CVCL::TheoryQuant::semCheckSat(), CVCL::TheoryRecords::setup(), CVCL::TheoryBitvector::setupExpr(), theoryOf(), CVCL::BitvectorTheoremProducer::typePredBit(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

Type Theory::getBaseType ( const Type & tp )

Compute the base type from an arbitrary type.

Definition at line 279 of file theory.cpp.
References computeBaseType(), CVCL::Type::getExpr(), getName(), CVCL::Type::isNull(), CVCL::Expr::isNull(), CVCL::Expr::lookupType(), CVCL::Expr::setType(), theoryOf(), CVCL::Type::toString(), and CVCL::TRACE.

Expr Theory::getTypePred ( const Type & t,

const Expr & e

)

Calls the correct theory to compute a type predicate.

Definition at line 298 of file theory.cpp.
References computeTypePred(), CVCL::Type::getExpr(), CVCL::Expr::getKind(), getName(), theoryOf(), CVCL::Type::toString(), and CVCL::TRACE.
Referenced by CVCL::TheoryUF::computeTCC(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryRecords::computeTCC(), CVCL::TheoryArray::computeTCC(), CVCL::TheoryRecords::computeTypePred(), TheoryCore::computeTypePred(), and CVCL::CoreTheoremProducer::typePred().

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 309 of file theory.cpp.
References CVCL::Expr::arity(), d_commonRules, find(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), reflexivityRule(), and CVCL::CommonProofRules::substitutivityRule().
Referenced by CVCL::TheoryRecords::update(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryBitvector::update(), CVCL::TheoryArray::update(), CVCL::TheoryArith::update(), and updateCC().

void Theory::setupCC ( const Expr & e )

Setup a term for congruence closure (must have sig and rep attributes).

Definition at line 329 of file theory.cpp.
References CVCL::Expr::addToNotify(), CVCL::Expr::arity(), getName(), reflexivityRule(), CVCL::Expr::setRep(), CVCL::Expr::setSig(), and CVCL::TRACE.
Referenced by CVCL::TheoryUF::setup(), CVCL::TheoryRecords::setup(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::TheoryBitvector::setup(), and CVCL::TheoryBitvector::setupExpr().

void Theory::updateCC ( const Theorem & e,

const Expr & d

)

Update a term w.r.t. congruence closure (must be setup with setupCC()).

Definition at line 342 of file theory.cpp.
References CVCL::Expr::addToNotify(), CVCL::Expr::arity(), enqueueFact(), CVCL::Theorem::getExpr(), getName(), CVCL::Expr::getRep(), CVCL::Theorem::getRHS(), CVCL::Expr::getSig(), CVCL::Theorem::isNull(), CVCL::Expr::setRep(), CVCL::Expr::setSig(), symmetryRule(), CVCL::Expr::toString(), CVCL::TRACE, transitivityRule(), and updateHelper().
Referenced by CVCL::TheoryUF::update(), CVCL::TheoryRecords::update(), and CVCL::TheoryBitvector::update().

Theorem Theory::rewriteCC ( const Expr & e )

Rewrite a term w.r.t. congruence closure (must be setup with setupCC()).

Definition at line 376 of file theory.cpp.
References CVCL::Expr::getRep(), CVCL::Theorem::isNull(), reflexivityRule(), and symmetryRule().
Referenced by CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryUF::rewrite(), CVCL::TheoryRecords::rewrite(), and CVCL::TheoryBitvector::rewriteBV().

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

Referenced by TheoryCore::collectBasicVars().

Theorem Theory::getModelValue ( const Expr & e )

Fetch the concrete assignment to the variable during model generation.

Reimplemented in CVCL::TheoryCore.
Definition at line 405 of file theory.cpp.
References d_theoryCore, and CVCL::TheoryCore::getModelValue().
Referenced by CVCL::TheoryUF::computeModel(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryBitvector::computeModel(), and CVCL::TheoryArray::computeModel().

void Theory::addSplitter ( const Expr & e,

int priority = 0

)

Suggest a splitter to the SearchEngine.

Definition at line 152 of file theory.cpp.
References CVCL::TheoryCore::d_coreSatAPI, d_theoryCore, getName(), CVCL::int2string(), and CVCL::TRACE.
Referenced by CVCL::TheoryArith::assertFact(), CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatype::checkSat(), CVCL::TheoryArith::normalizeProjectIneqs(), and CVCL::TheoryArith::refineCounterExample().

bool CVCL::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 507 of file theory.h.
References CVCL::Expr::isVar(), and theoryOf().
Referenced by CVCL::TheoryArith::canonRec(), CVCL::TheoryBitvector::collectSharedSubterms(), isLeafIn(), CVCL::TheoryArith::isSyntacticUMinusVar(), CVCL::TheoryArith::kidsCanonical(), leavesAreSimp(), CVCL::TheoryArith::printMinus(), CVCL::TheoryArith::printPlus(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::rewrite(), CVCL::TheoryArith::solve(), and CVCL::TheoryArith::substAndCanonize().

bool Theory::isLeafIn ( const Expr & e1,

const Expr & e2

)

Test if e1 is an i-leaf in e2.

See also:
isLeaf

Definition at line 410 of file theory.cpp.
References CVCL::Expr::begin(), CVCL::Expr::end(), isLeaf(), and theoryOf().
Referenced by CVCL::TheoryArith::processRealEq(), and CVCL::TheoryArith::solve().

bool Theory::leavesAreSimp ( const Expr & e )

Test if all i-leaves of e are simplified.

See also:
isLeaf

Definition at line 421 of file theory.cpp.
References CVCL::Expr::arity(), CVCL::Expr::getFind(), CVCL::Theorem::getRHS(), IF_DEBUG(), isLeaf(), CVCL::Expr::toString(), and CVCL::TRACE.

Type CVCL::Theory::boolType ( ) [inline]

Return BOOLEAN type.

Definition at line 527 of file theory.h.
References d_em, and CVCL::Type::typeBool().
Referenced by TheoryCore::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::TheoryArith::computeType(), and CVCL::TheoryQuant::mapTermsByType().

const Expr& CVCL::Theory::trueExpr ( ) [inline]

Return TRUE Expr.

Definition at line 533 of file theory.h.
References d_em, and CVCL::ExprManager::trueExpr().
Referenced by CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConstant(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::TheoryUF::computeTCC(), CVCL::TheoryDatatype::computeTCC(), computeTCC(), CVCL::BitvectorTheoremProducer::eqConst(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::ExprTransform::getNeg(), getTCC(), CVCL::ExprTransform::ite_simplify(), CVCL::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVCL::TheoryQuant::mapTermsByType(), CVCL::DatatypeTheoremProducer::rewriteTestCons(), CVCL::TheoryArith::rewriteToDiff(), CVCL::BitvectorTheoremProducer::signBVLTRule(), and CVCL::TheoryArith::update().

Expr CVCL::Theory::newVar ( const std::string & name,

const Type & type

)

Create a new variable given its name and type.
Add the variable to the database for resolving IDs in parseExpr
Referenced by CVCL::TheoryDatatype::getConstant().

Expr CVCL::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

Op CVCL::Theory::newFunction ( const std::string & name,

const Type & type,

bool computeTransClosure

)

Create a new uninterpreted function.
Add the definition to the database for resolving IDs in parseExpr

Op CVCL::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

Expr CVCL::Theory::addBoundVar ( const std::string & name,

const Type & type

)

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.
Referenced by CVCL::TheoryUF::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), TheoryCore::parseExprOp(), and CVCL::TheoryArray::parseExprOp().

Expr CVCL::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

Expr CVCL::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.

Type CVCL::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

Type CVCL::Theory::newTypeExpr ( const std::string & name,

const Type & def

)

Create a new type abbreviation with the given name.

Expr CVCL::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.

Returns:
an expression to use in place of the identifier, or Null if cannot resolve the name.

Referenced by CVCL::TheoryUF::assertFact(), CVCL::TheoryDatatype::checkType(), CVCL::TheoryUF::computeType(), CVCL::TheoryDatatype::getConstant(), TheoryCore::parseExpr(), and CVCL::TheoryUF::parseExprOp().

void CVCL::Theory::installID ( const std::string & name,

const Expr & e

)

Install name as a new identifier associated with Expr e.

Theorem Theory::typePred ( const Expr & e )

Return BOOLEAN type.

Reimplemented in CVCL::TheoryCore.
Definition at line 685 of file theory.cpp.
References d_theoryCore, and CVCL::TheoryCore::typePred().
Referenced by CVCL::TheoryArith::isIntegerThm(), and CVCL::TheoryArith::rewrite().

Theorem Theory::subtypePredicate ( const Expr & e )

e: T ==> |- [all the subtype-related facts for e and its subterms]

Reimplemented in CVCL::TheoryCore.
Definition at line 690 of file theory.cpp.
References d_theoryCore, and CVCL::TheoryCore::subtypePredicate().

Theorem CVCL::Theory::symmetryRule ( const Theorem & a1_eq_a2 ) [inline]

a1 == a2 ==> a2 == a1

Definition at line 619 of file theory.h.
References d_commonRules, and CVCL::CommonProofRules::symmetryRule().
Referenced by TheoryCore::assertFormula(), TheoryCore::assignValue(), TheoryCore::checkSat(), CVCL::TheoryUF::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryArith::doSolve(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processSimpleIntEq(), TheoryCore::rewrite(), CVCL::TheoryBitvector::rewriteBV(), rewriteCC(), CVCL::TheoryRecords::setup(), CVCL::TheoryBitvector::setupExpr(), CVCL::TheoryDatatype::solve(), CVCL::TheoryBitvector::solve(), CVCL::TheoryArray::solve(), CVCL::TheoryArith::solve(), CVCL::RefinedArithTheoremProducer::symm(), CVCL::TheoryUF::update(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryBitvector::update(), CVCL::TheoryArray::update(), CVCL::TheoryArith::update(), and updateCC().

Theorem CVCL::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 633 of file theory.h.
References d_commonRules, and CVCL::CommonProofRules::substitutivityRule().