CVCL::TheoryQuant Class Reference
[Theories]

This theory handles quantifiers. More...

#include <theory_quant.h>

Inheritance diagram for CVCL::TheoryQuant:

[legend]Collaboration diagram for CVCL::TheoryQuant:

[legend]List of all members.

Public Member Functions

TheoryQuant (TheoryCore *core)
categorizes all the terms contained in an expressions by type. Constructor
~TheoryQuant ()
Destructor.
QuantProofRules * createProofRules ()
Destructor.
void addSharedTerm (const Expr &e)
Theory interface.
void assertFact (const Theorem &e)
Theory interface function to assert quantified formulas.
void checkSat (bool fullEffort)
Check for satisfiability in the theory.
void setup (const Expr &e)
Set up the term e for call-backs when e or its children change.
void update (const Theorem &e, const Expr &d)
Notify a theory of a new equality.
void notifyInconsistent (const Theorem &thm)
Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent.
void computeType (const Expr &e)
computes the type of a quantified term. Always a boolean.
Expr computeTCC (const Expr &e)
virtual Expr parseExprOp (const Expr &e)
Theory-specific parsing implemented by the DP.
ExprStream & print (ExprStream &os, const Expr &e)
Theory-specific pretty-printing.

Private Types

typedef std::map< Type, std::vector<
size_t >, TypeComp > typeMap
used to facilitate instantiation of universal quantifiers

Private Member Functions

bool recursiveMap (const Expr &term)
categorizes all the terms contained in an expressions by type.
void mapTermsByType (const CDList< Expr > &terms)
categorizes all the terms contained in a vector of expressions by type.
void instantiate (Theorem univ, bool all, bool savedMap, size_t newIndex)
Queues up all possible instantiations of bound variables.
void recInstantiate (Theorem &univ, bool all, bool savedMap, size_t newIndex, std::vector< Expr > &varReplacements)
does most of the work of the instantiate function.
void findInstAssumptions (const Theorem &thm)
A recursive function used to find instantiated universals in the hierarchy of assumptions.
void synCheckSat (bool)
void semCheckSat (bool)
void naiveCheckSat (bool)
void synInst (const Theorem &univ, size_t tBegin)
void semInst (const Theorem &univ, size_t tBegin)
void goodSynMatch (const Expr &e, const std::vector< Expr > &boundVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)
bool recSynMatch (const Expr &gterm, const Expr &vterm, ExprMap< Expr > &env)
bool hasGoodSynInst (const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)
void recGoodSemMatch (const Expr &e, const std::vector< Expr > &bVars, std::vector< Expr > &newInst, std::set< std::vector< Expr > > &instSet)
bool hasGoodSemInst (const Expr &e, std::vector< Expr > &bVars, std::set< std::vector< Expr > > &instSet, size_t tBegin)
std::string getHead (const Expr &e)
get the head string of function and array
void setupTriggers (const Theorem &thm)
void enqueueInst (const Theorem thm)

Private Attributes

CDList< Theorem > d_univs
database of universally quantified theorems
CDO< size_t > d_savedTermsPos
tracks a possition in the savedTerms map
CDO< size_t > d_univsSavedPos
tracks a possition in the database of universals
CDO< size_t > d_univsPosFull
tracks a possition in the database of universals
CDO< size_t > d_univsContextPos
tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.
CDO< int > d_instCount
number of instantiations made in given context
std::map< Type, CDList< size_t > *,
TypeComp > d_contextMap
a map of types to posisitions in the d_contextTerms list
CDList< Expr > d_contextTerms
a list of all the terms appearing in the current context
CDMap< Expr, bool > d_contextCache
chache of expressions
typeMap d_savedMap
a map of types to positions in the d_savedTerms vector
ExprMap< bool > d_savedCache
std::vector< Expr > d_savedTerms
a vector of all of the terms that have produced conflicts.
ExprMap< std::vector< Expr > > d_insts
a map of instantiated universals to a vector of their instantiations
QuantProofRules * d_rules
quantifier theorem production rules
const int * d_maxQuantInst
Command line option.
const bool * d_useNew
const bool * d_useLazyInst
const bool * d_useSemMatch
const bool * d_useAtomSem
int d_instThisRound
int d_callThisRound
ExprMap< std::vector< Expr > > d_univsTriggers
std::map< Type, std::vector<
Expr >, TypeComp > d_typeExprMap
std::set< std::string > cacheHead
StatCounter d_allInstCount
CDO< int > d_instRound

