CVC3
Classes | Public Member Functions | Private Types | Private Member Functions | Private Attributes | Friends

CVC3::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>

Inherits CVC3::Theory.

Collaboration diagram for CVC3::TheoryCore:
Collaboration graph
[legend]

List of all members.

Classes

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Friends


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 53 of file theory_core.h.


Member Enumeration Documentation

Effort level for processFactQueue.

LOW means just process facts, don't call theory checkSat methods NORMAL means call theory checkSat methods without full effort FULL means call theory checkSat methods with full effort

Enumerator:
LOW 
NORMAL 
FULL 

Definition at line 258 of file theory_core.h.


Constructor & Destructor Documentation

TheoryCore::TheoryCore ( ContextManager cm,
ExprManager em,
TheoremManager tm,
Translator tr,
const CLFlags flags,
Statistics statistics 
)
TheoryCore::~TheoryCore ( )

Member Function Documentation

CoreProofRules * 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). Method is implemented in core_theorem_producer.cpp

Definition at line 45 of file core_theorem_producer.cpp.

Referenced by TheoryCore().

bool TheoryCore::processFactQueue ( EffortLevel  effort = NORMAL) [private]

A helper function for addFact()

Returns true if lemmas were added to search engine, false otherwise

Definition at line 121 of file theory_core.cpp.

Referenced by addFact(), callTheoryPreprocess(), checkSATCore(), and registerAtom().

void TheoryCore::processNotify ( const Theorem e,
NotifyList L 
) [private]

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

Definition at line 173 of file theory_core.cpp.

References DebugAssert, CVC3::NotifyList::getExpr(), CVC3::NotifyList::getTheory(), CVC3::NotifyList::size(), and CVC3::Theory::update().

Referenced by assertEqualities().

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

Transitive composition of other rewrites with the above.

Definition at line 257 of file theory_core.cpp.

References DebugAssert, CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), and CVC3::Theorem::toString().

Referenced by rewrite().

void TheoryCore::setupSubFormulas ( const Expr s,
const Expr e,
const Theorem thm 
) [private]

Helper for registerAtom.

Definition at line 269 of file theory_core.cpp.

References CVC3::Expr::addToNotify(), CVC3::Expr::arity(), CVC3::Expr::isAbsAtomicFormula(), and CVC3::Expr::isAtomic().

Referenced by registerAtom().

void TheoryCore::processUpdates ( ) [private]
void TheoryCore::assertFactCore ( const Theorem e) [private]
void TheoryCore::assertFormula ( const Theorem e) [private]
Theorem CVC3::TheoryCore::rewriteCore ( const Expr e) [private]

Check that lhs and rhs of thm have same base type.

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

Definition at line 455 of file theory_core.cpp.

References CVC3::Expr::clearRewriteNormal(), DebugAssert, EQ, CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isEq(), CVC3::Theorem::isRefl(), CVC3::Expr::isRewriteNormal(), NOT, CVC3::Expr::setRewriteNormal(), and CVC3::Expr::toString().

void TheoryCore::setFindLiteral ( const Theorem thm) [private]

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

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

Definition at line 509 of file theory_core.cpp.

References DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getNotify(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isFalse(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isNot(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isTrue(), CVC3::PRESENTATION_LANG, CVC3::Expr::setFind(), CVC3::Expr::setImpliedLiteral(), CVC3::Expr::toString(), and TRACE.

Referenced by registerAtom(), and update().

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

Core rewrites for literals (NOT and EQ)

Definition at line 560 of file theory_core.cpp.

References DebugAssert, EQ, CVC3::Expr::getKind(), NOT, and CVC3::Expr::toString().

Referenced by rewrite().

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

Enqueue a fact to be sent to the SearchEngine.

Fetch the concrete assignment to the variable during model generation

Reimplemented from CVC3::Theory.

Definition at line 595 of file theory_core.cpp.

References CVC3::ExprHashMap< Data >::find().

Referenced by collectModelValues(), and CVC3::Theory::getModelValue().

Expr TheoryCore::processCond ( const Expr e,
int  i 
) [private]

An auxiliary recursive function to process COND expressions into ITE.

Definition at line 605 of file theory_core.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::Expr::getKind(), CVC3::Expr::getString(), ID, CVC3::int2string(), CVC3::Expr::iteExpr(), RAW_LIST, and CVC3::Expr::toString().

Referenced by parseExprOp().

bool TheoryCore::isBasicKind ( int  kind) [private]
void TheoryCore::checkEquation ( const Theorem thm) [private]

Helper check functions for solve.

Definition at line 1195 of file theory_core.cpp.

References d_solver, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::isEq(), CVC3::Theory::solve(), CVC3::Theory::theoryOf(), and CVC3::Expr::toString().

Referenced by checkSolved().

void TheoryCore::checkSolved ( const Theorem thm) [private]
bool TheoryCore::timeLimitReached ( ) [private]

Definition at line 4062 of file theory_core.cpp.

References d_timeBase, d_timeLimit, and setIncomplete().

ExprStream & TheoryCore::printSmtLibShared ( ExprStream os,
const Expr e 
) [private]
void CVC3::TheoryCore::getResource ( ) [inline]

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.

Definition at line 334 of file theory_core.h.

References CVC3::Statistics::counter(), d_resourceLimit, and getStatistics().

Referenced by addFact(), and enqueueFact().

void CVC3::TheoryCore::registerCoreSatAPI ( CoreSatAPI coreSatAPI) [inline]

Register a SatAPI for TheoryCore.

Definition at line 340 of file theory_core.h.

References d_coreSatAPI.

Referenced by CVC3::SearchImplBase::SearchImplBase(), and CVC3::SearchSat::SearchSat().

void CVC3::TheoryCore::addNotifyEq ( Theory t,
const Expr e 
) [inline]

Register a callback for every equality.

Definition at line 343 of file theory_core.h.

References CVC3::NotifyList::add(), and d_notifyEq.

Referenced by CVC3::TheoryQuant::TheoryQuant().

Theorem TheoryCore::callTheoryPreprocess ( const Expr e)
ContextManager* CVC3::TheoryCore::getCM ( ) const [inline]
TheoremManager* CVC3::TheoryCore::getTM ( ) const [inline]
const CLFlags& CVC3::TheoryCore::getFlags ( ) const [inline]
Statistics& CVC3::TheoryCore::getStatistics ( ) const [inline]
ExprTransform* CVC3::TheoryCore::getExprTrans ( ) const [inline]
CoreProofRules* CVC3::TheoryCore::getCoreRules ( ) const [inline]

Definition at line 353 of file theory_core.h.

References d_rules.

Referenced by CVC3::ExprTransform::ExprTransform().

Translator* CVC3::TheoryCore::getTranslator ( ) const [inline]

Definition at line 354 of file theory_core.h.

References d_translator.

Referenced by CVC3::TheoryUF::printSmtLibShared().

ExprMap<Expr>& CVC3::TheoryCore::tccCache ( ) [inline]

Access to tcc cache (needed by theory_bitvector)

Definition at line 357 of file theory_core.h.

References d_tccCache.

Referenced by CVC3::TheoryBitvector::computeTCC().

const CDList<Expr>& CVC3::TheoryCore::getTerms ( ) [inline]
int CVC3::TheoryCore::getCurQuantLevel ( )
void CVC3::TheoryCore::setInPP ( ) [inline]

Set the flag for the preprocessor.

Definition at line 365 of file theory_core.h.

References d_inPP.

Referenced by CVC3::ExprTransform::preprocess().

void CVC3::TheoryCore::clearInPP ( ) [inline]

Definition at line 366 of file theory_core.h.

References d_inPP.

Referenced by CVC3::ExprTransform::preprocess().

Theorem TheoryCore::getTheoremForTerm ( const Expr e)

Get theorem which was responsible for introducing this term.

Definition at line 868 of file theory_core.cpp.

References d_termTheorems, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), and TRACE.

Referenced by getQuantLevelForTerm().

unsigned TheoryCore::getQuantLevelForTerm ( const Expr e)
const CDList<Expr>& CVC3::TheoryCore::getPredicates ( ) [inline]

Get list of predicates.

Definition at line 373 of file theory_core.h.

References d_predicates.

Referenced by CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::debug(), and CVC3::TheoryQuant::synCheckSat().

bool CVC3::TheoryCore::inUpdate ( ) [inline]

Whether updates are being processed.

Definition at line 375 of file theory_core.h.

References d_inUpdate.

bool CVC3::TheoryCore::okToEnqueue ( ) [inline]

Whether its OK to add new facts (for use in rewrites)

Definition at line 377 of file theory_core.h.

References d_inAddFact, d_inCheckSATCore, d_inPP, and d_inRegisterAtom.

Referenced by enqueueFact().

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

Variables of uninterpreted types may be sent here, and they should be ignored.

Reimplemented from CVC3::Theory.

Definition at line 383 of file theory_core.h.

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

Definition at line 960 of file theory_core.cpp.

References DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), SKOLEM_VAR, CVC3::Theorem::toString(), UCONST, and CVC3::Expr::unnegate().

void CVC3::TheoryCore::checkSat ( bool  fullEffort) [inline, virtual]

Check for satisfiability in the theory.

Parameters:
fullEffortwhen 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 CVC3::Theory.

Definition at line 385 of file theory_core.h.

Theorem 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 CVC3::Theory.

Definition at line 968 of file theory_core.cpp.

References AND, AND_R, APPLY, CVC3::Expr::arity(), BOUND_VAR, CVC3::Theory::d_commonRules, d_rules, DebugAssert, DISTINCT, EQ, EXISTS, FALSE_EXPR, CVC3::Theory::find(), FORALL, CVC3::Theorem::getExpr(), getFlags(), CVC3::Expr::getKind(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), IFF, IFF_R, IMPLIES, CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Theorem::isRefl(), CVC3::Expr::isTrue(), ITE, ITE_R, LAMBDA, LETDECL, NOT, OR, CVC3::CommonProofRules::reflexivityRule(), CVC3::Theory::reflexivityRule(), CVC3::Theory::rewrite(), CVC3::Theory::rewriteAnd(), CVC3::CoreProofRules::rewriteAndSubterms(), rewriteCore(), CVC3::CoreProofRules::rewriteDistinct(), CVC3::CommonProofRules::rewriteIff(), CVC3::CoreProofRules::rewriteImplies(), CVC3::Theory::rewriteIte(), CVC3::CoreProofRules::rewriteIteCond(), CVC3::CoreProofRules::rewriteIteToAnd(), CVC3::CoreProofRules::rewriteIteToIff(), CVC3::CoreProofRules::rewriteIteToImp(), CVC3::CoreProofRules::rewriteIteToNot(), CVC3::CoreProofRules::rewriteIteToOr(), CVC3::CoreProofRules::rewriteLetDecl(), rewriteLitCore(), CVC3::Theory::rewriteOr(), CVC3::CoreProofRules::rewriteOrSubterms(), CVC3::Expr::setRewriteNormal(), simplify(), SKOLEM_VAR, CVC3::Theory::substitutivityRule(), CVC3::Theory::theoryOf(), CVC3::Type::toString(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), TRUE_EXPR, UCONST, XOR, and CVC3::CommonProofRules::xorToIff().

void CVC3::TheoryCore::setup ( const Expr e) [inline, virtual]

Only Boolean constants (TRUE and FALSE) and variables of uninterpreted types should appear here (they come from records and tuples). Just ignore them.

Reimplemented from CVC3::Theory.

Definition at line 390 of file theory_core.h.

void TheoryCore::update ( const Theorem e,
const Expr d 
) [virtual]
Theorem TheoryCore::solve ( const Theorem eThm) [virtual]

Function: TheoryCore::solve

Author: Clark Barrett

Created: Wed Feb 26 16:17:54 2003

This is a generalization of what's in my thesis. The goal is to rewrite e into an equisatisfiable conjunction of equations such that the left-hand side of each equation is a variable which does not appear as an i-leaf of the rhs, where i is the theory of the primary solver. Any solution which satisfies this is fine. "Solvers" from other theories can do whatever they want as long as we eventually reach this form.

Reimplemented from CVC3::Theory.

Definition at line 1248 of file theory_core.cpp.

References checkSolved(), d_solver, DebugAssert, CVC3::Theory::getBaseType(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), IF_DEBUG, CVC3::Expr::isAnd(), CVC3::Expr::isBoolConst(), CVC3::Expr::isEq(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTerm(), CVC3::Theory::solve(), and CVC3::Theory::theoryOf().

Theorem 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 CVC3::Theory.

Definition at line 1292 of file theory_core.cpp.

References AND, CVC3::Expr::arity(), CVC3::Theory::d_commonRules, d_rules, DebugAssert, EQ, FALSE_EXPR, CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), IF_DEBUG, IFF, CVC3::CommonProofRules::iffTrue(), IMPLIES, CVC3::Expr::isBoolConst(), CVC3::Expr::isFalse(), CVC3::Theorem::isRefl(), CVC3::Expr::isTrue(), ITE, NOT, OR, CVC3::Theory::reflexivityRule(), CVC3::Theory::rewriteAnd(), CVC3::CoreProofRules::rewriteImplies(), CVC3::CommonProofRules::rewriteIteSame(), CVC3::Theory::rewriteOr(), simplify(), CVC3::CommonProofRules::substitutivityRule(), CVC3::Theory::substitutivityRule(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), and TRUE_EXPR.

void TheoryCore::checkType ( const Expr e) [virtual]
Cardinality TheoryCore::finiteTypeInfo ( Expr e,
Unsigned n,
bool  enumerate,
bool  computeSize 
) [virtual]

Compute information related to finiteness of types.

Used by the TypeComputer defined in TheoryCore (theories should not call this funtion directly -- they should use the methods in Type instead). Each theory should implement this if it contains any types that could be non-infinite.

1. Returns Cardinality of the type (finite, infinite, or unknown) 2. If cardinality = finite and enumerate is true, sets e to the nth element of the type if it can sets e to NULL if n is out of bounds or if unable to compute nth element 3. If cardinality = finite and computeSize is true, sets n to the size of the type if it can sets n to 0 otherwise

Reimplemented from CVC3::Theory.

Definition at line 1443 of file theory_core.cpp.

References ANY_TYPE, BOOLEAN, CVC3::CARD_FINITE, CVC3::CARD_INFINITE, CVC3::CARD_UNKNOWN, CVC3::Theory::falseExpr(), FatalAssert, CVC3::Theory::getEM(), CVC3::Expr::getKind(), SUBTYPE, and CVC3::Theory::trueExpr().

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

Compute and store the type of e.

Parameters:
eis 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 CVC3::Theory.

Definition at line 1471 of file theory_core.cpp.

References AND, AND_R, CVC3::Type::anyType(), APPLY, CVC3::Type::arity(), CVC3::Expr::arity(), CVC3::Theory::boolType(), CVC3::Theory::d_em, DebugAssert, DISTINCT, EQ, CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOpExpr(), IFF, IFF_R, IMPLIES, CVC3::int2string(), CVC3::Expr::isApply(), CVC3::Type::isBool(), CVC3::Type::isFunction(), ITE, ITE_R, LETDECL, NOT, OR, RAW_LIST, CVC3::Expr::setType(), CVC3::Type::toString(), CVC3::Expr::toString(), and XOR.

Type TheoryCore::computeBaseType ( const Type tp) [virtual]
Expr TheoryCore::computeTCC ( const Expr e) [virtual]

Compute and cache the TCC of e.

Parameters:
eis 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 CVC3::Theory.

Definition at line 1650 of file theory_core.cpp.

References AND, CVC3::andExpr(), APPLY, CVC3::Expr::begin(), CVC3::Theory::computeTCC(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Theory::getTCC(), IMPLIES, ITE, NOT, OR, CVC3::orExpr(), CVC3::Theory::rewriteAnd(), CVC3::Theory::rewriteOr(), and CVC3::Theory::theoryOf().

Expr 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 CVC3::Theory.

Definition at line 1704 of file theory_core.cpp.

References CVC3::andExpr(), APPLY, CVC3::Theory::computeTypePred(), CVC3::Expr::getEM(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Theory::getTypePred(), CVC3::Expr::lookupType(), CVC3::Expr::mkOp(), SUBTYPE, CVC3::Theory::theoryOf(), and CVC3::ExprManager::trueExpr().

Expr TheoryCore::parseExprOp ( const Expr e) [virtual]
ExprStream & 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 CVC3::Theory.

Definition at line 2055 of file theory_core.cpp.

References AND, ANNOTATION, ANY_TYPE, ARITH_VAR_ORDER, CVC3::Expr::arity(), ARROW, ASSERT, ASSERTIONS, ASSUMPTIONS, CVC3::Expr::begin(), BOOLEAN, BOUND_VAR, CVC3::ExprHashMap< Data >::clear(), CONST, contains(), COUNTEREXAMPLE, COUNTERMODEL, CVC3::Theory::d_em, d_translator, DebugAssert, DISTINCT, CVC3::Expr::end(), std::endl(), EQ, CVC3::Translator::escapeSymbol(), FALSE_EXPR, CVC3::Theory::falseExpr(), CVC3::ExprManager::falseExpr(), CVC3::Translator::fixConstName(), CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Type::getExpr(), getFlags(), CVC3::Expr::getIndex(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::Expr::getString(), CVC3::Expr::getType(), ID, IFF, IMPLIES, CVC3::int2string(), CVC3::Type::isBool(), CVC3::Type::isNull(), CVC3::isReal(), CVC3::Expr::isString(), ITE, CVC3::ExprStream::lang(), LET, LETDECL, CVC3::LISP_LANG, CVC3::Expr::negate(), CVC3::nodag(), NOT, CVC3::Expr::notExpr(), OR, PF_APPLY, PF_HOLE, CVC3::pop(), POP, POP_SCOPE, CVC3::popSave(), POPTO, POPTO_SCOPE, CVC3::PRESENTATION_LANG, CVC3::Expr::print(), CVC3::Expr::printAST(), printSmtLibShared(), PUSH, CVC3::push(), PUSH_SCOPE, CVC3::pushRestore(), QUERY, CVC3::Translator::quoteAnnotation(), RAW_LIST, RESET, CVC3::SIMPLIFY_LANG, SKOLEM_VAR, CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, CVC3::space(), CVC3::SPASS_LANG, STRING_EXPR, SUBTYPE, CVC3::to_lower(), CVC3::to_upper(), CVC3::Expr::toString(), CVC3::TPTP_LANG, TRANSFORM, TRUE_EXPR, CVC3::Theory::trueExpr(), CVC3::ExprManager::trueExpr(), TYPE, TYPEDEF, UCONST, WHERE, and XOR.

void TheoryCore::refineCounterExample ( ) [virtual]
bool TheoryCore::refineCounterExample ( Theorem thm)
void TheoryCore::computeModelBasic ( const std::vector< Expr > &  v) [virtual]

Assign concrete values to basic-type variables in v.

Reimplemented from CVC3::Theory.

Definition at line 3449 of file theory_core.cpp.

References assignValue(), CVC3::Theory::d_em, DebugAssert, CVC3::Theory::find(), CVC3::Theorem::getRHS(), TRACE, and CVC3::ExprManager::trueExpr().

void TheoryCore::addFact ( const Theorem e)
Theorem TheoryCore::simplify ( const Expr e) [virtual]
bool CVC3::TheoryCore::inconsistent ( ) [inline, virtual]

Check if the current context is inconsistent.

Reimplemented from CVC3::Theory.

Definition at line 422 of file theory_core.h.

References d_inconsistent.

Referenced by CVC3::SearchEngineFast::bcp(), buildModel(), CVC3::Theory::inconsistent(), refineCounterExample(), and CVC3::SearchEngineFast::split().

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

Get the proof of inconsistency for the current context.

Returns:
Theorem(FALSE)

Definition at line 425 of file theory_core.h.

References d_incThm.

Referenced by CVC3::SearchEngineFast::bcp(), buildModel(), CVC3::SearchEngine::getConcreteModel(), and refineCounterExample().

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

Definition at line 3507 of file theory_core.cpp.

References d_inCheckSATCore, d_queue, d_queueSE, d_update_data, d_update_thms, DebugAssert, FULL, IF_DEBUG, and processFactQueue().

Referenced by CVC3::SearchEngineFast::split().

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

Check if the current decision branch is marked as incomplete.

Definition at line 435 of file theory_core.h.

References d_incomplete, and CVC3::CDMap< Key, Data, HashFcn >::size().

Referenced by assertEqualities(), CVC3::SearchEngineFast::checkSAT(), and CVC3::SearchSimple::checkValidMain().

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

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

Definition at line 3528 of file theory_core.cpp.

References CVC3::CDMap< Key, Data, HashFcn >::begin(), d_incomplete, CVC3::CDMap< Key, Data, HashFcn >::end(), and CVC3::CDMap< Key, Data, HashFcn >::size().

void TheoryCore::registerAtom ( const Expr e,
const Theorem thm 
) [virtual]
Theorem TheoryCore::getImpliedLiteral ( void  )

Return the next implied literal (NULL Theorem if none)

Definition at line 3571 of file theory_core.cpp.

References d_impliedLiterals, d_impliedLiteralsIdx, and CVC3::CDList< T >::size().

Referenced by CVC3::SearchImplBase::getImpliedLiteral().

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

Return total number of implied literals.

Definition at line 448 of file theory_core.h.

References d_impliedLiterals, and CVC3::CDList< T >::size().

Theorem TheoryCore::getImpliedLiteralByIndex ( unsigned  index)

Return an implied literal by index.

Definition at line 3582 of file theory_core.cpp.

References d_impliedLiterals, DebugAssert, and CVC3::CDList< T >::size().

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

Expr TheoryCore::parseExpr ( const Expr e) [virtual]
Expr CVC3::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 461 of file theory_core.h.

References d_boundVarStack, d_parseCache, d_parseCacheTop, and parseExpr().

void TheoryCore::assignValue ( const Expr t,
const Expr val 
) [virtual]
void TheoryCore::assignValue ( const Theorem thm) [virtual]
void TheoryCore::addToVarDB ( const Expr e)

Adds expression to var database.

Definition at line 3756 of file theory_core.cpp.

References d_vars, and TRACE.

Referenced by CVC3::Theory::newFunction(), CVC3::Theory::newVar(), and CVC3::Theory::renameExpr().

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

Definition at line 3763 of file theory_core.cpp.

References CVC3::Theory::addSharedTerm(), CVC3::ExprHashMap< Data >::clear(), CVC3::ExprHashMap< Data >::count(), d_basicModelVars, d_simplifiedModelVars, d_varAssignments, d_varModelMap, d_vars, DebugAssert, CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::Theory::getModelTerm(), CVC3::Theorem::getRHS(), RAW_LIST, CVC3::Theory::theoryOf(), TRACE, and TRACE_MSG.

Referenced by CVC3::SearchEngine::getConcreteModel(), and CVC3::SearchEngine::tryModelGeneration().

void TheoryCore::buildModel ( ExprMap< Expr > &  m)
bool TheoryCore::buildModel ( Theorem thm)
void TheoryCore::collectModelValues ( const Expr e,
ExprMap< Expr > &  m 
)

Recursively build a compound-type variable assignment for e.

Not all theories may implement aggregation of compound values. If a compound variable is not assigned by a theory, add the more primitive variable assignments to 'm'.

Some variables may simplify to something else (simplifiedVars map). INVARIANT: e is always simplified (it's not in simplifiedVars map). Also, if v simplifies to e, and e is assigned, then v must be assigned.

Definition at line 3954 of file theory_core.cpp.

References assignValue(), CVC3::Theory::computeModel(), CVC3::ExprHashMap< Data >::count(), d_simplifiedModelVars, d_varAssignments, d_varModelMap, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), getModelValue(), CVC3::Theory::getName(), CVC3::Theorem::getRHS(), IF_DEBUG, RAW_LIST, CVC3::Theory::reflexivityRule(), CVC3::Theory::theoryOf(), TRACE, and CVC3::Theory::transitivityRule().

Referenced by buildModel().

void CVC3::TheoryCore::setResourceLimit ( unsigned  limit) [inline]

Set the resource limit (0==unlimited).

Definition at line 488 of file theory_core.h.

References d_resourceLimit.

unsigned CVC3::TheoryCore::getResourceLimit ( ) [inline]

Get the resource limit.

Definition at line 490 of file theory_core.h.

References d_resourceLimit.

bool CVC3::TheoryCore::outOfResources ( ) [inline]

Return true if resources are exhausted.

Definition at line 492 of file theory_core.h.

References d_resourceLimit.

Referenced by addFact(), CVC3::SearchEngineFast::checkSAT(), and enqueueFact().

void TheoryCore::initTimeLimit ( )

Initialize base time used for !setTimeLimit.

Definition at line 4058 of file theory_core.cpp.

References d_timeBase.

Referenced by setTimeLimit().

void TheoryCore::setTimeLimit ( unsigned  limit)

Set the time limit in seconds (0==unlimited).

Definition at line 4053 of file theory_core.cpp.

References d_timeLimit, and initTimeLimit().

Theorem TheoryCore::rewriteLiteral ( const Expr e)
Expr TheoryCore::getAssignment ( )
Expr TheoryCore::getValue ( Expr  e)

Get the value of an arbitrary formula or term.

Definition at line 4333 of file theory_core.cpp.

References d_exprTrans, CVC3::Theory::d_theoryCore, CVC3::Theorem::getRHS(), CVC3::ExprTransform::preprocess(), and simplify().

void 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

Invariants:

  • The input theorem e is either an equality or a conjunction of equalities;
  • In each equality e1=e2, the RHS e2 i-leaf-simplified;
  • At the time of calling update(), all equalities in the queue are processed by assertFormula() and the equivalence classes are merged in the union-find database.

In other words, the entire equality queue is processed "in parallel".

Reimplemented from CVC3::Theory.

Definition at line 4093 of file theory_core.cpp.

References CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), assertFormula(), CVC3::Theory::checkAssertEqInvariant(), CVC3::Theory::d_commonRules, CVC3::Theory::d_em, d_inconsistent, d_notifyEq, d_solver, DebugAssert, CVC3::Theory::find(), CVC3::Theory::findReduced(), getCM(), CVC3::Expr::getEqNext(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getNotify(), CVC3::Theorem::getRHS(), IF_DEBUG, incomplete(), CVC3::ExprManager::invalidateSimpCache(), CVC3::Expr::isAnd(), CVC3::Expr::isFalse(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTerm(), processNotify(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), setInconsistent(), CVC3::Theory::symmetryRule(), CVC3::Expr::toString(), TRACE, and CVC3::Theory::transitivityRule().

Referenced by CVC3::Theory::assertEqualities().

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

Mark the branch as incomplete.

Reimplemented from CVC3::Theory.

Definition at line 4180 of file theory_core.cpp.

References d_incomplete, and CVC3::CDMap< Key, Data, HashFcn >::insert().

Referenced by addFact(), enqueueFact(), CVC3::Theory::setIncomplete(), and timeLimitReached().

Theorem TheoryCore::typePred ( const Expr e) [private]

Return a theorem for the type predicate of e.

Note: used only by theory_arith

Reimplemented from CVC3::Theory.

Definition at line 4186 of file theory_core.cpp.

References d_rules, and CVC3::CoreProofRules::typePred().

Referenced by CVC3::Theory::typePred().

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

Check if the current context is inconsistent.

Reimplemented from CVC3::Theory.

Definition at line 588 of file theory_core.cpp.

References DebugAssert.

Referenced by CVC3::Theory::enqueueSE().

void TheoryCore::setInconsistent ( const Theorem e) [virtual]
void TheoryCore::setupTerm ( const Expr e,
Theory i,
const Theorem thm 
)

Friends And Related Function Documentation

friend class Theory [friend]

Definition at line 54 of file theory_core.h.

friend class CoreNotifyObj [friend]

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

Definition at line 175 of file theory_core.h.


Member Data Documentation

Context manager.

Definition at line 57 of file theory_core.h.

Referenced by enqueueFact(), and getCM().

Theorem manager.

Definition at line 60 of file theory_core.h.

Referenced by getTM().

Core proof rules.

Definition at line 63 of file theory_core.h.

Referenced by getCoreRules(), rewrite(), setupTerm(), simplifyOp(), TheoryCore(), typePred(), and ~TheoryCore().

Reference to command line flags.

Definition at line 66 of file theory_core.h.

Referenced by getFlags().

Reference to statistics.

Definition at line 69 of file theory_core.h.

Referenced by getStatistics().

PrettyPrinter (we own it)

Definition at line 72 of file theory_core.h.

Referenced by TheoryCore(), and ~TheoryCore().

Type Computer.

Definition at line 75 of file theory_core.h.

Referenced by TheoryCore(), and ~TheoryCore().

Expr Transformer.

Definition at line 78 of file theory_core.h.

Referenced by getAssignment(), getExprTrans(), getValue(), TheoryCore(), and ~TheoryCore().

Translator.

Definition at line 81 of file theory_core.h.

Referenced by getTranslator(), print(), and printSmtLibShared().

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

Assertion queue.

Definition at line 84 of file theory_core.h.

Referenced by addFact(), checkSATCore(), and enqueueFact().

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

Queue of facts to be sent to the SearchEngine.

Definition at line 86 of file theory_core.h.

Referenced by addFact(), checkSATCore(), and setInconsistent().

Inconsistent flag.

Definition at line 89 of file theory_core.h.

Referenced by addFact(), assertEqualities(), enqueueFact(), inconsistent(), and setInconsistent().

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

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

Definition at line 91 of file theory_core.h.

Referenced by incomplete(), and setIncomplete().

Proof of inconsistent.

Definition at line 94 of file theory_core.h.

Referenced by inconsistentThm(), and setInconsistent().

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

Definition at line 96 of file theory_core.h.

Referenced by getTerms(), and setupTerm().

Map from active terms to theorems that introduced those terms.

Definition at line 99 of file theory_core.h.

Referenced by getTheoremForTerm(), registerAtom(), and setupTerm().

List of all active non-equality atomic formulas in the system (for quantifier instantiation)

Definition at line 103 of file theory_core.h.

Referenced by getPredicates(), and setupTerm().

std::vector<Expr> CVC3::TheoryCore::d_vars [private]

List of variables that were created up to this point.

Definition at line 105 of file theory_core.h.

Referenced by addToVarDB(), buildModel(), and collectBasicVars().

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

Database of declared identifiers.

Definition at line 107 of file theory_core.h.

Referenced by CVC3::Theory::installID(), and CVC3::Theory::resolveID().

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

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

Definition at line 109 of file theory_core.h.

Referenced by CVC3::Theory::addBoundVar(), parseExpr(), and parseExprTop().

Map for bound vars.

Definition at line 111 of file theory_core.h.

Referenced by CVC3::Theory::addBoundVar(), parseExpr(), and CVC3::Theory::resolveID().

Top-level cache for parser.

Definition at line 114 of file theory_core.h.

Referenced by CVC3::Theory::addBoundVar(), parseExpr(), and parseExprTop().

Alternative cache for parser when not at top-level.

Definition at line 118 of file theory_core.h.

Referenced by CVC3::Theory::addBoundVar().

Current cache being used for parser.

Definition at line 120 of file theory_core.h.

Referenced by CVC3::Theory::addBoundVar(), parseExpr(), parseExprOp(), and parseExprTop().

Cache for tcc's.

Definition at line 122 of file theory_core.h.

Referenced by CVC3::Theory::getTCC(), and tccCache().

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

Array mapping kinds to theories.

Definition at line 128 of file theory_core.h.

Referenced by CVC3::Theory::hasTheory(), CVC3::Theory::registerKinds(), CVC3::Theory::theoryOf(), and CVC3::Theory::unregisterKinds().

The theory which has the solver (if any)

Definition at line 131 of file theory_core.h.

Referenced by assertEqualities(), checkEquation(), CVC3::Theory::registerTheory(), solve(), and CVC3::Theory::unregisterTheory().

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

Definition at line 134 of file theory_core.h.

Referenced by collectBasicVars(), and collectModelValues().

Mapping of intermediate variables to their values.

Definition at line 136 of file theory_core.h.

Referenced by assignValue(), buildModel(), collectBasicVars(), and collectModelValues().

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

List of basic variables (temporary storage for model generation)

Definition at line 138 of file theory_core.h.

Referenced by buildModel(), and collectBasicVars().

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 145 of file theory_core.h.

Referenced by buildModel(), collectBasicVars(), and collectModelValues().

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

Command line flag whether to simplify in place.

Definition at line 148 of file theory_core.h.

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

Which recursive simplifier to use.

Definition at line 150 of file theory_core.h.

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 157 of file theory_core.h.

Referenced by getResource(), getResourceLimit(), outOfResources(), and setResourceLimit().

unsigned CVC3::TheoryCore::d_timeBase [private]

Time limit (0==unlimited, >0==total available cpu time in seconds).

Currently, if exhausted processFactQueue will not perform any more reasoning with FULL effor and an incomplete flag is set.

Definition at line 163 of file theory_core.h.

Referenced by initTimeLimit(), and timeLimitReached().

unsigned CVC3::TheoryCore::d_timeLimit [private]

Definition at line 164 of file theory_core.h.

Referenced by setTimeLimit(), and timeLimitReached().

Definition at line 166 of file theory_core.h.

Referenced by checkSATCore(), and okToEnqueue().

Definition at line 167 of file theory_core.h.

Referenced by addFact(), and okToEnqueue().

Definition at line 168 of file theory_core.h.

Referenced by okToEnqueue(), and registerAtom().

bool CVC3::TheoryCore::d_inPP [private]

Definition at line 169 of file theory_core.h.

Referenced by clearInPP(), okToEnqueue(), and setInPP().

Definition at line 183 of file theory_core.h.

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

Definition at line 186 of file theory_core.h.

Referenced by getImpliedLiteral(), getImpliedLiteralByIndex(), and numImpliedLiterals().

Next index in d_impliedLiterals that has not yet been fetched.

Definition at line 189 of file theory_core.h.

Referenced by getImpliedLiteral().

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

List of theorems from calls to update()

Definition at line 194 of file theory_core.h.

Referenced by addFact(), checkSATCore(), and update().

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

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

Definition at line 197 of file theory_core.h.

Referenced by addFact(), checkSATCore(), and update().

Notify list that gets processed on every equality.

Definition at line 200 of file theory_core.h.

Referenced by addNotifyEq(), and assertEqualities().

unsigned CVC3::TheoryCore::d_inUpdate [private]

Whether we are in the middle of doing updates.

Definition at line 203 of file theory_core.h.

Referenced by inUpdate().

std::vector< std::pair<Expr, Expr> > CVC3::TheoryCore::d_assignment [private]

The set of named expressions to evaluate on a GET_ASSIGNMENT request.

Definition at line 206 of file theory_core.h.

Referenced by getAssignment(), and parseExpr().


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