CVCL::TheoryCore Class Reference
[Theories]

This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories. More...

#include <theory_core.h>

Inheritance diagram for CVCL::TheoryCore:

[legend]Collaboration diagram for CVCL::TheoryCore:

[legend]List of all members.

Public Member Functions

void registerCoreSatAPI (CoreSatAPI *coreSatAPI)
Register a SatAPI for TheoryCore.
bool isEquivCheckExpr (const Expr &e)
Check if the expr is Equiv. Check Expr.
const Expr & getE0 (const Expr &e)
Access LHS of the equiv. check expr.
const Expr & getE1 (const Expr &e)
Access RHS of the equiv. check expr.
TheoryCore (ContextManager *cm, ExprManager *em, TheoremManager *tm, const CLFlags &flags, Statistics &statistics)
Constructor.
~TheoryCore ()
Destructor.
ContextManager * getCM () const
TheoremManager * getTM () const
const CLFlags & getFlags () const
Statistics & getStatistics () const
ExprTransform * getExprTrans () const
CoreProofRules * getCoreRules () const
const CDList< Expr > & getTerms ()
Get list of terms.
void addSharedTerm (const Expr &e)
void assertFact (const Theorem &e)
Assert a new fact to the decision procedure.
void checkSat (bool fullEffort)
Check for satisfiability in the theory.
Theorem rewrite (const Expr &e)
Theory-specific rewrite rules.
void setup (const Expr &e)
Set up the term e for call-backs when e or its children change.
void update (const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Theorem solve (const Theorem &e)
An optional solver.
Theorem simplifyOp (const Expr &e)
Recursive simplification step.
void checkType (const Expr &e)
Check that e is a valid Type expr.
void computeType (const Expr &e)
Compute and store the type of e.
Type computeBaseType (const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
Expr computeTCC (const Expr &e)
Compute and cache the TCC of e.
Expr computeTypePred (const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e.
Expr parseExprOp (const Expr &e)
Theory-specific parsing implemented by the DP.
ExprStream & print (ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
void refineCounterExample ()
Calls for other theories to add facts to refine a coutnerexample.
void computeModelBasic (const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
void setResourceLimit (unsigned limit)
Set the resource limit (0==unlimited).
bool inconsistent ()
Check if the current context is inconsistent.
Theorem inconsistentThm ()
Get the proof of inconsistency for the current context.
void addFact (const Theorem &e)
Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure; use enqueueFact().
Theorem simplify (const Expr &e, bool forceRebuild=true)
Top-level simplifier.
bool checkSATCore ()
To be called by SearchEngine when it believes the context is satisfiable.
void registerAtom (const Expr &e)
Register an atomic formula of interest.
Theorem getImpliedLiteral (void)
Return the next implied literal (NULL Theorem if none).
unsigned numImpliedLiterals ()
Return total number of implied literals.
Theorem getImpliedLiteralByIndex (unsigned index)
Return an implied literal by index.
bool incomplete ()
Check if the current decision branch is marked as incomplete.
bool incomplete (std::vector< std::string > &reasons)
Check if the branch is incomplete, and return the reasons (strings).
Theorem rewriteLiteral (const Expr &e)
Called by search engine.
Expr parseExpr (const Expr &e)
Parse the generic expression.
Expr parseExprTop (const Expr &e)
Top-level call to parseExpr, clears the bound variable stack.
void assignValue (const Expr &t, const Expr &val)
Assign t a concrete value val. Used in model generation.
void assignValue (const Theorem &thm)
Record a derived assignment to a variable (LHS).
void addToVarDB (const Expr &e)
Adds expression to var database.
void collectBasicVars ()
Split compound vars into basic type variables.
void buildModel (ExprMap< Expr > &m)
Calls theory specific computeModel, results are placed in map.
void collectModelValues (const Expr &e, ExprMap< Expr > &m)
Recursively build a compound-type variable assignment for e.
Theorem typePred (const Expr &e)
Return BOOLEAN type.
Theorem subtypePredicate (const Expr &e)
Compute and cache the subtyping predicates for the expression.
void enqueueFact (const Theorem &e)
Enqueue a new fact.
void setInconsistent (const Theorem &e)
Make the context inconsistent; The formula proved by e must FALSE.
void setupTerm (const Expr &e, Theory *i)
Setup additional terms within a theory-specific setup().
Theorem3 queryTCC (const Theorem &phi, const Theorem &D_phi)
Theorem3 implIntro3 (const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs)

Private Member Functions

IF_DEBUG (const std::string *d_dumpTrace)
Command line flag whether to dump debugging info on every new fact.
IF_DEBUG (bool d_inCheckSATCore)
IF_DEBUG (bool d_inAddFact)
IF_DEBUG (bool d_inSimplify)
IF_DEBUG (bool d_inRegisterAtom)
IF_DEBUG (void dumpTrace(const Expr &fact, const std::string &title);) void setFindLiteral(const Theorem &thm
Set the find pointer of an atomic formula and notify SearchEngine.
Theorem rewriteIte (const Expr &e)
Derived rule for rewriting ITE.
Theorem rewriteLitCore (const Expr &e)
Core rewrites for literals (NOT and EQ).
Theorem rewriteN (const Expr &e, int n)
Rewrite n levels deep. WARNING: no caching here, be careful.
bool processEquality (const Theorem &thm, ExprMap< Theorem > &q)
An auxiliary function for assertEqualities(); return true if inconsistency is derived.
CoreProofRules * createProofRules (TheoremManager *tm)
Private method to get a new theorem producer.
void enqueueSE (const Theorem &thm)
Enqueue a fact to be sent to the SearchEngine.
Theorem getModelValue (const Expr &e)
Fetch the concrete assignment to the variable during model generation.
Expr newEquivCkExpr (const Expr &e0, const Expr &e1)
Create a new equiv. check Expr (private, only TheoryCore can do that).
Expr processCond (const Expr &e, int i)
An auxiliary recursive function to process COND expressions into ITE.
bool getResource ()
Request a unit of resource.
void enqueueEquality (const Theorem &e)
Enqueue a new equality.
void assertEqualities (const Theorem &e)
Assert a system of equations (1 or more).
void setIncomplete (const std::string &reason)
Mark the branch as incomplete.
void processFactQueue ()
A helper function for addFact().
void processNotify (const Theorem &e, NotifyList *L)
Process a notify list triggered as a result of new theorem e.
Theorem simplifyRec (const Expr &e)
The recursive simplifier (to be used only in DP-specific simplifyOp()).
Theorem simplifyFullRec (const Expr &e)
The full recursive simplifier.
Theorem simplifyInPlaceRec (const Expr &e)
The recursive simplifier with the in-place rewriting optimization.
Theorem rewriteCore (const Theorem &e)
Transitive composition of other rewrites with the above.
void setupSubFormulas (const Expr &s, const Expr &e)
Helper for registerAtom.
void processUpdates ()
Process updates recorded by calls to update().
void assertFactCore (const Theorem &e)
The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface function name.
void assertFormula (const Theorem &e)
Process a newly derived formula.
Theorem rewriteCore (const Expr &e)
Returns phi |= e = rewriteCore(e). "Core" added to avoid conflict with theory interface function name.

Private Attributes

ContextManager * d_cm
Context manager.
TheoremManager * d_tm
Theorem manager.
CoreProofRules * d_rules
Core proof rules.
const CLFlags & d_flags
Reference to command line flags.
Statistics & d_statistics
Reference to statistics.
PrettyPrinter * d_printer
PrettyPrinter (we own it).
ExprManager::TypeComputer * d_typeComputer
Type Computer.
ExprTransform * d_exprTrans
Expr Transformer.
std::queue< Theorem > d_queue
Assertion queue.
std::vector< Theorem > d_queueSE
Queue of facts to be sent to the SearchEngine.
std::vector< Theorem > d_equalityQueue
Equality queue.
CDO< bool > d_inconsistent
Inconsistent flag.
CDMap< std::string, bool > d_incomplete
The set of reasons for incompleteness (empty when we are complete).
CDList< Theorem > d_diseq
List of known disequalities (to be processed at every checkSat() call).
CDO< Theorem > d_incThm
Proof of inconsistent.
CDList< Expr > d_terms
List of all active terms in the system (for quantifier instantiation).
CDList< Expr > d_vars
List of variables that were created up to this point.
std::map< std::string, Expr > d_globals
Database of declared identifiers.
std::vector< std::pair< std::string,
Expr > > d_boundVarStack
Bound variable stack: a vector of pairs <name, var>.
CDMap< Expr, Theory * > d_sharedTerms
List of all terms that are shared between theories (alien subterms).
std::map< Expr, bool > d_typePredAsserted
std::vector< Theory * > d_theories
Array of registered theories.
std::map< int, Theory * > d_theoryMap
Array mapping kinds to theories.
Theory * d_solver
The theory which has the solver (if any).
ExprHashMap< std::vector<
Expr > > d_varModelMap
Mapping of compound type variables to simpler types (model generation).
ExprHashMap< Theorem > d_varAssignments
Mapping of intermediate variables to their valies.
std::vector< Expr > d_basicModelVars
List of basic variables (temporary storage for model generation).
ExprHashMap< Theorem > d_simplifiedModelVars
Mapping of basic variables to simplified expressions (temp. storage).
const bool * d_simplifyInPlace
Command line flag whether to simplify in place.
Theorem(TheoryCore::* d_currentRecursiveSimplifier )(const Expr &)
Which recursive simplifier to use.
const bool * d_cnfOption
Command line flag whether to convert to CNF.
unsigned d_resourceLimit
Resource limit (0==unlimited, 1==no more resources, >=2 - available).
CoreNotifyObj d_notifyObj
size_t d_equivCheckMMidx
Memory Manager index for equiv. check Expr.
CDList< Theorem > d_impliedLiterals
List of implied literals, based on registered atomic formulas of interest.
CDO< unsigned > d_impliedLiteralsIdx
Next index in d_impliedLiterals that has not yet been fetched.
std::vector< Theorem > d_update_thms
List of theorems from calls to update().
std::vector< Expr > d_update_data
List of data accompanying above theorems from calls to update().
CoreSatAPI * d_coreSatAPI
bool notifySAT

Friends

class Theory
class CoreNotifyObj
So we get notified every time there's a pop.

Classes

class CoreNotifyObj
class CoreSatAPI

Detailed Description

This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories.

Author: Clark Barrett

Created: Sat Feb 8 14:54:05 2003

Definition at line 54 of file theory_core.h.

Constructor & Destructor Documentation

CVCL::TheoryCore::TheoryCore ( ContextManager * cm,

ExprManager * em,

TheoremManager * tm,

const CLFlags & flags,

Statistics & statistics

)

Constructor.

CVCL::TheoryCore::~TheoryCore ( )

Destructor.

Member Function Documentation

CVCL::TheoryCore::IF_DEBUG ( const std::string * d_dumpTrace ) [private]

Command line flag whether to dump debugging info on every new fact.

Referenced by TheoryCore::addFact(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), TheoryCore::checkSat(), TheoryCore::checkSATCore(), TheoryCore::collectModelValues(), TheoryCore::computeType(), TheoryCore::enqueueEquality(), TheoryCore::enqueueFact(), TheoryCore::processEquality(), TheoryCore::processFactQueue(), TheoryCore::registerAtom(), TheoryCore::rewriteCore(), TheoryCore::setupTerm(), TheoryCore::simplify(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyOp(), and TheoryCore::solve().

CVCL::TheoryCore::IF_DEBUG ( bool d_inCheckSATCore ) [private]

CVCL::TheoryCore::IF_DEBUG ( bool d_inAddFact ) [private]

CVCL::TheoryCore::IF_DEBUG ( bool d_inSimplify ) [private]

CVCL::TheoryCore::IF_DEBUG ( bool d_inRegisterAtom ) [private]

CVCL::TheoryCore::IF_DEBUG ( void dumpTrace(const Expr &fact, const std::string &title); ) const [private]

Set the find pointer of an atomic formula and notify SearchEngine.

Parameters:

thm is a Theorem(phi) or Theorem(NOT phi), where phi is an atomic formula to get a find pointer to TRUE or FALSE, respectively.

notifySAT indicates whether to notify the Search Engine of this literal.

Theorem CVCL::TheoryCore::rewriteIte ( const Expr & e ) [private]

Derived rule for rewriting ITE.

Theorem CVCL::TheoryCore::rewriteLitCore ( const Expr & e ) [private]

Core rewrites for literals (NOT and EQ).

Referenced by TheoryCore::rewrite(), and TheoryCore::rewriteCore().

Theorem CVCL::TheoryCore::rewriteN ( const Expr & e,

int n

) [private]

Rewrite n levels deep. WARNING: no caching here, be careful.

Referenced by TheoryCore::rewrite(), and TheoryCore::rewriteN().

bool CVCL::TheoryCore::processEquality ( const Theorem & thm,

ExprMap< Theorem > & q

) [private]

An auxiliary function for assertEqualities(); return true if inconsistency is derived.

Referenced by TheoryCore::assertEqualities(), and TheoryCore::processEquality().

CoreProofRules* CVCL::TheoryCore::createProofRules ( TheoremManager * tm ) [private]

Private method to get a new theorem producer.
This method is used ONLY by the TheoryCore constructor. The only reason to have this method is to separate the trusted part of the constructor into a separate .cpp file (Alternative is to make the entire constructer trusted, which is not very safe).

void CVCL::TheoryCore::enqueueSE ( const Theorem & thm ) [private]

Enqueue a fact to be sent to the SearchEngine.

Referenced by TheoryCore::assertFactCore(), and TheoryCore::assertFormula().

Theorem CVCL::TheoryCore::getModelValue ( const Expr & e ) [private]

Fetch the concrete assignment to the variable during model generation.

Reimplemented from CVCL::Theory.
Referenced by TheoryCore::collectModelValues(), and CVCL::Theory::getModelValue().

Expr CVCL::TheoryCore::newEquivCkExpr ( const Expr & e0,

const Expr & e1

) [private]

Create a new equiv. check Expr (private, only TheoryCore can do that).

Expr CVCL::TheoryCore::processCond ( const Expr & e,

int i

) [private]

An auxiliary recursive function to process COND expressions into ITE.

Referenced by TheoryCore::parseExprOp(), and TheoryCore::processCond().

bool CVCL::TheoryCore::getResource ( ) [private]

Request a unit of resource.
It will be subtracted from the resource limit.

Returns:
true if resource unit is granted, false if no more resources available.

Referenced by TheoryCore::enqueueFact().

void CVCL::TheoryCore::registerCoreSatAPI ( CoreSatAPI * coreSatAPI ) [inline]

Register a SatAPI for TheoryCore.

Definition at line 279 of file theory_core.h.
References d_coreSatAPI.
Referenced by CVCL::SearchImplBase::SearchImplBase(), and CVCL::SearchSat::SearchSat().

bool CVCL::TheoryCore::isEquivCheckExpr ( const Expr & e )

Check if the expr is Equiv. Check Expr.

const Expr& CVCL::TheoryCore::getE0 ( const Expr & e )

Access LHS of the equiv. check expr.

const Expr& CVCL::TheoryCore::getE1 ( const Expr & e )

Access RHS of the equiv. check expr.

ContextManager* CVCL::TheoryCore::getCM ( ) const [inline]

Definition at line 296 of file theory_core.h.
References d_cm.
Referenced by CVCL::SearchSat::addLemma(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::TheoryUF::assertFact(), CVCL::SearchSat::check(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), CVCL::SearchEngine::getConcreteModel(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::TheoryQuant::mapTermsByType(), CVCL::SearchSat::newUserAssumption(), CVCL::DecisionEngine::popDecision(), CVCL::DecisionEngine::popTo(), CVCL::TheoryArith::projectInequalities(), CVCL::DecisionEngine::pushDecision(), CVCL::TheoryQuant::recursiveMap(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::SearchSat::returnFromCheck(), CVCL::SearchImplBase::scopeLevel(), CVCL::SearchImplBase::SearchImplBase(), CVCL::TheoryQuant::semCheckSat(), and CVCL::TheoryQuant::synCheckSat().

TheoremManager* CVCL::TheoryCore::getTM ( ) const [inline]

Definition at line 297 of file theory_core.h.
References d_tm.
Referenced by CVCL::SearchEngine::createRules(), CVCL::SearchImplBase::getAssumptionsUsed(), CVCL::SearchImplBase::getProof(), and CVCL::SearchSat::SearchSat().

const CLFlags& CVCL::TheoryCore::getFlags ( ) const [inline]

Definition at line 298 of file theory_core.h.
References d_flags.
Referenced by CVCL::TheoryBitvector::assertFact(), CVCL::TheoryBitvector::assertTypePred(), CVCL::SearchEngineFast::bcp(), CVCL::TheoryArith::pickMonomial(), CVCL::ExprTransform::preprocess(), CVCL::TheoryArith::print(), TheoryCore::rewrite(), CVCL::SearchEngineFast::SearchEngineFast(), CVCL::SearchImplBase::SearchImplBase(), CVCL::SearchSimple::SearchSimple(), TheoryCore::simplifyFullRec(), and TheoryCore::simplifyOp().

Statistics& CVCL::TheoryCore::getStatistics ( ) const [inline]

Definition at line 299 of file theory_core.h.
References d_statistics.
Referenced by CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchImplBase::findInCNFCache(), and CVCL::SearchEngineFast::split().

ExprTransform* CVCL::TheoryCore::getExprTrans ( ) const [inline]

Definition at line 300 of file theory_core.h.
References d_exprTrans.
Referenced by CVCL::SearchSat::check(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), and CVCL::SearchImplBase::newUserAssumption().

CoreProofRules* CVCL::TheoryCore::getCoreRules ( ) const [inline]

Definition at line 301 of file theory_core.h.
References d_rules.
Referenced by CVCL::ExprTransform::ExprTransform().

const CDList<Expr>& CVCL::TheoryCore::getTerms ( ) [inline]

Get list of terms.

Definition at line 304 of file theory_core.h.
References d_terms.
Referenced by CVCL::TheoryQuant::goodSynMatch(), CVCL::TheoryQuant::naiveCheckSat(), CVCL::TheoryQuant::semCheckSat(), and CVCL::TheoryQuant::synCheckSat().

void CVCL::TheoryCore::addSharedTerm ( const Expr & e ) [inline, virtual]

Variables of uninterpreted types may be sent here, and they should be ignored.
Reimplemented from CVCL::Theory.
Definition at line 309 of file theory_core.h.

void CVCL::TheoryCore::assertFact ( const Theorem & e ) [virtual]

Assert a new fact to the decision procedure.
Each fact that makes it into the core framework is assigned to exactly one theory: the theory associated with that fact. assertFact is called to inform the theory that a new fact has been assigned to the theory.
Implements CVCL::Theory.

void CVCL::TheoryCore::checkSat ( bool fullEffort ) [virtual]

Check for satisfiability in the theory.

Parameters:

fullEffort when it is false, checkSat can do as much or as little work as it likes, though simple inferences and checks for consistency should be done to increase efficiency. If fullEffort is true, checkSat must check whether the set of facts given by assertFact together with the arrangement of shared terms (provided by addSharedTerm) induced by the global find database equivalence relation are satisfiable. If satisfiable, checkSat does nothing.

If satisfiability can be acheived by merging some of the shared terms, a new fact must be enqueued using enqueueFact (this fact need not be a literal). If there is no way to make things satisfiable, setInconsistent must be called.
Implements CVCL::Theory.

Theorem CVCL::TheoryCore::rewrite ( const Expr & e ) [virtual]

Theory-specific rewrite rules.
By default, rewrite just returns a reflexive theorem stating that the input expression is equivalent to itself. However, rewrite is allowed to return any theorem which describes how the input expression is equivalent to some new expression. rewrite should be used to perform simplifications, normalization, and any other preprocessing on theory-specific expressions that needs to be done.
Reimplemented from CVCL::Theory.
Referenced by TheoryCore::rewrite(), and TheoryCore::rewriteN().

void CVCL::TheoryCore::setup ( const Expr & e ) [virtual]

Set up the term e for call-backs when e or its children change.
setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update.
See also:
update

Reimplemented from CVCL::Theory.

void CVCL::TheoryCore::update ( const Theorem & e,

const Expr & d

) [virtual]

Notify a theory of a new equality.
update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2.
To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup.

See also:
setup

Reimplemented from CVCL::Theory.

Theorem CVCL::TheoryCore::solve ( const Theorem & e ) [virtual]

An optional solver.
The solve method can be used to implement a Shostak-style solver. Since solvers do not in general combine, the following technique is used. One theory is designated as the primary solver (in our case, it is the theory of arithmetic). For each equation that enters the core framework, the primary solver is called to ensure that the equation is in solved form with respect to the primary theory.
After the primary solver, the solver for the theory associated with the equation is called. This solver can do whatever it likes, as long as the result is still in solved form with respect to the primary solver. This is a slight generalization of what is described in my (Clark)'s PhD thesis.
Reimplemented from CVCL::Theory.
Referenced by TheoryCore::assertFactCore().

Theorem CVCL::TheoryCore::simplifyOp ( const Expr & e ) [virtual]

Recursive simplification step.
INVARIANT: the result is a Theorem(e=e'), where e' is a fully simplified version of e. To simplify subexpressions recursively, call simplify() function.
This theory-specific method is called when the simplifier descends top-down into the expression. Normally, every kid is simplified recursively, and the results are combined into the new parent with the same operator (Op). This functionality is provided with the default implementation.
However, in some expressions some kids may not matter in the result, and can be skipped. For instance, if the first kid in a long AND simplifies to FALSE, then the entire expression simplifies to FALSE, and the remaining kids do not need to be simplified.
This call is a chance for a DP to provide these types of optimizations during the top-down phase of simplification.
Reimplemented from CVCL::Theory.
Referenced by TheoryCore::simplifyOp().

void CVCL::TheoryCore::checkType ( const Expr & e ) [virtual]

Check that e is a valid Type expr.

Reimplemented from CVCL::Theory.

void CVCL::TheoryCore::computeType ( const Expr & e ) [virtual]

Compute and store the type of e.

Parameters:

e is the expression whose type is computed.

This function computes the type of the top-level operator of e, and recurses into children using getType(), if necessary.
Reimplemented from CVCL::Theory.

Type CVCL::TheoryCore::computeBaseType ( const Type & t ) [virtual]

Compute the base type of the top-level operator of an arbitrary type.

Reimplemented from CVCL::Theory.

Expr CVCL::TheoryCore::computeTCC ( const Expr & e ) [virtual]

Compute and cache the TCC of e.

Parameters:

e is an expression (term or formula). This function computes the TCC of e which is true iff the expression is defined.

This function computes the TCC or predicate of the top-level operator of e, and recurses into children using getTCC(), if necessary.
The default implementation is to compute TCCs recursively for all children, and return their conjunction.
Reimplemented from CVCL::Theory.

Expr CVCL::TheoryCore::computeTypePred ( const Type & t,

const Expr & e

) [virtual]

Theory specific computation of the subtyping predicate for type t applied to the expression e.
By default returns true. Each theory needs to compute subtype predicates for the types associated with it. So, for example, the theory of records will take a record type [# f1: T1, f2: T2 #] and an expression e and will return the subtyping predicate for e, namely: computeTypePred(T1, e.f1) AND computeTypePred(T2, e.f2)
Reimplemented from CVCL::Theory.

Expr CVCL::TheoryCore::parseExprOp ( const Expr & e ) [virtual]

Theory-specific parsing implemented by the DP.

Reimplemented from CVCL::Theory.

ExprStream& CVCL::TheoryCore::print ( ExprStream & os,

const Expr & e

) [virtual]

Theory-specific pretty-printing.
By default, print the top node in AST, and resume pretty-printing the children. The same call e.print(os) can be used in DP-specific printers to use AST printing for the given node. In fact, it is strongly recommended to add e.print(os) as the default for all the cases/kinds that are not handled by the particular pretty-printer.
Reimplemented from CVCL::Theory.

void CVCL::TheoryCore::refineCounterExample ( ) [virtual]

Calls for other theories to add facts to refine a coutnerexample.

Reimplemented from CVCL::Theory.
Referenced by CVCL::SearchEngine::getConcreteModel().

void CVCL::TheoryCore::computeModelBasic ( const std::vector< Expr > & v ) [virtual]

Assign concrete values to basic-type variables in v.

Reimplemented from CVCL::Theory.

void CVCL::TheoryCore::setResourceLimit ( unsigned limit )

Set the resource limit (0==unlimited).

bool CVCL::TheoryCore::inconsistent ( ) [inline, virtual]

Check if the current context is inconsistent.

Reimplemented from CVCL::Theory.
Definition at line 335 of file theory_core.h.
References d_inconsistent.
Referenced by CVCL::SearchEngineFast::bcp(), TheoryCore::buildModel(), CVCL::SearchSimple::checkValidRec(), TheoryCore::enqueueFact(), CVCL::Theory::inconsistent(), TheoryCore::refineCounterExample(), and CVCL::SearchEngineFast::split().

Theorem CVCL::TheoryCore::inconsistentThm ( ) [inline]

Get the proof of inconsistency for the current context.

Returns:
Theorem(FALSE)

Definition at line 338 of file theory_core.h.
References d_incThm.
Referenced by CVCL::SearchEngineFast::bcp(), TheoryCore::buildModel(), CVCL::SearchSimple::checkValidRec(), CVCL::SearchEngine::getConcreteModel(), and TheoryCore::refineCounterExample().

void CVCL::TheoryCore::addFact ( const Theorem & e )

Add a new assertion to the core from the user or a SAT solver. Do NOT use it in a decision procedure; use enqueueFact().

See also:
enqueueFact

Referenced by CVCL::SearchSat::assertLit(), TheoryCore::assignValue(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::commitFacts(), CVCL::SearchSat::newUserAssumption(), CVCL::SearchImplBase::newUserAssumption(), CVCL::Circuit::propagate(), CVCL::DecisionEngine::pushDecision(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), and CVCL::SearchEngineFast::split().

Theorem CVCL::TheoryCore::simplify ( const Expr & e,

bool forceRebuild = true

) [virtual]

Top-level simplifier.

Reimplemented from CVCL::Theory.
Referenced by TheoryCore::assertFactCore(), CVCL::ExprTransform::preprocess(), TheoryCore::processUpdates(), TheoryCore::registerAtom(), CVCL::Theory::simplify(), CVCL::SearchImplBase::simplify(), and CVCL::SearchEngineFast::split().

bool CVCL::TheoryCore::checkSATCore ( )

To be called by SearchEngine when it believes the context is satisfiable.

Returns:
true if definitely consistent or inconsistent and false if consistency is unknown.

Referenced by CVCL::SearchSimple::checkValidRec(), and CVCL::SearchEngineFast::split().

void CVCL::TheoryCore::registerAtom ( const Expr & e )

Register an atomic formula of interest.
If e or its negation is later deduced, we will add the implied literal to d_impliedLiterals
Referenced by CVCL::SearchSat::addLemma(), CVCL::SearchSat::check(), CVCL::SearchSat::registerAtom(), and CVCL::SearchImplBase::registerAtom().

Theorem CVCL::TheoryCore::getImpliedLiteral ( void )

Return the next implied literal (NULL Theorem if none).

Referenced by CVCL::SearchSat::getImplication(), and CVCL::SearchImplBase::getImpliedLiteral().

unsigned CVCL::TheoryCore::numImpliedLiterals ( ) [inline]

Return total number of implied literals.

Definition at line 366 of file theory_core.h.
References d_impliedLiterals, and CVCL::CDList< T >::size().

Theorem CVCL::TheoryCore::getImpliedLiteralByIndex ( unsigned index )

Return an implied literal by index.

Referenced by CVCL::SearchSat::getImpliedLiteral().

bool CVCL::TheoryCore::incomplete ( ) [inline]

Check if the current decision branch is marked as incomplete.

Definition at line 372 of file theory_core.h.
References d_incomplete, and CVCL::CDMap< Key, Data, HashFcn >::size().

bool CVCL::TheoryCore::incomplete ( std::vector< std::string > & reasons )

Check if the branch is incomplete, and return the reasons (strings).

Theorem CVCL::TheoryCore::rewriteLiteral ( const Expr & e )

Called by search engine.

Referenced by CVCL::SearchImplBase::replaceITE().

Expr CVCL::TheoryCore::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 from CVCL::Theory.
Referenced by TheoryCore::parseExpr(), CVCL::Theory::parseExpr(), TheoryCore::parseExprOp(), parseExprTop(), and TheoryCore::processCond().

Expr CVCL::TheoryCore::parseExprTop ( const Expr & e ) [inline]

Top-level call to parseExpr, clears the bound variable stack.
Use it in VCL instead of parseExpr().
Definition at line 387 of file theory_core.h.
References d_boundVarStack, and parseExpr().

void CVCL::TheoryCore::assignValue ( const Expr & t,

const Expr & val

) [virtual]

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

Reimplemented from CVCL::Theory.
Referenced by CVCL::Theory::assignValue(), TheoryCore::buildModel(), TheoryCore::collectModelValues(), and TheoryCore::computeModelBasic().

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

Record a derived assignment to a variable (LHS).

Reimplemented from CVCL::Theory.

void CVCL::TheoryCore::addToVarDB ( const Expr & e )

Adds expression to var database.

Referenced by CVCL::TheoryArray::renameExpr().

void CVCL::TheoryCore::collectBasicVars ( )

Split compound vars into basic type variables.
The results are saved in d_basicModelVars and d_simplifiedModelVars. Also, add new basic vars as shared terms whenever their type belongs to a different theory than the term itself.
Referenced by CVCL::SearchEngine::getConcreteModel().

void CVCL::TheoryCore::buildModel ( ExprMap< Expr > & m )

Calls theory specific computeModel, results are placed in map.

Referenced by CVCL::SearchEngine::getConcreteModel().

void CVCL::TheoryCore::collectModelValues ( const Expr & e,

ExprMap< Expr > & m

)

Recursively build a compound-type variable assignment for e.

Referenced by TheoryCore::buildModel(), and TheoryCore::collectModelValues().

Theorem CVCL::TheoryCore::typePred ( const Expr & e )

Return BOOLEAN type.

Reimplemented from CVCL::Theory.
Referenced by CVCL::Theory::typePred().

Theorem CVCL::TheoryCore::subtypePredicate ( const Expr & e )

Compute and cache the subtyping predicates for the expression.
Note: e caches the conjunction of all predicates for its subexpressions. So, when doing a look-up, it is sufficient to assert just the predicate for the top-level e, without traversing e recursively.
Reimplemented from CVCL::Theory.
Referenced by TheoryCore::subtypePredicate(), and CVCL::Theory::subtypePredicate().

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

Enqueue a new fact.

Reimplemented from CVCL::Theory.
Referenced by CVCL::SearchImplBase::addCNFFact(), TheoryCore::addFact(), CVCL::SearchEngineFast::addNonLiteralFact(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::SearchEngineFast::commitFacts(), and CVCL::Theory::enqueueFact().

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

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

Reimplemented from CVCL::Theory.
Referenced by TheoryCore::assertFactCore(), TheoryCore::assertFormula(), TheoryCore::checkSat(), TheoryCore::enqueueFact(), TheoryCore::processEquality(), CVCL::Theory::setInconsistent(), CVCL::SearchEngineFast::setInconsistent(), and TheoryCore::setupTerm().

void CVCL::TheoryCore::setupTerm ( const Expr & e,

Theory * i

)

Setup additional terms within a theory-specific setup().

Referenced by TheoryCore::assertFormula(), CVCL::TheoryArray::setup(), CVCL::TheoryBitvector::setupExpr(), TheoryCore::setupSubFormulas(), TheoryCore::setupTerm(), and CVCL::TheoryBitvector::update().

void CVCL::TheoryCore::enqueueEquality ( const Theorem & e ) [private, virtual]

Enqueue a new equality.

Reimplemented from CVCL::Theory.
Referenced by TheoryCore::assertEqualities(), and CVCL::Theory::enqueueEquality().

void CVCL::TheoryCore::assertEqualities ( const Theorem & e ) [private, virtual]

Assert a system of equations (1 or more).
e is either a single equation, or a conjunction of equations
Reimplemented from CVCL::Theory.
Referenced by CVCL::Theory::assertEqualities(), and TheoryCore::assertFactCore().

void CVCL::TheoryCore::setIncomplete ( const std::string & reason ) [private, virtual]

Mark the branch as incomplete.

Reimplemented from CVCL::Theory.
Referenced by TheoryCore::enqueueFact().

void CVCL::TheoryCore::processFactQueue ( ) [private]

A helper function for addFact().

Referenced by TheoryCore::addFact(), TheoryCore::checkSATCore(), and TheoryCore::setupSubFormulas().

void CVCL::TheoryCore::processNotify ( const Theorem & e,

NotifyList * L

) [private]

Process a notify list triggered as a result of new theorem e.

Referenced by TheoryCore::assertEqualities(), and TheoryCore::assertFormula().

Theorem CVCL::TheoryCore::simplifyRec ( const Expr & e ) [private, virtual]

The recursive simplifier (to be used only in DP-specific simplifyOp()).

Reimplemented from CVCL::Theory.
Referenced by TheoryCore::rewrite(), TheoryCore::simplify(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), TheoryCore::simplifyOp(), and CVCL::Theory::simplifyRec().

Theorem CVCL::TheoryCore::simplifyFullRec ( const Expr & e ) [private]

The full recursive simplifier.

Referenced by TheoryCore::simplify().

Theorem CVCL::TheoryCore::simplifyInPlaceRec ( const Expr & e ) [private]

The recursive simplifier with the in-place rewriting optimization.

Referenced by TheoryCore::simplify(), and TheoryCore::simplifyInPlaceRec().

Theorem CVCL::TheoryCore::rewriteCore ( const Theorem & e ) [private]

Transitive composition of other rewrites with the above.

Referenced by TheoryCore::rewrite(), TheoryCore::rewriteCore(), TheoryCore::simplifyFullRec(), and TheoryCore::simplifyInPlaceRec().

void CVCL::TheoryCore::setupSubFormulas ( const Expr & s,

const Expr & e

) [private]

Helper for registerAtom.

Referenced by TheoryCore::registerAtom(), and TheoryCore::setupSubFormulas().

void CVCL::TheoryCore::processUpdates ( ) [private]

Process updates recorded by calls to update().

Referenced by TheoryCore::assertEqualities(), and TheoryCore::assertFactCore().

void CVCL::TheoryCore::assertFactCore ( const Theorem & e ) [private]

The assumptions for e must be in H or phi. "Core" added to avoid conflict with theory interface function name.

Referenced by TheoryCore::assertFactCore(), and TheoryCore::processFactQueue().

void CVCL::TheoryCore::assertFormula ( const Theorem & e ) [private]

Process a newly derived formula.

Referenced by TheoryCore::assertEqualities(), and TheoryCore::assertFactCore().

Theorem CVCL::TheoryCore::rewriteCore ( const Expr & e ) [private]

Returns phi |= e = rewriteCore(e). "Core" added to avoid conflict with theory interface function name.

Theorem3 CVCL::TheoryCore::queryTCC ( const Theorem & phi,

const Theorem & D_phi

)

Theorem3 CVCL::TheoryCore::implIntro3 ( const Theorem3 & phi,

const std::vector< Expr > & assump,

const std::vector< Theorem > & tccs

)

Referenced by CVCL::VCL::deriveClosure().

Friends And Related Function Documentation

friend class Theory [friend]

Definition at line 55 of file theory_core.h.

friend class CoreNotifyObj [friend]

So we get notified every time there's a pop.

Definition at line 165 of file theory_core.h.

Member Data Documentation

ContextManager* CVCL::TheoryCore::d_cm [private]

Context manager.

Definition at line 58 of file theory_core.h.
Referenced by TheoryCore::enqueueEquality(), TheoryCore::enqueueFact(), and getCM().

TheoremManager* CVCL::TheoryCore::d_tm [private]

Theorem manager.

Definition at line 61 of file theory_core.h.
Referenced by getTM().

CoreProofRules* CVCL::TheoryCore::d_rules [private]

Core proof rules.

Definition at line 64 of file theory_core.h.
Referenced by getCoreRules(), TheoryCore::implIntro3(), TheoryCore::queryTCC(), TheoryCore::rewrite(), TheoryCore::rewriteIte(), TheoryCore::setupTerm(), TheoryCore::simplifyOp(), TheoryCore::subtypePredicate(), TheoryCore::typePred(), and TheoryCore::~TheoryCore().

const CLFlags& CVCL::TheoryCore::d_flags [private]

Reference to command line flags.

Definition at line 67 of file theory_core.h.
Referenced by getFlags().

Statistics& CVCL::TheoryCore::d_statistics [private]

Reference to statistics.

Definition at line 70 of file theory_core.h.
Referenced by getStatistics().

PrettyPrinter* CVCL::TheoryCore::d_printer [private]

PrettyPrinter (we own it).

Definition at line 73 of file theory_core.h.
Referenced by TheoryCore::~TheoryCore().

ExprManager::TypeComputer* CVCL::TheoryCore::d_typeComputer [private]

Type Computer.

Definition at line 76 of file theory_core.h.
Referenced by TheoryCore::~TheoryCore().

ExprTransform* CVCL::TheoryCore::d_exprTrans [private]

Expr Transformer.

Definition at line 79 of file theory_core.h.
Referenced by getExprTrans(), TheoryCore::simplifyOp(), and TheoryCore::~TheoryCore().

std::queue<Theorem> CVCL::TheoryCore::d_queue [private]

Assertion queue.

Definition at line 82 of file theory_core.h.
Referenced by TheoryCore::addFact(), TheoryCore::checkSATCore(), TheoryCore::enqueueFact(), and TheoryCore::processFactQueue().

std::vector<Theorem> CVCL::TheoryCore::d_queueSE [private]

Queue of facts to be sent to the SearchEngine.

Definition at line 84 of file theory_core.h.
Referenced by TheoryCore::addFact(), TheoryCore::checkSATCore(), TheoryCore::processFactQueue(), and TheoryCore::setInconsistent().

std::vector<Theorem> CVCL::TheoryCore::d_equalityQueue [private]

Equality queue.
Contains Theorems in the form of e1==e2, where e2 is i-leaf simplified in the current context.

See also:
enqueueEquality().

Definition at line 93 of file theory_core.h.
Referenced by TheoryCore::assertEqualities(), and TheoryCore::enqueueEquality().

CDO<bool> CVCL::TheoryCore::d_inconsistent [private]

Inconsistent flag.

Definition at line 96 of file theory_core.h.
Referenced by TheoryCore::addFact(), TheoryCore::checkSATCore(), inconsistent(), TheoryCore::processFactQueue(), and TheoryCore::setInconsistent().

CDMap<std::string, bool> CVCL::TheoryCore::d_incomplete [private]

The set of reasons for incompleteness (empty when we are complete).

Definition at line 98 of file theory_core.h.
Referenced by incomplete(), TheoryCore::incomplete(), and TheoryCore::setIncomplete().

CDList<Theorem> CVCL::TheoryCore::d_diseq [private]

List of known disequalities (to be processed at every checkSat() call).

Definition at line 100 of file theory_core.h.
Referenced by TheoryCore::assertFormula(), and TheoryCore::checkSat().

CDO<Theorem> CVCL::TheoryCore::d_incThm [private]

Proof of inconsistent.

Definition at line 103 of file theory_core.h.
Referenced by inconsistentThm(), and TheoryCore::setInconsistent().

CDList<Expr> CVCL::TheoryCore::d_terms [private]

List of all active terms in the system (for quantifier instantiation).

Definition at line 105 of file theory_core.h.
Referenced by getTerms(), and TheoryCore::setupTerm().

CDList<Expr> CVCL::TheoryCore::d_vars [private]

List of variables that were created up to this point.

Definition at line 107 of file theory_core.h.
Referenced by TheoryCore::addToVarDB(), TheoryCore::buildModel(), and TheoryCore::collectBasicVars().

std::map<std::string, Expr> CVCL::TheoryCore::d_globals [private]

Database of declared identifiers.

Definition at line 109 of file theory_core.h.

std::vector<std::pair<std::string, Expr> > CVCL::TheoryCore::d_boundVarStack [private]

Bound variable stack: a vector of pairs <name, var>.

Definition at line 111 of file theory_core.h.
Referenced by TheoryCore::parseExpr(), and parseExprTop().

CDMap<Expr, Theory*> CVCL::TheoryCore::d_sharedTerms [private]

List of all terms that are shared between theories (alien subterms).
Maps each shared term to its own theory.
Definition at line 115 of file theory_core.h.
Referenced by TheoryCore::collectBasicVars(), and TheoryCore::setupTerm().

std::map<Expr, bool> CVCL::TheoryCore::d_typePredAsserted [private]

Definition at line 117 of file theory_core.h.
Referenced by TheoryCore::setupTerm().

std::vector<Theory*> CVCL::TheoryCore::d_theories [private]

Array of registered theories.

Definition at line 120 of file theory_core.h.
Referenced by TheoryCore::buildModel(), TheoryCore::checkSATCore(), CVCL::Theory::getNumTheories(), TheoryCore::processFactQueue(), TheoryCore::refineCounterExample(), and TheoryCore::setInconsistent().

std::map<int, Theory*> CVCL::TheoryCore::d_theoryMap [private]

Array mapping kinds to theories.

Definition at line 123 of file theory_core.h.
Referenced by CVCL::Theory::hasTheory(), and CVCL::Theory::theoryOf().

Theory* CVCL::TheoryCore::d_solver [private]

The theory which has the solver (if any).

Definition at line 126 of file theory_core.h.
Referenced by TheoryCore::solve().

ExprHashMap<std::vector<Expr> > CVCL::TheoryCore::d_varModelMap [private]

Mapping of compound type variables to simpler types (model generation).

Definition at line 129 of file theory_core.h.
Referenced by TheoryCore::collectBasicVars(), and TheoryCore::collectModelValues().

ExprHashMap<Theorem> CVCL::TheoryCore::d_varAssignments [private]

Mapping of intermediate variables to their valies.

Definition at line 131 of file theory_core.h.
Referenced by TheoryCore::assignValue(), TheoryCore::buildModel(), TheoryCore::collectBasicVars(), and TheoryCore::collectModelValues().

std::vector<Expr> CVCL::TheoryCore::d_basicModelVars [private]

List of basic variables (temporary storage for model generation).

Definition at line 133 of file theory_core.h.
Referenced by TheoryCore::buildModel(), and TheoryCore::collectBasicVars().

ExprHashMap<Theorem> CVCL::TheoryCore::d_simplifiedModelVars [private]

Mapping of basic variables to simplified expressions (temp. storage).
There may be some vars which simplify to something else; we save those separately, and keep only those which simplify to themselves. Once the latter vars are assigned, we'll re-simplify the former variables and use the results as concrete values.
Definition at line 140 of file theory_core.h.
Referenced by TheoryCore::buildModel(), TheoryCore::collectBasicVars(), and TheoryCore::collectModelValues().

const bool* CVCL::TheoryCore::d_simplifyInPlace [private]

Command line flag whether to simplify in place.

Definition at line 143 of file theory_core.h.
Referenced by TheoryCore::simplify(), and TheoryCore::simplifyFullRec().

Theorem(TheoryCore::* CVCL::TheoryCore::d_currentRecursiveSimplifier)(const Expr &) [private]

Which recursive simplifier to use.

Referenced by TheoryCore::simplify(), and TheoryCore::simplifyRec().

const bool* CVCL::TheoryCore::d_cnfOption [private]

Command line flag whether to convert to CNF.

Definition at line 148 of file theory_core.h.

unsigned CVCL::TheoryCore::d_resourceLimit [private]

Resource limit (0==unlimited, 1==no more resources, >=2 - available).
Currently, it is the number of enqueued facts. Once the resource is exhausted, the remaining facts will be dropped, and an incomplete flag is set.
Definition at line 155 of file theory_core.h.
Referenced by TheoryCore::getResource(), and TheoryCore::setResourceLimit().

CoreNotifyObj CVCL::TheoryCore::d_notifyObj [private]

Definition at line 173 of file theory_core.h.

size_t CVCL::TheoryCore::d_equivCheckMMidx [private]

Memory Manager index for equiv. check Expr.

Definition at line 178 of file theory_core.h.

CDList<Theorem> CVCL::TheoryCore::d_impliedLiterals [private]

List of implied literals, based on registered atomic formulas of interest.

Definition at line 181 of file theory_core.h.
Referenced by TheoryCore::getImpliedLiteral(), TheoryCore::getImpliedLiteralByIndex(), numImpliedLiterals(), TheoryCore::processUpdates(), and TheoryCore::registerAtom().

CDO<unsigned> CVCL::TheoryCore::d_impliedLiteralsIdx [private]

Next index in d_impliedLiterals that has not yet been fetched.

Definition at line 184 of file theory_core.h.
Referenced by TheoryCore::getImpliedLiteral().