Classes

class TypeComp

Detailed Description

This theory handles quantifiers.

Author: Daniel Wichs

Created: Wednesday July 2, 2003

Definition at line 53 of file theory_quant.h.

Member Typedef Documentation

typedef std::map<Type, std::vector<size_t>, TypeComp > CVCL::TheoryQuant::typeMap [private]

used to facilitate instantiation of universal quantifiers

Definition at line 62 of file theory_quant.h.

Constructor & Destructor Documentation

TheoryQuant::TheoryQuant ( TheoryCore * core )

categorizes all the terms contained in an expressions by type. Constructor
Updates d_contextTerms, d_contextMap, d_contextCache accordingly. returns true if the expression does not contain bound variables, false otherwise.
Parameters:

core Constructor

Definition at line 49 of file theory_quant.cpp.
References createProofRules(), d_instCount, d_rules, d_univs, CVCL::EXISTS, CVCL::FORALL, IF_DEBUG(), and CVCL::Theory::registerTheory().

TheoryQuant::~TheoryQuant ( )

Destructor.

Definition at line 79 of file theory_quant.cpp.
References d_contextMap, and d_rules.

Member Function Documentation

bool TheoryQuant::recursiveMap ( const Expr & term ) [private]

categorizes all the terms contained in an expressions by type.
Updates d_contextTerms, d_contextMap, d_contextCache accordingly. returns true if the expression does not contain bound variables, false otherwise.
Definition at line 1003 of file theory_quant.cpp.
References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BOUND_VAR, CVCL::ExprMap< Data >::count(), CVCL::CDMap< Key, Data, HashFcn >::count(), d_contextCache, d_contextMap, d_contextTerms, d_savedCache, CVCL::Expr::end(), CVCL::EXISTS, CVCL::FORALL, CVCL::Theory::getBaseType(), CVCL::Expr::getBody(), CVCL::TheoryCore::getCM(), CVCL::ContextManager::getCurrentContext(), CVCL::Expr::getKind(), CVCL::Type::isBool(), CVCL::CDList< T >::push_back(), CVCL::CDList< T >::size(), CVCL::Theory::theoryCore(), CVCL::Type::toString(), CVCL::Expr::toString(), and CVCL::TRACE.
Referenced by mapTermsByType().

void TheoryQuant::mapTermsByType ( const CDList< Expr > & terms ) [private]

categorizes all the terms contained in a vector of expressions by type.
Updates d_contextTerms, d_contextMap, d_contextCache accordingly.
Definition at line 975 of file theory_quant.cpp.
References CVCL::Theory::boolType(), d_contextMap, d_contextTerms, d_univs, CVCL::Theory::falseExpr(), CVCL::TheoryCore::getCM(), CVCL::ContextManager::getCurrentContext(), CVCL::CDList< T >::push_back(), recursiveMap(), CVCL::CDList< T >::size(), CVCL::Theory::theoryCore(), and CVCL::Theory::trueExpr().
Referenced by naiveCheckSat().

void TheoryQuant::instantiate ( Theorem univ,

bool all,

bool savedMap,

size_t newIndex

) [private]

Queues up all possible instantiations of bound variables.
The savedMap boolean indicates whether to use savedMap or d_contextMap the all boolean indicates weather to use all instantiation or only new ones and newIndex is the index where new instantiations begin.
Definition at line 890 of file theory_quant.cpp.
References d_contextTerms, d_savedTerms, recInstantiate(), CVCL::CDList< T >::size(), and CVCL::TRACE.
Referenced by naiveCheckSat().

