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 registerCoreSatAPI (CoreSatAPI *coreSatAPI)

  Register a SatAPI for TheoryCore.
  

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

  Get list of terms.
  

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

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

• void computeType (const Expr &e)

  Compute and store the type of e.
  

• Type computeBaseType (const Type &t)

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

• Expr computeTCC (const Expr &e)

  Compute and cache the TCC of e.
  

• Expr computeTypePred (const Type &t, const Expr &e)

  Theory specific computation of the subtyping predicate for type t applied to the expression e.
  

• Expr parseExprOp (const Expr &e)

  Theory-specific parsing implemented by the DP.
  

• ExprStream & print (ExprStream &os, const Expr &e)

  Theory-specific pretty-printing.
  

• void refineCounterExample ()

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

• void computeModelBasic (const std::vector< Expr > &v)

  Assign concrete values to basic-type variables in v.
  

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

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

• Theorem rewriteLiteral (const Expr &e)

  Called by search engine.
  

• void enqueueFact (const Theorem &e)

  Enqueue a new fact.
  

• 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 isSorted (const std::vector< Expr > &v)

  Check if the vector<Expr> is sorted w.r.t. operator<.
  

• void intersect (const std::vector< Expr > &a, const std::vector< Expr > &b, std::vector< Expr > &res)
• void difference (const std::vector< Expr > &a, const std::vector< Expr > &b, std::vector< Expr > &res)

  Set difference of sorted vectors of Exprs: res := a - b.
  

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

• void checkRewriteType (const Theorem &thm)

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

• Theorem rewriteCore (const Expr &e)

  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 rewriteIte (const Expr &e)

  Derived rule for rewriting ITE.
  

• Theorem rewriteLitCore (const Expr &e)

  Core rewrites for literals (NOT and EQ).
  

• Theorem rewriteN (const Expr &e, int n)

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

• bool processEquality (const Theorem &thm, ExprMap< Theorem > &q)

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

• void enqueueSE (const Theorem &thm)

  Enqueue a fact to be sent to the SearchEngine.
  

• Theorem getModelValue (const Expr &e)

  Fetch the concrete assignment to the variable during model generation.
  

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

  An auxiliary recursive function to process COND expressions into ITE.
  

• void getResource ()

  Request a unit of resource.
  

• bool isBasicKind (int kind)

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

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

• bool d_inCheckSATCore
• bool d_inAddFact
• bool d_inRegisterAtom
• ExprMap< bool > d_simpStack
• 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().
  

• 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 47 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 242 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 778 of file theory_core.cpp.

References CVC3::AND, CVC3::AND_R, CVC3::ANY_TYPE, CVC3::APPLY, 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::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 921 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 CVC3::TheoryCore::isSorted

(

const std::vector< Expr > &

v

)

[private]

Check if the vector<Expr> is sorted w.r.t. operator<.

Referenced by difference().

void CVC3::TheoryCore::intersect	(	const std::vector< Expr > &	a,
		const std::vector< Expr > &	b,
		std::vector< Expr > &	res
	)			[private]

ASSUMPTION: a and b are sorted in ascending order w.r.t. operator<

void TheoryCore::difference	(	const std::vector< Expr > &	a,
		const std::vector< Expr > &	b,
		std::vector< Expr > &	res
	)			[private]

Set difference of sorted vectors of Exprs: res := a - b.

ASSUMPTION: a and b are sorted in ascending order w.r.t. operator<

Definition at line 142 of file theory_core.cpp.

References DebugAssert, and isSorted().

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

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

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

References d_inconsistent, 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 269 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 281 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 303 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 338 of file theory_core.cpp.

References CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), assertEqualities(), assertFormula(), CVC3::Debug::counter(), CVC3::Theory::d_commonRules, d_inconsistent, DebugAssert, CVC3::debugger, enqueueSE(), getCM(), CVC3::Theorem::getExpr(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Theory::iffMP(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isAnd(), CVC3::Expr::isEq(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::Theorem::isRefl(), 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 388 of file theory_core.cpp.

References CVC3::Expr::addToNotify(), CVC3::Theory::assertFact(), CVC3::Debug::counter(), CVC3::Theory::d_commonRules, DebugAssert, CVC3::debugger, enqueueFact(), CVC3::Expr::eqExpr(), CVC3::Theory::getBaseType(), getCM(), CVC3::Theorem::getExpr(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::CommonProofRules::iffFalseElim(), CVC3::CommonProofRules::iffTrue(), CVC3::CommonProofRules::iffTrueElim(), CVC3::Expr::isAbsLiteral(), CVC3::Expr::isEq(), CVC3::Expr::isExists(), CVC3::Expr::isNot(), CVC3::CommonProofRules::notToIff(), 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().

void CVC3::TheoryCore::checkRewriteType

(

const Theorem &

thm

)

[private]

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

Theorem CVC3::TheoryCore::rewriteCore

(

const Expr &

e

)

[private]

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, 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(), CVC3::Theory::theoryOf(), and CVC3::Expr::toString().

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 500 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::Expr::setFind(), CVC3::Expr::setImpliedLiteral(), setInconsistent(), CVC3::Expr::toString(), and CVC3::TRACE.

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

Theorem TheoryCore::rewriteIte

(

const Expr &

e

)

[private]

Derived rule for rewriting ITE.

Definition at line 551 of file theory_core.cpp.

References d_rules, CVC3::Theory::reflexivityRule(), CVC3::CoreProofRules::rewriteIteFalse(), CVC3::CoreProofRules::rewriteIteSame(), and CVC3::CoreProofRules::rewriteIteTrue().

Theorem TheoryCore::rewriteLitCore

(

const Expr &

e

)

[private]

Core rewrites for literals (NOT and EQ).

Definition at line 567 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::rewriteN	(	const Expr &	e,
		int	n
	)			[private]

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

Definition at line 595 of file theory_core.cpp.

References CVC3::Theorem::getRHS(), CVC3::Theory::reflexivityRule(), rewrite(), CVC3::Theory::substitutivityRule(), CVC3::Theory::theoryOf(), and CVC3::Theory::transitivityRule().

bool TheoryCore::processEquality	(	const Theorem &	thm,
		ExprMap< Theorem > &	q
	)			[private]

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

Fill in the copy of the equality queue with single equalities by processing the input 'eq', which can be an equality, a conjunction of equalities, or an existential quantifier of the above.

Definition at line 625 of file theory_core.cpp.

References CVC3::AND, CVC3::CommonProofRules::andElim(), CVC3::Expr::arity(), CVC3::CommonProofRules::contradictionRule(), CVC3::Debug::counter(), CVC3::Theory::d_commonRules, DebugAssert, CVC3::debugger, CVC3::EQ, CVC3::EXISTS, CVC3::FALSE_EXPR, CVC3::Theory::find(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::CommonProofRules::iffFalseElim(), setInconsistent(), CVC3::CommonProofRules::skolemize(), and CVC3::Expr::toString().

void TheoryCore::enqueueSE

(

const Theorem &

thm

)

[private]

Enqueue a fact to be sent to the SearchEngine.

Definition at line 670 of file theory_core.cpp.

References d_inAddFact, d_inCheckSATCore, d_inRegisterAtom, d_queueSE, and DebugAssert.

Referenced by assertFactCore().

Theorem TheoryCore::getModelValue

(

const Expr &

e

)

[private]

Fetch the concrete assignment to the variable during model generation.

Reimplemented from CVC3::Theory.

Definition at line 677 of file theory_core.cpp.

References d_varAssignments, and CVC3::Theory::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 687 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().

void CVC3::TheoryCore::getResource

(

)

[inline, private]

Request a unit of resource.

It will be subtracted from the resource limit.

Returns:

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

Definition at line 301 of file theory_core.h.

References d_resourceLimit.

Referenced by addFact(), and enqueueFact().

bool TheoryCore::isBasicKind

(

int

kind

)

[private]

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

Definition at line 712 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::EQ, 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::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 CVC3::TheoryCore::registerCoreSatAPI

(

CoreSatAPI *

coreSatAPI

)

[inline]

Register a SatAPI for TheoryCore.

Definition at line 315 of file theory_core.h.

References d_coreSatAPI.

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

ContextManager* CVC3::TheoryCore::getCM

(

)

const [inline]

Definition at line 317 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::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::DecisionEngineMBTF::goalSatisfied(), CVC3::DecisionEngineCaching::goalSatisfied(), CVC3::TheoryQuant::hasGoodSynMultiInst(), CVC3::TheoryQuant::mapTermsByType(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::SearchImplBase::pop(), CVC3::DecisionEngine::popDecision(), CVC3::DecisionEngine::popTo(), CVC3::TheoryArithOld::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 318 of file theory_core.h.

References d_tm.

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

const CLFlags& CVC3::TheoryCore::getFlags

(

)

const [inline]

Definition at line 319 of file theory_core.h.

References d_flags.

Referenced by CVC3::SearchEngineFast::bcp(), CVC3::Theory::newSubtypeExpr(), CVC3::ExprTransform::preprocess(), rewrite(), CVC3::SearchImplBase::SearchImplBase(), CVC3::SearchSat::SearchSat(), and CVC3::TheoryQuant::TheoryQuant().

Statistics& CVC3::TheoryCore::getStatistics

(

)

const [inline]

Definition at line 320 of file theory_core.h.

References d_statistics.

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

ExprTransform* CVC3::TheoryCore::getExprTrans

(

)

const [inline]

Definition at line 321 of file theory_core.h.

References d_exprTrans.

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

CoreProofRules* CVC3::TheoryCore::getCoreRules

(

)

const [inline]

Definition at line 322 of file theory_core.h.

References d_rules.

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

Translator* CVC3::TheoryCore::getTranslator

(

)

const [inline]

Definition at line 323 of file theory_core.h.

References d_translator.

Referenced by CVC3::TheoryArith::rewriteToDiff().

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

(

)

[inline]

Get list of terms.

Definition at line 326 of file theory_core.h.

References d_terms.

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

Theorem TheoryCore::getTheoremForTerm

(

const Expr &

e

)

Get theorem which was responsible for introducing this term.

Definition at line 931 of file theory_core.cpp.

References d_termTheorems, DebugAssert, CVC3::Expr::hasFind(), and CVC3::Expr::isStoredPredicate().

Referenced by getQuantLevelForTerm().

unsigned TheoryCore::getQuantLevelForTerm

(

const Expr &

e

)

Get quantification level at which this term was introduced.

Definition at line 951 of file theory_core.cpp.

References CVC3::Theorem::getQuantLevel(), getTheoremForTerm(), CVC3::Expr::hasFind(), CVC3::Theorem::isNull(), CVC3::Expr::isStoredPredicate(), 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 332 of file theory_core.h.

References d_predicates.

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

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 337 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 976 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 339 of file theory_core.h.

Referenced by processFactQueue().

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 984 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::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::CoreProofRules::rewriteIteCond(), CVC3::CoreProofRules::rewriteIteFalse(), CVC3::CoreProofRules::rewriteIteSame(), CVC3::CoreProofRules::rewriteIteToAnd(), CVC3::CoreProofRules::rewriteIteToIff(), CVC3::CoreProofRules::rewriteIteToImp(), CVC3::CoreProofRules::rewriteIteToNot(), CVC3::CoreProofRules::rewriteIteToOr(), CVC3::CoreProofRules::rewriteIteTrue(), 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().

Referenced by rewriteN().

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 344 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 1160 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::Expr::isFalse(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isNot(), CVC3::Expr::isRegisteredAtom(), 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 1222 of file theory_core.cpp.

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

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

References CVC3::AND, CVC3::Expr::arity(), CVC3::Debug::counter(), CVC3::Theory::d_commonRules, d_rules, DebugAssert, CVC3::debugger, CVC3::EQ, CVC3::FALSE_EXPR, CVC3::Expr::getKind(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::IFF, CVC3::CommonProofRules::iffTrue(), CVC3::IMPLIES, CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), CVC3::ITE, CVC3::NOT, CVC3::OR, CVC3::Theory::reflexivityRule(), CVC3::Theory::rewriteAnd(), CVC3::CoreProofRules::rewriteImplies(), CVC3::CoreProofRules::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 1389 of file theory_core.cpp.

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

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 1424 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::Expr::setType(), CVC3::Type::toString(), CVC3::Expr::toString(), and CVC3::XOR.

Type TheoryCore::computeBaseType

(

const Type &

t

)

[virtual]

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

Reimplemented from CVC3::Theory.

Definition at line 1565 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 1595 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 1649 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 1669 of file theory_core.cpp.

References CVC3::Theory::addBoundVar(), CVC3::Expr::arity(), CVC3::BOOLEAN, CVC3::COND, d_parseCache, DebugAssert, CVC3::FALSE_EXPR, CVC3::Expr::getEM(), CVC3::Theory::getEM(), CVC3::Type::getExpr(), 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 1855 of file theory_core.cpp.

References CVC3::AND, CVC3::ANY_TYPE, 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(), CVC3::Expr::getIndex(), CVC3::Expr::getKind(), CVC3::Expr::getName(), CVC3::Expr::getString(), CVC3::Expr::getType(), CVC3::Expr::getUid(), 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::SIMPLIFY_LANG, CVC3::SKOLEM_VAR, CVC3::SMTLIB_LANG, CVC3::space(), CVC3::STRING_EXPR, CVC3::SUBTYPE, CVC3::Expr::toString(), 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 2628 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().

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 2648 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 2667 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::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 213 of file theory_core.cpp.

References CVC3::ExprMap< Data >::count(), d_simpStack, DebugAssert, CVC3::ExprMap< Data >::erase(), 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::ExprMap< Data >::size(), CVC3::Theory::theoryOf(), CVC3::Expr::toString(), and CVC3::Expr::validSimpCache().

Referenced by assertFactCore(), processUpdates(), registerAtom(), rewrite(), CVC3::Theory::simplify(), CVC3::SearchImplBase::simplify(), simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::ExprTransform::smartSimplify(), and CVC3::SearchEngineFast::split().

bool CVC3::TheoryCore::inconsistent

(

)

[inline, virtual]

Check if the current context is inconsistent.

Reimplemented from CVC3::Theory.

Definition at line 372 of file theory_core.h.

References d_inconsistent.

Referenced by CVC3::SearchEngineFast::bcp(), buildModel(), CVC3::SearchSat::check(), CVC3::SearchSat::checkConsistent(), CVC3::SearchSimple::checkValidRec(), 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 375 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(), 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 2700 of file theory_core.cpp.

References CVC3::Debug::counter(), d_inCheckSATCore, d_queue, d_queueSE, DebugAssert, CVC3::debugger, 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 385 of file theory_core.h.

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

Referenced by CVC3::SearchSat::check(), 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 2717 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
	)

Register an atomic formula of interest.

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

Definition at line 2730 of file theory_core.cpp.

References CVC3::Theory::d_commonRules, d_inRegisterAtom, d_termTheorems, DebugAssert, CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::CommonProofRules::iffFalseElim(), CVC3::CommonProofRules::iffTrueElim(), CVC3::Expr::isAbsAtomicFormula(), CVC3::Expr::isFalse(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isTrue(), LOW, processFactQueue(), setFindLiteral(), CVC3::Expr::setRegisteredAtom(), setupSubFormulas(), simplify(), and CVC3::Theory::theoryOf().

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

Theorem TheoryCore::getImpliedLiteral

(

void

)

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

Definition at line 2755 of file theory_core.cpp.

References d_impliedLiterals, and d_impliedLiteralsIdx.

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

unsigned CVC3::TheoryCore::numImpliedLiterals

(

)

[inline]

Return total number of implied literals.

Definition at line 398 of file theory_core.h.

References d_impliedLiterals.

Theorem TheoryCore::getImpliedLiteralByIndex

(

unsigned

index

)

Return an implied literal by index.

Definition at line 2766 of file theory_core.cpp.

References d_impliedLiterals, and DebugAssert.

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

References CVC3::Expr::arity(), CVC3::Expr::begin(), d_boundVarMap, d_boundVarStack, d_parseCache, DebugAssert, CVC3::Expr::end(), 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(), 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 411 of file theory_core.h.

References d_boundVarStack, d_parseCache, and 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 2871 of file theory_core.cpp.

References CVC3::TheoryCore::CoreSatAPI::addAssumption(), addFact(), 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 2892 of file theory_core.cpp.

References addFact(), 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 2914 of file theory_core.cpp.

References d_vars, 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 2921 of file theory_core.cpp.

References CVC3::Theory::addSharedTerm(), 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(), CVC3::RAW_LIST, CVC3::Theory::theoryOf(), CVC3::TRACE, and TRACE_MSG.

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

void TheoryCore::buildModel

(

ExprMap< Expr > &

m

)

Calls theory specific computeModel, results are placed in map.

Definition at line 2974 of file theory_core.cpp.

References assignValue(), collectModelValues(), d_basicModelVars, CVC3::Theory::d_em, d_simplifiedModelVars, d_theories, d_varAssignments, d_vars, DebugAssert, CVC3::Theory::find(), CVC3::Theory::getBaseType(), CVC3::Theorem::getLeafAssumptions(), 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().

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

References assignValue(), CVC3::Theory::computeModel(), d_simplifiedModelVars, d_varAssignments, d_varModelMap, 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 437 of file theory_core.h.

References d_resourceLimit.

unsigned CVC3::TheoryCore::getResourceLimit

(

)

[inline]

Get the resource limit.

Definition at line 439 of file theory_core.h.

References d_resourceLimit.

bool CVC3::TheoryCore::outOfResources

(

)

[inline]

Return true if resources are exhausted.

Definition at line 441 of file theory_core.h.

References d_resourceLimit.

Referenced by addFact(), CVC3::SearchEngineFast::checkSAT(), CVC3::SearchSimple::checkValidRec(), enqueueFact(), and CVC3::SearchSatTheoryAPI::outOfResources().

Theorem TheoryCore::rewriteLiteral

(

const Expr &

e

)

Called by search engine.

Definition at line 3141 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 3180 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_solver, DebugAssert, CVC3::Theory::find(), CVC3::Theory::findReduced(), getCM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getNotify(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::ExprManager::invalidateSimpCache(), CVC3::Expr::isAnd(), CVC3::Expr::isFalse(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTerm(), processNotify(), CVC3::Expr::setFind(), setInconsistent(), CVC3::Theorem::toString(), CVC3::Expr::toString(), and CVC3::TRACE.

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

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

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

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

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

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

void TheoryCore::enqueueFact

(

const Theorem &

e

)

[virtual]

Enqueue a new fact.

not private because used in search_fast.cpp

Reimplemented from CVC3::Theory.

Definition at line 3284 of file theory_core.cpp.

References d_cm, d_inAddFact, d_inCheckSATCore, d_inconsistent, d_inRegisterAtom, d_queue, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), getResource(), CVC3::Theorem::getRHS(), CVC3::Theorem::getScope(), hasBoundVar(), CVC3::Expr::isFalse(), CVC3::Theorem::isRewrite(), outOfResources(), CVC3::ContextManager::scopeLevel(), setIncomplete(), setInconsistent(), and CVC3::Expr::toString().

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

void TheoryCore::setInconsistent

(

const Theorem &

e

)

[virtual]

not private because used in search_fast.cpp

Reimplemented from CVC3::Theory.

Definition at line 3316 of file theory_core.cpp.

References d_inconsistent, d_incThm, d_queueSE, d_theories, CVC3::Theory::getNumTheories(), and CVC3::Theory::notifyInconsistent().

Referenced by assertEqualities(), assertFactCore(), enqueueFact(), processEquality(), 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 3327 of file theory_core.cpp.

References CVC3::Theory::addSharedTerm(), CVC3::Expr::arity(), CVC3::Theory::assertTypePred(), CVC3::Debug::counter(), CVC3::Theory::d_commonRules, d_predicates, d_rules, d_terms, d_termTheorems, DebugAssert, CVC3::debugger, CVC3::Theorem::getExpr(), CVC3::Theorem::getQuantLevel(), CVC3::Expr::hasFind(), IF_DEBUG, CVC3::Expr::isAbsLiteral(), CVC3::Expr::isFalse(), CVC3::Expr::isStoredPredicate(), CVC3::Expr::isTerm(), CVC3::Expr::isTrue(), CVC3::CommonProofRules::reflexivityRule(), setInconsistent(), CVC3::Expr::setStoredPredicate(), CVC3::Theory::setup(), CVC3::Theory::theoryOf(), CVC3::TRACE, and CVC3::CoreProofRules::typePred().

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

---

Friends And Related Function Documentation

friend class Theory [friend]

Definition at line 48 of file theory_core.h.

friend class CoreNotifyObj [friend]

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

Definition at line 151 of file theory_core.h.

---

Member Data Documentation

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

Context manager.

Definition at line 51 of file theory_core.h.

Referenced by enqueueFact(), and getCM().

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

Theorem manager.

Definition at line 54 of file theory_core.h.

Referenced by getTM().

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

Core proof rules.

Definition at line 57 of file theory_core.h.

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

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

Reference to command line flags.

Definition at line 60 of file theory_core.h.

Referenced by getFlags().

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

Reference to statistics.

Definition at line 63 of file theory_core.h.

Referenced by getStatistics().

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

PrettyPrinter (we own it).

Definition at line 66 of file theory_core.h.

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

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

Type Computer.

Definition at line 69 of file theory_core.h.

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

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

Expr Transformer.

Definition at line 72 of file theory_core.h.

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

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

Translator.

Definition at line 75 of file theory_core.h.

Referenced by getTranslator(), and print().

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

Assertion queue.

Definition at line 78 of file theory_core.h.

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

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

Queue of facts to be sent to the SearchEngine.

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

Referenced by addFact(), assertEqualities(), assertFactCore(), enqueueFact(), 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 85 of file theory_core.h.

Referenced by incomplete(), and setIncomplete().

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

Proof of inconsistent.

Definition at line 88 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 90 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 92 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 95 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 97 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 99 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 101 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 103 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 105 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 107 of file theory_core.h.

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

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

Array of registered theories.

Definition at line 110 of file theory_core.h.

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

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

Array mapping kinds to theories.

Definition at line 113 of file theory_core.h.

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

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

The theory which has the solver (if any).

Definition at line 116 of file theory_core.h.

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

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

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

Definition at line 119 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 121 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 123 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 130 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 133 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 142 of file theory_core.h.

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

bool CVC3::TheoryCore::d_inCheckSATCore [private]

Definition at line 144 of file theory_core.h.

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

bool CVC3::TheoryCore::d_inAddFact [private]

Definition at line 145 of file theory_core.h.

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

bool CVC3::TheoryCore::d_inRegisterAtom [private]

Definition at line 146 of file theory_core.h.

Referenced by enqueueFact(), enqueueSE(), and registerAtom().

ExprMap<bool> CVC3::TheoryCore::d_simpStack [private]

Definition at line 147 of file theory_core.h.

Referenced by simplify().

CoreNotifyObj CVC3::TheoryCore::d_notifyObj [private]

Definition at line 159 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 162 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 165 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 170 of file theory_core.h.

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

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

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

Definition at line 206 of file theory_core.h.

Referenced by 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

---