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

[legend]Collaboration diagram for CVC3::TheoryCore:

[legend]List of all members.

Public Member Functions

• TheoryCore (ContextManager *cm, ExprManager *em, TheoremManager *tm, Translator *tr, const CLFlags &flags, Statistics &statistics)

  Constructor.
  

• ~TheoryCore ()

  Destructor.
  

• void getResource ()

  Request a unit of resource.
  

• void registerCoreSatAPI (CoreSatAPI *coreSatAPI)

  Register a SatAPI for TheoryCore.
  

• void addNotifyEq (Theory *t, const Expr &e)

  Register a callback for every equality.
  

• Theorem callTheoryPreprocess (const Expr &e)

  Call theory-specific preprocess routines.
  

• ContextManager * getCM () const
• TheoremManager * getTM () const
• const CLFlags & getFlags () const
• Statistics & getStatistics () const
• ExprTransform * getExprTrans () const
• CoreProofRules * getCoreRules () const
• Translator * getTranslator () const
• ExprMap< Expr > & tccCache ()

  Access to tcc cache (needed by theory_bitvector).
  

• const CDList< Expr > & getTerms ()

  Get list of terms.
  

• int getCurQuantLevel ()
• void setInPP ()

  Set the flag for the preprocessor.
  

• void clearInPP ()
• Theorem getTheoremForTerm (const Expr &e)

  Get theorem which was responsible for introducing this term.
  

• unsigned getQuantLevelForTerm (const Expr &e)

  Get quantification level at which this term was introduced.
  

• const CDList< Expr > & getPredicates ()

  Get list of predicates.
  

• bool inUpdate ()

  Whether updates are being processed.
  

• bool okToEnqueue ()

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

• 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)
• void update (const Theorem &e, const Expr &d)
• Theorem solve (const Theorem &e)
• Theorem simplifyOp (const Expr &e)

  Recursive simplification step.
  

• void checkType (const Expr &e)

  Check that e is a valid Type expr.
  

• Cardinality finiteTypeInfo (Expr &e, Unsigned &n, bool enumerate, bool computeSize)

  Compute information related to finiteness of types.
  

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

• bool refineCounterExample (Theorem &thm)
• void computeModelBasic (const std::vector< Expr > &v)

  Assign concrete values to basic-type variables in v.
  

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

  Top-level simplifier.
  

• bool inconsistent ()

  Check if the current context is inconsistent.
  

• Theorem inconsistentThm ()

  Get the proof of inconsistency for the current context.
  

• bool checkSATCore ()

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

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

• void registerAtom (const Expr &e, const Theorem &thm)

  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.
  

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

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

  Recursively build a compound-type variable assignment for e.
  

• void setResourceLimit (unsigned limit)

  Set the resource limit (0==unlimited).
  

• unsigned getResourceLimit ()

  Get the resource limit.
  

• bool outOfResources ()

  Return true if resources are exhausted.
  

• void initTimeLimit ()

  Initialize base time used for !setTimeLimit.
  

• void setTimeLimit (unsigned limit)

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

• Theorem rewriteLiteral (const Expr &e)

  Called by search engine.
  

• void enqueueFact (const Theorem &e)

  Enqueue a new fact.
  

• void enqueueSE (const Theorem &thm)

  Check if the current context is inconsistent.
  

• void setInconsistent (const Theorem &e)
• void setupTerm (const Expr &e, Theory *i, const Theorem &thm)

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

Private Types

• enum EffortLevel { LOW, NORMAL, FULL }

  Effort level for processFactQueue. More...
  

Private Member Functions

• CoreProofRules * createProofRules (TheoremManager *tm)

  Private method to get a new theorem producer.
  

• bool processFactQueue (EffortLevel effort=NORMAL)

  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 rewriteCore (const Theorem &e)

  Transitive composition of other rewrites with the above.
  

• void setupSubFormulas (const Expr &s, const Expr &e, const Theorem &thm)

  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)

  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.
  

• void setFindLiteral (const Theorem &thm)

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

• Theorem rewriteLitCore (const Expr &e)

  Core rewrites for literals (NOT and EQ).
  

• Theorem getModelValue (const Expr &e)

  Fetch the concrete assignment to the variable during model generation.
  

• Expr processCond (const Expr &e, int i)

  An auxiliary recursive function to process COND expressions into ITE.
  

• bool isBasicKind (int kind)

  Return true if no special parsing is required for this kind.
  

• void checkEquation (const Theorem &thm)

  Helper check functions for solve.
  

• void checkSolved (const Theorem &thm)

  Helper check functions for solve.
  

• bool timeLimitReached ()
• void assertEqualities (const Theorem &e)

  Assert a system of equations (1 or more).
  

• void setIncomplete (const std::string &reason)

  Mark the branch as incomplete.
  

• Theorem typePred (const Expr &e)

  Return a theorem for the type predicate of e.
  

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.
  

• Translator * d_translator

  Translator.
  

• std::queue< Theorem > d_queue

  Assertion queue.
  

• std::vector< Theorem > d_queueSE

  Queue of facts to be sent to the SearchEngine.
  

• CDO< bool > d_inconsistent

  Inconsistent flag.
  

• CDMap< std::string, bool > d_incomplete

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

• CDO< Theorem > d_incThm

  Proof of inconsistent.
  

• CDList< Expr > d_terms

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

• std::hash_map< Expr, Theorem > d_termTheorems

  Map from active terms to theorems that introduced those terms.
  

• CDList< Expr > d_predicates

  List of all active non-equality atomic formulas 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>.
  

• std::hash_map< std::string,
  Expr > d_boundVarMap

  Map for bound vars.
  

• ExprMap< Expr > d_parseCache

  Cache for parser.
  

• ExprMap< Expr > d_tccCache

  Cache for tcc's.
  

• std::vector< Theory * > d_theories

  Array of registered theories.
  

• std::hash_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.
  

• unsigned d_resourceLimit

  Resource limit (0==unlimited, 1==no more resources, >=2 - available).
  

• unsigned d_timeBase

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

• unsigned d_timeLimit
• bool d_inCheckSATCore
• bool d_inAddFact
• bool d_inRegisterAtom
• bool d_inPP
• CoreNotifyObj d_notifyObj
• 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().
  

• NotifyList d_notifyEq

  Notify list that gets processed on every equality.
  

• unsigned d_inUpdate

  Whether we are in the middle of doing updates.
  

• CoreSatAPI * d_coreSatAPI

Friends