void TheoryQuant::recInstantiate ( Theorem & univ,

bool all,

bool savedMap,

size_t newIndex,

std::vector< Expr > & varReplacements

) [private]

does most of the work of the instantiate function.

Definition at line 906 of file theory_quant.cpp.
References d_contextMap, d_contextTerms, d_instCount, d_insts, d_maxQuantInst, d_rules, d_savedMap, d_savedTerms, enqueueInst(), CVCL::Theory::getBaseType(), CVCL::Theorem::getExpr(), CVCL::Expr::getVars(), CVCL::CDList< T >::size(), CVCL::Theorem::toString(), CVCL::TRACE, and CVCL::QuantProofRules::universalInst().
Referenced by instantiate().

void TheoryQuant::findInstAssumptions ( const Theorem & thm ) [private]

A recursive function used to find instantiated universals in the hierarchy of assumptions.

Definition at line 1079 of file theory_quant.cpp.
References CVCL::Assumptions::begin(), CVCL::ExprMap< Data >::count(), d_insts, d_savedCache, d_savedMap, d_savedTerms, CVCL::Assumptions::end(), CVCL::Theorem::getAssumptionsRef(), CVCL::Theory::getBaseType(), CVCL::Theorem::getExpr(), CVCL::Theorem::isAssump(), CVCL::Theorem::isFlagged(), CVCL::Theorem::isNull(), CVCL::Theorem::setFlag(), and CVCL::TRACE.
Referenced by notifyInconsistent().

void TheoryQuant::synCheckSat ( bool ) [private]

Definition at line 655 of file theory_quant.cpp.
References d_callThisRound, d_instRound, d_savedTermsPos, d_univs, d_univsSavedPos, std::endl(), CVCL::TheoryCore::getCM(), CVCL::TheoryCore::getTerms(), CVCL::ContextManager::scopeLevel(), CVCL::CDO< T >::set(), CVCL::Theory::setIncomplete(), CVCL::CDList< T >::size(), synInst(), CVCL::Theory::theoryCore(), and CVCL::TRACE.
Referenced by checkSat().

void TheoryQuant::semCheckSat ( bool ) [private]

Definition at line 731 of file theory_quant.cpp.
References CVCL::Expr::arity(), cacheHead, canGetHead(), d_callThisRound, d_instRound, d_savedTermsPos, d_typeExprMap, d_univs, d_univsSavedPos, d_useAtomSem, std::endl(), CVCL::Theory::getBaseType(), CVCL::TheoryCore::getCM(), getHead(), CVCL::TheoryCore::getTerms(), CVCL::ContextManager::scopeLevel(), semInst(), CVCL::CDO< T >::set(), CVCL::Theory::setIncomplete(), CVCL::CDList< T >::size(), CVCL::Theory::theoryCore(), and CVCL::TRACE.
Referenced by checkSat().

void TheoryQuant::naiveCheckSat ( bool ) [private]

Definition at line 826 of file theory_quant.cpp.
References d_contextTerms, d_instCount, d_maxQuantInst, d_savedTerms, d_savedTermsPos, d_univs, d_univsContextPos, d_univsSavedPos, CVCL::CDO< T >::get(), CVCL::TheoryCore::getTerms(), IF_DEBUG(), instantiate(), CVCL::int2string(), mapTermsByType(), CVCL::CDO< T >::set(), CVCL::Theory::setIncomplete(), CVCL::CDList< T >::size(), CVCL::Theory::theoryCore(), and CVCL::TRACE.
Referenced by checkSat().

void TheoryQuant::synInst ( const Theorem & univ,

size_t tBegin

) [private]

