CVCL::TheoryCore Class Reference

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:

Inheritance graph
Collaboration diagram for CVCL::TheoryCore:

Collaboration graph
List of all members.

Public Member Functions

Private Member Functions

Private Attributes



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


CVCL::TheoryCore::~TheoryCore  ) 


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.

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

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

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

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

Expr CVCL::TheoryCore::processCond const Expr e,
int  i

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.

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.

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:

Reimplemented from CVCL::Theory.

void CVCL::TheoryCore::update const Theorem e,
const Expr d

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:

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.

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.

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

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

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.


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:

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

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.

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

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

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

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:

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

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

List of theorems from calls to update().

Definition at line 189 of file theory_core.h.

Referenced by TheoryCore::addFact(), TheoryCore::processUpdates(), and TheoryCore::update().

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

List of data accompanying above theorems from calls to update().

Definition at line 192 of file theory_core.h.

Referenced by TheoryCore::addFact(), TheoryCore::processUpdates(), and TheoryCore::update().

CoreSatAPI* CVCL::TheoryCore::d_coreSatAPI [private]

Definition at line 225 of file theory_core.h.

Referenced by CVCL::Theory::addSplitter(), TheoryCore::assignValue(), TheoryCore::processFactQueue(), and registerCoreSatAPI().

bool CVCL::TheoryCore::notifySAT [private]

Definition at line 241 of file theory_core.h.

The documentation for this class was generated from the following file:
Generated on Thu Apr 13 16:57:44 2006 for CVC Lite by  doxygen 1.4.4