• class Theory
• class CoreNotifyObj

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

Classes

• class CoreNotifyObj
• class CoreSatAPI

  Interface class for callbacks to SAT from Core. More...
  

---

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

---

Member Enumeration Documentation

enum CVC3::TheoryCore::EffortLevel [private]

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

---

Constructor & Destructor Documentation

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

Constructor.

Definition at line 695 of file theory_core.cpp.

References CVC3::AND, CVC3::AND_R, CVC3::ANY_TYPE, CVC3::APPLY, CVC3::ARITH_VAR_ORDER, CVC3::ASSERT, CVC3::ASSERTIONS, CVC3::ASSUMPTIONS, CVC3::BOOLEAN, CVC3::BOUND_VAR, CVC3::CALL, CVC3::CHECK_TYPE, CVC3::COND, CVC3::CONST, CVC3::CONTEXT, CVC3::COUNTEREXAMPLE, CVC3::COUNTERMODEL, createProofRules(), CVC3::Theory::d_commonRules, CVC3::Theory::d_em, d_exprTrans, CVC3::Theory::d_name, d_printer, d_rules, CVC3::Theory::d_theoryCore, CVC3::Theory::d_theoryUsed, d_typeComputer, CVC3::DBG, CVC3::DEFUN, CVC3::DISTINCT, CVC3::DUMP_ASSUMPTIONS, CVC3::DUMP_CLOSURE, CVC3::DUMP_CLOSURE_PROOF, CVC3::DUMP_PROOF, CVC3::DUMP_SIG, CVC3::DUMP_TCC, CVC3::DUMP_TCC_ASSUMPTIONS, CVC3::DUMP_TCC_PROOF, CVC3::ECHO, CVC3::ELSE, CVC3::EQ, CVC3::FALSE_EXPR, CVC3::FORGET, CVC3::GET_CHILD, CVC3::GET_TYPE, CVC3::TheoremManager::getRules(), CVC3::HELP, CVC3::ID, CVC3::IF, CVC3::IFF, CVC3::IFF_R, CVC3::IFTHEN, CVC3::IMPLIES, CVC3::ITE, CVC3::ITE_R, CVC3::LET, CVC3::LETDECL, CVC3::LETDECLS, CVC3::NEQ, CVC3::NOT, CVC3::OPTION, CVC3::OR, CVC3::PF_APPLY, CVC3::PF_HOLE, CVC3::POP, CVC3::POP_SCOPE, CVC3::POPTO, CVC3::POPTO_SCOPE, CVC3::PRINT, CVC3::PUSH, CVC3::PUSH_SCOPE, CVC3::QUERY, CVC3::RAW_LIST, CVC3::ExprManager::registerPrettyPrinter(), CVC3::Theory::registerTheory(), CVC3::ExprManager::registerTypeComputer(), CVC3::RESET, CVC3::SEQ, CVC3::SKOLEM_VAR, CVC3::STRING_EXPR, CVC3::SUBSTITUTE, CVC3::SUBTYPE, CVC3::THEOREM_KIND, CVC3::TRACE, CVC3::TRANSFORM, CVC3::TRUE_EXPR, CVC3::TYPE, CVC3::TYPEDEF, CVC3::UCONST, CVC3::UNTRACE, CVC3::VARDECL, CVC3::VARDECLS, CVC3::VARLIST, CVC3::WHERE, and CVC3::XOR.

TheoryCore::~TheoryCore

(

)

Destructor.

Definition at line 842 of file theory_core.cpp.

References CVC3::Theory::d_em, d_exprTrans, d_printer, d_rules, d_typeComputer, and CVC3::ExprManager::unregisterPrettyPrinter().

---

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 120 of file theory_core.cpp.

References CVC3::TheoryCore::CoreSatAPI::addLemma(), assertFactCore(), d_coreSatAPI, d_inconsistent, d_queue, d_queueSE, d_theories, d_update_data, d_update_thms, FULL, LOW, processUpdates(), and timeLimitReached().

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 172 of file theory_core.cpp.

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

Referenced by assertEqualities(), and setFindLiteral().

Theorem TheoryCore::rewriteCore

(

const Theorem &

e

)

[private]

Transitive composition of other rewrites with the above.

Definition at line 256 of file theory_core.cpp.

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

Referenced by rewrite(), rewriteCore(), and simplify().

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

Helper for registerAtom.

Definition at line 268 of file theory_core.cpp.

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

Referenced by registerAtom().

void TheoryCore::processUpdates

(

)

[private]

Process updates recorded by calls to update().

Definition at line 290 of file theory_core.cpp.