Definition at line 557 of file theory_quant.cpp.
References d_rules, d_univsTriggers, enqueueInst(), genInstSetThm(), CVCL::Theorem::getExpr(), CVCL::Expr::getVars(), hasGoodSynInst(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::QuantProofRules::universalInst().
Referenced by synCheckSat().

void TheoryQuant::semInst ( const Theorem & univ,

size_t tBegin

) [private]

Definition at line 598 of file theory_quant.cpp.
References d_rules, d_univsTriggers, enqueueInst(), genInstSetThm(), CVCL::Theorem::getExpr(), CVCL::Expr::getVars(), hasGoodSemInst(), CVCL::Theorem::toString(), CVCL::Expr::toString(), CVCL::TRACE, and CVCL::QuantProofRules::universalInst().
Referenced by semCheckSat().

void TheoryQuant::goodSynMatch ( const Expr & e,

const std::vector< Expr > & boundVars,

std::set< std::vector< Expr > > & instSet,

size_t tBegin

) [private]

Definition at line 425 of file theory_quant.cpp.
References CVCL::Expr::arity(), canGetHead(), CVCL::ExprMap< Data >::clear(), CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), getHead(), CVCL::TheoryCore::getTerms(), recSynMatch(), CVCL::ExprMap< Data >::size(), CVCL::CDList< T >::size(), CVCL::Theory::theoryCore(), CVCL::Expr::toString(), and CVCL::TRACE.
Referenced by hasGoodSynInst().

bool TheoryQuant::recSynMatch ( const Expr & gterm,

const Expr & vterm,

ExprMap< Expr > & env

) [private]

Definition at line 338 of file theory_quant.cpp.
References CVCL::Expr::arity(), CVCL::BOUND_VAR, canGetHead(), CVCL::ExprMap< Data >::end(), CVCL::ExprMap< Data >::find(), getHead(), CVCL::Expr::getKind(), CVCL::Theory::simplifyExpr(), CVCL::Expr::toString(), and CVCL::TRACE.
Referenced by goodSynMatch().

bool TheoryQuant::hasGoodSynInst ( const Expr & e,

std::vector< Expr > & bVars,

std::set< std::vector< Expr > > & instSet,

size_t tBegin

) [private]

Definition at line 460 of file theory_quant.cpp.
References getBoundVars(), and goodSynMatch().
Referenced by synInst().

void TheoryQuant::recGoodSemMatch ( const Expr & e,

const std::vector< Expr > & bVars,

std::vector< Expr > & newInst,

std::set< std::vector< Expr > > & instSet

) [private]

Definition at line 306 of file theory_quant.cpp.
References d_typeExprMap, CVCL::Theory::getBaseType(), CVCL::Expr::hasFind(), CVCL::Theory::simplifyExpr(), CVCL::Expr::substExpr(), CVCL::Expr::toString(), and CVCL::TRACE.
Referenced by hasGoodSemInst().

bool TheoryQuant::hasGoodSemInst ( const Expr & e,

std::vector< Expr > & boundVars,

std::set< std::vector< Expr > > & instSet,

size_t tBegin

) [private]

find if a good instantiation can be get from a term e if found, return boundVars used and inseSet of all good instantiations
Definition at line 490 of file theory_quant.cpp.
References cacheHead, getBoundVars(), getHead(), inStrCache(), and recGoodSemMatch().
Referenced by semInst().

std::string TheoryQuant::getHead ( const Expr & e ) [private]

get the head string of function and array

Definition at line 105 of file theory_quant.cpp.
References std::endl(), CVCL::Op::getExpr(), CVCL::Expr::getKind(), CVCL::Expr::getName(), CVCL::Expr::getOp(), CVCL::Expr::toString(), and CVCL::UFUNC.
Referenced by goodSynMatch(), hasGoodSemInst(), recSynMatch(), and semCheckSat().

void TheoryQuant::setupTriggers ( const Theorem & thm ) [private]

Definition at line 214 of file theory_quant.cpp.
References d_univsTriggers, CVCL::Theorem::getExpr(), getSubTerms(), isGoodTrigger(), CVCL::ExprMap< Data >::size(), CVCL::Expr::toString(), and CVCL::TRACE.
Referenced by assertFact().

void TheoryQuant::enqueueInst ( const Theorem thm ) [private]

