CVC3  2.4.1
Classes | Public Member Functions | Private Types | Private Member Functions | Private Attributes | Friends
CVC3::TheoryCore Class Reference

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

#include <theory_core.h>

Inheritance diagram for CVC3::TheoryCore:
CVC3::Theory

List of all members.

Classes

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

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.
ContextManagergetCM () const
TheoremManagergetTM () const
const CLFlagsgetFlags () const
StatisticsgetStatistics () const
ExprTransformgetExprTrans () const
CoreProofRulesgetCoreRules () const
TranslatorgetTranslator () 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.
ExprStreamprint (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.
Expr getAssignment ()
 Get the value of all :named terms.
Expr getValue (Expr e)
 Get the value of an arbitrary formula or term.
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().
- Public Member Functions inherited from CVC3::Theory
 Theory (TheoryCore *theoryCore, const std::string &name)
 Whether theory has been used (for smtlib translator)
virtual ~Theory (void)
 Destructor.
ExprManagergetEM ()
 Access to ExprManager.
TheoryCoretheoryCore ()
 Get a pointer to theoryCore.
CommonProofRulesgetCommonRules ()
 Get a pointer to common proof rules.
const std::string & getName () const
 Get the name of the theory (for debugging purposes)
virtual void setUsed ()
 Set the "used" flag on this theory (for smtlib translator)
virtual bool theoryUsed ()
 Get whether theory has been used (for smtlib translator)
virtual Theorem theoryPreprocess (const Expr &e)
 Theory-specific preprocessing.
virtual void checkAssertEqInvariant (const Theorem &e)
 A debug check used by the primary solver.
virtual void computeModelTerm (const Expr &e, std::vector< Expr > &v)
 Add variables from 'e' to 'v' for constructing a concrete model.
virtual void computeModel (const Expr &e, std::vector< Expr > &vars)
 Compute the value of a compound variable from the more primitive ones.
virtual void assertTypePred (const Expr &e, const Theorem &pred)
 Receives all the type predicates for the types of the given theory.
virtual Theorem rewriteAtomic (const Expr &e)
 Theory-specific rewrites for atomic formulas.
virtual void notifyInconsistent (const Theorem &thm)
 Notification of conflict.
virtual void registerAtom (const Expr &e)
 Theory-specific registration of atoms.
Expr simplifyExpr (const Expr &e)
 Simplify a term e w.r.t. the current context.
void registerKinds (Theory *theory, std::vector< int > &kinds)
 Register new kinds with the given theory.
void unregisterKinds (Theory *theory, std::vector< int > &kinds)
 Unregister kinds for a theory.
void registerTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver=false)
 Register a new theory.
void unregisterTheory (Theory *theory, std::vector< int > &kinds, bool hasSolver)
 Unregister a theory.
int getNumTheories ()
 Return the number of registered theories.
bool hasTheory (int kind)
 Test whether a kind maps to any theory.
TheorytheoryOf (int kind)
 Return the theory associated with a kind.
TheorytheoryOf (const Type &e)
 Return the theory associated with a type.
TheorytheoryOf (const Expr &e)
 Return the theory associated with an Expr.
Theorem find (const Expr &e)
 Return the theorem that e is equal to its find.
const TheoremfindRef (const Expr &e)
 Return the find as a reference: expr must have a find.
Theorem findReduce (const Expr &e)
 Return find-reduced version of e.
bool findReduced (const Expr &e)
 Return true iff e is find-reduced.
Expr findExpr (const Expr &e)
 Return the find of e, or e if it has no find.
Expr getTCC (const Expr &e)
 Compute the TCC of e, or the subtyping predicate, if e is a type.
Type getBaseType (const Expr &e)
 Compute (or look up in cache) the base type of e and return the result.
Type getBaseType (const Type &tp)
 Compute the base type from an arbitrary type.
Expr getTypePred (const Type &t, const Expr &e)
 Calls the correct theory to compute a type predicate.
Theorem updateHelper (const Expr &e)
 Update the children of the term e.