References CVC3::Expr::addToNotify(), CVC3::Theory::d_commonRules, d_inconsistent, d_update_data, d_update_thms, DebugAssert, CVC3::Theory::find(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::CommonProofRules::iffFalseElim(), CVC3::CommonProofRules::iffTrueElim(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Type::isBool(), CVC3::Theorem::isRewrite(), setFindLiteral(), and simplify().

Referenced by processFactQueue().

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

Definition at line 320 of file theory_core.cpp.

References CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), assertEqualities(), assertFormula(), CVC3::Theory::d_commonRules, d_inconsistent, DebugAssert, std::endl(), enqueueSE(), CVC3::Theory::find(), getCM(), CVC3::Theorem::getExpr(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Theory::iffMP(), incomplete(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isAnd(), CVC3::Expr::isEq(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Expr::isTrue(), CVC3::PRESENTATION_LANG, setFindLiteral(), setInconsistent(), simplify(), solve(), CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by processFactQueue().

void TheoryCore::assertFormula

(

const Theorem &

e

)

[private]

Process a newly derived formula.

Definition at line 384 of file theory_core.cpp.

References CVC3::Expr::addToNotify(), CVC3::Theory::assertFact(), CVC3::Theory::d_commonRules, DebugAssert, enqueueFact(), CVC3::EQ, CVC3::Expr::eqExpr(), CVC3::EXISTS, CVC3::Theory::getBaseType(), getCM(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::CommonProofRules::iffTrue(), CVC3::CommonProofRules::iffTrueElim(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isNot(), CVC3::NOT, CVC3::PRESENTATION_LANG, CVC3::CommonProofRules::rewriteUsingSymmetry(), setFindLiteral(), setupTerm(), CVC3::CommonProofRules::skolemize(), CVC3::Theory::theoryOf(), CVC3::Expr::toString(), CVC3::Theorem::toString(), CVC3::TRACE, and CVC3::Theory::transitivityRule().

Referenced by assertEqualities(), and assertFactCore().

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 454 of file theory_core.cpp.

References CVC3::Expr::clearRewriteNormal(), CVC3::Theory::d_commonRules, d_inUpdate, DebugAssert, CVC3::EQ, CVC3::Theory::find(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isEq(), CVC3::Expr::isRewriteNormal(), CVC3::NOT, CVC3::Theory::reflexivityRule(), CVC3::Theory::rewrite(), rewriteCore(), CVC3::CommonProofRules::rewriteNotNot(), CVC3::CommonProofRules::rewriteReflexivity(), CVC3::CommonProofRules::rewriteUsingSymmetry(), CVC3::Expr::setRewriteNormal(), simplify(), CVC3::Theory::theoryOf(), CVC3::Expr::toString(), and CVC3::Theory::transitivityRule().

void TheoryCore::setFindLiteral

(

const Theorem &

thm

)

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

Definition at line 508 of file theory_core.cpp.

References CVC3::Theory::d_commonRules, CVC3::Theory::d_em, d_impliedLiterals, DebugAssert, CVC3::Theory::find(), getCM(), CVC3::Theorem::getExpr(), CVC3::Expr::getNotify(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Theory::iffMP(), CVC3::CommonProofRules::iffTrue(), CVC3::CommonProofRules::iffTrueElim(), CVC3::ExprManager::invalidateSimpCache(), CVC3::Expr::isFalse(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isNot(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isTrue(), CVC3::CommonProofRules::notToIff(), CVC3::PRESENTATION_LANG, processNotify(), CVC3::CDList< T >::push_back(), CVC3::Expr::setFind(), CVC3::Expr::setImpliedLiteral(), setInconsistent(), CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by assertFactCore(), assertFormula(), processUpdates(), registerAtom(), and update().

Theorem TheoryCore::rewriteLitCore

(

const Expr &

e

)

[private]

Core rewrites for literals (NOT and EQ).

Definition at line 559 of file theory_core.cpp.

References CVC3::Theory::d_commonRules, DebugAssert, CVC3::EQ, CVC3::Expr::getKind(), CVC3::NOT, CVC3::Theory::reflexivityRule(), CVC3::CommonProofRules::rewriteNotFalse(), CVC3::CommonProofRules::rewriteNotNot(), CVC3::CommonProofRules::rewriteNotTrue(), CVC3::CommonProofRules::rewriteReflexivity(), and CVC3::CommonProofRules::rewriteUsingSymmetry().

Referenced by rewrite().

Theorem TheoryCore::getModelValue

(

const Expr &

e

)

[private]

Fetch the concrete assignment to the variable during model generation.

Reimplemented from CVC3::Theory.

Definition at line 594 of file theory_core.cpp.

References d_varAssignments, CVC3::ExprHashMap< Data >::end(), CVC3::Theory::find(), and 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 604 of file theory_core.cpp.

References CVC3::Expr::arity(), DebugAssert, CVC3::ID, CVC3::Expr::iteExpr(), parseExpr(), CVC3::RAW_LIST, and CVC3::Expr::toString().

Referenced by parseExprOp().

bool TheoryCore::isBasicKind

(

int

kind

)

[private]

Return true if no special parsing is required for this kind.

Definition at line 629 of file theory_core.cpp.

References CVC3::AND, CVC3::ASSERT, CVC3::ASSERTIONS, CVC3::ASSUMPTIONS, CVC3::CALL, CVC3::CHECK_TYPE, CVC3::CHECKSAT, CVC3::CONTEXT, CVC3::CONTINUE, CVC3::COUNTEREXAMPLE, CVC3::COUNTERMODEL, CVC3::DBG, CVC3::DISTINCT, CVC3::DUMP_ASSUMPTIONS, CVC3::DUMP_CLOSURE, CVC3::DUMP_CLOSURE_PROOF, CVC3::DUMP_PROOF, CVC3::DUMP_SIG, CVC3::DUMP_TCC, CVC3::DUMP_TCC_ASSUMPTIONS, CVC3::DUMP_TCC_PROOF, CVC3::ECHO, CVC3::ELSE, CVC3::FORGET, CVC3::GET_CHILD, CVC3::GET_TYPE, CVC3::HELP, CVC3::IFF, CVC3::IMPLIES, CVC3::LETDECL, CVC3::LETDECLS, CVC3::NOT, CVC3::OPTION, CVC3::OR, CVC3::POP, CVC3::POP_SCOPE, CVC3::POPTO, CVC3::POPTO_SCOPE, CVC3::PRINT, CVC3::PUSH, CVC3::PUSH_SCOPE, CVC3::QUERY, CVC3::RESET, CVC3::RESTART, CVC3::SEQ, CVC3::SUBSTITUTE, CVC3::TRACE, CVC3::TRANSFORM, CVC3::TYPEDEF, CVC3::UNTRACE, CVC3::VARDECL, CVC3::VARDECLS, CVC3::VARLIST, CVC3::WHERE, and CVC3::XOR.

Referenced by parseExprOp().

void TheoryCore::checkEquation

(

const Theorem &

thm

)

[private]

Helper check functions for solve.

Definition at line 1190 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]

Helper check functions for solve.

Definition at line 1215 of file theory_core.cpp.

References CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), checkEquation(), CVC3::Theory::d_commonRules, CVC3::Theorem::getExpr(), CVC3::Expr::isAnd(), and CVC3::Expr::isBoolConst().

Referenced by solve().

bool TheoryCore::timeLimitReached

(

)

[private]

Definition at line 3613 of file theory_core.cpp.

References d_timeBase, d_timeLimit, and setIncomplete().

Referenced by processFactQueue().

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

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

Referenced by addFact(), CVC3::TheoryArithOld::addToBuffer(), and CVC3::TheoryArithOld::DifferenceLogicGraph::getEdge().

void CVC3::TheoryCore::registerCoreSatAPI

(

CoreSatAPI *

coreSatAPI

)

[inline]

Register a SatAPI for TheoryCore.

Definition at line 323 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 326 of file theory_core.h.

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

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

Theorem TheoryCore::callTheoryPreprocess

(

const Expr &

e

)

Call theory-specific preprocess routines.

Definition at line 852 of file theory_core.cpp.

References d_theories, CVC3::Theorem::getRHS(), LOW, processFactQueue(), CVC3::Theory::reflexivityRule(), CVC3::Theory::theoryPreprocess(), and CVC3::Theory::transitivityRule().

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

ContextManager* CVC3::TheoryCore::getCM

(

)

const [inline]

Definition at line 331 of file theory_core.h.

References d_cm.

Referenced by CVC3::TheoryQuant::add_parent(), addFact(), CVC3::SearchEngineFast::addNonLiteralFact(), assertEqualities(), CVC3::TheoryUF::assertFact(), assertFactCore(), assertFormula(), CVC3::SearchSat::assertLit(), CVC3::SearchSat::check(), CVC3::CoreSatAPI_implBase::check(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchSimple::checkValidMain(), CVC3::SearchEngineFast::checkValidMain(), CVC3::TheoryQuant::combineOldNewTrigs(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdge(), CVC3::TheoryQuant::mapTermsByType(), CVC3::ExprTransform::newPPrec(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchImplBase::pop(), CVC3::DecisionEngine::popDecision(), CVC3::DecisionEngine::popTo(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::SearchImplBase::push(), CVC3::DecisionEngine::pushDecision(), CVC3::SearchSat::recordNewRootLit(), CVC3::TheoryQuant::recursiveMap(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::SearchSat::restorePre(), CVC3::SearchImplBase::scopeLevel(), CVC3::SearchImplBase::SearchImplBase(), CVC3::SearchSat::SearchSat(), setFindLiteral(), and CVC3::TheoryQuant::synNewInst().

TheoremManager* CVC3::TheoryCore::getTM

(

)

const [inline]

Definition at line 332 of file theory_core.h.

References d_tm.

Referenced by CVC3::SearchSat::check(), CVC3::SearchEngine::createRules(), CVC3::SearchImplBase::getAssumptionsUsed(), CVC3::SearchImplBase::getCounterExample(), CVC3::SearchSat::getProof(), CVC3::SearchImplBase::getProof(), SAT::DPLLTMiniSat::getSatProof(), and CVC3::SearchSat::SearchSat().

const CLFlags& CVC3::TheoryCore::getFlags

(

)

const [inline]

Definition at line 333 of file theory_core.h.

References d_flags.

Referenced by CVC3::SearchEngineFast::bcp(), CVC3::Translator::finish(), CVC3::Theory::newSubtypeExpr(), CVC3::SearchSat::newUserAssumptionIntHelper(), parseExprOp(), CVC3::ExprTransform::preprocess(), CVC3::Translator::preprocessRec(), print(), CVC3::Translator::processType(), rewrite(), CVC3::SearchImplBase::SearchImplBase(), CVC3::SearchSat::SearchSat(), and CVC3::TheoryQuant::TheoryQuant().

Statistics& CVC3::TheoryCore::getStatistics

(

)

const [inline]

Definition at line 334 of file theory_core.h.

References d_statistics.

Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::SearchImplBase::findInCNFCache(), getResource(), CVC3::SearchSat::SearchSat(), and CVC3::SearchEngineFast::split().

ExprTransform* CVC3::TheoryCore::getExprTrans

(

)

const [inline]

Definition at line 335 of file theory_core.h.

References d_exprTrans.

Referenced by CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSat::newUserAssumptionInt(), and CVC3::VCL::simplifyThm().

CoreProofRules* CVC3::TheoryCore::getCoreRules

(

)

const [inline]

Definition at line 336 of file theory_core.h.

References d_rules.

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

Translator* CVC3::TheoryCore::getTranslator

(

)

const [inline]

Definition at line 337 of file theory_core.h.

References d_translator.

Referenced by CVC3::TheoryUF::print(), and CVC3::TheoryArith::rewriteToDiff().

ExprMap<Expr>& CVC3::TheoryCore::tccCache

(

)

[inline]

Access to tcc cache (needed by theory_bitvector).

Definition at line 340 of file theory_core.h.

References d_tccCache.

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

const CDList<Expr>& CVC3::TheoryCore::getTerms

(

)

[inline]

Get list of terms.

Definition at line 343 of file theory_core.h.

References d_terms.

Referenced by CVC3::SearchSat::check(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::debug(), and CVC3::TheoryQuant::naiveCheckSat().

int CVC3::TheoryCore::getCurQuantLevel

(

)

void CVC3::TheoryCore::setInPP

(

)

[inline]

Set the flag for the preprocessor.

Definition at line 348 of file theory_core.h.

References d_inPP.

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

void CVC3::TheoryCore::clearInPP

(

)

[inline]

Definition at line 349 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 863 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 CVC3::TRACE.

Referenced by getQuantLevelForTerm().

unsigned TheoryCore::getQuantLevelForTerm

(

const Expr &

e

)

Get quantification level at which this term was introduced.

Definition at line 899 of file theory_core.cpp.

References CVC3::Expr::getIndex(), getTheoremForTerm(), CVC3::Expr::inUserAssumption(), CVC3::Expr::isIff(), CVC3::Expr::isNot(), CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by CVC3::TheoryQuant::enqueueInst(), CVC3::TheoryQuant::getExprScore(), and CVC3::QuantTheoremProducer::universalInst().

const CDList<Expr>& CVC3::TheoryCore::getPredicates

(

)

[inline]

Get list of predicates.

Definition at line 356 of file theory_core.h.

References d_predicates.

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

bool CVC3::TheoryCore::inUpdate

(

)

[inline]

Whether updates are being processed.

Definition at line 358 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 360 of file theory_core.h.

References d_inAddFact, d_inCheckSATCore, d_inPP, and d_inRegisterAtom.

Referenced by enqueueSE(), and CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

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 366 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 955 of file theory_core.cpp.

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

void CVC3::TheoryCore::checkSat

(

bool

fullEffort

)

[inline, 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 CVC3::Theory.

Definition at line 368 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 963 of file theory_core.cpp.

References CVC3::AND, CVC3::AND_R, CVC3::APPLY, CVC3::Expr::arity(), CVC3::BOUND_VAR, CVC3::Theory::d_commonRules, d_rules, DebugAssert, CVC3::DISTINCT, CVC3::EQ, CVC3::EXISTS, CVC3::FALSE_EXPR, CVC3::Theory::find(), CVC3::FORALL, CVC3::Theorem::getExpr(), getFlags(), CVC3::Expr::getKind(), CVC3::Theorem::getLHS(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::IFF, CVC3::IFF_R, CVC3::IMPLIES, CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::Theorem::isRefl(), CVC3::ITE, CVC3::ITE_R, CVC3::LAMBDA, CVC3::LETDECL, CVC3::NOT, CVC3::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(), CVC3::SKOLEM_VAR, CVC3::Theory::substitutivityRule(), CVC3::Theory::theoryOf(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), CVC3::TRUE_EXPR, CVC3::UCONST, CVC3::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 373 of file theory_core.h.

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

We use the update method of theory core to track registered atomic formulas. Updates are recorded and then processed by calling processUpdates once all equalities have been processed.

Reimplemented from CVC3::Theory.

Definition at line 1136 of file theory_core.cpp.

References CVC3::Expr::addToNotify(), CVC3::Theory::d_commonRules, d_update_data, d_update_thms, DebugAssert, CVC3::Theory::find(), CVC3::Theorem::getRHS(), CVC3::Expr::hasFind(), CVC3::CommonProofRules::iffFalseElim(), CVC3::Theory::iffMP(), CVC3::CommonProofRules::iffTrueElim(), CVC3::Expr::isFalse(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isNot(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isTrue(), CVC3::CommonProofRules::rewriteUsingSymmetry(), setFindLiteral(), setInconsistent(), CVC3::CommonProofRules::substitutivityRule(), CVC3::Theory::symmetryRule(), and CVC3::Theory::transitivityRule().

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

Referenced by assertFactCore().

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 1287 of file theory_core.cpp.

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

Referenced by simplify().

void TheoryCore::checkType

(

const Expr &

e

)

[virtual]

Check that e is a valid Type expr.

Reimplemented from CVC3::Theory.

Definition at line 1403 of file theory_core.cpp.

References CVC3::ANY_TYPE, CVC3::Expr::arity(), CVC3::BOOLEAN, FatalAssert, CVC3::Theory::getEM(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::Type::isFunction(), CVC3::SUBTYPE, and CVC3::Expr::toString().

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 1438 of file theory_core.cpp.

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

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

Definition at line 1466 of file theory_core.cpp.

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

Type TheoryCore::computeBaseType

(

const Type &

tp

)

[virtual]

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

Reimplemented from CVC3::Theory.

Definition at line 1610 of file theory_core.cpp.

References CVC3::ANY_TYPE, CVC3::Expr::arity(), CVC3::BOOLEAN, DebugAssert, CVC3::Theory::getBaseType(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::Type::isFunction(), CVC3::SUBTYPE, CVC3::Type::toString(), CVC3::Expr::toString(), and CVC3::TYPEDEF.

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

Definition at line 1640 of file theory_core.cpp.

References CVC3::AND, CVC3::andExpr(), CVC3::APPLY, CVC3::Expr::begin(), CVC3::Theory::computeTCC(), CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Theory::getTCC(), CVC3::IMPLIES, CVC3::ITE, CVC3::NOT, CVC3::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 1694 of file theory_core.cpp.

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

Expr TheoryCore::parseExprOp

(

const Expr &

e

)

[virtual]

Theory-specific parsing implemented by the DP.

Reimplemented from CVC3::Theory.

Definition at line 1714 of file theory_core.cpp.

References CVC3::Theory::addBoundVar(), CVC3::Expr::arity(), CVC3::BOOLEAN, CVC3::Theory::boolType(), CVC3::COND, d_parseCache, DebugAssert, CVC3::ExprMap< Data >::end(), CVC3::EQ, CVC3::FALSE_EXPR, CVC3::ExprMap< Data >::find(), CVC3::Expr::getEM(), CVC3::Theory::getEM(), CVC3::Type::getExpr(), getFlags(), CVC3::ExprManager::getKind(), CVC3::Expr::getKind(), CVC3::ID, CVC3::IF, isBasicKind(), CVC3::LET, CVC3::NEQ, CVC3::ExprManager::newLeafExpr(), CVC3::Theory::newSubtypeExpr(), CVC3::NULL_KIND, parseExpr(), processCond(), CVC3::RAW_LIST, CVC3::SUBTYPE, CVC3::Expr::toString(), CVC3::TRUE_EXPR, CVC3::TYPE, CVC3::TYPEDECL, and CVC3::TYPEDEF.

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 1905 of file theory_core.cpp.

References CVC3::AND, CVC3::ANY_TYPE, CVC3::ARITH_VAR_ORDER, CVC3::Expr::arity(), CVC3::ARROW, CVC3::ASSERT, CVC3::ASSERTIONS, CVC3::ASSUMPTIONS, CVC3::Expr::begin(), CVC3::BOOLEAN, CVC3::BOUND_VAR, CVC3::CONST, CVC3::COUNTEREXAMPLE, CVC3::COUNTERMODEL, d_translator, DebugAssert, CVC3::DISTINCT, CVC3::Expr::end(), std::endl(), CVC3::EQ, CVC3::FALSE_EXPR, CVC3::Translator::fixConstName(), CVC3::Theory::getEM(), CVC3::Type::getExpr(), getFlags(), CVC3::Expr::getIndex(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::Expr::getString(), CVC3::Expr::getType(), CVC3::ID, CVC3::IFF, CVC3::IMPLIES, CVC3::Type::isBool(), CVC3::Type::isNull(), CVC3::Expr::isString(), CVC3::ITE, CVC3::ExprStream::lang(), CVC3::LET, CVC3::LETDECL, CVC3::LISP_LANG, CVC3::nodag(), CVC3::NOT, CVC3::OR, CVC3::PF_APPLY, CVC3::PF_HOLE, CVC3::pop(), CVC3::POP, CVC3::POP_SCOPE, CVC3::popSave(), CVC3::POPTO, CVC3::POPTO_SCOPE, CVC3::PRESENTATION_LANG, CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::PUSH, CVC3::push(), CVC3::PUSH_SCOPE, CVC3::pushRestore(), CVC3::QUERY, CVC3::RAW_LIST, CVC3::RESET, CVC3::SIMPLIFY_LANG, CVC3::SKOLEM_VAR, CVC3::SMTLIB_LANG, CVC3::space(), CVC3::STRING_EXPR, CVC3::SUBTYPE, CVC3::Expr::toString(), CVC3::TPTP_LANG, CVC3::TRANSFORM, CVC3::TRUE_EXPR, CVC3::TYPE, CVC3::TYPEDEF, CVC3::UCONST, CVC3::WHERE, and CVC3::XOR.

void TheoryCore::refineCounterExample

(

)

[virtual]

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

Reimplemented from CVC3::Theory.

Definition at line 3003 of file theory_core.cpp.

References CVC3::Theory::d_em, d_theories, CVC3::Theorem::getLeafAssumptions(), CVC3::Theory::getName(), CVC3::Theory::getNumTheories(), inconsistent(), inconsistentThm(), CVC3::RAW_LIST, and CVC3::Expr::toString().

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

bool TheoryCore::refineCounterExample

(

Theorem &

thm

)

Definition at line 2989 of file theory_core.cpp.

References d_theories, CVC3::Theory::getNumTheories(), inconsistent(), and inconsistentThm().

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 3023 of file theory_core.cpp.

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

void 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

Definition at line 3042 of file theory_core.cpp.

References d_inAddFact, d_inconsistent, d_queue, d_queueSE, d_update_data, d_update_thms, DebugAssert, getCM(), CVC3::Theorem::getExpr(), getResource(), IF_DEBUG, outOfResources(), CVC3::PRESENTATION_LANG, processFactQueue(), setIncomplete(), CVC3::Expr::toString(), and CVC3::TRACE.

Referenced by CVC3::SearchSat::assertLit(), assignValue(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::commitFacts(), CVC3::ExprTransform::newPPrec(), CVC3::SearchImplBase::newUserAssumption(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::Circuit::propagate(), CVC3::DecisionEngine::pushDecision(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), and CVC3::SearchEngineFast::split().

Theorem TheoryCore::simplify

(

const Expr &

e

)

[virtual]

Top-level simplifier.

Reimplemented from CVC3::Theory.

Definition at line 183 of file theory_core.cpp.

References d_inUpdate, DebugAssert, CVC3::Theory::find(), CVC3::Expr::getOpKind(), CVC3::Theorem::getRHS(), CVC3::Expr::getSimpCache(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isVar(), CVC3::Theory::reflexivityRule(), rewriteCore(), CVC3::Expr::setSimpCache(), simplifyOp(), CVC3::Theory::theoryOf(), CVC3::Expr::toString(), CVC3::Theory::transitivityRule(), and CVC3::Expr::validSimpCache().

Referenced by assertFactCore(), CVC3::ExprTransform::newPPrec(), processUpdates(), registerAtom(), rewrite(), rewriteCore(), setupTerm(), CVC3::Theory::simplify(), CVC3::SearchImplBase::simplify(), simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::VCL::simplifyThm(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::smartSimplify(), CVC3::ExprTransform::specialSimplify(), and CVC3::SearchEngineFast::split().

bool CVC3::TheoryCore::inconsistent

(

)

[inline, virtual]

Check if the current context is inconsistent.

Reimplemented from CVC3::Theory.

Definition at line 405 of file theory_core.h.

References d_inconsistent.

Referenced by CVC3::SearchEngineFast::bcp(), buildModel(), CVC3::SearchSat::check(), CVC3::SearchSat::checkConsistent(), CVC3::SearchSimple::checkValidRec(), CVC3::VCL::inconsistent(), 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 408 of file theory_core.h.

References d_incThm.

Referenced by CVC3::SearchEngineFast::bcp(), buildModel(), CVC3::SearchSat::check(), CVC3::SearchSat::checkConsistent(), CVC3::SearchSimple::checkValidRec(), CVC3::SearchEngine::getConcreteModel(), CVC3::VCL::inconsistent(), 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 3081 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::SearchSat::checkConsistent(), CVC3::SearchSimple::checkValidRec(), and CVC3::SearchEngineFast::split().

bool CVC3::TheoryCore::incomplete

(

)

[inline]

Check if the current decision branch is marked as incomplete.

Definition at line 418 of file theory_core.h.

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

Referenced by assertEqualities(), assertFactCore(), CVC3::SearchSat::check(), CVC3::SearchEngineFast::checkSAT(), CVC3::SearchSimple::checkValidMain(), CVC3::VCL::incomplete(), and CVC3::VCL::tryModelGeneration().

bool CVC3::TheoryCore::incomplete

(

std::vector< std::string > &

reasons

)

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

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

Register an atomic formula of interest.

If e or its negation is later deduced, we will add the implied literal to d_impliedLiterals

Reimplemented from CVC3::Theory.

Definition at line 3115 of file theory_core.cpp.

References CVC3::Theory::d_commonRules, d_inRegisterAtom, d_termTheorems, DebugAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::Theorem::getRHS(), CVC3::CommonProofRules::iffFalseElim(), CVC3::CommonProofRules::iffTrueElim(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isEq(), CVC3::Expr::isFalse(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isTrue(), LOW, processFactQueue(), setFindLiteral(), CVC3::Expr::setRegisteredAtom(), setupSubFormulas(), simplify(), and CVC3::Theory::theoryOf().

Referenced by CVC3::Theory::registerAtom(), and CVC3::SearchSat::registerAtom().

Theorem TheoryCore::getImpliedLiteral

(

void

)

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

Definition at line 3145 of file theory_core.cpp.

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

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

unsigned CVC3::TheoryCore::numImpliedLiterals

(

)

[inline]

Return total number of implied literals.

Definition at line 431 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 3156 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]

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

Definition at line 3163 of file theory_core.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::ExprMap< Data >::clear(), d_boundVarMap, d_boundVarStack, d_parseCache, DebugAssert, Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end(), CVC3::Expr::end(), CVC3::ExprMap< Data >::end(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::erase(), Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find(), CVC3::ExprMap< Data >::find(), CVC3::Theory::getEM(), CVC3::ExprManager::getKind(), CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), CVC3::Theory::hasTheory(), CVC3::ID, CVC3::Expr::isApply(), CVC3::Expr::isNull(), CVC3::LAMBDA, CVC3::Expr::mkOp(), CVC3::NULL_KIND, CVC3::Theory::parseExprOp(), CVC3::RAW_LIST, CVC3::Theory::resolveID(), CVC3::Theory::theoryOf(), and CVC3::Expr::toString().

Referenced by CVC3::Theory::parseExpr(), parseExprOp(), parseExprTop(), CVC3::VCL::parseType(), and processCond().

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

References CVC3::ExprMap< Data >::clear(), d_boundVarStack, d_parseCache, and parseExpr().

Referenced by CVC3::VCL::parseExpr().

void TheoryCore::assignValue	(	const Expr &	t,
		const Expr &	val
	)			[virtual]

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

Reimplemented from CVC3::Theory.

Definition at line 3264 of file theory_core.cpp.

References CVC3::TheoryCore::CoreSatAPI::addAssumption(), addFact(), CVC3::ExprHashMap< Data >::count(), d_coreSatAPI, d_varAssignments, DebugAssert, CVC3::Expr::eqExpr(), CVC3::Theory::find(), CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::Expr::toString(), and CVC3::Theory::transitivityRule().

Referenced by CVC3::Theory::assignValue(), buildModel(), collectModelValues(), and computeModelBasic().

void TheoryCore::assignValue

(

const Theorem &

thm

)

[virtual]

Record a derived assignment to a variable (LHS).

Reimplemented from CVC3::Theory.

Definition at line 3285 of file theory_core.cpp.

References addFact(), CVC3::ExprHashMap< Data >::count(), d_varAssignments, DebugAssert, CVC3::Theory::find(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::Theory::symmetryRule(), CVC3::Expr::toString(), CVC3::Theorem::toString(), and CVC3::Theory::transitivityRule().

void TheoryCore::addToVarDB

(

const Expr &

e

)

Adds expression to var database.

Definition at line 3307 of file theory_core.cpp.

References d_vars, CVC3::CDList< T >::push_back(), and CVC3::TRACE.

Referenced by CVC3::Theory::newFunction(), CVC3::Theory::newVar(), and CVC3::TheoryArray::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 3314 of file theory_core.cpp.

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

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

void TheoryCore::buildModel

(

ExprMap< Expr > &

m

)

Calls theory specific computeModel, results are placed in map.

Definition at line 3413 of file theory_core.cpp.

References assignValue(), CVC3::CDList< T >::begin(), collectModelValues(), CVC3::ExprHashMap< Data >::count(), d_basicModelVars, CVC3::Theory::d_em, d_simplifiedModelVars, d_theories, d_varAssignments, d_vars, DebugAssert, CVC3::CDList< T >::end(), CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Theorem::getLeafAssumptions(), CVC3::Theorem::getLHS(), CVC3::Theory::getName(), CVC3::Theory::getNumTheories(), CVC3::Theorem::getRHS(), inconsistent(), inconsistentThm(), CVC3::Theorem::isNull(), CVC3::RAW_LIST, CVC3::Theory::theoryOf(), CVC3::Expr::toString(), CVC3::TRACE, TRACE_MSG, and CVC3::Theory::transitivityRule().

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

bool TheoryCore::buildModel

(

Theorem &

thm

)

Definition at line 3368 of file theory_core.cpp.

References d_basicModelVars, d_simplifiedModelVars, d_theories, DebugAssert, CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Theory::getName(), CVC3::Theory::getNumTheories(), CVC3::Theorem::getRHS(), inconsistent(), inconsistentThm(), CVC3::Theory::theoryOf(), and CVC3::TRACE.

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 3505 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, CVC3::RAW_LIST, CVC3::Theory::reflexivityRule(), CVC3::Theory::theoryOf(), CVC3::TRACE, and CVC3::Theory::transitivityRule().

Referenced by buildModel().

void CVC3::TheoryCore::setResourceLimit

(

unsigned

limit

)

[inline]

Set the resource limit (0==unlimited).

Definition at line 471 of file theory_core.h.

References d_resourceLimit.

Referenced by CVC3::VCL::setResourceLimit().

unsigned CVC3::TheoryCore::getResourceLimit

(

)

[inline]

Get the resource limit.

Definition at line 473 of file theory_core.h.

References d_resourceLimit.

bool CVC3::TheoryCore::outOfResources

(

)

[inline]

Return true if resources are exhausted.

Definition at line 475 of file theory_core.h.

References d_resourceLimit.

Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), addFact(), CVC3::SearchEngineFast::checkSAT(), and CVC3::SearchSimple::checkValidRec().

void TheoryCore::initTimeLimit

(

)

Initialize base time used for !setTimeLimit.

Definition at line 3609 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 3604 of file theory_core.cpp.

References d_timeLimit, and initTimeLimit().

Referenced by CVC3::VCL::setTimeLimit().

Theorem TheoryCore::rewriteLiteral

(

const Expr &

e

)

Called by search engine.

Definition at line 3580 of file theory_core.cpp.

References CVC3::Theory::d_commonRules, DebugAssert, CVC3::Theory::getBaseType(), CVC3::CommonProofRules::iffContrapositive(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isNot(), CVC3::Theory::rewriteAtomic(), CVC3::Theory::theoryOf(), and CVC3::Expr::toString().

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

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

Reimplemented from CVC3::Theory.

Definition at line 3644 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(), CVC3::TRACE, and CVC3::Theory::transitivityRule().

Referenced by CVC3::Theory::assertEqualities(), and assertFactCore().

void TheoryCore::setIncomplete

(

const std::string &

reason

)

[private, virtual]

Mark the branch as incomplete.

Reimplemented from CVC3::Theory.

Definition at line 3731 of file theory_core.cpp.

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

Referenced by addFact(), 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 3737 of file theory_core.cpp.

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

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

void CVC3::TheoryCore::enqueueFact

(

const Theorem &

e

)

[virtual]

Enqueue a new fact.

not private because used in search_fast.cpp

Reimplemented from CVC3::Theory.

Referenced by CVC3::SearchImplBase::addCNFFact(), CVC3::SearchEngineFast::addNonLiteralFact(), assertFormula(), CVC3::SearchEngineFast::commitFacts(), CVC3::Theory::enqueueFact(), and CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

void TheoryCore::enqueueSE

(

const Theorem &

e

)

[virtual]

Check if the current context is inconsistent.

Reimplemented from CVC3::Theory.

Definition at line 587 of file theory_core.cpp.

References d_queueSE, DebugAssert, and okToEnqueue().

Referenced by assertFactCore(), and CVC3::Theory::enqueueSE().

void TheoryCore::setInconsistent

(

const Theorem &

e

)

[virtual]

not private because used in search_fast.cpp

Reimplemented from CVC3::Theory.

Definition at line 3796 of file theory_core.cpp.

References d_inconsistent, d_incThm, d_queueSE, d_theories, DebugAssert, CVC3::Theory::falseExpr(), CVC3::Theorem::getExpr(), and CVC3::Theory::notifyInconsistent().

Referenced by assertEqualities(), assertFactCore(), setFindLiteral(), CVC3::Theory::setInconsistent(), CVC3::SearchEngineFast::setInconsistent(), setupTerm(), and update().

void TheoryCore::setupTerm	(	const Expr &	e,
		Theory *	i,
		const Theorem &	thm
	)

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

not private because used in theory_bitvector.cpp

Definition at line 3811 of file theory_core.cpp.

References CVC3::Theory::addSharedTerm(), CVC3::Expr::arity(), CVC3::Theory::assertTypePred(), d_predicates, d_rules, d_terms, d_termTheorems, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getIndex(), CVC3::Theorem::getQuantLevel(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Theory::iffMP(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isFalse(), CVC3::Expr::isStoredPredicate(), CVC3::Expr::isTerm(), CVC3::Expr::isTrue(), CVC3::CDList< T >::push_back(), CVC3::Theory::reflexivityRule(), setInconsistent(), CVC3::Expr::setStoredPredicate(), CVC3::Theory::setup(), simplify(), CVC3::Theory::theoryOf(), CVC3::Theorem::toString(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::CoreProofRules::typePred().

Referenced by CVC3::TheoryArithOld::addToBuffer(), assertFormula(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryRecords::setup(), CVC3::TheoryArray::setup(), and setupSubFormulas().

---

Friends And Related Function Documentation

friend class Theory [friend]

Definition at line 52 of file theory_core.h.

friend class CoreNotifyObj [friend]

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

Definition at line 166 of file theory_core.h.

---

Member Data Documentation

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

Context manager.

Definition at line 55 of file theory_core.h.

Referenced by getCM().

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

Theorem manager.

Definition at line 58 of file theory_core.h.

Referenced by getTM().

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

Core proof rules.

Definition at line 61 of file theory_core.h.

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

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

Reference to command line flags.

Definition at line 64 of file theory_core.h.

Referenced by getFlags().

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

Reference to statistics.

Definition at line 67 of file theory_core.h.

Referenced by getStatistics().

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

PrettyPrinter (we own it).

Definition at line 70 of file theory_core.h.

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

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

Type Computer.

Definition at line 73 of file theory_core.h.

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

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

Expr Transformer.

Definition at line 76 of file theory_core.h.

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

Translator* CVC3::TheoryCore::d_translator [private]

Translator.

Definition at line 79 of file theory_core.h.

Referenced by getTranslator(), and print().

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

Assertion queue.

Definition at line 82 of file theory_core.h.

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

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

Queue of facts to be sent to the SearchEngine.

Definition at line 84 of file theory_core.h.

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

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

Inconsistent flag.

Definition at line 87 of file theory_core.h.

Referenced by addFact(), assertEqualities(), assertFactCore(), inconsistent(), processFactQueue(), processNotify(), processUpdates(), 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 89 of file theory_core.h.

Referenced by incomplete(), and setIncomplete().

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

Proof of inconsistent.

Definition at line 92 of file theory_core.h.

Referenced by inconsistentThm(), and setInconsistent().

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

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

Definition at line 94 of file theory_core.h.

Referenced by getTerms(), and setupTerm().

std::hash_map<Expr, Theorem> CVC3::TheoryCore::d_termTheorems [private]

Map from active terms to theorems that introduced those terms.

Definition at line 97 of file theory_core.h.

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

CDList<Expr> CVC3::TheoryCore::d_predicates [private]

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

Definition at line 101 of file theory_core.h.

Referenced by getPredicates(), and setupTerm().

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

List of variables that were created up to this point.

Definition at line 103 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 105 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 107 of file theory_core.h.

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

std::hash_map<std::string, Expr> CVC3::TheoryCore::d_boundVarMap [private]

Map for bound vars.

Definition at line 109 of file theory_core.h.

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

ExprMap<Expr> CVC3::TheoryCore::d_parseCache [private]

Cache for parser.

Definition at line 111 of file theory_core.h.

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

ExprMap<Expr> CVC3::TheoryCore::d_tccCache [private]

Cache for tcc's.

Definition at line 113 of file theory_core.h.

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

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

Array of registered theories.

Definition at line 116 of file theory_core.h.

Referenced by buildModel(), callTheoryPreprocess(), CVC3::Theory::getNumTheories(), processFactQueue(), refineCounterExample(), CVC3::Theory::registerTheory(), setInconsistent(), and CVC3::Theory::unregisterTheory().

std::hash_map<int, Theory*> CVC3::TheoryCore::d_theoryMap [private]

Array mapping kinds to theories.

Definition at line 119 of file theory_core.h.

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

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

The theory which has the solver (if any).

Definition at line 122 of file theory_core.h.

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

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

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

Definition at line 125 of file theory_core.h.

Referenced by collectBasicVars(), and collectModelValues().

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

Mapping of intermediate variables to their valies.

Definition at line 127 of file theory_core.h.

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

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

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

Definition at line 129 of file theory_core.h.

Referenced by buildModel(), and collectBasicVars().

ExprHashMap<Theorem> CVC3::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 136 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 139 of file theory_core.h.

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

Which recursive simplifier to use.

unsigned CVC3::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 148 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 154 of file theory_core.h.

Referenced by initTimeLimit(), and timeLimitReached().

unsigned CVC3::TheoryCore::d_timeLimit [private]

Definition at line 155 of file theory_core.h.

Referenced by setTimeLimit(), and timeLimitReached().

bool CVC3::TheoryCore::d_inCheckSATCore [private]

Definition at line 157 of file theory_core.h.

Referenced by checkSATCore(), and okToEnqueue().

bool CVC3::TheoryCore::d_inAddFact [private]

Definition at line 158 of file theory_core.h.

Referenced by addFact(), and okToEnqueue().

bool CVC3::TheoryCore::d_inRegisterAtom [private]

Definition at line 159 of file theory_core.h.

Referenced by okToEnqueue(), and registerAtom().

bool CVC3::TheoryCore::d_inPP [private]

Definition at line 160 of file theory_core.h.

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

CoreNotifyObj CVC3::TheoryCore::d_notifyObj [private]

Definition at line 174 of file theory_core.h.

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

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

Definition at line 177 of file theory_core.h.

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

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

Next index in d_impliedLiterals that has not yet been fetched.

Definition at line 180 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 185 of file theory_core.h.

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

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

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

Definition at line 188 of file theory_core.h.

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

NotifyList CVC3::TheoryCore::d_notifyEq [private]

Notify list that gets processed on every equality.

Definition at line 191 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 194 of file theory_core.h.

Referenced by inUpdate(), processNotify(), rewriteCore(), and simplify().

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

Definition at line 228 of file theory_core.h.

Referenced by CVC3::Theory::addGlobalLemma(), CVC3::Theory::addSplitter(), assignValue(), CVC3::Theory::newSubtypeExpr(), processFactQueue(), and registerCoreSatAPI().

---

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

• theory_core.h
• core_theorem_producer.cpp
• theory_core.cpp

---