Definition at line 90 of file theory_quant.cpp.
References d_allInstCount, d_instThisRound, and CVCL::Theory::enqueueFact().
Referenced by recInstantiate(), semInst(), and synInst().

QuantProofRules * TheoryQuant::createProofRules ( )

Destructor.

Definition at line 47 of file quant_theorem_producer.cpp.
References CVCL::Theory::theoryCore().
Referenced by TheoryQuant().

void CVCL::TheoryQuant::addSharedTerm ( const Expr & e ) [inline, virtual]

Theory interface.

Reimplemented from CVCL::Theory.
Definition at line 206 of file theory_quant.h.

void TheoryQuant::assertFact ( const Theorem & e ) [virtual]

Theory interface function to assert quantified formulas.
pushes in negations and converts to either universally or existentially quantified theorems. Universals are stored in a database while existentials are enqueued to be handled by the search engine.
Implements CVCL::Theory.
Definition at line 257 of file theory_quant.cpp.
References CVCL::QuantProofRules::boundVarElim(), d_rules, d_univs, CVCL::Theory::enqueueFact(), CVCL::Theorem::getExpr(), CVCL::Theory::iffMP(), CVCL::Expr::isExists(), CVCL::Expr::isForall(), CVCL::Expr::isNot(), CVCL::CDList< T >::push_back(), CVCL::QuantProofRules::rewriteNotExists(), CVCL::QuantProofRules::rewriteNotForall(), setupTriggers(), CVCL::Expr::toString(), CVCL::Theorem::toString(), and CVCL::TRACE.