void setupCC (const Expr &e)
 Setup a term for congruence closure (must have sig and rep attributes)
void updateCC (const Theorem &e, const Expr &d)
 Update a term w.r.t. congruence closure (must be setup with setupCC())
Theorem rewriteCC (const Expr &e)
 Rewrite a term w.r.t. congruence closure (must be setup with setupCC())
void getModelTerm (const Expr &e, std::vector< Expr > &v)
 Calls the correct theory to get all of the terms that need to be assigned values in the concrete model.
void addSplitter (const Expr &e, int priority=0)
 Suggest a splitter to the SearchEngine.
void addGlobalLemma (const Theorem &thm, int priority=0)
 Add a global lemma.
bool isLeaf (const Expr &e)
 Test if e is an i-leaf term for the current theory.
bool isLeafIn (const Expr &e1, const Expr &e2)
 Test if e1 is an i-leaf in e2.
bool leavesAreSimp (const Expr &e)
 Test if all i-leaves of e are simplified.
Type boolType ()
 Return BOOLEAN type.
const ExprfalseExpr ()
 Return FALSE Expr.
const ExprtrueExpr ()
 Return TRUE Expr.
Expr newVar (const std::string &name, const Type &type)
 Create a new variable given its name and type.
Expr newVar (const std::string &name, const Type &type, const Expr &def)
 Create a new named expression given its name, type, and definition.
Op newFunction (const std::string &name, const Type &type, bool computeTransClosure)
 Create a new uninterpreted function.
Op lookupFunction (const std::string &name, Type *type)
 Look up a function by name.
Op newFunction (const std::string &name, const Type &type, const Expr &def)
 Create a new defined function.
Expr addBoundVar (const std::string &name, const Type &type)
 Create and add a new bound variable to the stack, for parseExprOp().
Expr addBoundVar (const std::string &name, const Type &type, const Expr &def)
 Create and add a new bound named def to the stack, for parseExprOp().
Expr lookupVar (const std::string &name, Type *type)
 Lookup variable and return it and its type. Return NULL Expr if it doesn't exist yet.
Type newTypeExpr (const std::string &name)
 Create a new uninterpreted type with the given name.
Type lookupTypeExpr (const std::string &name)
 Lookup type by name. Return Null if no such type exists.
Type newTypeExpr (const std::string &name, const Type &def)
 Create a new type abbreviation with the given name.
Type newSubtypeExpr (const Expr &pred, const Expr &witness)
 Create a new subtype expression.
Expr resolveID (const std::string &name)
 Resolve an identifier, for use in parseExprOp()
void installID (const std::string &name, const Expr &e)
 Install name as a new identifier associated with Expr e.
Theorem reflexivityRule (const Expr &a)
 ==> a == a
Theorem symmetryRule (const Theorem &a1_eq_a2)
 a1 == a2 ==> a2 == a1
Theorem transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
 (a1 == a2) & (a2 == a3) ==> (a1 == a3)
Theorem substitutivityRule (const Op &op, const std::vector< Theorem > &thms)
 (c_1 == d_1) & ... & (c_n == d_n) ==> op(c_1,...,c_n) == op(d_1,...,d_n)
Theorem substitutivityRule (const Expr &e, const Theorem &t)
 Special case for unary operators.
Theorem substitutivityRule (const Expr &e, const Theorem &t1, const Theorem &t2)
 Special case for binary operators.
Theorem substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms)
 Optimized: only positions which changed are included.
Theorem substitutivityRule (const Expr &e, int changed, const Theorem &thm)
 Optimized: only a single position changed.
Theorem iffMP (const Theorem &e1, const Theorem &e1_iff_e2)
 e1 AND (e1 IFF e2) ==> e2
Theorem rewriteAnd (const Expr &e)
 ==> AND(e1,e2) IFF [simplified expr]
Theorem rewriteOr (const Expr &e)
 ==> OR(e1,...,en) IFF [simplified expr]
Theorem rewriteIte (const Expr &e)
 Derived rule for rewriting ITE.
Theorem renameExpr (const Expr &e)
 Derived rule to create a new name for an expression.

Private Types

enum  EffortLevel { LOW, NORMAL, FULL }
 Effort level for processFactQueue. More...

Private Member Functions

CoreProofRulescreateProofRules (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.
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)
 Enqueue a fact to be sent to the SearchEngine.
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 ()
ExprStreamprintSmtLibShared (ExprStream &os, const Expr &e)
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

ContextManagerd_cm
 Context manager.
TheoremManagerd_tm
 Theorem manager.
CoreProofRulesd_rules
 Core proof rules.
const CLFlagsd_flags
 Reference to command line flags.
Statisticsd_statistics
 Reference to statistics.
PrettyPrinterd_printer
 PrettyPrinter (we own it)
ExprManager::TypeComputerd_typeComputer
 Type Computer.
ExprTransformd_exprTrans
 Expr Transformer.
Translatord_translator
 Translator.
std::queue< Theoremd_queue
 Assertion queue.
std::vector< Theoremd_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< Theoremd_incThm
 Proof of inconsistent.
CDList< Exprd_terms
 List of all active terms in the system (for quantifier instantiation)
std::hash_map< Expr, Theoremd_termTheorems
 Map from active terms to theorems that introduced those terms.
CDList< Exprd_predicates
 List of all active non-equality atomic formulas in the system (for quantifier instantiation)
std::vector< Exprd_vars
 List of variables that were created up to this point.
std::map< std::string, Exprd_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, Exprd_boundVarMap
 Map for bound vars.
ExprMap< Exprd_parseCacheTop
 Top-level cache for parser.
ExprMap< Exprd_parseCacheOther
 Alternative cache for parser when not at top-level.
ExprMap< Expr > * d_parseCache
 Current cache being used for parser.
ExprMap< Exprd_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.
Theoryd_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< Theoremd_varAssignments
 Mapping of intermediate variables to their values.
std::vector< Exprd_basicModelVars
 List of basic variables (temporary storage for model generation)
ExprHashMap< Theoremd_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< Theoremd_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< Theoremd_update_thms
 List of theorems from calls to update()
std::vector< Exprd_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.
std::vector< std::pair< Expr,
Expr > > 
d_assignment
 The set of named expressions to evaluate on a GET_ASSIGNMENT request.
CoreSatAPId_coreSatAPI

Friends

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

Additional Inherited Members

- Protected Attributes inherited from CVC3::Theory
bool d_theoryUsed

Detailed Description

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

Author: Clark Barrett

Created: Sat Feb 8 14:54:05 2003

Definition at line 53 of file theory_core.h.


Member Enumeration Documentation

Effort level for processFactQueue.

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

Enumerator:
LOW 
NORMAL 
FULL 

Definition at line 258 of file theory_core.h.


Constructor & Destructor Documentation

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

Member Function Documentation

CoreProofRules * TheoryCore::createProofRules ( TheoremManager tm)
private

Private method to get a new theorem producer.

This method is used ONLY by the TheoryCore constructor. The only reason to have this method is to separate the trusted part of the constructor into a separate .cpp file (Alternative is to make the entire constructer trusted, which is not very safe). Method is implemented in core_theorem_producer.cpp

Definition at line 45 of file core_theorem_producer.cpp.

Referenced by TheoryCore().

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

A helper function for addFact()

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

Definition at line 121 of file theory_core.cpp.

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

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

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

Definition at line 173 of file theory_core.cpp.

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

Referenced by assertEqualities().

Theorem TheoryCore::rewriteCore ( const Theorem e)
private

Transitive composition of other rewrites with the above.

Definition at line 257 of file theory_core.cpp.

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

Referenced by rewrite().

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

Helper for registerAtom.

Definition at line 269 of file theory_core.cpp.

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

Referenced by registerAtom().

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

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

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

Definition at line 455 of file theory_core.cpp.

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

void TheoryCore::setFindLiteral ( const Theorem thm)
private

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

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

Definition at line 509 of file theory_core.cpp.

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