void TheoryQuant::checkSat ( bool fullEffort ) [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 CVCL::Theory.
Definition at line 639 of file theory_quant.cpp.
References d_instThisRound, d_useNew, d_useSemMatch, naiveCheckSat(), semCheckSat(), and synCheckSat().

void TheoryQuant::setup ( const Expr & e ) [virtual]

Set up the term e for call-backs when e or its children change.
setup is called once for each expression associated with the theory. It is typically used to setup theory-specific data for an expression and to add call-back information for use with update.
See also:
update

Reimplemented from CVCL::Theory.
Definition at line 87 of file theory_quant.cpp.

void TheoryQuant::update ( const Theorem & e,

const Expr & d

) [virtual]

Notify a theory of a new equality.
update is a call-back used by the notify mechanism of the core theory. It works as follows. When an equation t1 = t2 makes it into the core framework, the two find equivalence classes for t1 and t2 are merged. The result is that t2 is the new equivalence class representative and t1 is no longer an equivalence class representative. When this happens, the notify list of t1 is traversed. Notify list entries consist of a theory and an expression d. For each entry (i,d), i->update(e, d) is called, where e is the theorem corresponding to the equality t1=t2.
To add the entry (i,d) to a term t1's notify list, a call must be made to t1.addNotify(i,d). This is typically done in setup.

See also:
setup

Reimplemented from CVCL::Theory.
Definition at line 88 of file theory_quant.cpp.

void TheoryQuant::notifyInconsistent ( const Theorem & thm ) [virtual]

Used to notify the quantifier algorithm of possible instantiations that were used in proving a context inconsistent.

Reimplemented from CVCL::Theory.
Definition at line 1059 of file theory_quant.cpp.
References CVCL::Theorem::clearAllFlags(), d_savedTerms, d_univs, CVCL::FALSE, findInstAssumptions(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::CDList< T >::size(), CVCL::Theorem::toString(), and CVCL::TRACE.

void TheoryQuant::computeType ( const Expr & e ) [virtual]

computes the type of a quantified term. Always a boolean.

Reimplemented from CVCL::Theory.
Definition at line 1109 of file theory_quant.cpp.
References CVCL::EXISTS, CVCL::FORALL, CVCL::Expr::getBody(), CVCL::Expr::getKind(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::setType(), CVCL::Type::toString(), and CVCL::Expr::toString().

Expr TheoryQuant::computeTCC ( const Expr & e ) [virtual]

TCC(forall x.phi(x)) = (forall x. TCC(phi(x))) OR (exists x. TCC(phi(x)) & !phi(x)) TCC(exists x.phi(x)) = (forall x. TCC(phi(x))) OR (exists x. TCC(phi(x)) & phi(x))
Reimplemented from CVCL::Theory.
Definition at line 1140 of file theory_quant.cpp.
References CVCL::EXISTS, CVCL::FORALL, CVCL::Expr::getBody(), CVCL::Theory::getEM(), CVCL::Expr::getKind(), CVCL::Theory::getTCC(), CVCL::Expr::getVars(), CVCL::Expr::isQuantifier(), CVCL::ExprManager::newClosureExpr(), and CVCL::Expr::toString().

Expr TheoryQuant::parseExprOp ( const Expr & e ) [virtual]

Theory-specific parsing implemented by the DP.

Reimplemented from CVCL::Theory.
Definition at line 1272 of file theory_quant.cpp.
References CVCL::Theory::addBoundVar(), CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::EXISTS, CVCL::FORALL, CVCL::Theory::getEM(), CVCL::ExprManager::getKind(), CVCL::Expr::getKind(), CVCL::Expr::getString(), CVCL::ID, CVCL::ExprManager::newClosureExpr(), CVCL::Theory::parseExpr(), CVCL::RAW_LIST, CVCL::Expr::toString(), and CVCL::TRACE.

ExprStream & TheoryQuant::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 CVCL::Theory.
Definition at line 1155 of file theory_quant.cpp.
References CVCL::Theory::d_theoryUsed, CVCL::EXISTS, CVCL::FORALL, CVCL::Expr::getBody(), CVCL::Theory::getEM(), CVCL::Expr::getKind(), CVCL::Expr::getVars(), CVCL::Expr::isQuantifier(), CVCL::ExprStream::lang(), CVCL::LISP_LANG, CVCL::pop(), CVCL::popdag(), CVCL::PRESENTATION_LANG, CVCL::Expr::printAST(), CVCL::push(), CVCL::pushdag(), CVCL::SMTLIB_LANG, and CVCL::space().

Member Data Documentation

CDList<Theorem> CVCL::TheoryQuant::d_univs [private]

database of universally quantified theorems

Definition at line 65 of file theory_quant.h.
Referenced by assertFact(), mapTermsByType(), naiveCheckSat(), notifyInconsistent(), semCheckSat(), synCheckSat(), and TheoryQuant().

CDO<size_t> CVCL::TheoryQuant::d_savedTermsPos [private]

tracks a possition in the savedTerms map

Definition at line 68 of file theory_quant.h.
Referenced by naiveCheckSat(), semCheckSat(), and synCheckSat().

CDO<size_t> CVCL::TheoryQuant::d_univsSavedPos [private]

tracks a possition in the database of universals

Definition at line 70 of file theory_quant.h.
Referenced by naiveCheckSat(), semCheckSat(), and synCheckSat().

CDO<size_t> CVCL::TheoryQuant::d_univsPosFull [private]

tracks a possition in the database of universals

Definition at line 72 of file theory_quant.h.

CDO<size_t> CVCL::TheoryQuant::d_univsContextPos [private]

tracks a possition in the database of universals if fulleffort mode, the d_univsSavedPos now uesed when fulleffort=0 only.

Definition at line 75 of file theory_quant.h.
Referenced by naiveCheckSat().

CDO<int> CVCL::TheoryQuant::d_instCount [private]

number of instantiations made in given context

Definition at line 78 of file theory_quant.h.
Referenced by naiveCheckSat(), recInstantiate(), and TheoryQuant().

std::map<Type, CDList<size_t>* ,TypeComp> CVCL::TheoryQuant::d_contextMap [private]

a map of types to posisitions in the d_contextTerms list

Definition at line 81 of file theory_quant.h.
Referenced by mapTermsByType(), recInstantiate(), recursiveMap(), and ~TheoryQuant().

CDList<Expr> CVCL::TheoryQuant::d_contextTerms [private]

a list of all the terms appearing in the current context

Definition at line 83 of file theory_quant.h.
Referenced by instantiate(), mapTermsByType(), naiveCheckSat(), recInstantiate(), and recursiveMap().

CDMap<Expr, bool> CVCL::TheoryQuant::d_contextCache [private]

chache of expressions

Definition at line 84 of file theory_quant.h.
Referenced by recursiveMap().

typeMap CVCL::TheoryQuant::d_savedMap [private]

a map of types to positions in the d_savedTerms vector

Definition at line 87 of file theory_quant.h.
Referenced by findInstAssumptions(), and recInstantiate().

ExprMap<bool> CVCL::TheoryQuant::d_savedCache [private]

cache of expressions
Definition at line 88 of file theory_quant.h.
Referenced by findInstAssumptions(), and recursiveMap().

std::vector<Expr> CVCL::TheoryQuant::d_savedTerms [private]

a vector of all of the terms that have produced conflicts.

Definition at line 90 of file theory_quant.h.
Referenced by findInstAssumptions(), instantiate(), naiveCheckSat(), notifyInconsistent(), and recInstantiate().

ExprMap<std::vector<Expr> > CVCL::TheoryQuant::d_insts [private]

a map of instantiated universals to a vector of their instantiations

Definition at line 93 of file theory_quant.h.
Referenced by findInstAssumptions(), and recInstantiate().

QuantProofRules* CVCL::TheoryQuant::d_rules [private]

quantifier theorem production rules

Definition at line 96 of file theory_quant.h.
Referenced by assertFact(), recInstantiate(), semInst(), synInst(), TheoryQuant(), and ~TheoryQuant().

const int* CVCL::TheoryQuant::d_maxQuantInst [private]

Command line option.

Definition at line 98 of file theory_quant.h.
Referenced by naiveCheckSat(), and recInstantiate().

const bool* CVCL::TheoryQuant::d_useNew [private]

Definition at line 137 of file theory_quant.h.
Referenced by checkSat().

const bool* CVCL::TheoryQuant::d_useLazyInst [private]

Definition at line 138 of file theory_quant.h.

const bool* CVCL::TheoryQuant::d_useSemMatch [private]

Definition at line 139 of file theory_quant.h.
Referenced by checkSat().

const bool* CVCL::TheoryQuant::d_useAtomSem [private]

Definition at line 140 of file theory_quant.h.
Referenced by semCheckSat().

int CVCL::TheoryQuant::d_instThisRound [private]

Definition at line 142 of file theory_quant.h.
Referenced by checkSat(), and enqueueInst().

int CVCL::TheoryQuant::d_callThisRound [private]

Definition at line 143 of file theory_quant.h.
Referenced by semCheckSat(), and synCheckSat().

ExprMap<std::vector<Expr> > CVCL::TheoryQuant::d_univsTriggers [private]

Definition at line 145 of file theory_quant.h.
Referenced by semInst(), setupTriggers(), and synInst().

std::map<Type, std::vector<Expr>,TypeComp > CVCL::TheoryQuant::d_typeExprMap [private]

Definition at line 146 of file theory_quant.h.
Referenced by recGoodSemMatch(), and semCheckSat().

std::set<std::string> CVCL::TheoryQuant::cacheHead [private]

Definition at line 147 of file theory_quant.h.
Referenced by hasGoodSemInst(), and semCheckSat().

StatCounter CVCL::TheoryQuant::d_allInstCount [private]

Definition at line 149 of file theory_quant.h.
Referenced by enqueueInst().

CDO<int> CVCL::TheoryQuant::d_instRound [private]

Definition at line 150 of file theory_quant.h.
Referenced by semCheckSat(), and synCheckSat().

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

Generated on Thu Apr 13 16:57:44 2006 for CVC Lite by

1.4.4

CVCL::TheoryQuant Class Reference [Theories]