Referenced by registerAtom(), and update().

Theorem TheoryCore::rewriteLitCore ( const Expr e)
private

Core rewrites for literals (NOT and EQ)

Definition at line 560 of file theory_core.cpp.

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

Referenced by rewrite().

Theorem TheoryCore::getModelValue ( const Expr e)
private

Enqueue a fact to be sent to the SearchEngine.

Fetch the concrete assignment to the variable during model generation

Reimplemented from CVC3::Theory.

Definition at line 595 of file theory_core.cpp.

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

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

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

An auxiliary recursive function to process COND expressions into ITE.

Definition at line 605 of file theory_core.cpp.

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

Referenced by parseExprOp().

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

Helper check functions for solve.

Definition at line 1195 of file theory_core.cpp.

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

Referenced by checkSolved().

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

Definition at line 4062 of file theory_core.cpp.

References d_timeBase, d_timeLimit, and setIncomplete().

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

Request a unit of resource.

It will be subtracted from the resource limit.

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

Definition at line 334 of file theory_core.h.

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

Referenced by addFact().

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

Register a SatAPI for TheoryCore.

Definition at line 340 of file theory_core.h.

References d_coreSatAPI.

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

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

Register a callback for every equality.

Definition at line 343 of file theory_core.h.

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

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

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

Definition at line 353 of file theory_core.h.

References d_rules.

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

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

Definition at line 354 of file theory_core.h.

References d_translator.

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

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

Access to tcc cache (needed by theory_bitvector)

Definition at line 357 of file theory_core.h.

References d_tccCache.

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

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

Set the flag for the preprocessor.

Definition at line 365 of file theory_core.h.

References d_inPP.

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

void CVC3::TheoryCore::clearInPP ( )
inline

Definition at line 366 of file theory_core.h.

References d_inPP.

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

Theorem TheoryCore::getTheoremForTerm ( const Expr e)

Get theorem which was responsible for introducing this term.

Definition at line 868 of file theory_core.cpp.

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

Referenced by getQuantLevelForTerm().

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

Get list of predicates.

Definition at line 373 of file theory_core.h.

References d_predicates.

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

bool CVC3::TheoryCore::inUpdate ( )
inline

Whether updates are being processed.

Definition at line 375 of file theory_core.h.

References d_inUpdate.

bool CVC3::TheoryCore::okToEnqueue ( )
inline

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

Definition at line 377 of file theory_core.h.

References d_inAddFact, d_inCheckSATCore, d_inPP, and d_inRegisterAtom.

void CVC3::TheoryCore::addSharedTerm ( const Expr e)
inlinevirtual

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

Reimplemented from CVC3::Theory.

Definition at line 383 of file theory_core.h.

void TheoryCore::assertFact ( const Theorem e)
virtual

Assert a new fact to the decision procedure.

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

Implements CVC3::Theory.

Definition at line 960 of file theory_core.cpp.

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

void CVC3::TheoryCore::checkSat ( bool  fullEffort)
inlinevirtual

Check for satisfiability in the theory.

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

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

Implements CVC3::Theory.

Definition at line 385 of file theory_core.h.

Theorem TheoryCore::rewrite ( const Expr e)
virtual

Theory-specific rewrite rules.

By default, rewrite just returns a reflexive theorem stating that the input expression is equivalent to itself. However, rewrite is allowed to return any theorem which describes how the input expression is equivalent to some new expression. rewrite should be used to perform simplifications, normalization, and any other preprocessing on theory-specific expressions that needs to be done.

Reimplemented from CVC3::Theory.

Definition at line 968 of file theory_core.cpp.

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

void CVC3::TheoryCore::setup ( const Expr e)
inlinevirtual

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

Reimplemented from CVC3::Theory.

Definition at line 390 of file theory_core.h.

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

Function: TheoryCore::solve

Author: Clark Barrett

Created: Wed Feb 26 16:17:54 2003

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

Reimplemented from CVC3::Theory.

Definition at line 1248 of file theory_core.cpp.

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

Theorem TheoryCore::simplifyOp ( const Expr e)
virtual

Recursive simplification step.

INVARIANT: the result is a Theorem(e=e'), where e' is a fully simplified version of e. To simplify subexpressions recursively, call simplify() function.

This theory-specific method is called when the simplifier descends top-down into the expression. Normally, every kid is simplified recursively, and the results are combined into the new parent with the same operator (Op). This functionality is provided with the default implementation.

However, in some expressions some kids may not matter in the result, and can be skipped. For instance, if the first kid in a long AND simplifies to FALSE, then the entire expression simplifies to FALSE, and the remaining kids do not need to be simplified.

This call is a chance for a DP to provide these types of optimizations during the top-down phase of simplification.

Reimplemented from CVC3::Theory.

Definition at line 1292 of file theory_core.cpp.

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

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

Compute information related to finiteness of types.

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

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

Reimplemented from CVC3::Theory.

Definition at line 1443 of file theory_core.cpp.

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

void TheoryCore::computeType ( const Expr e)
virtual

Compute and store the type of e.

Parameters:
eis the expression whose type is computed.

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

Reimplemented from CVC3::Theory.

Definition at line 1471 of file theory_core.cpp.

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

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

Compute and cache the TCC of e.

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

This function computes the TCC or predicate of the top-level operator of e, and recurses into children using getTCC(), if necessary.

The default implementation is to compute TCCs recursively for all children, and return their conjunction.

Reimplemented from CVC3::Theory.

Definition at line 1650 of file theory_core.cpp.

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

Expr TheoryCore::computeTypePred ( const Type t,
const Expr e 
)
virtual

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

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

Reimplemented from CVC3::Theory.

Definition at line 1704 of file theory_core.cpp.

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

Expr TheoryCore::parseExprOp ( const Expr e)
virtual
ExprStream & TheoryCore::print ( ExprStream os,
const Expr e 
)
virtual

Theory-specific pretty-printing.

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

Reimplemented from CVC3::Theory.

Definition at line 2055 of file theory_core.cpp.

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

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

Assign concrete values to basic-type variables in v.

Reimplemented from CVC3::Theory.

Definition at line 3449 of file theory_core.cpp.

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

void TheoryCore::addFact ( const Theorem e)
Theorem TheoryCore::simplify ( const Expr e)
virtual
bool CVC3::TheoryCore::inconsistent ( )
inlinevirtual

Check if the current context is inconsistent.

Reimplemented from CVC3::Theory.

Definition at line 422 of file theory_core.h.

References d_inconsistent.

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

Theorem CVC3::TheoryCore::inconsistentThm ( )
inline

Get the proof of inconsistency for the current context.

Returns:
Theorem(FALSE)

Definition at line 425 of file theory_core.h.

References d_incThm.

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

bool TheoryCore::checkSATCore ( )

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

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

Definition at line 3507 of file theory_core.cpp.

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

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

bool CVC3::TheoryCore::incomplete ( )
inline

Check if the current decision branch is marked as incomplete.

Definition at line 435 of file theory_core.h.

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

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

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

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

Definition at line 3528 of file theory_core.cpp.

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

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

Return the next implied literal (NULL Theorem if none)

Definition at line 3571 of file theory_core.cpp.

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

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

unsigned CVC3::TheoryCore::numImpliedLiterals ( )
inline

Return total number of implied literals.

Definition at line 448 of file theory_core.h.

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

Theorem TheoryCore::getImpliedLiteralByIndex ( unsigned  index)

Return an implied literal by index.

Definition at line 3582 of file theory_core.cpp.

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

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

Expr TheoryCore::parseExpr ( const Expr e)
virtual
Expr CVC3::TheoryCore::parseExprTop ( const Expr e)
inline

Top-level call to parseExpr, clears the bound variable stack.

Use it in VCL instead of parseExpr().

Definition at line 461 of file theory_core.h.

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

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

Adds expression to var database.

Definition at line 3756 of file theory_core.cpp.

References d_vars, and TRACE.

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

void TheoryCore::collectBasicVars ( )

Split compound vars into basic type variables.

The results are saved in d_basicModelVars and d_simplifiedModelVars. Also, add new basic vars as shared terms whenever their type belongs to a different theory than the term itself.

Definition at line 3763 of file theory_core.cpp.

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

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

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

Recursively build a compound-type variable assignment for e.

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

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

Definition at line 3954 of file theory_core.cpp.

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

Referenced by buildModel().

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

Set the resource limit (0==unlimited).

Definition at line 488 of file theory_core.h.

References d_resourceLimit.

unsigned CVC3::TheoryCore::getResourceLimit ( )
inline

Get the resource limit.

Definition at line 490 of file theory_core.h.

References d_resourceLimit.

bool CVC3::TheoryCore::outOfResources ( )
inline

Return true if resources are exhausted.

Definition at line 492 of file theory_core.h.

References d_resourceLimit.

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

void TheoryCore::initTimeLimit ( )

Initialize base time used for !setTimeLimit.

Definition at line 4058 of file theory_core.cpp.

References d_timeBase.

Referenced by setTimeLimit().

void TheoryCore::setTimeLimit ( unsigned  limit)

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

Definition at line 4053 of file theory_core.cpp.

References d_timeLimit, and initTimeLimit().

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

Get the value of an arbitrary formula or term.

Definition at line 4333 of file theory_core.cpp.

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

void TheoryCore::assertEqualities ( const Theorem e)
privatevirtual

Assert a system of equations (1 or more).

e is either a single equation, or a conjunction of equations

Invariants:

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

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

Reimplemented from CVC3::Theory.

Definition at line 4093 of file theory_core.cpp.

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

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

void TheoryCore::setIncomplete ( const std::string &  reason)
privatevirtual

Mark the branch as incomplete.

Reimplemented from CVC3::Theory.

Definition at line 4180 of file theory_core.cpp.

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

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

Theorem TheoryCore::typePred ( const Expr e)
private

Return a theorem for the type predicate of e.

Note: used only by theory_arith

Reimplemented from CVC3::Theory.

Definition at line 4186 of file theory_core.cpp.

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

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

void CVC3::TheoryCore::enqueueFact ( const Theorem e)
virtual
void TheoryCore::enqueueSE ( const Theorem e)
virtual

Check if the current context is inconsistent.

Reimplemented from CVC3::Theory.

Definition at line 588 of file theory_core.cpp.

References DebugAssert.

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

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

Friends And Related Function Documentation

friend class Theory
friend

Definition at line 54 of file theory_core.h.

friend class CoreNotifyObj
friend

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

Definition at line 175 of file theory_core.h.


Member Data Documentation

ContextManager* CVC3::TheoryCore::d_cm
private

Context manager.

Definition at line 57 of file theory_core.h.

Referenced by getCM().

TheoremManager* CVC3::TheoryCore::d_tm
private

Theorem manager.

Definition at line 60 of file theory_core.h.

Referenced by getTM().

CoreProofRules* CVC3::TheoryCore::d_rules
private

Core proof rules.

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

Referenced by getFlags().

Statistics& CVC3::TheoryCore::d_statistics
private

Reference to statistics.

Definition at line 69 of file theory_core.h.

Referenced by getStatistics().

PrettyPrinter* CVC3::TheoryCore::d_printer
private

PrettyPrinter (we own it)

Definition at line 72 of file theory_core.h.

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

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

Type Computer.

Definition at line 75 of file theory_core.h.

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

ExprTransform* CVC3::TheoryCore::d_exprTrans
private

Expr Transformer.

Definition at line 78 of file theory_core.h.

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

Translator* CVC3::TheoryCore::d_translator
private

Translator.

Definition at line 81 of file theory_core.h.

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

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

Assertion queue.

Definition at line 84 of file theory_core.h.

Referenced by addFact(), and checkSATCore().

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

Queue of facts to be sent to the SearchEngine.

Definition at line 86 of file theory_core.h.

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

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

Inconsistent flag.

Definition at line 89 of file theory_core.h.

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

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

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

Definition at line 91 of file theory_core.h.

Referenced by incomplete(), and setIncomplete().

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

Proof of inconsistent.

Definition at line 94 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 96 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 99 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 103 of file theory_core.h.

Referenced by getPredicates(), and setupTerm().

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

List of variables that were created up to this point.

Definition at line 105 of file theory_core.h.

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

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

Database of declared identifiers.

Definition at line 107 of file theory_core.h.

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

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

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

Definition at line 109 of file theory_core.h.

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

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

Map for bound vars.

Definition at line 111 of file theory_core.h.

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

ExprMap<Expr> CVC3::TheoryCore::d_parseCacheTop
private

Top-level cache for parser.

Definition at line 114 of file theory_core.h.

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

ExprMap<Expr> CVC3::TheoryCore::d_parseCacheOther
private

Alternative cache for parser when not at top-level.

Definition at line 118 of file theory_core.h.

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

ExprMap<Expr>* CVC3::TheoryCore::d_parseCache
private

Current cache being used for parser.

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

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

std::vector<Theory*> CVC3::TheoryCore::d_theories
private
std::hash_map<int, Theory*> CVC3::TheoryCore::d_theoryMap
private

Array mapping kinds to theories.

Definition at line 128 of file theory_core.h.

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

Theory* CVC3::TheoryCore::d_solver
private

The theory which has the solver (if any)

Definition at line 131 of file theory_core.h.

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

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

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

Definition at line 134 of file theory_core.h.

Referenced by collectBasicVars(), and collectModelValues().

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

Mapping of intermediate variables to their values.

Definition at line 136 of file theory_core.h.

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

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

List of basic variables (temporary storage for model generation)

Definition at line 138 of file theory_core.h.

Referenced by buildModel(), and collectBasicVars().

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

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

const bool* CVC3::TheoryCore::d_simplifyInPlace
private

Command line flag whether to simplify in place.

Definition at line 148 of file theory_core.h.

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

Which recursive simplifier to use.

Definition at line 150 of file theory_core.h.

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

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

unsigned CVC3::TheoryCore::d_timeBase
private

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

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

Definition at line 163 of file theory_core.h.

Referenced by initTimeLimit(), and timeLimitReached().

unsigned CVC3::TheoryCore::d_timeLimit
private

Definition at line 164 of file theory_core.h.

Referenced by setTimeLimit(), and timeLimitReached().

bool CVC3::TheoryCore::d_inCheckSATCore
private

Definition at line 166 of file theory_core.h.

Referenced by checkSATCore(), and okToEnqueue().

bool CVC3::TheoryCore::d_inAddFact
private

Definition at line 167 of file theory_core.h.

Referenced by addFact(), and okToEnqueue().

bool CVC3::TheoryCore::d_inRegisterAtom
private

Definition at line 168 of file theory_core.h.

Referenced by okToEnqueue(), and registerAtom().

bool CVC3::TheoryCore::d_inPP
private

Definition at line 169 of file theory_core.h.

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

CoreNotifyObj CVC3::TheoryCore::d_notifyObj
private

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

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

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

Next index in d_impliedLiterals that has not yet been fetched.

Definition at line 189 of file theory_core.h.

Referenced by getImpliedLiteral().

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

List of theorems from calls to update()

Definition at line 194 of file theory_core.h.

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

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

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

Definition at line 197 of file theory_core.h.

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

NotifyList CVC3::TheoryCore::d_notifyEq
private

Notify list that gets processed on every equality.

Definition at line 200 of file theory_core.h.

Referenced by addNotifyEq(), and assertEqualities().

unsigned CVC3::TheoryCore::d_inUpdate
private

Whether we are in the middle of doing updates.

Definition at line 203 of file theory_core.h.

Referenced by inUpdate().

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

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

Definition at line 206 of file theory_core.h.

Referenced by getAssignment(), and parseExpr().

CoreSatAPI* CVC3::TheoryCore::d_coreSatAPI
private

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