Expression Package
[Building Blocks]

Collaboration diagram for Expression Package:

Modules

• Smart Pointer Functionality in Expr
• Private methods

Classes

• class CVCL::Expr

  Data structure of expressions in CVC Lite. More...
  

• class CVCL::Expr::iterator

Enumerations

• enum CVCL::Expr::StaticFlagsEnum {
    CVCL::Expr::VALID_TYPE = 0x1, CVCL::Expr::VALID_IS_ATOMIC = 0x2, CVCL::Expr::IS_ATOMIC = 0x4, CVCL::Expr::REWRITE_NORMAL = 0x8,
    CVCL::Expr::IS_FINITE = 0x400, CVCL::Expr::WELL_FOUNDED = 0x800, CVCL::Expr::COMPUTE_TRANS_CLOSURE = 0x1000
  }

  bit-masks for static flags More...
  

• enum CVCL::Expr::DynamicFlagsEnum {
    CVCL::Expr::IMPLIED_LITERAL = 0x10, CVCL::Expr::IS_USER_ASSUMPTION = 0x20, CVCL::Expr::IS_INT_ASSUMPTION = 0x40, CVCL::Expr::IS_JUSTIFIED = 0x80,
    CVCL::Expr::IS_TRANSLATED = 0x100, CVCL::Expr::IS_USER_REGISTERED_ATOM = 0x200, CVCL::Expr::IS_SELECTED = 0x2000
  }

  bit-masks for dynamic flags More...
  

Functions

• CVCL::Expr::Expr (ExprValue *expr)

  Private constructor, simply wraps around the pointer.
  

• Expr CVCL::Expr::recursiveSubst (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const
• CVCL::Expr::Expr ()

  Default constructor creates the Null Expr.
  

• CVCL::Expr::Expr (const Expr &e)

  Copy constructor and assignment (copy the pointer and take care of the refcount).
  

• Expr & CVCL::Expr::operator= (const Expr &e)

  Assignment operator: take care of the refcounting and GC.
  

• CVCL::Expr::Expr (const Op &op, const Expr &child)
• CVCL::Expr::Expr (const Op &op, const Expr &child0, const Expr &child1)
• CVCL::Expr::Expr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)
• CVCL::Expr::Expr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2, const Expr &child3)
• CVCL::Expr::Expr (const Op &op, const std::vector< Expr > &children, ExprManager *em=NULL)
• CVCL::Expr::~Expr ()

  Destructor.
  

• Expr CVCL::Expr::eqExpr (const Expr &right) const
• Expr CVCL::Expr::notExpr () const
• Expr CVCL::Expr::negate () const
• Expr CVCL::Expr::andExpr (const Expr &right) const
• Expr CVCL::Expr::orExpr (const Expr &right) const
• Expr CVCL::Expr::iteExpr (const Expr &thenpart, const Expr &elsepart) const
• Expr CVCL::Expr::iffExpr (const Expr &right) const
• Expr CVCL::Expr::impExpr (const Expr &right) const
• Expr CVCL::Expr::skolemExpr (int i) const

  Create a Skolem constant for the i'th variable of an existential (*this).
  

• Expr CVCL::Expr::rebuild (ExprManager *em) const

  Rebuild Expr with a new ExprManager.
  

• Expr CVCL::Expr::substExpr (const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const
• Expr CVCL::Expr::substExpr (const ExprHashMap< Expr > &oldToNew) const
• Expr CVCL::Expr::operator! () const
• Expr CVCL::Expr::operator && (const Expr &right) const
• Expr CVCL::Expr::operator|| (const Expr &right) const
• static size_t CVCL::Expr::hash (const Expr &e)
• size_t CVCL::Expr::hash () const
• bool CVCL::Expr::isFalse () const
• bool CVCL::Expr::isTrue () const
• bool CVCL::Expr::isBoolConst () const
• bool CVCL::Expr::isVar () const
• bool CVCL::Expr::isBoundVar () const
• bool CVCL::Expr::isString () const
• bool CVCL::Expr::isClosure () const
• bool CVCL::Expr::isQuantifier () const
• bool CVCL::Expr::isLambda () const
• bool CVCL::Expr::isApply () const
• bool CVCL::Expr::isSymbol () const
• bool CVCL::Expr::isType () const

  Expr represents a type.
  

• const ExprValue * CVCL::Expr::getExprValue () const

  Provide access to ExprValue for client subclasses of ExprValue *only*.
  

• bool CVCL::Expr::isTerm () const

  Test if e is a term (as opposed to a predicate/formula).
  

• bool CVCL::Expr::isAtomic () const

  Test if e is atomic.
  

• bool CVCL::Expr::isAtomicFormula () const

  Test if e is an atomic formula.
  

• bool CVCL::Expr::isAbsAtomicFormula () const

  An abstract atomic formua is an atomic formula or a quantified formula.
  

• bool CVCL::Expr::isLiteral () const

  Test if e is a literal.
  

• bool CVCL::Expr::isAbsLiteral () const

  Test if e is an abstract literal.
  

• bool CVCL::Expr::isBoolConnective () const

  A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool).
  

• bool CVCL::Expr::isPropAtom () const

  True iff expr is not a Bool connective.
  

• bool CVCL::Expr::isPropLiteral () const

  PropAtom or negation of PropAtom.
  

• bool CVCL::Expr::isEq () const
• bool CVCL::Expr::isNot () const
• bool CVCL::Expr::isAnd () const
• bool CVCL::Expr::isOr () const
• bool CVCL::Expr::isITE () const
• bool CVCL::Expr::isIff () const
• bool CVCL::Expr::isImpl () const
• bool CVCL::Expr::isXor () const
• bool CVCL::Expr::isForall () const
• bool CVCL::Expr::isExists () const
• bool CVCL::Expr::isRational () const
• bool CVCL::Expr::isSkolem () const
• const std::string & CVCL::Expr::getName () const
• const std::string & CVCL::Expr::getUid () const

  For BOUND_VAR, get the UID.
  

• const std::string & CVCL::Expr::getString () const
• const std::vector< Expr > & CVCL::Expr::getVars () const

  Get bound variables from a closure Expr.
  

• const Expr & CVCL::Expr::getExistential () const

  Get the existential axiom expression for skolem constant.
  

• int CVCL::Expr::getBoundIndex () const

  Get the index of the bound var that skolem constant comes from.
  

• const Expr & CVCL::Expr::getBody () const

  Get the body of the closure Expr.
  

• const Rational & CVCL::Expr::getRational () const

  Get the Rational value out of RATIONAL_EXPR.
  

• ExprManager * CVCL::Expr::getEM () const
• const std::vector< Expr > & CVCL::Expr::getKids () const
• int CVCL::Expr::getKind () const
• ExprIndex CVCL::Expr::getIndex () const
• bool CVCL::Expr::hasLastIndex () const
• Op CVCL::Expr::mkOp () const

  Make the expr into an operator.
  

• Op CVCL::Expr::getOp () const

  Get operator from expression.
  

• Expr CVCL::Expr::getOpExpr () const

  Get expression of operator (for APPLY Exprs only).
  

• int CVCL::Expr::getOpKind () const

  Get kind of operator (for APPLY Exprs only).
  

• int CVCL::Expr::arity () const
• const Expr & CVCL::Expr::operator[] (int i) const
• const Expr & CVCL::Expr::unnegate () const

  Remove leading NOT if any.
  

• iterator CVCL::Expr::begin () const

  Begin iterator.
  

• iterator CVCL::Expr::end () const

  End iterator.
  

• bool CVCL::Expr::isNull () const
• bool CVCL::Expr::isInitialized () const
• size_t CVCL::Expr::getMMIndex () const

  Get the memory manager index (it uniquely identifies the subclass).
  

• bool CVCL::Expr::hasFind () const
• Theorem CVCL::Expr::getFind () const
• NotifyList * CVCL::Expr::getNotify () const
• const Type CVCL::Expr::getType () const

  Get the type. Recursively compute if necessary.
  

• const Type CVCL::Expr::lookupType () const

  Look up the current type. Do not recursively compute (i.e. may be NULL).
  

• const Expr CVCL::Expr::lookupTCC () const

  Look up the cached TCC (may return Null).
  

• const Theorem CVCL::Expr::lookupSubtypePred () const

  Look up the cached subtyping predicate (may return Null).
  

• bool CVCL::Expr::validSimpCache () const

  Return true if there is a valid cached value for calling simplify on this Expr.
  

• const Theorem & CVCL::Expr::getSimpCache () const
• bool CVCL::Expr::isValidType () const
• bool CVCL::Expr::validIsAtomicFlag () const
• bool CVCL::Expr::getIsAtomicFlag () const
• bool CVCL::Expr::isRewriteNormal () const
• bool CVCL::Expr::isFinite () const
• bool CVCL::Expr::isWellFounded () const
• bool CVCL::Expr::computeTransClosure () const
• bool CVCL::Expr::isImpliedLiteral () const
• bool CVCL::Expr::isUserAssumption () const
• bool CVCL::Expr::isIntAssumption () const
• bool CVCL::Expr::isJustified () const
• bool CVCL::Expr::isTranslated () const
• bool CVCL::Expr::isUserRegisteredAtom () const
• bool CVCL::Expr::isSelected () const
• bool CVCL::Expr::getFlag () const

  Check if the generic flag is set.
  

• void CVCL::Expr::setFlag () const

  Set the generic flag.
  

• void CVCL::Expr::clearFlags () const

  Clear the generic flag in all Exprs.
  

• std::string CVCL::Expr::toString () const

  Print the expression to a string.
  

• std::string CVCL::Expr::toString (InputLanguage lang) const

  Print the expression to a string using the given output language.
  

• void CVCL::Expr::print (InputLanguage lang, bool dagify=true) const

  Print the expression in the specified format.
  

• void CVCL::Expr::print () const

  Print the expression as AST (lisp-like format).
  

• void CVCL::Expr::printnodag () const

  Print the expression as AST without dagifying.
  

• void CVCL::Expr::pprint () const

  Pretty-print the expression.
  

• void CVCL::Expr::pprintnodag () const

  Pretty-print without dagifying.
  

• ExprStream & CVCL::Expr::print (ExprStream &os) const

  Print a leaf node.
  

• ExprStream & CVCL::Expr::printAST (ExprStream &os) const

  Print the top node and then recurse through the children */.
  

• Expr & CVCL::Expr::indent (int n, bool permanent=false)

  Set initial indentation to n.
  

• void CVCL::Expr::setFind (const Theorem &e) const

  Set the find attribute to e.
  

• void CVCL::Expr::addToNotify (Theory *i, const Expr &e) const

  Add (e,i) to the notify list of this expression.
  

• void CVCL::Expr::setType (const Type &t) const

  Set the cached type.
  

• void CVCL::Expr::setTCC (const Expr &tcc) const

  Set the cached TCC.
  

• void CVCL::Expr::setSubtypePred (const Theorem &pred) const

  Set the cached subtyping predicate.
  

• void CVCL::Expr::setSimpCache (const Theorem &e) const
• void CVCL::Expr::setValidType () const
• void CVCL::Expr::setIsAtomicFlag (bool value) const
• void CVCL::Expr::setRewriteNormal () const
• void CVCL::Expr::clearRewriteNormal () const
• void CVCL::Expr::setFinite () const
• void CVCL::Expr::setWellFounded () const
• void CVCL::Expr::setComputeTransClosure () const
• void CVCL::Expr::setImpliedLiteral () const
• void CVCL::Expr::setUserAssumption (int scope=-1) const
• void CVCL::Expr::setIntAssumption () const
• void CVCL::Expr::setJustified () const
• void CVCL::Expr::setTranslated (int scope=-1) const

  Set the translated flag for this Expr.
  

• void CVCL::Expr::setUserRegisteredAtom () const

  Set the UserRegisteredAtom flag for this Expr.
  

• void CVCL::Expr::setSelected () const

  Set the Selected flag for this Expr.
  

• bool CVCL::Expr::subExprOf (const Expr &e) const

  Check if the current Expr (*this) is a subexpression of e.
  

• int CVCL::Expr::getHeight () const
• int CVCL::Expr::getHighestKid () const
• bool CVCL::Expr::hasSimpFrom () const
• const Expr & CVCL::Expr::getSimpFrom () const
• void CVCL::Expr::setSimpFrom (const Expr &simpFrom)
• bool CVCL::Expr::hasSig () const
• bool CVCL::Expr::hasRep () const
• const Theorem & CVCL::Expr::getSig () const
• const Theorem & CVCL::Expr::getRep () const
• void CVCL::Expr::setSig (const Theorem &e) const
• void CVCL::Expr::setRep (const Theorem &e) const

Variables

• static Expr CVCL::Expr::s_null

  Convenient null expr.
  

• ExprValue * CVCL::Expr::d_expr

---

Enumeration Type Documentation

enum CVCL::Expr::StaticFlagsEnum [private, inherited]

bit-masks for static flags Enumerator: VALID_TYPE  Whether is valid TYPE expr. VALID_IS_ATOMIC  Whether IS_ATOMIC flag is valid (initialized). IS_ATOMIC  Whether the expression is an atomic term or formula. REWRITE_NORMAL  Expression is the result of a "normal" (idempotent) rewrite. IS_FINITE  Finite type. WELL_FOUNDED  Well-founded (used in datatypes). COMPUTE_TRANS_CLOSURE  Compute transitive closure (for binary uninterpreted predicates). Definition at line 145 of file expr.h.

enum CVCL::Expr::DynamicFlagsEnum [private, inherited]

bit-masks for dynamic flags Enumerator: IMPLIED_LITERAL  Whether expr has been added as an implied literal. IS_USER_ASSUMPTION  IS_INT_ASSUMPTION  IS_JUSTIFIED  IS_TRANSLATED  IS_USER_REGISTERED_ATOM  IS_SELECTED  Definition at line 164 of file expr.h.

---

Function Documentation

CVCL::Expr::Expr (  ExprValue *  expr  )  [inline, private, inherited]

Private constructor, simply wraps around the pointer. Definition at line 707 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::incRefcount().

Expr CVCL::Expr::recursiveSubst (  const ExprHashMap< Expr > &  subst, ExprHashMap< Expr > &  visited )  const [private, inherited]

Definition at line 53 of file expr.cpp. References CVCL::Expr::begin(), CVCL::ExprHashMap< Data >::begin(), CVCL::ExprHashMap< Data >::clear(), CVCL::Expr::clearFlags(), CVCL::ExprHashMap< Data >::count(), CVCL::Debug::counter(), CVCL::debugger, CVCL::Expr::end(), CVCL::ExprHashMap< Data >::end(), CVCL::ExprHashMap< Data >::erase(), CVCL::Expr::Expr(), CVCL::Expr::getBody(), CVCL::Expr::getEM(), CVCL::Expr::getFlag(), CVCL::Expr::getIndex(), CVCL::Expr::getKind(), CVCL::Expr::getOp(), CVCL::Expr::getVars(), IF_DEBUG(), CVCL::ExprHashMap< Data >::insert(), CVCL::Expr::isClosure(), CVCL::ExprManager::newClosureExpr(), CVCL::Expr::recursiveSubst(), and CVCL::Expr::setFlag(). Referenced by CVCL::Expr::recursiveSubst(), and CVCL::Expr::substExpr().

CVCL::Expr::Expr (   )  [inline, inherited]

Default constructor creates the Null Expr. Definition at line 266 of file expr.h. Referenced by CVCL::Expr::andExpr(), CVCL::Expr::eqExpr(), CVCL::Expr::iffExpr(), CVCL::Expr::impExpr(), CVCL::Expr::iteExpr(), CVCL::Expr::notExpr(), CVCL::Expr::orExpr(), and CVCL::Expr::recursiveSubst().

CVCL::Expr::Expr (  const Expr &  e  )  [inline, inherited]

Copy constructor and assignment (copy the pointer and take care of the refcount). Definition at line 709 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::incRefcount().

Expr & CVCL::Expr::operator= (  const Expr &  e  )  [inline, inherited]

Assignment operator: take care of the refcounting and GC. Definition at line 713 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::decRefcount(), and CVCL::ExprValue::incRefcount().

CVCL::Expr::Expr (  const Op &  op, const Expr &  child )  [inline, inherited]

Definition at line 724 of file expr.h. References CVCL::Expr::d_expr, CVCL::Expr::getEM(), CVCL::Op::getExpr(), CVCL::Op::getKind(), CVCL::ExprValue::incRefcount(), CVCL::Expr::isNull(), and CVCL::ExprManager::newExprValue().

CVCL::Expr::Expr (  const Op &  op, const Expr &  child0, const Expr &  child1 )  [inline, inherited]

Definition at line 738 of file expr.h. References CVCL::Expr::d_expr, CVCL::Expr::getEM(), CVCL::Op::getExpr(), CVCL::Op::getKind(), CVCL::ExprValue::incRefcount(), CVCL::Expr::isNull(), and CVCL::ExprManager::newExprValue().

CVCL::Expr::Expr (  const Op &  op, const Expr &  child0, const Expr &  child1, const Expr &  child2 )  [inline, inherited]

Definition at line 753 of file expr.h. References CVCL::Expr::d_expr, CVCL::Expr::getEM(), CVCL::Op::getExpr(), CVCL::Op::getKind(), CVCL::ExprValue::incRefcount(), CVCL::Expr::isNull(), and CVCL::ExprManager::newExprValue().

CVCL::Expr::Expr (  const Op &  op, const Expr &  child0, const Expr &  child1, const Expr &  child2, const Expr &  child3 )  [inline, inherited]

Definition at line 770 of file expr.h. References CVCL::Expr::d_expr, CVCL::Expr::getEM(), CVCL::Op::getExpr(), CVCL::Op::getKind(), CVCL::ExprValue::incRefcount(), CVCL::Expr::isNull(), and CVCL::ExprManager::newExprValue().

CVCL::Expr::Expr (  const Op &  op, const std::vector< Expr > &  children, ExprManager *  em = NULL )  [inline, inherited]

Definition at line 788 of file expr.h. References CVCL::Expr::d_expr, CVCL::Expr::getEM(), CVCL::Op::getExpr(), CVCL::Op::getKind(), CVCL::ExprValue::incRefcount(), CVCL::Expr::isNull(), and CVCL::ExprManager::newExprValue().

CVCL::Expr::~Expr (   )  [inline, inherited]

Destructor. Definition at line 861 of file expr.h. References CVCL::ExprManager::d_disableGC, CVCL::ExprValue::d_em, CVCL::Expr::d_expr, and CVCL::ExprValue::decRefcount().

Expr CVCL::Expr::eqExpr (  const Expr &  right  )  const [inline, inherited]

Definition at line 809 of file expr.h. References CVCL::EQ, and CVCL::Expr::Expr(). Referenced by TheoryCore::assertFormula(), TheoryCore::assignValue(), CVCL::BitvectorTheoremProducer::bitvectorFalseRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::TheoryArray::computeModel(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::VCL::eqExpr(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::VCCmd::evaluateCommand(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::ReflexivityTheoremValue::getExpr(), CVCL::RWTheoremValue::getExpr(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::ArrayTheoremProducer::interchangeIndices(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::multEqn(), TheoryCore::parseExprOp(), CVCL::TheoryArith::refineCounterExample(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::BitvectorTheoremProducer::typePredBit(), and CVCL::CommonTheoremProducer::varIntroRule().

Expr CVCL::Expr::notExpr (   )  const [inline, inherited]

Definition at line 813 of file expr.h. References CVCL::Expr::Expr(), and CVCL::NOT. Referenced by CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::Expr::negate(), and CVCL::Expr::operator!().

Expr CVCL::Expr::negate (   )  const [inline, inherited]

Definition at line 817 of file expr.h. References CVCL::Expr::isNot(), and CVCL::Expr::notExpr(). Referenced by CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::VCL::checkUnsat(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), CVCL::Circuit::Circuit(), CVCL::SearchEngineTheoremProducer::convertToCNF(), CVCL::VariableValue::getNegExpr(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::DecisionEngine::pushDecision(), CVCL::VCL::query(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CoreTheoremProducer::rewriteIteToIff(), and CVCL::CommonTheoremProducer::rewriteOr().

Expr CVCL::Expr::andExpr (  const Expr &  right  )  const [inline, inherited]

Definition at line 821 of file expr.h. References CVCL::AND, and CVCL::Expr::Expr(). Referenced by CVCL::BitvectorTheoremProducer::computeCarry(), CVCL::BitvectorTheoremProducer::computeCarryPreComputed(), CVCL::TheoryRecords::computeTCC(), CVCL::TheoryDatatype::computeTCC(), CVCL::TheoryArray::computeTCC(), CVCL::TheoryArith::computeTCC(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::Expr::operator &&(), CVCL::CoreTheoremProducer::orDistributivityRule(), TheoryCore::rewrite(), CVCL::CoreTheoremProducer::rewriteIteBool(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), and CVCL::BitvectorTheoremProducer::signBVLTRule().

Expr CVCL::Expr::orExpr (  const Expr &  right  )  const [inline, inherited]

Definition at line 831 of file expr.h. References CVCL::Expr::Expr(), and CVCL::OR. Referenced by CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::BitvectorTheoremProducer::computeCarryPreComputed(), CVCL::SearchEngineTheoremProducer::convertToCNF(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::Expr::operator||(), TheoryCore::rewrite(), CVCL::CoreTheoremProducer::rewriteIteBool(), and CVCL::BitvectorTheoremProducer::signBVLTRule().

Expr CVCL::Expr::iteExpr (  const Expr &  thenpart, const Expr &  elsepart )  const [inline, inherited]

Definition at line 841 of file expr.h. References CVCL::Expr::Expr(), and CVCL::ITE. Referenced by CVCL::CoreTheoremProducer::AndToIte(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::TheoryUF::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::ExprTransform::getNeg(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::ArrayTheoremProducer::interchangeIndices(), CVCL::ExprTransform::ite_reorder(), CVCL::VCL::iteExpr(), CVCL::CoreTheoremProducer::OrToIte(), TheoryCore::parseExprOp(), CVCL::Translator::preprocessRec(), TheoryCore::processCond(), CVCL::CoreTheoremProducer::rewriteIteBool(), and CVCL::ArrayTheoremProducer::rewriteReadWrite().

Expr CVCL::Expr::iffExpr (  const Expr &  right  )  const [inline, inherited]

Definition at line 845 of file expr.h. References CVCL::Expr::Expr(), and CVCL::IFF. Referenced by TheoryCore::assignValue(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitvectorFalseRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::ReflexivityTheoremValue::getExpr(), CVCL::RWTheoremValue::getExpr(), CVCL::CoreTheoremProducer::iffAndDistrib(), CVCL::VCL::iffExpr(), CVCL::CoreTheoremProducer::iffOrDistrib(), CVCL::ArrayTheoremProducer::interchangeIndices(), TheoryCore::rewrite(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::VCCmd::skolemizeAx(), CVCL::CommonTheoremProducer::skolemizeRewrite(), CVCL::CommonTheoremProducer::skolemizeRewriteVar(), and CVCL::CommonTheoremProducer::varIntroRule().

Expr CVCL::Expr::impExpr (  const Expr &  right  )  const [inline, inherited]

Definition at line 849 of file expr.h. References CVCL::Expr::Expr(), and CVCL::IMPLIES. Referenced by CVCL::VCL::impliesExpr(), CVCL::CommonTheoremProducer::implIntro(), and CVCL::ArrayTheoremProducer::rewriteSameStore().

Expr CVCL::Expr::skolemExpr (  int  i  )  const [inline, inherited]

Create a Skolem constant for the i'th variable of an existential (*this). Definition at line 853 of file expr.h. References CVCL::Expr::getEM(), and CVCL::ExprManager::newSkolemExpr(). Referenced by CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::CommonTheoremProducer::skolemize(), CVCL::VCCmd::skolemizeAx(), and CVCL::CommonTheoremProducer::skolemizeRewriteVar().

Expr CVCL::Expr::rebuild (  ExprManager *  em  )  const [inline, inherited]

Rebuild Expr with a new ExprManager. Definition at line 857 of file expr.h. References CVCL::ExprManager::rebuild().

Expr CVCL::Expr::substExpr (  const std::vector< Expr > &  oldTerms, const std::vector< Expr > &  newTerms )  const [inherited]

Referenced by CVCL::UFTheoremProducer::applyLambda(), CVCL::ArrayTheoremProducer::readArrayLiteral(), CVCL::TheoryQuant::recGoodSemMatch(), CVCL::CommonTheoremProducer::skolemize(), and CVCL::VCCmd::skolemizeAx().

Expr CVCL::Expr::substExpr (  const ExprHashMap< Expr > &  oldToNew  )  const [inherited]

Definition at line 178 of file expr.cpp. References CVCL::ExprHashMap< Data >::begin(), CVCL::Expr::clearFlags(), CVCL::ExprHashMap< Data >::end(), CVCL::Expr::recursiveSubst(), and CVCL::ExprHashMap< Data >::size().

Expr CVCL::Expr::operator! (   )  const [inline, inherited]

Definition at line 310 of file expr.h. References CVCL::Expr::notExpr().

Expr CVCL::Expr::operator && (  const Expr &  right  )  const [inline, inherited]

Definition at line 311 of file expr.h. References CVCL::Expr::andExpr().

Expr CVCL::Expr::operator|| (  const Expr &  right  )  const [inline, inherited]

Definition at line 312 of file expr.h. References CVCL::Expr::orExpr().

size_t CVCL::Expr::hash (  const Expr &  e  )  [inline, static, inherited]

Definition at line 867 of file expr.h. References CVCL::Expr::getEM(), and CVCL::ExprManager::hash(). Referenced by CVCL::ExprClosure::computeHash(), CVCL::VariableManager::HashLV::operator()(), and endif::hash< CVCL::Expr >::operator()().

size_t CVCL::Expr::hash (   )  const [inline, inherited]

Definition at line 873 of file expr.h. References CVCL::Expr::getEM(), and CVCL::ExprManager::hash(). Referenced by CVCL::Expr::print().

bool CVCL::Expr::isFalse (   )  const [inline, inherited]

Definition at line 328 of file expr.h. References CVCL::FALSE, and CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::SearchEngineFast::bcp(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::SearchSat::check(), CVCL::SearchSimple::checkValidRec(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), TheoryCore::enqueueFact(), CVCL::DecisionEngine::findSplitterRec(), CVCL::BitvectorTheoremProducer::generalIneqn(), SAT::CNF_Manager::getCNFLit(), CVCL::ExprTransform::getNeg(), CVCL::CommonTheoremProducer::iffFalseElim(), CVCL::Expr::isBoolConst(), CVCL::ExprTransform::ite_reorder(), CVCL::CNF_TheoremProducer::learnedClause(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::CoreTheoremProducer::NotToIte(), TheoryCore::processEquality(), CVCL::TheoryArith::processIntEq(), CVCL::SearchImplBase::processResult(), TheoryCore::processUpdates(), CVCL::TheoryArith::projectInequalities(), CVCL::SearchEngineTheoremProducer::proofByContradiction(), TheoryCore::registerAtom(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteToAnd(), CVCL::CoreTheoremProducer::rewriteIteToNot(), CVCL::CommonTheoremProducer::rewriteNotFalse(), CVCL::CommonTheoremProducer::rewriteOr(), TheoryCore::setupTerm(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), TheoryCore::simplifyOp(), and SAT::CNF_Manager::translateExprRec().

bool CVCL::Expr::isTrue (   )  const [inline, inherited]

Definition at line 329 of file expr.h. References CVCL::Expr::getKind(), and CVCL::TRUE. Referenced by TheoryCore::assertFactCore(), CVCL::SearchEngineFast::bcp(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::SearchSat::check(), CVCL::TheoryBitvector::checkSat(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchSimple::checkValidMain(), CVCL::SearchEngineFast::checkValidMain(), CVCL::SearchSimple::checkValidRec(), CVCL::TheoryBitvector::computeModel(), CVCL::SearchEngineFast::findSplitter(), CVCL::DecisionEngine::findSplitterRec(), CVCL::BitvectorTheoremProducer::generalIneqn(), SAT::CNF_Manager::getCNFLit(), CVCL::ExprTransform::getNeg(), CVCL::CommonTheoremProducer::iffTrueElim(), CVCL::Expr::isBoolConst(), CVCL::ExprTransform::ite_reorder(), CVCL::CoreTheoremProducer::NotToIte(), CVCL::TheoryArith::processBuffer(), TheoryCore::processUpdates(), CVCL::TheoryArith::projectInequalities(), TheoryCore::registerAtom(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CoreTheoremProducer::rewriteIteToImp(), CVCL::CoreTheoremProducer::rewriteIteToNot(), CVCL::CoreTheoremProducer::rewriteIteToOr(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::CommonTheoremProducer::rewriteNotTrue(), CVCL::CommonTheoremProducer::rewriteOr(), TheoryCore::setupTerm(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), TheoryCore::simplifyOp(), CVCL::SearchEngineFast::split(), SAT::CNF_Manager::translateExprRec(), and CVCL::TheoryUF::update().

bool CVCL::Expr::isBoolConst (   )  const [inline, inherited]

Definition at line 330 of file expr.h. References CVCL::Expr::isFalse(), and CVCL::Expr::isTrue(). Referenced by CVCL::TheoryBitvector::bitBlastTerm(), CVCL::SearchSat::check(), CVCL::TheoryBitvector::computeModel(), TheoryCore::computeModelBasic(), CVCL::SearchEngineFast::findSplitter(), CVCL::Expr::isAtomic(), CVCL::ExprTransform::ite_simplify(), TheoryCore::simplifyInPlaceRec(), and CVCL::SearchEngineFast::split().

bool CVCL::Expr::isVar (   )  const [inline, inherited]

Definition at line 880 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::isVar(). Referenced by CVCL::TypeComputerCore::computeType(), CVCL::Theory::getTCC(), CVCL::Theory::isLeaf(), CVCL::ExprTransform::ite_simplify(), CVCL::TheoremProducer::newPf(), CVCL::Expr::printAST(), recursiveGetSubTerm(), and CVCL::Theory::theoryOf().

bool CVCL::Expr::isBoundVar (   )  const [inline, inherited]

Definition at line 332 of file expr.h. References CVCL::BOUND_VAR, and CVCL::Expr::getKind().

bool CVCL::Expr::isString (   )  const [inline, inherited]

Definition at line 881 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::isString(). Referenced by CVCL::TheoryDatatype::checkType(), CVCL::VCCmd::evaluateCommand(), CVCL::Expr::getString(), CVCL::ExprTransform::ite_simplify(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryUF::print(), CVCL::TheoryDatatype::print(), TheoryCore::print(), CVCL::PrettyPrinterCore::print(), and CVCL::Expr::printAST().

bool CVCL::Expr::isClosure (   )  const [inline, inherited]

Definition at line 882 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::isClosure(). Referenced by CVCL::TheoryArray::computeType(), CVCL::VCCmd::findAxioms(), CVCL::Expr::getBody(), CVCL::Expr::getVars(), CVCL::isArrayLiteral(), CVCL::Expr::isLambda(), CVCL::Expr::isQuantifier(), CVCL::isTrivialExpr(), CVCL::Expr::printAST(), CVCL::ArrayTheoremProducer::readArrayLiteral(), recursiveGetBoundVars(), recursiveGetSubTerm(), and CVCL::Expr::recursiveSubst().

bool CVCL::Expr::isQuantifier (   )  const [inline, inherited]

Definition at line 883 of file expr.h. References CVCL::EXISTS, CVCL::FORALL, CVCL::Expr::getKind(), and CVCL::Expr::isClosure(). Referenced by CVCL::TheoryQuant::computeTCC(), CVCL::Expr::isAbsAtomicFormula(), CVCL::TheoryQuant::print(), and CVCL::Expr::print().

bool CVCL::Expr::isLambda (   )  const [inline, inherited]

Definition at line 886 of file expr.h. References CVCL::Expr::getKind(), CVCL::Expr::isClosure(), and CVCL::LAMBDA. Referenced by CVCL::UFTheoremProducer::applyLambda(), CVCL::TheoryUF::checkSat(), CVCL::TheoryUF::computeTCC(), CVCL::TheoryUF::print(), and CVCL::VCL::subtypeType().

bool CVCL::Expr::isApply (   )  const [inline, inherited]

Definition at line 889 of file expr.h. References CVCL::APPLY, CVCL::Expr::d_expr, CVCL::Expr::getKind(), and CVCL::ExprValue::isApply(). Referenced by CVCL::UFTheoremProducer::applyLambda(), CVCL::TheoryUF::assertFact(), CVCL::TheoryUF::computeType(), CVCL::TheoryDatatype::computeType(), CVCL::TypeComputerCore::computeType(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::TheoryBitvector::getBVMultParam(), CVCL::TheoryBitvector::getBVPlusParam(), CVCL::getConstructor(), CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::TheoryRecords::getField(), CVCL::TheoryRecords::getFields(), CVCL::TheoryBitvector::getFixedLeftShiftParam(), CVCL::TheoryBitvector::getFixedRightShiftParam(), CVCL::TheoryRecords::getIndex(), CVCL::Expr::getOp(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::TheoryBitvector::getSXIndex(), CVCL::TheoryBitvector::getTypePredType(), CVCL::isConstructor(), CVCL::TheoryRecords::isRecord(), CVCL::TheoryRecords::isRecordAccess(), CVCL::TheoryRecords::isRecordType(), CVCL::isSelector(), CVCL::isTester(), CVCL::TheoryRecords::isTuple(), CVCL::TheoryRecords::isTupleAccess(), CVCL::TheoryRecords::isTupleType(), CVCL::ExprTransform::ite_simplify(), TheoryCore::parseExpr(), CVCL::PrettyPrinterCore::print(), CVCL::TheoryBitvector::print(), CVCL::Expr::printAST(), CVCL::UFTheoremProducer::relToClosure(), CVCL::TheoryUF::rewrite(), CVCL::UFTheoremProducer::rewriteOpDef(), CVCL::Theory::theoryOf(), CVCL::TheoryUF::update(), CVCL::TheoryDatatypeLazy::update(), and CVCL::TheoryDatatype::update().

bool CVCL::Expr::isSymbol (   )  const [inline, inherited]

Definition at line 893 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::isSymbol(). Referenced by CVCL::TheoryUF::assertFact(), CVCL::TheoryUF::computeType(), CVCL::TheoryUF::print(), CVCL::TheoryDatatype::print(), CVCL::Expr::print(), and CVCL::Expr::printAST().

bool CVCL::Expr::isType (   )  const [inline, inherited]

Expr represents a type. Definition at line 894 of file expr.h. References CVCL::Expr::getEM(), CVCL::Expr::getOpKind(), and CVCL::ExprManager::isTypeKind(). Referenced by CVCL::TypeComputerCore::checkType().

const ExprValue * CVCL::Expr::getExprValue (   )  const [inline, inherited]

Provide access to ExprValue for client subclasses of ExprValue *only*. Definition at line 875 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::getExprValue(). Referenced by CVCL::computeBVConst(), CVCL::TheoryBitvector::getBVConstSize(), and CVCL::TheoryBitvector::getBVConstValue().

bool CVCL::Expr::isTerm (   )  const [inline, inherited]

Test if e is a term (as opposed to a predicate/formula). Definition at line 895 of file expr.h. References CVCL::Expr::getType(), and CVCL::Type::isBool(). Referenced by TheoryCore::assertEqualities(), TheoryCore::collectBasicVars(), CVCL::TheoryArith::isStale(), CVCL::ExprTransform::pushNegation(), CVCL::ExprTransform::pushNegationRec(), recursiveGetSubTerm(), CVCL::TheoryArith::rewrite(), CVCL::TheoryRecords::setup(), CVCL::TheoryArith::setup(), CVCL::TheoryBitvector::setupExpr(), TheoryCore::setupTerm(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), and CVCL::TheoryDatatype::solve().

bool CVCL::Expr::isAtomic (   )  const [inherited]

Test if e is atomic. An atomic expression is one that does not contain a formula (including not being a formula itself). See also: isAtomicFormula Definition at line 370 of file expr.cpp. References CVCL::Expr::arity(), CVCL::Expr::getIsAtomicFlag(), CVCL::Expr::getType(), CVCL::Expr::isBoolConst(), CVCL::Expr::setIsAtomicFlag(), CVCL::TRACE, and CVCL::Expr::validIsAtomicFlag(). Referenced by CVCL::DecisionEngine::findSplitterRec(), SAT::CNF_Manager::replaceITErec(), CVCL::TheoryArith::rewrite(), CVCL::TheoryArray::setup(), TheoryCore::setupSubFormulas(), TheoryCore::simplifyInPlaceRec(), and CVCL::TheoryArray::update().

bool CVCL::Expr::isAtomicFormula (   )  const [inherited]

Test if e is an atomic formula. An atomic formula is TRUE or FALSE or an application of a predicate (possibly 0-ary) which does not properly contain any formula. For instance, the formula "x = IF f THEN y ELSE z ENDIF is not an atomic formula, since it contains the condition "f", which is a formula. Definition at line 396 of file expr.cpp. References CVCL::AND, CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::EXISTS, CVCL::FORALL, CVCL::Expr::getKind(), CVCL::Expr::getType(), CVCL::IFF, CVCL::IMPLIES, CVCL::ITE, CVCL::NOT, CVCL::OR, CVCL::TRACE, and CVCL::XOR. Referenced by CVCL::Expr::isAbsAtomicFormula(), and CVCL::Expr::isLiteral().

bool CVCL::Expr::isAbsAtomicFormula (   )  const [inline, inherited]

An abstract atomic formua is an atomic formula or a quantified formula. Definition at line 365 of file expr.h. References CVCL::Expr::isAtomicFormula(), and CVCL::Expr::isQuantifier(). Referenced by CVCL::SearchSat::addLemma(), CVCL::SearchSat::check(), CVCL::SearchSat::findSplitterRec(), CVCL::DecisionEngine::findSplitterRec(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::Expr::isAbsLiteral(), TheoryCore::processUpdates(), TheoryCore::registerAtom(), TheoryCore::setupSubFormulas(), and SAT::CNF_Manager::translateExprRec().

bool CVCL::Expr::isLiteral (   )  const [inline, inherited]

Test if e is a literal. A literal is an atomic formula, or its negation. See also: isAtomicFormula Definition at line 370 of file expr.h. References CVCL::Expr::isAtomicFormula(), and CVCL::Expr::isNot().

bool CVCL::Expr::isAbsLiteral (   )  const [inline, inherited]

Test if e is an abstract literal. Definition at line 373 of file expr.h. References CVCL::Expr::isAbsAtomicFormula(), and CVCL::Expr::isNot(). Referenced by CVCL::SearchSat::addLemma(), CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::SearchImplBase::addSplitter(), CVCL::SearchEngineFast::addSplitter(), CVCL::SearchImplBase::applyCNFRules(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::SearchSat::assertLit(), CVCL::SearchEngineFast::bcp(), CVCL::SearchSat::check(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::Theorem::isAbsLiteral(), CVCL::SearchImplBase::isClause(), CVCL::SearchEngineFast::newIntAssumption(), CVCL::SearchSat::newUserAssumption(), CVCL::SearchEngineFast::propagate(), CVCL::DecisionEngine::pushDecision(), CVCL::SearchImplBase::replaceITE(), CVCL::TheoryArith::rewrite(), TheoryCore::rewriteLiteral(), TheoryCore::setupTerm(), TheoryCore::simplify(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), and CVCL::SearchEngineFast::updateLitCounts().

bool CVCL::Expr::isBoolConnective (   )  const [inline, inherited]

A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool). Definition at line 896 of file expr.h. References CVCL::AND, CVCL::Expr::getKind(), CVCL::Expr::getType(), CVCL::IFF, CVCL::IMPLIES, CVCL::ITE, CVCL::NOT, CVCL::OR, and CVCL::XOR. Referenced by CVCL::Expr::isPropAtom().

bool CVCL::Expr::isPropAtom (   )  const [inline, inherited]

True iff expr is not a Bool connective. Definition at line 378 of file expr.h. References CVCL::Expr::isBoolConnective(). Referenced by CVCL::Expr::isPropLiteral().

bool CVCL::Expr::isPropLiteral (   )  const [inline, inherited]

PropAtom or negation of PropAtom. Definition at line 380 of file expr.h. References CVCL::Expr::isNot(), and CVCL::Expr::isPropAtom(). Referenced by CVCL::SearchImplBase::applyCNFRules(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::SearchImplBase::isPropClause(), and CVCL::SearchImplBase::replaceITE().

bool CVCL::Expr::isEq (   )  const [inline, inherited]

Definition at line 383 of file expr.h. References CVCL::EQ, and CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::compare(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::BitvectorTheoremProducer::eqConst(), CVCL::TheoremProducer::newTheorem(), CVCL::TheoremProducer::newTheorem3(), CVCL::TheoryArith::normalize(), CVCL::TheoryArith::print(), CVCL::TheoryArith::printMinus(), CVCL::TheoryArith::printPlus(), CVCL::TheoryArith::printRational(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryArith::rewrite(), CVCL::TheoryBitvector::rewriteAtomic(), TheoryCore::rewriteCore(), TheoryCore::rewriteLiteral(), CVCL::CommonTheoremProducer::rewriteReflexivity(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::TheoryArray::setup(), CVCL::TheoryArith::setup(), CVCL::CommonTheoremProducer::skolemizeRewriteVar(), TheoryCore::solve(), CVCL::TheoryArray::solve(), CVCL::TheoryArith::solve(), CVCL::Theorem::Theorem(), and CVCL::Theory::theoryOf().

bool CVCL::Expr::isNot (   )  const [inline, inherited]

Definition at line 384 of file expr.h. References CVCL::Expr::getKind(), and CVCL::NOT. Referenced by CVCL::SearchImplBase::addToCNFCache(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryQuant::assertFact(), CVCL::TheoryDatatype::assertFact(), CVCL::TheoryArith::assertFact(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::SearchSat::check(), CVCL::Circuit::Circuit(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::SearchImplBase::findInCNFCache(), SAT::CNF_Manager::getCNFLit(), CVCL::Expr::isAbsLiteral(), CVCL::SearchImplBase::isGoodSplitter(), CVCL::Expr::isLiteral(), CVCL::Expr::isPropLiteral(), CVCL::Expr::negate(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::CommonTheoremProducer::notNotElim(), CVCL::CommonTheoremProducer::notToIff(), CVCL::CoreTheoremProducer::NotToIte(), CVCL::SearchImplBase::processResult(), CVCL::ExprTransform::pushNegation1(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::ExprTransform::pushNegationRec(), CVCL::Theorem::refutes(), TheoryCore::rewrite(), CVCL::TheoryBitvector::rewriteBoolean(), TheoryCore::rewriteCore(), TheoryCore::rewriteLiteral(), CVCL::CoreTheoremProducer::rewriteNotAnd(), CVCL::QuantTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotFalse(), CVCL::QuantTheoremProducer::rewriteNotForall(), CVCL::CommonTheoremProducer::rewriteNotForall(), CVCL::CoreTheoremProducer::rewriteNotIff(), CVCL::CoreTheoremProducer::rewriteNotIte(), CVCL::CommonTheoremProducer::rewriteNotNot(), CVCL::CoreTheoremProducer::rewriteNotOr(), CVCL::CommonTheoremProducer::rewriteNotTrue(), CVCL::TheoryArray::setup(), CVCL::TheoryArith::setup(), CVCL::VariableValue::setValue(), CVCL::SearchEngineFast::split(), CVCL::Theory::theoryOf(), SAT::CNF_Manager::translateExprRec(), CVCL::SearchEngineTheoremProducer::unitProp(), and CVCL::Expr::unnegate().

bool CVCL::Expr::isAnd (   )  const [inline, inherited]

Definition at line 385 of file expr.h. References CVCL::AND, and CVCL::Expr::getKind(). Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::CommonTheoremProducer::andElim(), CVCL::CoreTheoremProducer::AndToIte(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryArith::assertFact(), TheoryCore::assertFactCore(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::TheoryArith::isIntegerDerive(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::CoreTheoremProducer::orDistributivityRule(), CVCL::TheoryArith::processIntEq(), CVCL::TheoryArith::processSimpleIntEq(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CoreTheoremProducer::rewriteAndSubterms(), and CVCL::CoreTheoremProducer::rewriteNotAnd().

bool CVCL::Expr::isOr (   )  const [inline, inherited]

Definition at line 386 of file expr.h. References CVCL::Expr::getKind(), and CVCL::OR. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::TheoryArith::assertFact(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::ClauseValue::ClauseValue(), CVCL::SearchEngineTheoremProducer::conflictRule(), SAT::CNF_Manager::convertLemma(), CVCL::SearchEngineFast::fixConflict(), CVCL::SearchImplBase::isClause(), CVCL::SearchImplBase::isPropClause(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::CoreTheoremProducer::orDistributivityRule(), CVCL::CoreTheoremProducer::OrToIte(), TheoryCore::rewrite(), CVCL::CoreTheoremProducer::rewriteNotOr(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::CoreTheoremProducer::rewriteOrSubterms(), and CVCL::SearchEngineTheoremProducer::unitProp().

bool CVCL::Expr::isITE (   )  const [inline, inherited]

Definition at line 387 of file expr.h. References CVCL::Expr::getKind(), and CVCL::ITE. Referenced by CVCL::DecisionEngine::findSplitterRec(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::CoreTheoremProducer::rewriteIteCond(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteSame(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::CoreTheoremProducer::rewriteIteToAnd(), CVCL::CoreTheoremProducer::rewriteIteToIff(), CVCL::CoreTheoremProducer::rewriteIteToImp(), CVCL::CoreTheoremProducer::rewriteIteToNot(), CVCL::CoreTheoremProducer::rewriteIteToOr(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::CoreTheoremProducer::rewriteNotIte(), and TheoryCore::simplifyOp().

bool CVCL::Expr::isIff (   )  const [inline, inherited]

Definition at line 388 of file expr.h. References CVCL::Expr::getKind(), and CVCL::IFF. Referenced by CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::BitvectorTheoremProducer::bitvectorFalseRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::compare(), CVCL::CoreTheoremProducer::iffAndDistrib(), CVCL::CoreTheoremProducer::iffOrDistrib(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::TheoremProducer::newTheorem(), CVCL::TheoremProducer::newTheorem3(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteIff(), CVCL::CoreTheoremProducer::rewriteNotIff(), CVCL::CommonTheoremProducer::rewriteReflexivity(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::CommonTheoremProducer::skolemizeRewriteVar(), and CVCL::Theorem::Theorem().

bool CVCL::Expr::isImpl (   )  const [inline, inherited]

Definition at line 389 of file expr.h. References CVCL::Expr::getKind(), and CVCL::IMPLIES. Referenced by CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implMP(), CVCL::CoreTheoremProducer::ImpToIte(), and CVCL::CoreTheoremProducer::rewriteImplies().

bool CVCL::Expr::isXor (   )  const [inline, inherited]

Definition at line 390 of file expr.h. References CVCL::Expr::getKind(), and CVCL::XOR.

bool CVCL::Expr::isForall (   )  const [inline, inherited]

Definition at line 392 of file expr.h. References CVCL::FORALL, and CVCL::Expr::getKind(). Referenced by CVCL::TheoryQuant::assertFact(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::QuantTheoremProducer::rewriteNotForall(), and CVCL::CommonTheoremProducer::rewriteNotForall().

bool CVCL::Expr::isExists (   )  const [inline, inherited]

Definition at line 393 of file expr.h. References CVCL::EXISTS, and CVCL::Expr::getKind(). Referenced by CVCL::TheoryQuant::assertFact(), TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::SearchEngineFast::bcp(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::QuantTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::skolemize(), CVCL::CommonTheoremProducer::skolemizeRewrite(), CVCL::CommonTheoremProducer::skolemizeRewriteVar(), and CVCL::CommonTheoremProducer::varIntroSkolem().

bool CVCL::Expr::isRational (   )  const [inline, inherited]

Definition at line 395 of file expr.h. References CVCL::Expr::getKind(), and CVCL::RATIONAL_EXPR. Referenced by CVCL::TheoryArith::addToBuffer(), CVCL::TheoryArith::assertFact(), CVCL::TheoryArith::assignVariables(), CVCL::TheoryArith::canon(), CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonMultConstMult(), CVCL::ArithTheoremProducer::canonMultConstPlus(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::ArithTheoremProducer::canonPowConst(), CVCL::TheoryArith::computeType(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::ArithTheoremProducer::create_t2(), CVCL::ArithTheoremProducer::create_t3(), CVCL::TheoryArith::doSolve(), CVCL::VCCmd::evaluateCommand(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::Expr::getRational(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::ArithTheoremProducer::greaterthan(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::isIntegerConst(), CVCL::TheoryArith::isolateVariable(), CVCL::isRational(), CVCL::TheoryArith::isSyntacticRational(), CVCL::TheoryArith::isSyntacticUMinusVar(), CVCL::ExprTransform::ite_simplify(), CVCL::ArithTheoremProducer::multEqn(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::TheoryArith::normalize(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArith::rewrite(), CVCL::TheoryArith::rewriteToDiff(), and CVCL::TheoryArith::separateMonomial().

bool CVCL::Expr::isSkolem (   )  const [inline, inherited]

Definition at line 396 of file expr.h. References CVCL::Expr::getKind(), and CVCL::SKOLEM_VAR. Referenced by CVCL::VCCmd::findAxioms(), CVCL::Expr::getBoundIndex(), CVCL::Expr::getExistential(), and CVCL::TheoryArray::renameExpr().

const std::string & CVCL::Expr::getName (   )  const [inline, inherited]

Definition at line 916 of file expr.h. References CVCL::Expr::d_expr, and CVCL::Expr::isNull(). Referenced by CVCL::TheoryUF::assertFact(), CVCL::TheoryUF::computeType(), CVCL::TheoryRecords::getField(), CVCL::TheoryQuant::getHead(), CVCL::TheoryUF::print(), CVCL::TheoryDatatype::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::UFTheoremProducer::relToClosure(), and CVCL::UFTheoremProducer::relTrans().

const std::string & CVCL::Expr::getUid (   )  const [inline, inherited]

For BOUND_VAR, get the UID. Definition at line 961 of file expr.h. References CVCL::AST_LANG, CVCL::BOUND_VAR, CVCL::Expr::d_expr, CVCL::Expr::getKind(), CVCL::ExprValue::getUid(), and CVCL::Expr::toString(). Referenced by CVCL::Expr::print(), and CVCL::Expr::printAST().

const std::string & CVCL::Expr::getString (   )  const [inline, inherited]

Definition at line 921 of file expr.h. References CVCL::AST_LANG, CVCL::Expr::d_expr, CVCL::ExprValue::getString(), CVCL::Expr::isString(), and CVCL::Expr::toString(). Referenced by CVCL::VCCmd::evaluateCommand(), CVCL::RecordsTheoremProducer::expandRecord(), CVCL::TheoryRecords::getField(), TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), CVCL::TheoryDatatype::parseExprOp(), TheoryCore::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::TheoryUF::print(), CVCL::TheoryDatatype::print(), TheoryCore::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), and TheoryCore::processCond().

const std::vector< Expr > & CVCL::Expr::getVars (   )  const [inline, inherited]

Get bound variables from a closure Expr. Definition at line 928 of file expr.h. References CVCL::AST_LANG, CVCL::Expr::d_expr, CVCL::ExprValue::getVars(), CVCL::Expr::isClosure(), and CVCL::Expr::toString(). Referenced by CVCL::UFTheoremProducer::applyLambda(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::TheoryUF::computeTCC(), CVCL::TheoryQuant::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheoryArray::computeType(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::TheoryUF::print(), CVCL::TheoryQuant::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::ArrayTheoremProducer::readArrayLiteral(), CVCL::TheoryQuant::recInstantiate(), CVCL::Expr::recursiveSubst(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotForall(), CVCL::TheoryQuant::semInst(), CVCL::CommonTheoremProducer::skolemize(), CVCL::VCCmd::skolemizeAx(), CVCL::CommonTheoremProducer::skolemizeRewriteVar(), CVCL::VCL::subtypeType(), CVCL::TheoryQuant::synInst(), and CVCL::CommonTheoremProducer::varIntroSkolem().

const Expr & CVCL::Expr::getExistential (   )  const [inline, inherited]

Get the existential axiom expression for skolem constant. Definition at line 942 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::getExistential(), and CVCL::Expr::isSkolem(). Referenced by CVCL::VCCmd::findAxioms(), and CVCL::Expr::printAST().

int CVCL::Expr::getBoundIndex (   )  const [inline, inherited]

Get the index of the bound var that skolem constant comes from. Definition at line 947 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::getBoundIndex(), and CVCL::Expr::isSkolem().

const Expr & CVCL::Expr::getBody (   )  const [inline, inherited]

Get the body of the closure Expr. Definition at line 935 of file expr.h. References CVCL::AST_LANG, CVCL::Expr::d_expr, CVCL::ExprValue::getBody(), CVCL::Expr::isClosure(), and CVCL::Expr::toString(). Referenced by CVCL::UFTheoremProducer::applyLambda(), CVCL::QuantTheoremProducer::boundVarElim(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::TheoryUF::computeTCC(), CVCL::TheoryQuant::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheoryQuant::computeType(), CVCL::TheoryArray::computeType(), CVCL::VCCmd::findAxioms(), CVCL::TheoryUF::print(), CVCL::TheoryQuant::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::ArrayTheoremProducer::readArrayLiteral(), CVCL::QuantTheoremProducer::recFindBoundVars(), recursiveGetBoundVars(), recursiveGetSubTerm(), CVCL::TheoryQuant::recursiveMap(), CVCL::Expr::recursiveSubst(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotForall(), CVCL::CommonTheoremProducer::skolemize(), CVCL::VCCmd::skolemizeAx(), CVCL::CommonTheoremProducer::skolemizeRewriteVar(), and CVCL::VCL::subtypeType().

const Rational & CVCL::Expr::getRational (   )  const [inline, inherited]

Get the Rational value out of RATIONAL_EXPR. Definition at line 954 of file expr.h. References CVCL::AST_LANG, CVCL::Expr::d_expr, CVCL::ExprValue::getRational(), CVCL::Expr::isRational(), and CVCL::Expr::toString(). Referenced by CVCL::TheoryArith::addToBuffer(), CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonDivideConst(), CVCL::ArithTheoremProducer::canonDivideMult(), CVCL::ArithTheoremProducer::canonDivideVar(), CVCL::ArithTheoremProducer::canonInvertConst(), CVCL::ArithTheoremProducer::canonMultConstConst(), CVCL::ArithTheoremProducer::canonMultConstMult(), CVCL::ArithTheoremProducer::canonMultConstTerm(), CVCL::ArithTheoremProducer::canonMultLeafOrPowMult(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::ArithTheoremProducer::canonMultPowLeaf(), CVCL::ArithTheoremProducer::canonMultPowPow(), CVCL::ArithTheoremProducer::canonPowConst(), CVCL::TheoryArith::checkType(), CVCL::TheoryArith::computeNormalFactor(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryArith::computeType(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::create_t2(), CVCL::ArithTheoremProducer::create_t3(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::TheoryArith::doSolve(), CVCL::RefinedArithTheoremProducer::eval(), CVCL::VCCmd::evaluateCommand(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::TheoryArith::findRationalBound(), CVCL::TheoryArith::freeConstIneq(), CVCL::TheoryBitvector::getBitvectorTypeParam(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::TheoryBitvector::getBVMultParam(), CVCL::TheoryBitvector::getBVPlusParam(), CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::TheoryBitvector::getFixedLeftShiftParam(), CVCL::TheoryBitvector::getFixedRightShiftParam(), CVCL::TheoryRecords::getIndex(), CVCL::TheoryBitvector::getSXIndex(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::ArithTheoremProducer::greaterthan(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::isIntegerConst(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::isSyntacticRational(), CVCL::TheoryArith::isSyntacticUMinusVar(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::ArithTheoremProducer::multEqn(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::TheoryArith::normalize(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArith::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArith::rewrite(), CVCL::TheoryArith::rewriteToDiff(), CVCL::ArithTheoremProducer::splitGrayShadow(), CVCL::TheoryArith::updateStats(), and CVCL::TheoryArith::updateSubsumptionDB().

ExprManager * CVCL::Expr::getEM (   )  const [inline, inherited]

Definition at line 968 of file expr.h. References CVCL::ExprValue::d_em, and CVCL::Expr::d_expr. Referenced by CVCL::ExprStream::addLetHeader(), CVCL::Expr::addToNotify(), CVCL::arrayLiteral(), CVCL::Expr::begin(), CVCL::Expr::clearFlags(), TheoryCore::computeTypePred(), CVCL::TheoryArith::computeTypePred(), CVCL::Theory::computeTypePred(), CVCL::Expr::end(), CVCL::Expr::Expr(), CVCL::Expr::getFlag(), CVCL::Expr::getKids(), CVCL::Expr::getType(), CVCL::Expr::hash(), hf(), CVCL::Expr::indent(), CVCL::Expr::isType(), CVCL::ExprManager::newLeafExpr(), CVCL::ExprManager::newSkolemExpr(), CVCL::operator<<(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), TheoryCore::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::Expr::pprint(), CVCL::Expr::pprintnodag(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::ExprManager::rebuild(), CVCL::Expr::recursiveSubst(), CVCL::QuantTheoremProducer::rewriteNotExists(), CVCL::QuantTheoremProducer::rewriteNotForall(), CVCL::Expr::setFind(), CVCL::Expr::setFlag(), CVCL::Expr::setRep(), CVCL::Expr::setSig(), CVCL::Expr::setSimpCache(), CVCL::Expr::skolemExpr(), CVCL::Expr::toString(), CVCL::Type::Type(), and CVCL::Expr::validSimpCache().

const std::vector< Expr > & CVCL::Expr::getKids (   )  const [inline, inherited]

Definition at line 974 of file expr.h. References CVCL::Expr::d_expr, CVCL::Expr::getEM(), CVCL::ExprManager::getEmptyVector(), CVCL::ExprValue::getKids(), and CVCL::Expr::isNull(). Referenced by CVCL::CoreTheoremProducer::AndToIte(), CVCL::UFTheoremProducer::applyLambda(), CVCL::Expr::begin(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::Expr::end(), CVCL::VCCmd::evaluateCommand(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::TheoryRecords::getFields(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::ExprTransform::ite_convert(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::CoreTheoremProducer::OrToIte(), TheoryCore::rewrite(), CVCL::RecordsTheoremProducer::rewriteLitUpdate(), CVCL::UFTheoremProducer::rewriteOpDef(), CVCL::TheoryArith::separateMonomial(), and TheoryCore::simplifyInPlaceRec().

int CVCL::Expr::getKind (   )  const [inline, inherited]

Definition at line 980 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_kind, and CVCL::NULL_KIND. Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::TheoryDatatype::addSharedTerm(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryUF::assertFact(), CVCL::TheoryRecords::assertFact(), TheoryCore::assertFact(), CVCL::TheoryArith::assertFact(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractConstant(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), canGetHead(), CVCL::TheoryArith::canon(), CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonDivide(), CVCL::ArithTheoremProducer::canonFlattenSum(), CVCL::ArithTheoremProducer::canonInvert(), CVCL::ArithTheoremProducer::canonInvertMult(), CVCL::ArithTheoremProducer::canonInvertPow(), CVCL::ArithTheoremProducer::canonMult(), CVCL::ArithTheoremProducer::canonMultConstMult(), CVCL::ArithTheoremProducer::canonMultConstPlus(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::canonMultLeafOrPowMult(), CVCL::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::ArithTheoremProducer::canonMultPlusPlus(), CVCL::ArithTheoremProducer::canonMultPowLeaf(), CVCL::ArithTheoremProducer::canonMultPowPow(), CVCL::ArithTheoremProducer::canonPlus(), CVCL::ArithTheoremProducer::canonPowConst(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::TheoryUF::checkType(), CVCL::TheoryDatatype::checkType(), TheoryCore::checkType(), CVCL::TheoryArray::checkType(), CVCL::TheoryArith::checkType(), CVCL::TheoryUF::computeBaseType(), TheoryCore::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryArith::computeBaseType(), CVCL::computeBVConst(), CVCL::TheoryBitvector::computeBVConst(), CVCL::TheoryArray::computeModel(), CVCL::TheoryArray::computeModelTerm(), CVCL::TheoryArith::computeModelTerm(), CVCL::TheoryBitvector::computeNegBVConst(), CVCL::TheoryArith::computeNormalFactor(), CVCL::TheoryUF::computeTCC(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryQuant::computeTCC(), CVCL::TheoryDatatype::computeTCC(), TheoryCore::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), CVCL::TheoryQuant::computeType(), CVCL::TheoryDatatype::computeType(), TheoryCore::computeType(), CVCL::TypeComputerCore::computeType(), CVCL::TheoryArray::computeType(), CVCL::TheoryArith::computeType(), TheoryCore::computeTypePred(), CVCL::TheoryArith::computeTypePred(), CVCL::SearchEngineTheoremProducer::confAndrAF(), CVCL::SearchEngineTheoremProducer::confAndrAT(), CVCL::SearchEngineTheoremProducer::confIffr(), CVCL::SearchEngineTheoremProducer::confIterIfThen(), CVCL::SearchEngineTheoremProducer::confIterThenElse(), constantKids(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::SearchEngineTheoremProducer::convertToCNF(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::RefinedArithTheoremProducer::eval(), CVCL::VCCmd::evaluateCommand(), CVCL::VCCmd::evaluateNext(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::SearchSat::findSplitterRec(), CVCL::TheoryArith::freeConstIneq(), CVCL::TheoryBitvector::getBitvectorTypeParam(), CVCL::TheoryBitvector::getBVConstSize(), CVCL::TheoryBitvector::getBVConstValue(), CVCL::TheoryDatatype::getConsForTester(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryQuant::getHead(), CVCL::ExprTransform::getNeg(), CVCL::Expr::getOp(), CVCL::Expr::getOpKind(), CVCL::TheoryDatatype::getSelectorInfo(), CVCL::Theory::getTCC(), CVCL::Theory::getTypePred(), CVCL::Expr::getUid(), CVCL::ArithTheoremProducer::greaterthan(), CVCL::Expr::isAnd(), CVCL::Expr::isApply(), CVCL::isArray(), CVCL::isArrayLiteral(), CVCL::TheoryArith::isAtomicArithFormula(), CVCL::TheoryArith::isAtomicArithTerm(), CVCL::Expr::isAtomicFormula(), CVCL::Type::isBool(), CVCL::Expr::isBoolConnective(), CVCL::Expr::isBoundVar(), CVCL::isConstructor(), CVCL::isDarkShadow(), CVCL::isDatatype(), CVCL::isDivide(), CVCL::Expr::isEq(), CVCL::Expr::isExists(), CVCL::Expr::isFalse(), CVCL::Expr::isForall(), CVCL::Type::isFunction(), CVCL::isGE(), CVCL::isGrayShadow(), CVCL::isGT(), CVCL::Expr::isIff(), CVCL::Expr::isImpl(), CVCL::isInt(), CVCL::isIntPred(), CVCL::Expr::isITE(), CVCL::Expr::isLambda(), CVCL::isLE(), CVCL::isLT(), CVCL::isMinus(), CVCL::isMult(), CVCL::Expr::isNot(), CVCL::TheoryArith::isolateVariable(), CVCL::Expr::isOr(), CVCL::isPlus(), CVCL::Expr::isQuantifier(), CVCL::Expr::isRational(), CVCL::isRead(), CVCL::isReal(), CVCL::Expr::isSkolem(), CVCL::Type::isSubtype(), CVCL::isTrivialExpr(), CVCL::Expr::isTrue(), CVCL::isUMinus(), CVCL::isWrite(), CVCL::Expr::isXor(), CVCL::ExprTransform::ite_convert(), CVCL::ExprTransform::ite_reorder(), CVCL::ExprTransform::ite_simplify(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::ExprManager::newBoundVarExpr(), CVCL::TheoryArith::normalize(), CVCL::TheoryBitvector::normalizeBVArith(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::BitvectorTheoremProducer::notBVLTRule(), CVCL::TheoryQuant::notifyInconsistent(), CVCL::operator<<(), TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), CVCL::TheoryDatatype::parseExprOp(), TheoryCore::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::Translator::preprocessRec(), CVCL::TheoryUF::print(), CVCL::TheorySimulate::print(), CVCL::TheoryQuant::print(), CVCL::TheoryDatatype::print(), TheoryCore::print(), CVCL::PrettyPrinterCore::print(), CVCL::TheoryArray::print(), CVCL::TheoryArith::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::TheoryArith::printLhs(), CVCL::VCL::printV(), TheoryCore::processCond(), TheoryCore::processEquality(), CVCL::Circuit::propagate(), CVCL::SearchEngineTheoremProducer::propAndrAF(), CVCL::SearchEngineTheoremProducer::propAndrAT(), CVCL::SearchEngineTheoremProducer::propAndrLF(), CVCL::SearchEngineTheoremProducer::propAndrLRT(), CVCL::SearchEngineTheoremProducer::propAndrRF(), CVCL::SearchEngineTheoremProducer::propIffr(), CVCL::SearchEngineTheoremProducer::propIterIfThen(), CVCL::SearchEngineTheoremProducer::propIterIte(), CVCL::SearchEngineTheoremProducer::propIterThen(), CVCL::ExprTransform::pushNegation1(), CVCL::ArrayTheoremProducer::readArrayLiteral(), CVCL::ArithTheoremProducer::realShadow(), CVCL::QuantTheoremProducer::recFindBoundVars(), CVCL::TheoryQuant::recSynMatch(), recursiveGetBoundVars(), recursiveGetSubTerm(), CVCL::TheoryQuant::recursiveMap(), CVCL::Expr::recursiveSubst(), SAT::CNF_Manager::replaceITErec(), CVCL::TheoryUF::rewrite(), CVCL::TheorySimulate::rewrite(), TheoryCore::rewrite(), CVCL::TheoryArith::rewrite(), CVCL::TheoryRecords::rewriteAux(), CVCL::TheoryBitvector::rewriteBoolean(), CVCL::TheoryBitvector::rewriteBV(), CVCL::CoreTheoremProducer::rewriteConstDef(), CVCL::CommonTheoremProducer::rewriteIff(), CVCL::CoreTheoremProducer::rewriteLetDecl(), TheoryCore::rewriteLitCore(), CVCL::UFTheoremProducer::rewriteOpDef(), CVCL::TheoryArith::rewriteToDiff(), CVCL::ArithTheoremProducer::rightMinusLeft(), CVCL::TheoryUF::setup(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::TheoryBitvector::setup(), CVCL::TheoryArith::setup(), CVCL::TheoryBitvector::setupExpr(), CVCL::BitvectorTheoremProducer::signBVLTRule(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), TheoryCore::simplifyOp(), CVCL::TheoryBitvector::simplifyOp(), CVCL::TheoryBitvector::solve(), CVCL::Theory::theoryOf(), SAT::CNF_Manager::translateExprRec(), and CVCL::TheoryBitvector::update().

ExprIndex CVCL::Expr::getIndex (   )  const [inline, inherited]

Definition at line 985 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::d_index. Referenced by cf(), CVCL::compare(), CVCL::Expr::hasLastIndex(), CVCL::Expr::printAST(), and CVCL::Expr::recursiveSubst().

bool CVCL::Expr::hasLastIndex (   )  const [inline, inherited]

Definition at line 987 of file expr.h. References CVCL::ExprValue::d_em, CVCL::Expr::d_expr, CVCL::Expr::getIndex(), and CVCL::ExprManager::lastIndex(). Referenced by CVCL::Theorem::Theorem().

Op CVCL::Expr::mkOp (   )  const [inline, inherited]

Make the expr into an operator. Definition at line 990 of file expr.h. References CVCL::Expr::isNull(), and CVCL::Expr::Op. Referenced by CVCL::TheoryUF::computeTCC(), TheoryCore::computeTypePred(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::TheoryDatatype::getConstant(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), and CVCL::UFTheoremProducer::rewriteOpDef().

Op CVCL::Expr::getOp (   )  const [inline, inherited]

Get operator from expression. Definition at line 995 of file expr.h. References CVCL::Expr::arity(), CVCL::Expr::d_expr, CVCL::Expr::getKind(), CVCL::ExprValue::getOp(), CVCL::Expr::isApply(), CVCL::Expr::isNull(), and CVCL::Expr::Op. Referenced by CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::ArithTheoremProducer::canonMultConstPlus(), CVCL::TheoryArith::canonPred(), CVCL::TheoryArith::canonPredEquiv(), CVCL::TheoryUF::checkSat(), CVCL::TheoryBitvector::checkSat(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryDatatype::computeType(), CVCL::BitvectorTheoremProducer::concatFlatten(), CVCL::TheoryQuant::getHead(), CVCL::Expr::getOpExpr(), CVCL::Expr::getOpKind(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::ExprTransform::ite_convert(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::Translator::preprocessRec(), CVCL::TheoryUF::print(), CVCL::TheoryBitvector::print(), CVCL::Expr::printAST(), CVCL::ExprTransform::pushNegation1(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::Expr::recursiveSubst(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), TheoryCore::rewrite(), CVCL::CoreTheoremProducer::rewriteAndSubterms(), CVCL::TheoryBitvector::rewriteBV(), CVCL::CoreTheoremProducer::rewriteOrSubterms(), CVCL::ArithTheoremProducer::rightMinusLeft(), and CVCL::CommonTheoremProducer::skolemizeRewriteVar().

Expr CVCL::Expr::getOpExpr (   )  const [inline, inherited]

Get expression of operator (for APPLY Exprs only). Definition at line 1003 of file expr.h. References CVCL::Op::getExpr(), CVCL::Expr::getOp(), and CVCL::Expr::isApply(). Referenced by CVCL::UFTheoremProducer::applyLambda(), CVCL::TheoryUF::assertFact(), CVCL::TheoryDatatype::assertFact(), CVCL::TheoryDatatype::canCollapse(), CVCL::TheoryDatatype::checkSat(), CVCL::TheoryUF::computeType(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::TheoryBitvector::getBVMultParam(), CVCL::TheoryBitvector::getBVPlusParam(), CVCL::getConstructor(), CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::TheoryRecords::getField(), CVCL::TheoryRecords::getFields(), CVCL::TheoryBitvector::getFixedLeftShiftParam(), CVCL::TheoryBitvector::getFixedRightShiftParam(), CVCL::TheoryRecords::getIndex(), CVCL::TheoryBitvector::getSXIndex(), CVCL::TheoryBitvector::getTypePredType(), CVCL::DatatypeTheoremProducer::noCycle(), CVCL::TheoryUF::print(), CVCL::TheoryDatatype::print(), CVCL::UFTheoremProducer::relTrans(), CVCL::TheoryUF::rewrite(), CVCL::UFTheoremProducer::rewriteOpDef(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), CVCL::DatatypeTheoremProducer::rewriteTestCons(), CVCL::TheoryUF::update(), CVCL::TheoryDatatypeLazy::update(), and CVCL::TheoryDatatype::update().

int CVCL::Expr::getOpKind (   )  const [inline, inherited]

Get kind of operator (for APPLY Exprs only). Definition at line 1008 of file expr.h. References CVCL::Op::getExpr(), CVCL::Expr::getKind(), CVCL::Expr::getOp(), and CVCL::Expr::isApply(). Referenced by CVCL::BitvectorTheoremProducer::andZero(), CVCL::UFTheoremProducer::applyLambda(), CVCL::TheoryUF::assertFact(), CVCL::TheoryRecords::assertFact(), CVCL::TheoryDatatype::assertFact(), CVCL::TheoryBitvector::assertFact(), CVCL::TheoryBitvector::assertTypePred(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bitExtractRewrite(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::TheoryBitvector::BVSize(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), CVCL::BitvectorTheoremProducer::bvuminusBVMult(), CVCL::BitvectorTheoremProducer::bvuminusBVUminus(), CVCL::BitvectorTheoremProducer::bvuminusToBVPlus(), CVCL::BitvectorTheoremProducer::bvuminusVar(), CVCL::TheoryRecords::checkType(), CVCL::TheoryBitvector::checkType(), CVCL::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), CVCL::TheoryRecords::computeBaseType(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryBitvector::computeModel(), CVCL::TheoryRecords::computeModelTerm(), CVCL::TheoryBitvector::computeModelTerm(), CVCL::TheoryRecords::computeType(), CVCL::TheoryDatatype::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::TheoryRecords::computeTypePred(), CVCL::TheoryBitvector::computeTypePred(), CVCL::BitvectorTheoremProducer::concatConst(), CVCL::BitvectorTheoremProducer::concatFlatten(), CVCL::BitvectorTheoremProducer::concatMergeExtract(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::RecordsTheoremProducer::expandTuple(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::extractExtract(), CVCL::BitvectorTheoremProducer::extractWhole(), CVCL::TheoryBitvector::flattenBVPlus(), CVCL::BitvectorTheoremProducer::flattenBVPlus(), CVCL::BitvectorTheoremProducer::flipBVMult(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::TheoryBitvector::getBVMultParam(), CVCL::TheoryBitvector::getBVPlusParam(), CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::TheoryRecords::getField(), CVCL::TheoryRecords::getFields(), CVCL::TheoryBitvector::getFixedLeftShiftParam(), CVCL::TheoryBitvector::getFixedRightShiftParam(), CVCL::TheoryRecords::getIndex(), CVCL::TheoryBitvector::getSXIndex(), CVCL::TheoryBitvector::getTypePredExpr(), CVCL::TheoryBitvector::getTypePredType(), CVCL::isConstructor(), CVCL::TheoryRecords::isRecord(), CVCL::TheoryRecords::isRecordAccess(), CVCL::TheoryRecords::isRecordType(), CVCL::isSelector(), CVCL::isTester(), CVCL::TheoryRecords::isTuple(), CVCL::TheoryRecords::isTupleAccess(), CVCL::TheoryRecords::isTupleType(), CVCL::Expr::isType(), CVCL::BitvectorTheoremProducer::iteBVnegRule(), CVCL::BitvectorTheoremProducer::iteExtractRule(), CVCL::BitvectorTheoremProducer::leftShiftToConcat(), CVCL::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVCL::BitvectorTheoremProducer::negBVand(), CVCL::BitvectorTheoremProducer::negBVor(), CVCL::BitvectorTheoremProducer::negConcat(), CVCL::BitvectorTheoremProducer::negConst(), CVCL::BitvectorTheoremProducer::negNeg(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoryBitvector::newBVAndExpr(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVNandExpr(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newBVNorExpr(), CVCL::TheoryBitvector::newBVOrExpr(), CVCL::TheoryBitvector::newBVUminusExpr(), CVCL::TheoryBitvector::newBVXnorExpr(), CVCL::TheoryBitvector::newBVXorExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoryBitvector::newFixedLeftShiftExpr(), CVCL::TheoryBitvector::newFixedRightShiftExpr(), CVCL::TheoryBitvector::newSBVLEExpr(), CVCL::TheoryBitvector::newSBVLTExpr(), CVCL::TheoryBitvector::newSXExpr(), CVCL::TheoryBitvector::normalizeBVArith(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::BitvectorTheoremProducer::notBVLTRule(), CVCL::BitvectorTheoremProducer::oneCoeffBVMult(), CVCL::BitvectorTheoremProducer::orOne(), CVCL::TheoryBitvector::pad(), CVCL::BitvectorTheoremProducer::pad(), CVCL::BitvectorTheoremProducer::padBVLTRule(), CVCL::BitvectorTheoremProducer::padBVMult(), CVCL::TheoryBitvector::padBVPlus(), CVCL::BitvectorTheoremProducer::padBVPlus(), CVCL::BitvectorTheoremProducer::padSBVLTRule(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::print(), CVCL::TheoryBitvector::print(), CVCL::TheoryBitvector::pushNegation(), CVCL::UFTheoremProducer::relTrans(), CVCL::TheoryRecords::rewrite(), CVCL::TheoryBitvector::rewriteAtomic(), CVCL::TheoryBitvector::rewriteBV(), CVCL::TheoryBitvector::rewriteConst(), CVCL::RecordsTheoremProducer::rewriteLitSelect(), CVCL::RecordsTheoremProducer::rewriteLitUpdate(), CVCL::RecordsTheoremProducer::rewriteUpdateSelect(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), CVCL::BitvectorTheoremProducer::sameKidCheck(), CVCL::TheoryRecords::setup(), CVCL::TheoryBitvector::setup(), CVCL::TheoryBitvector::setupExpr(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::TheoryBitvector::signExtendBVLT(), CVCL::BitvectorTheoremProducer::signExtendRule(), CVCL::TheoryBitvector::simplifyOp(), CVCL::Theory::theoryOf(), CVCL::BitvectorTheoremProducer::typePredBit(), CVCL::TheoryUF::update(), CVCL::TheoryRecords::update(), CVCL::TheoryBitvector::update(), CVCL::BitvectorTheoremProducer::zeroCoeffBVMult(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

int CVCL::Expr::arity (   )  const [inline, inherited]

Definition at line 1013 of file expr.h. References CVCL::ExprValue::arity(), CVCL::Expr::d_expr, and CVCL::Expr::isNull(). Referenced by CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::CommonTheoremProducer::andElim(), CVCL::BitvectorTheoremProducer::andZero(), CVCL::SearchImplBase::applyCNFRules(), CVCL::UFTheoremProducer::applyLambda(), CVCL::Type::arity(), CVCL::TheoryUF::assertFact(), CVCL::TheoryArith::assertFact(), TheoryCore::assertFactCore(), CVCL::Expr::begin(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvMultAssocRule(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::TheoryDatatype::canCollapse(), CVCL::TheoryArith::canon(), CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonInvertMult(), CVCL::ArithTheoremProducer::canonMult(), CVCL::ArithTheoremProducer::canonMultConstMult(), CVCL::ArithTheoremProducer::canonMultConstPlus(), CVCL::ArithTheoremProducer::canonMultLeafOrPowMult(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::ArithTheoremProducer::canonPowConst(), CVCL::TheoryArith::canonPred(), CVCL::TheoryArith::canonPredEquiv(), CVCL::TheoryUF::checkType(), CVCL::TheoryDatatype::checkType(), TheoryCore::checkType(), CVCL::TheoryArray::checkType(), CVCL::TheoryArith::checkType(), CVCL::Circuit::Circuit(), CVCL::ClauseValue::ClauseValue(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), TheoryCore::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryRecords::computeModelTerm(), CVCL::TheoryArith::computeNormalFactor(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), CVCL::TheoryRecords::computeType(), CVCL::TheoryDatatype::computeType(), TheoryCore::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::TheoryArray::computeType(), CVCL::TheoryArith::computeType(), CVCL::TheoryRecords::computeTypePred(), CVCL::BitvectorTheoremProducer::concatConst(), CVCL::BitvectorTheoremProducer::concatFlatten(), CVCL::BitvectorTheoremProducer::concatMergeExtract(), CVCL::SearchEngineTheoremProducer::conflictRule(), constantKids(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::Expr::end(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::RefinedArithTheoremProducer::eval(), CVCL::VCCmd::evaluateCommand(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::extractExtract(), CVCL::BitvectorTheoremProducer::extractWhole(), CVCL::VCCmd::findAxioms(), CVCL::DecisionEngine::findSplitterRec(), CVCL::BitvectorTheoremProducer::flattenBVPlus(), CVCL::BitvectorTheoremProducer::flipBVMult(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::TheoryDatatype::getConstant(), CVCL::Expr::getOp(), CVCL::TheoryQuant::goodSynMatch(), CVCL::ArithTheoremProducer::greaterthan(), CVCL::CoreTheoremProducer::iffAndDistrib(), CVCL::CoreTheoremProducer::iffOrDistrib(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implMP(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::Expr::isAtomic(), CVCL::TheoryArith::isAtomicArithTerm(), CVCL::TheoryArith::isIntegerDerive(), CVCL::isTrivialExpr(), CVCL::ExprTransform::ite_convert(), CVCL::BitvectorTheoremProducer::iteBVnegRule(), CVCL::BitvectorTheoremProducer::iteExtractRule(), CVCL::TheoryArith::kidsCanonical(), CVCL::Theory::leavesAreSimp(), CVCL::BitvectorTheoremProducer::leftShiftToConcat(), CVCL::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::BitvectorTheoremProducer::negBVand(), CVCL::BitvectorTheoremProducer::negBVor(), CVCL::BitvectorTheoremProducer::negConcat(), CVCL::BitvectorTheoremProducer::negConst(), CVCL::BitvectorTheoremProducer::negNeg(), CVCL::DatatypeTheoremProducer::noCycle(), CVCL::TheoryBitvector::normalizeBVArith(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::BitvectorTheoremProducer::oneCoeffBVMult(), CVCL::Expr::operator[](), CVCL::CoreTheoremProducer::orDistributivityRule(), CVCL::BitvectorTheoremProducer::orOne(), CVCL::BitvectorTheoremProducer::padBVLTRule(), CVCL::BitvectorTheoremProducer::padBVMult(), CVCL::BitvectorTheoremProducer::padBVPlus(), CVCL::BitvectorTheoremProducer::padSBVLTRule(), TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), CVCL::TheoryDatatype::parseExprOp(), TheoryCore::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::Translator::preprocessRec(), CVCL::TheoryUF::print(), CVCL::TheorySimulate::print(), CVCL::TheoryRecords::print(), CVCL::TheoryDatatype::print(), TheoryCore::print(), CVCL::TheoryBitvector::print(), CVCL::TheoryArray::print(), CVCL::TheoryArith::print(), CVCL::Expr::print(), CVCL::TheoryArith::printLhs(), CVCL::TheoryArith::printPlus(), CVCL::VCL::printV(), TheoryCore::processCond(), TheoryCore::processEquality(), CVCL::TheoryArith::processIntEq(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::Circuit::propagate(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::TheoryQuant::recSynMatch(), CVCL::TheoryQuant::recursiveMap(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), CVCL::TheoryRecords::rewrite(), TheoryCore::rewrite(), CVCL::CoreTheoremProducer::rewriteAndSubterms(), CVCL::TheoryRecords::rewriteAux(), CVCL::TheoryBitvector::rewriteBV(), CVCL::CoreTheoremProducer::rewriteIteCond(), TheoryCore::rewriteLiteral(), TheoryCore::rewriteN(), CVCL::UFTheoremProducer::rewriteOpDef(), CVCL::CoreTheoremProducer::rewriteOrSubterms(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), CVCL::TheoryQuant::semCheckSat(), CVCL::TheoryArith::separateMonomial(), CVCL::TheoryRecords::setup(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::TheoryBitvector::setup(), CVCL::TheoryArray::setup(), CVCL::TheoryArith::setup(), CVCL::Theory::setupCC(), CVCL::TheoryBitvector::setupExpr(), CVCL::TheoryArith::setupRec(), TheoryCore::setupSubFormulas(), TheoryCore::setupTerm(), CVCL::BitvectorTheoremProducer::signBVLTRule(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), TheoryCore::simplifyOp(), CVCL::TheoryBitvector::simplifyOp(), CVCL::Theory::simplifyOp(), CVCL::TheoryArith::substAndCanonize(), CVCL::SearchEngineTheoremProducer::unitProp(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryArray::update(), CVCL::Theory::updateCC(), CVCL::Theory::updateHelper(), CVCL::TheoryArith::updateSubsumptionDB(), and CVCL::BitvectorTheoremProducer::zeroCoeffBVMult().

const Expr & CVCL::Expr::operator[] (  int  i  )  const [inline, inherited]

Definition at line 1018 of file expr.h. References CVCL::Expr::arity(), CVCL::Expr::d_expr, and CVCL::ExprValue::getKids().

const Expr& CVCL::Expr::unnegate (   )  const [inline, inherited]

Remove leading NOT if any. Definition at line 458 of file expr.h. References CVCL::Expr::isNot(). Referenced by TheoryCore::assertFact(), CVCL::SearchSat::check(), CVCL::SearchSat::getImplication(), and CVCL::SearchSat::getImpliedLiteral().

Expr::iterator CVCL::Expr::begin (   )  const [inherited]

Begin iterator. Definition at line 447 of file expr.cpp. References CVCL::Expr::arity(), CVCL::Expr::getEM(), and CVCL::Expr::getKids(). Referenced by CVCL::TheoryArith::addToBuffer(), CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonFlattenSum(), CVCL::ArithTheoremProducer::canonMult(), CVCL::ArithTheoremProducer::canonMultConstMult(), CVCL::ArithTheoremProducer::canonMultConstPlus(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::canonMultLeafOrPowMult(), CVCL::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::ArithTheoremProducer::canonMultPlusPlus(), CVCL::ArithTheoremProducer::canonPlus(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::TheoryUF::checkType(), CVCL::TheoryRecords::checkType(), CVCL::ClauseValue::ClauseValue(), CVCL::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVCL::ExprStream::collectShared(), CVCL::TheoryBitvector::collectSharedSubterms(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryBitvector::computeModelTerm(), CVCL::TheoryArith::computeModelTerm(), TheoryCore::computeTCC(), CVCL::Theory::computeTCC(), CVCL::TheoryRecords::computeType(), CVCL::TheoryDatatype::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::BitvectorTheoremProducer::concatFlatten(), constantKids(), SAT::CNF_Manager::convertLemma(), CVCL::SearchEngineTheoremProducer::convertToCNF(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::VCCmd::evaluateCommand(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::VCCmd::findAxioms(), CVCL::TheoryBitvector::flattenBVPlus(), CVCL::ArithTheoremProducer::greaterthan(), CVCL::Expr::isAtomicFormula(), CVCL::SearchImplBase::isClause(), CVCL::Theory::isLeafIn(), CVCL::SearchImplBase::isPropClause(), CVCL::TheoryArith::isStale(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::BitvectorTheoremProducer::negBVand(), CVCL::BitvectorTheoremProducer::negBVor(), CVCL::BitvectorTheoremProducer::negConcat(), CVCL::CoreTheoremProducer::orDistributivityRule(), CVCL::BitvectorTheoremProducer::padBVPlus(), TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), TheoryCore::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::pickMonomial(), CVCL::TheoryUF::print(), CVCL::TheoryDatatype::print(), CVCL::TheoryBitvector::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::QuantTheoremProducer::recFindBoundVars(), CVCL::TheoryRecords::recordExpr(), recursiveGetBoundVars(), recursiveGetSubTerm(), CVCL::TheoryQuant::recursiveMap(), CVCL::Expr::recursiveSubst(), SAT::CNF_Manager::replaceITErec(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::TheoryBitvector::rewriteBoolean(), CVCL::CoreTheoremProducer::rewriteNotAnd(), CVCL::CoreTheoremProducer::rewriteNotOr(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::TheoryRecords::setup(), CVCL::subExprRec(), CVCL::ArithTheoremProducer::substitute(), TheoryCore::subtypePredicate(), SAT::CNF_Manager::translateExprRec(), and CVCL::TheoryArith::updateSubsumptionDB().

Expr::iterator CVCL::Expr::end (   )  const [inherited]

End iterator. Definition at line 455 of file expr.cpp. References CVCL::Expr::arity(), CVCL::Expr::getEM(), and CVCL::Expr::getKids(). Referenced by CVCL::TheoryArith::addToBuffer(), CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::SearchImplBase::applyCNFRules(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonFlattenSum(), CVCL::ArithTheoremProducer::canonMult(), CVCL::ArithTheoremProducer::canonMultConstMult(), CVCL::ArithTheoremProducer::canonMultConstPlus(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::canonMultLeafOrPowMult(), CVCL::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVCL::ArithTheoremProducer::canonMultPlusPlus(), CVCL::ArithTheoremProducer::canonPlus(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::TheoryUF::checkType(), CVCL::TheoryRecords::checkType(), CVCL::ClauseValue::ClauseValue(), CVCL::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVCL::ExprStream::collectShared(), CVCL::TheoryBitvector::collectSharedSubterms(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryBitvector::computeModelTerm(), CVCL::TheoryArith::computeModelTerm(), TheoryCore::computeTCC(), CVCL::Theory::computeTCC(), CVCL::TheoryRecords::computeType(), CVCL::TheoryDatatype::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::BitvectorTheoremProducer::concatFlatten(), constantKids(), SAT::CNF_Manager::convertLemma(), CVCL::SearchEngineTheoremProducer::convertToCNF(), CVCL::SearchImplBase::enqueueCNFrec(), CVCL::VCCmd::evaluateCommand(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::VCCmd::findAxioms(), CVCL::TheoryBitvector::flattenBVPlus(), CVCL::ArithTheoremProducer::greaterthan(), CVCL::Expr::isAtomicFormula(), CVCL::SearchImplBase::isClause(), CVCL::Theory::isLeafIn(), CVCL::SearchImplBase::isPropClause(), CVCL::TheoryArith::isStale(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::BitvectorTheoremProducer::negBVand(), CVCL::BitvectorTheoremProducer::negBVor(), CVCL::BitvectorTheoremProducer::negConcat(), CVCL::CoreTheoremProducer::orDistributivityRule(), CVCL::BitvectorTheoremProducer::padBVPlus(), TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), TheoryCore::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::pickMonomial(), CVCL::TheoryUF::print(), CVCL::TheoryDatatype::print(), CVCL::TheoryBitvector::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryBitvector::pushNegationRec(), CVCL::QuantTheoremProducer::recFindBoundVars(), recursiveGetBoundVars(), recursiveGetSubTerm(), CVCL::TheoryQuant::recursiveMap(), CVCL::Expr::recursiveSubst(), SAT::CNF_Manager::replaceITErec(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::TheoryBitvector::rewriteBoolean(), CVCL::CoreTheoremProducer::rewriteNotAnd(), CVCL::CoreTheoremProducer::rewriteNotOr(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::TheoryRecords::setup(), CVCL::subExprRec(), CVCL::ArithTheoremProducer::substitute(), TheoryCore::subtypePredicate(), SAT::CNF_Manager::translateExprRec(), and CVCL::TheoryArith::updateSubsumptionDB().

bool CVCL::Expr::isNull (   )  const [inline, inherited]

Definition at line 1023 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_kind, and CVCL::NULL_KIND. Referenced by CVCL::SearchSat::addLemma(), CVCL::Expr::addToNotify(), CVCL::Expr::arity(), CVCL::TheoryUF::assertFact(), CVCL::SearchSat::assertLit(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::SearchSat::check(), CVCL::SearchSimple::checkValidRec(), CVCL::ExprManager::clear(), CVCL::Expr::clearFlags(), CVCL::Expr::clearRewriteNormal(), CVCL::TheoryArray::computeModel(), CVCL::TheoryUF::computeType(), CVCL::TypeComputerCore::computeType(), CVCL::ExprManager::computeType(), CVCL::VCCmd::evaluateCommand(), CVCL::VCCmd::evaluateNext(), CVCL::Expr::Expr(), CVCL::ExprApply::ExprApply(), CVCL::SearchEngineFast::findSplitter(), CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineDFS::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), CVCL::DecisionEngine::findSplitterRec(), CVCL::SearchEngineFast::fixConflict(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::Theory::getBaseType(), CVCL::TheoryDatatype::getConstant(), CVCL::ReflexivityTheoremValue::getExpr(), CVCL::RWTheoremValue::getExpr(), CVCL::Expr::getFlag(), CVCL::Expr::getKids(), CVCL::Expr::getMMIndex(), CVCL::Expr::getName(), CVCL::VariableValue::getNegExpr(), CVCL::Expr::getNotify(), CVCL::Expr::getOp(), CVCL::Expr::getRep(), CVCL::Expr::getSig(), CVCL::Theory::getTCC(), CVCL::Expr::getType(), CVCL::Expr::hasFind(), CVCL::ExprManager::hash(), CVCL::Expr::hasRep(), CVCL::Expr::hasSig(), CVCL::Expr::hasSimpFrom(), CVCL::Expr::indent(), CVCL::Type::isNull(), CVCL::Proof::isNull(), CVCL::ExprTransform::ite_simplify(), CVCL::Expr::lookupSubtypePred(), CVCL::Expr::lookupTCC(), CVCL::Expr::lookupType(), CVCL::Expr::mkOp(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::ExprManager::newLeafExpr(), CVCL::Op::Op(), CVCL::operator<<(), TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), CVCL::Expr::pprint(), CVCL::Expr::pprintnodag(), CVCL::TheoryArith::print(), CVCL::Expr::print(), CVCL::Expr::printAST(), CVCL::TheoryArith::printMinus(), CVCL::TheoryArith::printPlus(), CVCL::TheoryArith::printRational(), CVCL::ExprManager::rebuild(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::Expr::setComputeTransClosure(), CVCL::Expr::setFind(), CVCL::Expr::setFinite(), CVCL::Expr::setFlag(), CVCL::Expr::setImpliedLiteral(), CVCL::Expr::setIntAssumption(), CVCL::Expr::setIsAtomicFlag(), CVCL::Expr::setJustified(), CVCL::Expr::setRep(), CVCL::Expr::setRewriteNormal(), CVCL::Expr::setSelected(), CVCL::Expr::setSig(), CVCL::Expr::setSimpCache(), CVCL::Expr::setSubtypePred(), CVCL::Expr::setTCC(), CVCL::Expr::setTranslated(), CVCL::Expr::setType(), CVCL::Expr::setUserAssumption(), CVCL::Expr::setUserRegisteredAtom(), CVCL::Expr::setValidType(), CVCL::Expr::setWellFounded(), CVCL::SearchEngineFast::split(), CVCL::Theory::theoryOf(), CVCL::Expr::toString(), CVCL::Type::Type(), CVCL::TheoryDatatypeLazy::update(), and CVCL::TheoryDatatype::update().

bool CVCL::Expr::isInitialized (   )  const [inline, inherited]

Definition at line 469 of file expr.h. References CVCL::Expr::d_expr.

size_t CVCL::Expr::getMMIndex (   )  const [inline, inherited]

Get the memory manager index (it uniquely identifies the subclass). Definition at line 1027 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::getMMIndex(), and CVCL::Expr::isNull().

bool CVCL::Expr::hasFind (   )  const [inline, inherited]

Definition at line 1032 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_find, CVCL::CDO< T >::get(), CVCL::Theorem::isNull(), and CVCL::Expr::isNull(). Referenced by TheoryCore::assertFactCore(), TheoryCore::assertFormula(), CVCL::TheoryArith::canonSimplify(), CVCL::SearchSimple::checkValidRec(), CVCL::Theory::find(), CVCL::Theory::findExpr(), CVCL::Expr::getFind(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::TheoryDatatypeLazy::mergeLabels(), CVCL::TheoryDatatype::mergeLabels(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryQuant::recGoodSemMatch(), CVCL::TheoryRecords::rewriteAux(), CVCL::TheoryBitvector::rewriteAux(), CVCL::TheoryBitvector::rewriteBV(), TheoryCore::rewriteCore(), CVCL::TheoryRecords::setup(), CVCL::TheoryBitvector::setupExpr(), CVCL::TheoryArith::setupRec(), TheoryCore::setupTerm(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), CVCL::TheoryRecords::update(), CVCL::TheoryBitvector::update(), and CVCL::TheoryArith::update().

Theorem CVCL::Expr::getFind (   )  const [inline, inherited]

Definition at line 1037 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_find, CVCL::CDO< T >::get(), and CVCL::Expr::hasFind(). Referenced by CVCL::Theory::find(), CVCL::Theory::leavesAreSimp(), CVCL::TheoryRecords::rewriteAux(), TheoryCore::simplifyFullRec(), and TheoryCore::simplifyInPlaceRec().

NotifyList * CVCL::Expr::getNotify (   )  const [inline, inherited]

Definition at line 1042 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_notifyList, and CVCL::Expr::isNull(). Referenced by CVCL::Expr::addToNotify(), TheoryCore::assertEqualities(), and TheoryCore::assertFormula().

const Type CVCL::Expr::getType (   )  const [inline, inherited]

Get the type. Recursively compute if necessary. Definition at line 1047 of file expr.h. References CVCL::ExprManager::computeType(), CVCL::Expr::d_expr, CVCL::ExprValue::d_type, CVCL::Expr::getEM(), CVCL::Type::isNull(), CVCL::Expr::isNull(), and CVCL::Expr::s_null. Referenced by CVCL::TheoryDatatype::addSharedTerm(), CVCL::CoreTheoremProducer::AndToIte(), CVCL::VCL::assertFormula(), TheoryCore::assignValue(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::SearchSat::check(), CVCL::TheoryDatatype::checkSat(), TheoryCore::checkType(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), TheoryCore::computeBaseType(), CVCL::TheoryUF::computeModel(), CVCL::TheoryBitvector::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryRecords::computeModelTerm(), CVCL::TheoryBitvector::computeModelTerm(), CVCL::TheoryArray::computeModelTerm(), CVCL::TheoryUF::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheoryRecords::computeType(), CVCL::TheoryQuant::computeType(), TheoryCore::computeType(), CVCL::TypeComputerCore::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::TheoryArray::computeType(), CVCL::TheoryArith::computeType(), CVCL::ExprManager::computeType(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::Theory::getBaseType(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatype::getConstant(), CVCL::ReflexivityTheoremValue::getExpr(), CVCL::RWTheoremValue::getExpr(), CVCL::VCL::getType(), CVCL::CommonTheoremProducer::iffContrapositive(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::CoreTheoremProducer::ImpToIte(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::ArrayTheoremProducer::interchangeIndices(), CVCL::Expr::isAtomic(), CVCL::Expr::isAtomicFormula(), CVCL::Expr::isBoolConnective(), CVCL::isConstructor(), CVCL::TheoryArith::isIntegerThm(), CVCL::Expr::isTerm(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::TheoryDatatypeLazy::mergeLabels(), CVCL::TheoryDatatype::mergeLabels(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoryBitvector::newBVAndExpr(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVNandExpr(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newBVNorExpr(), CVCL::TheoryBitvector::newBVOrExpr(), CVCL::TheoryBitvector::newBVUminusExpr(), CVCL::TheoryBitvector::newBVXnorExpr(), CVCL::TheoryBitvector::newBVXorExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoryBitvector::newFixedLeftShiftExpr(), CVCL::TheoryBitvector::newFixedRightShiftExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoryBitvector::newSBVLEExpr(), CVCL::TheoryBitvector::newSBVLTExpr(), CVCL::TheoryBitvector::newSXExpr(), CVCL::DatatypeTheoremProducer::noCycle(), CVCL::CoreTheoremProducer::NotToIte(), CVCL::CoreTheoremProducer::OrToIte(), CVCL::TheoryBitvector::pad(), CVCL::BitvectorTheoremProducer::pad(), TheoryCore::print(), CVCL::VCL::printV(), TheoryCore::processUpdates(), CVCL::TheoryBitvector::pushNegation(), CVCL::VCL::query(), CVCL::TheoryArith::refineCounterExample(), CVCL::CommonTheoremProducer::reflexivityRule(), SAT::CNF_Manager::replaceITErec(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::TheoryUF::rewrite(), TheoryCore::rewrite(), CVCL::CoreTheoremProducer::rewriteIteBool(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteSame(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), TheoryCore::setupTerm(), CVCL::BitvectorTheoremProducer::signExtendRule(), CVCL::VCL::simplifyThm(), CVCL::VCL::simplifyThm2(), CVCL::VCL::subtypeType(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::CommonTheoremProducer::transitivityRule(), CVCL::CoreTheoremProducer::typePred(), CVCL::CommonTheoremProducer::varIntroRule(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

const Type CVCL::Expr::lookupType (   )  const [inline, inherited]

Look up the current type. Do not recursively compute (i.e. may be NULL). Definition at line 1053 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_type, CVCL::Expr::isNull(), and CVCL::Expr::s_null. Referenced by CVCL::TheoryDatatype::computeType(), CVCL::TypeComputerCore::computeType(), TheoryCore::computeTypePred(), CVCL::Theory::getBaseType(), and CVCL::ExprManager::newBoundVarExpr().

const Expr CVCL::Expr::lookupTCC (   )  const [inline, inherited]

Look up the cached TCC (may return Null). Definition at line 1058 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_tcc, CVCL::Expr::isNull(), and CVCL::Expr::s_null. Referenced by CVCL::Theory::getTCC().

const Theorem CVCL::Expr::lookupSubtypePred (   )  const [inline, inherited]

Look up the cached subtyping predicate (may return Null). Definition at line 1063 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_subtypePred, and CVCL::Expr::isNull(). Referenced by TheoryCore::subtypePredicate().

bool CVCL::Expr::validSimpCache (   )  const [inline, inherited]

Return true if there is a valid cached value for calling simplify on this Expr. Definition at line 1068 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_simpCacheTag, CVCL::Expr::getEM(), and CVCL::ExprManager::getSimpCacheTag(). Referenced by TheoryCore::simplifyFullRec(), and TheoryCore::simplifyInPlaceRec().

const Theorem & CVCL::Expr::getSimpCache (   )  const [inline, inherited]

Definition at line 1072 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::d_simpCache. Referenced by TheoryCore::simplifyFullRec(), and TheoryCore::simplifyInPlaceRec().

bool CVCL::Expr::isValidType (   )  const [inline, inherited]

Definition at line 1076 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::VALID_TYPE. Referenced by CVCL::ExprManager::checkType().

bool CVCL::Expr::validIsAtomicFlag (   )  const [inline, inherited]

Definition at line 1080 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::VALID_IS_ATOMIC. Referenced by CVCL::Expr::isAtomic().

bool CVCL::Expr::getIsAtomicFlag (   )  const [inline, inherited]

Definition at line 1084 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IS_ATOMIC. Referenced by CVCL::Expr::isAtomic().

bool CVCL::Expr::isRewriteNormal (   )  const [inline, inherited]

Definition at line 1088 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::REWRITE_NORMAL. Referenced by TheoryCore::rewriteCore().

bool CVCL::Expr::isFinite (   )  const [inline, inherited]

Definition at line 1092 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IS_FINITE. Referenced by CVCL::TheoryDatatype::checkSat(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryDatatypeLazy::instantiate(), and CVCL::TheoryDatatype::instantiate().

bool CVCL::Expr::isWellFounded (   )  const [inline, inherited]

Definition at line 1096 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::WELL_FOUNDED. Referenced by CVCL::TheoryDatatype::getConstant().

bool CVCL::Expr::computeTransClosure (   )  const [inline, inherited]

Definition at line 1100 of file expr.h. References CVCL::Expr::COMPUTE_TRANS_CLOSURE, CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, and CVCL::CDFlags::get(). Referenced by CVCL::TheoryUF::assertFact(), and CVCL::TheoryUF::update().

bool CVCL::Expr::isImpliedLiteral (   )  const [inline, inherited]

Definition at line 1104 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IMPLIED_LITERAL. Referenced by TheoryCore::processUpdates(), and TheoryCore::registerAtom().

bool CVCL::Expr::isUserAssumption (   )  const [inline, inherited]

Definition at line 1108 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IS_USER_ASSUMPTION. Referenced by CVCL::SearchSat::assertLit(), CVCL::SearchSat::check(), and CVCL::SearchSat::isAssumption().

bool CVCL::Expr::isIntAssumption (   )  const [inline, inherited]

Definition at line 1112 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IS_INT_ASSUMPTION. Referenced by CVCL::SearchSat::assertLit(), and CVCL::SearchSat::isAssumption().

bool CVCL::Expr::isJustified (   )  const [inline, inherited]

Definition at line 1116 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IS_JUSTIFIED. Referenced by CVCL::SearchSat::checkJustified().

bool CVCL::Expr::isTranslated (   )  const [inline, inherited]

Definition at line 1120 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IS_TRANSLATED. Referenced by SAT::CNF_Manager::getCNFLit(), CVCL::TheoryDatatypeLazy::instantiate(), and SAT::CNF_Manager::translateExprRec().

bool CVCL::Expr::isUserRegisteredAtom (   )  const [inline, inherited]

Definition at line 1124 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IS_USER_REGISTERED_ATOM. Referenced by CVCL::SearchSat::getImplication(), and CVCL::SearchSat::getImpliedLiteral().

bool CVCL::Expr::isSelected (   )  const [inline, inherited]

Definition at line 1128 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::CDFlags::get(), and CVCL::Expr::IS_SELECTED. Referenced by CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), and CVCL::TheoryDatatype::update().

bool CVCL::Expr::getFlag (   )  const [inline, inherited]

Check if the generic flag is set. Definition at line 1132 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_flag, CVCL::Expr::getEM(), and CVCL::Expr::isNull(). Referenced by recursiveGetBoundVars(), recursiveGetSubTerm(), CVCL::Expr::recursiveSubst(), and CVCL::subExprRec().

void CVCL::Expr::setFlag (   )  const [inline, inherited]

Set the generic flag. Definition at line 1137 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_flag, CVCL::Expr::getEM(), CVCL::ExprManager::getFlag(), and CVCL::Expr::isNull(). Referenced by recursiveGetBoundVars(), recursiveGetSubTerm(), CVCL::Expr::recursiveSubst(), and CVCL::subExprRec().

void CVCL::Expr::clearFlags (   )  const [inline, inherited]

Clear the generic flag in all Exprs. Definition at line 1142 of file expr.h. References CVCL::ExprManager::clearFlags(), CVCL::Expr::getEM(), and CVCL::Expr::isNull(). Referenced by getBoundVars(), getSubTerms(), CVCL::Expr::recursiveSubst(), CVCL::Expr::subExprOf(), and CVCL::Expr::substExpr().

string CVCL::Expr::toString (   )  const [inherited]

Print the expression to a string. Definition at line 195 of file expr.cpp. References CVCL::Expr::isNull(). Referenced by CVCL::TheoryArith::VarOrderGraph::addEdge(), CVCL::SearchEngineFast::addLiteralFact(), CVCL::SearchImplBase::addSplitter(), CVCL::SearchEngineFast::addSplitter(), CVCL::SearchImplBase::addToCNFCache(), CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::CoreTheoremProducer::AndToIte(), CVCL::BitvectorTheoremProducer::andZero(), CVCL::SearchImplBase::applyCNFRules(), CVCL::UFTheoremProducer::applyLambda(), CVCL::RefinedArithTheoremProducer::arithmetic(), TheoryCore::assertEqualities(), CVCL::TheoryUF::assertFact(), CVCL::TheoryRecords::assertFact(), CVCL::TheoryQuant::assertFact(), CVCL::TheoryArith::assertFact(), TheoryCore::assertFactCore(), CVCL::VCL::assertFormula(), CVCL::TheoryBitvector::assertTypePred(), TheoryCore::assignValue(), CVCL::Theory::assignValue(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::BitvectorTheoremProducer::bitBlastEqnRule(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractBVPlus(), CVCL::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVCL::BitvectorTheoremProducer::bitExtractConcatenation(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), CVCL::BitvectorTheoremProducer::bitExtractExtraction(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bitExtractNot(), CVCL::BitvectorTheoremProducer::bitExtractRewrite(), CVCL::BitvectorTheoremProducer::bitExtractToExtract(), CVCL::BitvectorTheoremProducer::bitvectorFalseRule(), CVCL::BitvectorTheoremProducer::bitvectorTrueRule(), CVCL::BitvectorTheoremProducer::bitwiseConcat(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::QuantTheoremProducer::boundVarElim(), TheoryCore::buildModel(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvMultDistRule(), CVCL::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVCL::TheoryBitvector::BVSize(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), CVCL::BitvectorTheoremProducer::bvuminusBVMult(), CVCL::BitvectorTheoremProducer::bvuminusBVUminus(), CVCL::BitvectorTheoremProducer::bvuminusToBVPlus(), CVCL::BitvectorTheoremProducer::bvuminusVar(), CVCL::TheoryArith::canon(), CVCL::ArithTheoremProducer::canonDivide(), CVCL::ArithTheoremProducer::canonDivideConst(), CVCL::ArithTheoremProducer::canonDivideMult(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonDivideVar(), CVCL::ArithTheoremProducer::canonFlattenSum(), CVCL::ArithTheoremProducer::canonInvert(), CVCL::ArithTheoremProducer::canonInvertConst(), CVCL::ArithTheoremProducer::canonInvertMult(), CVCL::ArithTheoremProducer::canonInvertPow(), CVCL::ArithTheoremProducer::canonMultConstConst(), CVCL::ArithTheoremProducer::canonMultConstMult(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::canonMultConstTerm(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::ArithTheoremProducer::canonMultTerm1Term2(), CVCL::ArithTheoremProducer::canonMultTermConst(), CVCL::ArithTheoremProducer::canonPowConst(), CVCL::TheoryArith::canonSimplify(), CVCL::SearchEngineTheoremProducer::caseSplit(), CVCL::SearchSat::check(), CVCL::TheoryDatatype::checkSat(), CVCL::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVCL::TheoryUF::checkType(), CVCL::TheoryDatatype::checkType(), TheoryCore::checkType(), CVCL::TypeComputerCore::checkType(), CVCL::TheoryArith::checkType(), CVCL::Theory::checkType(), CVCL::SearchSimple::checkValidInternal(), CVCL::SearchEngineFast::checkValidInternal(), TheoryCore::collectBasicVars(), CVCL::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVCL::TheoryBitvector::collectSharedSubterms(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), TheoryCore::computeBaseType(), CVCL::computeBVConst(), CVCL::TheoryBitvector::computeBVConst(), CVCL::TheoryUF::computeModel(), CVCL::TheoryRecords::computeModel(), CVCL::TheoryBitvector::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryArith::computeModelTerm(), CVCL::TheoryBitvector::computeNegBVConst(), CVCL::TheoryUF::computeTCC(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryQuant::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), CVCL::TheoryRecords::computeType(), CVCL::TheoryQuant::computeType(), CVCL::TheoryDatatype::computeType(), TheoryCore::computeType(), CVCL::TypeComputerCore::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::TheoryArray::computeType(), CVCL::TheoryArith::computeType(), CVCL::BitvectorTheoremProducer::concatConst(), CVCL::BitvectorTheoremProducer::concatFlatten(), CVCL::BitvectorTheoremProducer::concatMergeExtract(), CVCL::SearchEngineTheoremProducer::conflictRule(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::SearchEngineTheoremProducer::convertToCNF(), CVCL::ArithTheoremProducer::create_t(), CVCL::BitvectorTheoremProducer::createNewPlusCollection(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::SearchImplBase::enqueueCNFrec(), TheoryCore::enqueueFact(), CVCL::BitvectorTheoremProducer::eqConst(), CVCL::RefinedArithTheoremProducer::eval(), CVCL::VCCmd::evaluateCommand(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadow0(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::RecordsTheoremProducer::expandRecord(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::RecordsTheoremProducer::expandTuple(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::BitvectorTheoremProducer::extractBVMult(), CVCL::BitvectorTheoremProducer::extractBVPlus(), CVCL::BitvectorTheoremProducer::extractConcat(), CVCL::BitvectorTheoremProducer::extractConst(), CVCL::BitvectorTheoremProducer::extractExtract(), CVCL::BitvectorTheoremProducer::extractWhole(), CVCL::SearchImplBase::findInCNFCache(), CVCL::TheoryArith::findRationalBound(), CVCL::SearchEngineFast::findSplitter(), CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::TheoryBitvector::flattenBVPlus(), CVCL::BitvectorTheoremProducer::flattenBVPlus(), CVCL::BitvectorTheoremProducer::flipBVMult(), CVCL::ArithTheoremProducer::flipInequality(), CVCL::TheoryArith::freeConstIneq(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::TheoryBitvector::getBitvectorTypeParam(), CVCL::Expr::getBody(), CVCL::TheoryBitvector::getBoolExtractIndex(), CVCL::TheoryBitvector::getBVMultParam(), CVCL::TheoryBitvector::getBVPlusParam(), CVCL::SearchEngine::getConcreteModel(), CVCL::TheoryDatatype::getConsForTester(), CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatype::getConstant(), CVCL::TheoryBitvector::getExtractHi(), CVCL::TheoryBitvector::getExtractLow(), CVCL::TheoryRecords::getField(), CVCL::TheoryRecords::getFields(), CVCL::TheoryBitvector::getFixedLeftShiftParam(), CVCL::TheoryBitvector::getFixedRightShiftParam(), CVCL::TheoryQuant::getHead(), CVCL::Expr::getRational(), CVCL::TheoryDatatype::getSelectorInfo(), CVCL::Expr::getString(), getSubTerms(), CVCL::TheoryBitvector::getSXIndex(), CVCL::TheoryBitvector::getTypePredExpr(), CVCL::TheoryBitvector::getTypePredType(), CVCL::Expr::getUid(), CVCL::Expr::getVars(), CVCL::TheoryQuant::goodSynMatch(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::CoreTheoremProducer::iffAndDistrib(), CVCL::CoreTheoremProducer::iffOrDistrib(), CVCL::SearchEngineTheoremProducer::iffToClauses(), CVCL::CoreTheoremProducer::IffToIte(), CVCL::CNF_TheoremProducer::ifLiftRule(), CVCL::CoreTheoremProducer::ifLiftUnaryRule(), CVCL::CommonTheoremProducer::implContrapositive(), CVCL::CommonTheoremProducer::implIntro(), CVCL::CommonTheoremProducer::implMP(), CVCL::CoreTheoremProducer::ImpToIte(), CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::TheoryDatatypeLazy::instantiate(), CVCL::TheoryDatatype::instantiate(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::TheoryArith::isolateVariable(), CVCL::BitvectorTheoremProducer::iteBVnegRule(), CVCL::BitvectorTheoremProducer::iteExtractRule(), CVCL::SearchEngineTheoremProducer::iteToClauses(), CVCL::Theory::leavesAreSimp(), CVCL::BitvectorTheoremProducer::leftShiftToConcat(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::TheoryArith::lessThanVar(), CVCL::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::BitvectorTheoremProducer::negBVand(), CVCL::BitvectorTheoremProducer::negBVor(), CVCL::BitvectorTheoremProducer::negConcat(), CVCL::BitvectorTheoremProducer::negConst(), CVCL::SearchEngineTheoremProducer::negIntro(), CVCL::BitvectorTheoremProducer::negNeg(), CVCL::TheoryBitvector::newBoolExtractExpr(), CVCL::TheoryBitvector::newBVAndExpr(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVNandExpr(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newBVNorExpr(), CVCL::TheoryBitvector::newBVOrExpr(), CVCL::TheoryBitvector::newBVUminusExpr(), CVCL::TheoryBitvector::newBVXnorExpr(), CVCL::TheoryBitvector::newBVXorExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoryBitvector::newFixedLeftShiftExpr(), CVCL::TheoryBitvector::newFixedRightShiftExpr(), CVCL::SearchImplBase::newIntAssumption(), CVCL::TheoremProducer::newPf(), CVCL::TheoryBitvector::newSBVLEExpr(), CVCL::TheoryBitvector::newSBVLTExpr(), CVCL::TheoryBitvector::newSXExpr(), CVCL::TheoryArith::normalize(), CVCL::TheoryBitvector::normalizeBVArith(), CVCL::TheoryBitvector::normalizeConcat(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::BitvectorTheoremProducer::notBVLTRule(), CVCL::BitvectorTheoremProducer::oneCoeffBVMult(), CVCL::CoreTheoremProducer::orDistributivityRule(), CVCL::BitvectorTheoremProducer::orOne(), CVCL::CoreTheoremProducer::OrToIte(), CVCL::TheoryBitvector::pad(), CVCL::BitvectorTheoremProducer::pad(), CVCL::BitvectorTheoremProducer::padBVLTRule(), CVCL::BitvectorTheoremProducer::padBVMult(), CVCL::TheoryBitvector::padBVPlus(), CVCL::BitvectorTheoremProducer::padBVPlus(), CVCL::BitvectorTheoremProducer::padSBVLTRule(), TheoryCore::parseExpr(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryRecords::parseExprOp(), CVCL::TheoryQuant::parseExprOp(), CVCL::TheoryDatatype::parseExprOp(), TheoryCore::parseExprOp(), CVCL::TheoryBitvector::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::pickMonomial(), CVCL::VCL::printV(), CVCL::TheoryArith::processBuffer(), TheoryCore::processCond(), TheoryCore::processEquality(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processIntEq(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::SearchEngineFast::propagate(), CVCL::ExprTransform::pushNegation1(), CVCL::ExprTransform::pushNegationRec(), CVCL::VCL::query(), CVCL::CoreTheoremProducer::queryTCC(), CVCL::ArrayTheoremProducer::readArrayLiteral(), CVCL::ExprManager::rebuildRec(), CVCL::TheoryQuant::recGoodSemMatch(), CVCL::TheoryQuant::recSynMatch(), CVCL::TheoryQuant::recursiveMap(), TheoryCore::refineCounterExample(), CVCL::TheoryArith::refineCounterExample(), CVCL::CommonTheoremProducer::reflexivityRule(), CVCL::UFTheoremProducer::relToClosure(), CVCL::UFTheoremProducer::relTrans(), CVCL::SearchSimple::restartInternal(), CVCL::SearchEngineFast::restartInternal(), CVCL::TheoryRecords::rewrite(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteAnd(), CVCL::CoreTheoremProducer::rewriteAndSubterms(), CVCL::TheoryBitvector::rewriteAtomic(), CVCL::CoreTheoremProducer::rewriteConstDef(), TheoryCore::rewriteCore(), CVCL::CoreTheoremProducer::rewriteIteBool(), CVCL::CoreTheoremProducer::rewriteIteCond(), CVCL::CoreTheoremProducer::rewriteIteElse(), CVCL::CoreTheoremProducer::rewriteIteFalse(), CVCL::CoreTheoremProducer::rewriteIteSame(), CVCL::CoreTheoremProducer::rewriteIteThen(), CVCL::CoreTheoremProducer::rewriteIteToAnd(), CVCL::CoreTheoremProducer::rewriteIteToIff(), CVCL::CoreTheoremProducer::rewriteIteToImp(), CVCL::CoreTheoremProducer::rewriteIteToNot(), CVCL::CoreTheoremProducer::rewriteIteToOr(), CVCL::CoreTheoremProducer::rewriteIteTrue(), CVCL::CoreTheoremProducer::rewriteLetDecl(), TheoryCore::rewriteLiteral(), CVCL::RecordsTheoremProducer::rewriteLitSelect(), CVCL::RecordsTheoremProducer::rewriteLitUpdate(), CVCL::CoreTheoremProducer::rewriteNotAnd(), CVCL::QuantTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::QuantTheoremProducer::rewriteNotForall(), CVCL::CommonTheoremProducer::rewriteNotForall(), CVCL::CoreTheoremProducer::rewriteNotOr(), CVCL::UFTheoremProducer::rewriteOpDef(), CVCL::CommonTheoremProducer::rewriteOr(), CVCL::CoreTheoremProducer::rewriteOrSubterms(), CVCL::CommonTheoremProducer::rewriteReflexivity(), CVCL::RecordsTheoremProducer::rewriteUpdateSelect(), CVCL::CommonTheoremProducer::rewriteUsingSymmetry(), CVCL::BitvectorTheoremProducer::rightShiftToConcat(), CVCL::TheoryQuant::semInst(), CVCL::TheoryArith::separateMonomial(), CVCL::Expr::setRep(), CVCL::Expr::setSig(), CVCL::TheoryArith::setup(), TheoryCore::setupTerm(), CVCL::TheoryQuant::setupTriggers(), CVCL::VariableValue::setValue(), CVCL::BitvectorTheoremProducer::signBVLTRule(), CVCL::TheoryBitvector::signExtendBVLT(), CVCL::BitvectorTheoremProducer::signExtendRule(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyOp(), CVCL::VCL::simplifyThm(), CVCL::CommonTheoremProducer::skolemizeRewrite(), CVCL::CommonTheoremProducer::skolemizeRewriteVar(), TheoryCore::solve(), CVCL::TheoryArray::solve(), CVCL::SearchEngineFast::split(), CVCL::ArithTheoremProducer::splitGrayShadow(), CVCL::TheoryArith::substAndCanonize(), CVCL::VCL::subtypeType(), CVCL::CommonTheoremProducer::symmetryRule(), CVCL::TheoryQuant::synInst(), CVCL::Type::toString(), CVCL::TheoremValue::toString(), CVCL::SearchEngineFast::traceConflict(), CVCL::CommonTheoremProducer::transitivityRule(), CVCL::BitvectorTheoremProducer::typePredBit(), CVCL::SearchEngineTheoremProducer::unitProp(), CVCL::SearchEngineFast::unitPropagation(), CVCL::TheoryBitvector::update(), CVCL::TheoryArray::update(), CVCL::Theory::updateCC(), CVCL::TheoryArith::updateSubsumptionDB(), CVCL::CommonTheoremProducer::varIntroSkolem(), CVCL::BitvectorTheoremProducer::zeroCoeffBVMult(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

string CVCL::Expr::toString (  InputLanguage  lang  )  const [inherited]

Print the expression to a string using the given output language. Definition at line 202 of file expr.cpp. References CVCL::Expr::getEM(), CVCL::Expr::isNull(), CVCL::ExprStream::lang(), and CVCL::ExprStream::os().

void CVCL::Expr::print (  InputLanguage  lang, bool  dagify = true )  const [inherited]

Print the expression in the specified format. Definition at line 212 of file expr.cpp. References CVCL::ExprStream::dagFlag(), std::endl(), CVCL::Expr::getEM(), CVCL::Expr::isNull(), and CVCL::ExprStream::lang(). Referenced by TheoryCore::print(), CVCL::PrettyPrinterCore::print(), CVCL::TheoryArith::print(), and CVCL::Theorem::printx().

void CVCL::Expr::print (   )  const [inline, inherited]

Print the expression as AST (lisp-like format). Definition at line 563 of file expr.h. References CVCL::AST_LANG. Referenced by CVCL::Expr::printnodag().

void CVCL::Expr::printnodag (   )  const [inherited]

Print the expression as AST without dagifying. Definition at line 244 of file expr.cpp. References CVCL::AST_LANG, and CVCL::Expr::print().

void CVCL::Expr::pprint (   )  const [inherited]

Pretty-print the expression. Definition at line 223 of file expr.cpp. References std::endl(), CVCL::Expr::getEM(), and CVCL::Expr::isNull().

void CVCL::Expr::pprintnodag (   )  const [inherited]

Pretty-print without dagifying. Definition at line 233 of file expr.cpp. References CVCL::ExprStream::dagFlag(), std::endl(), CVCL::Expr::getEM(), and CVCL::Expr::isNull().

ExprStream & CVCL::Expr::print (  ExprStream &  os  )  const [inherited]

Print a leaf node. Definition at line 305 of file expr.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::BOUND_VAR, CVCL::Expr::end(), std::endl(), CVCL::EXISTS, CVCL::FORALL, CVCL::Expr::getBody(), CVCL::Expr::getEM(), CVCL::Expr::getKind(), CVCL::ExprManager::getKindName(), CVCL::Expr::getName(), CVCL::Expr::getRational(), CVCL::Expr::getString(), CVCL::Expr::getUid(), CVCL::Expr::getVars(), CVCL::Expr::hash(), CVCL::Expr::isNull(), CVCL::Expr::isQuantifier(), CVCL::Expr::isSymbol(), CVCL::NULL_KIND, CVCL::pop(), CVCL::push(), CVCL::RATIONAL_EXPR, CVCL::RAW_LIST, CVCL::ExprStream::resetIndent(), CVCL::SKOLEM_VAR, CVCL::space(), CVCL::STRING_EXPR, and CVCL::UCONST.

ExprStream & CVCL::Expr::printAST (  ExprStream &  os  )  const [inherited]

Print the top node and then recurse through the children */. Definition at line 250 of file expr.cpp. References CVCL::Expr::begin(), CVCL::BOUND_VAR, CVCL::Expr::end(), std::endl(), CVCL::Expr::getBody(), CVCL::Expr::getEM(), CVCL::Expr::getExistential(), CVCL::Op::getExpr(), CVCL::Expr::getIndex(), CVCL::Expr::getKind(), CVCL::ExprManager::getKindName(), CVCL::Expr::getName(), CVCL::Expr::getOp(), CVCL::Expr::getRational(), CVCL::Expr::getString(), CVCL::Expr::getUid(), CVCL::Expr::getVars(), CVCL::Expr::isApply(), CVCL::Expr::isClosure(), CVCL::Expr::isNull(), CVCL::Expr::isString(), CVCL::Expr::isSymbol(), CVCL::Expr::isVar(), CVCL::LETDECL, CVCL::nodag(), CVCL::pop(), CVCL::push(), CVCL::RATIONAL_EXPR, CVCL::ExprStream::resetIndent(), CVCL::SKOLEM_VAR, CVCL::space(), CVCL::STRING_EXPR, and CVCL::UCONST. Referenced by CVCL::operator<<(), CVCL::TheoryUF::print(), CVCL::TheorySimulate::print(), CVCL::TheoryRecords::print(), CVCL::TheoryQuant::print(), CVCL::TheoryDatatype::print(), TheoryCore::print(), CVCL::TheoryBitvector::print(), CVCL::TheoryArray::print(), CVCL::TheoryArith::print(), and CVCL::Theory::print().

Expr & CVCL::Expr::indent (  int  n, bool  permanent = false )  [inherited]

Set initial indentation to n. The indentation will be reset to default unless the second argument is true. Returns: reference to itself, so one can write `os << e.indent(5)' Definition at line 355 of file expr.cpp. References CVCL::Expr::getEM(), CVCL::ExprManager::indent(), and CVCL::Expr::isNull().

void CVCL::Expr::setFind (  const Theorem &  e  )  const [inline, inherited]

Set the find attribute to e. Definition at line 1147 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_find, CVCL::ExprManager::getCurrentContext(), CVCL::Expr::getEM(), CVCL::Theorem::getLHS(), IF_DEBUG(), CVCL::Expr::isNull(), and CVCL::CDO< T >::set(). Referenced by TheoryCore::assertEqualities(), TheoryCore::assertFormula(), CVCL::Theory::find(), CVCL::TheoryRecords::setup(), CVCL::TheoryBitvector::setupExpr(), CVCL::TheoryArith::setupRec(), TheoryCore::setupTerm(), TheoryCore::simplify(), TheoryCore::simplifyFullRec(), TheoryCore::simplifyInPlaceRec(), and CVCL::TheoryBitvector::update().

void CVCL::Expr::addToNotify (  Theory *  i, const Expr &  e )  const [inherited]

Add (e,i) to the notify list of this expression. Definition at line 362 of file expr.cpp. References CVCL::NotifyList::add(), CVCL::Expr::d_expr, CVCL::ExprValue::d_notifyList, CVCL::Expr::getEM(), CVCL::Expr::getNotify(), and CVCL::Expr::isNull(). Referenced by CVCL::TheoryDatatype::addSharedTerm(), TheoryCore::processUpdates(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::TheoryBitvector::setup(), CVCL::TheoryArray::setup(), CVCL::TheoryArith::setup(), CVCL::Theory::setupCC(), CVCL::TheoryBitvector::setupExpr(), TheoryCore::setupSubFormulas(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryArray::update(), and CVCL::Theory::updateCC().

void CVCL::Expr::setType (  const Type &  t  )  const [inline, inherited]

Set the cached type. Definition at line 1158 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_type, and CVCL::Expr::isNull(). Referenced by CVCL::TheoryUF::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), CVCL::TheoryRecords::computeType(), CVCL::TheoryQuant::computeType(), CVCL::TheoryDatatype::computeType(), TheoryCore::computeType(), CVCL::TheoryBitvector::computeType(), CVCL::TheoryArray::computeType(), CVCL::TheoryArith::computeType(), CVCL::ExprManager::ExprManager(), CVCL::Theory::getBaseType(), CVCL::ExprManager::newBoundVarExpr(), CVCL::CommonTheoremProducer::skolemize(), and CVCL::CommonTheoremProducer::skolemizeRewriteVar().

void CVCL::Expr::setTCC (  const Expr &  tcc  )  const [inline, inherited]

Set the cached TCC. Definition at line 1163 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_tcc, and CVCL::Expr::isNull(). Referenced by CVCL::Theory::getTCC().

void CVCL::Expr::setSubtypePred (  const Theorem &  pred  )  const [inline, inherited]

Set the cached subtyping predicate. Definition at line 1168 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_subtypePred, and CVCL::Expr::isNull(). Referenced by TheoryCore::subtypePredicate().

void CVCL::Expr::setSimpCache (  const Theorem &  e  )  const [inline, inherited]

Definition at line 1173 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::d_simpCache, CVCL::ExprValue::d_simpCacheTag, CVCL::Expr::getEM(), CVCL::ExprManager::getSimpCacheTag(), and CVCL::Expr::isNull(). Referenced by TheoryCore::simplifyFullRec(), and TheoryCore::simplifyInPlaceRec().

void CVCL::Expr::setValidType (   )  const [inline, inherited]

Definition at line 1179 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::isNull(), CVCL::CDFlags::set(), and CVCL::Expr::VALID_TYPE.

void CVCL::Expr::setIsAtomicFlag (  bool  value  )  const [inline, inherited]

Definition at line 1184 of file expr.h. References CVCL::CDFlags::clear(), CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IS_ATOMIC, CVCL::Expr::isNull(), CVCL::CDFlags::set(), and CVCL::Expr::VALID_IS_ATOMIC. Referenced by CVCL::Expr::isAtomic().

void CVCL::Expr::setRewriteNormal (   )  const [inline, inherited]

Definition at line 1191 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::isNull(), CVCL::Expr::REWRITE_NORMAL, CVCL::CDFlags::set(), and CVCL::TRACE. Referenced by CVCL::TheoryUF::rewrite(), TheoryCore::rewrite(), CVCL::TheoryArith::rewrite(), and TheoryCore::rewriteCore().

void CVCL::Expr::clearRewriteNormal (   )  const [inline, inherited]

Definition at line 1247 of file expr.h. References CVCL::CDFlags::clear(), CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::isNull(), and CVCL::Expr::REWRITE_NORMAL. Referenced by TheoryCore::rewriteCore().

void CVCL::Expr::setFinite (   )  const [inline, inherited]

Definition at line 1197 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IS_FINITE, CVCL::Expr::isNull(), and CVCL::CDFlags::set().

void CVCL::Expr::setWellFounded (   )  const [inline, inherited]

Definition at line 1202 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::isNull(), CVCL::CDFlags::set(), and CVCL::Expr::WELL_FOUNDED.

void CVCL::Expr::setComputeTransClosure (   )  const [inline, inherited]

Definition at line 1207 of file expr.h. References CVCL::Expr::COMPUTE_TRANS_CLOSURE, CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::isNull(), and CVCL::CDFlags::set().

void CVCL::Expr::setImpliedLiteral (   )  const [inline, inherited]

Definition at line 1212 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IMPLIED_LITERAL, CVCL::Expr::isNull(), and CVCL::CDFlags::set(). Referenced by TheoryCore::processUpdates(), and TheoryCore::registerAtom().

void CVCL::Expr::setUserAssumption (  int  scope = -1  )  const [inline, inherited]

Definition at line 1217 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IS_USER_ASSUMPTION, CVCL::Expr::isNull(), and CVCL::CDFlags::set(). Referenced by CVCL::SearchSat::newUserAssumption(), and CVCL::SearchImplBase::newUserAssumption().

void CVCL::Expr::setIntAssumption (   )  const [inline, inherited]

Definition at line 1222 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IS_INT_ASSUMPTION, CVCL::Expr::isNull(), and CVCL::CDFlags::set(). Referenced by CVCL::SearchSat::assertLit(), and CVCL::SearchImplBase::newIntAssumption().

void CVCL::Expr::setJustified (   )  const [inline, inherited]

Definition at line 1227 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IS_JUSTIFIED, CVCL::Expr::isNull(), and CVCL::CDFlags::set(). Referenced by CVCL::SearchSat::setJustified().

void CVCL::Expr::setTranslated (  int  scope = -1  )  const [inline, inherited]

Set the translated flag for this Expr. Definition at line 1232 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IS_TRANSLATED, CVCL::Expr::isNull(), and CVCL::CDFlags::set(). Referenced by CVCL::TheoryDatatypeLazy::instantiate(), and SAT::CNF_Manager::translateExprRec().

void CVCL::Expr::setUserRegisteredAtom (   )  const [inline, inherited]

Set the UserRegisteredAtom flag for this Expr. Definition at line 1237 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IS_USER_REGISTERED_ATOM, CVCL::Expr::isNull(), and CVCL::CDFlags::set(). Referenced by CVCL::SearchSat::registerAtom().

void CVCL::Expr::setSelected (   )  const [inline, inherited]

Set the Selected flag for this Expr. Definition at line 1242 of file expr.h. References CVCL::ExprValue::d_dynamicFlags, CVCL::Expr::d_expr, CVCL::Expr::IS_SELECTED, CVCL::Expr::isNull(), and CVCL::CDFlags::set(). Referenced by CVCL::TheoryDatatypeLazy::checkSat(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), and CVCL::TheoryDatatype::update().

bool CVCL::Expr::subExprOf (  const Expr &  e  )  const [inherited]

Check if the current Expr (*this) is a subexpression of e. Definition at line 148 of file expr.cpp. References CVCL::Expr::clearFlags(), and CVCL::subExprRec(). Referenced by CVCL::CommonTheoremProducer::skolemizeRewriteVar().

int CVCL::Expr::getHeight (   )  const [inline, inherited]

Definition at line 904 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::getHeight(). Referenced by CVCL::DecisionEngineMBTF::findSplitter(), and CVCL::DecisionEngineCaching::findSplitter().

int CVCL::Expr::getHighestKid (   )  const [inline, inherited]

Definition at line 905 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::getHighestKid(). Referenced by CVCL::DecisionEngine::findSplitterRec().

bool CVCL::Expr::hasSimpFrom (   )  const [inline, inherited]

Definition at line 907 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::getSimpFrom(), and CVCL::Expr::isNull(). Referenced by CVCL::Expr::getSimpFrom(), and CVCL::Theorem::Theorem().

const Expr & CVCL::Expr::getSimpFrom (   )  const [inline, inherited]

Definition at line 909 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprValue::getSimpFrom(), and CVCL::Expr::hasSimpFrom(). Referenced by CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::DecisionEngineMBTF::isBetter(), CVCL::DecisionEngineCaching::isBetter(), and CVCL::Theorem::Theorem().

void CVCL::Expr::setSimpFrom (  const Expr &  simpFrom  )  [inline, inherited]

Definition at line 911 of file expr.h. References CVCL::Expr::d_expr, and CVCL::ExprValue::setSimpFrom().

bool CVCL::Expr::hasSig (   )  const [inline, inherited]

Definition at line 1252 of file expr.h. References CVCL::Expr::d_expr, CVCL::CDO< T >::get(), CVCL::ExprValue::getSig(), CVCL::Theorem::isNull(), and CVCL::Expr::isNull().

bool CVCL::Expr::hasRep (   )  const [inline, inherited]

Definition at line 1258 of file expr.h. References CVCL::Expr::d_expr, CVCL::CDO< T >::get(), CVCL::ExprValue::getRep(), CVCL::Theorem::isNull(), and CVCL::Expr::isNull().

const Theorem & CVCL::Expr::getSig (   )  const [inline, inherited]

Definition at line 1264 of file expr.h. References CVCL::Expr::d_expr, CVCL::CDO< T >::get(), CVCL::ExprValue::getSig(), and CVCL::Expr::isNull(). Referenced by CVCL::TheoryUF::update(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryArray::update(), and CVCL::Theory::updateCC().

const Theorem & CVCL::Expr::getRep (   )  const [inline, inherited]

Definition at line 1273 of file expr.h. References CVCL::Expr::d_expr, CVCL::CDO< T >::get(), CVCL::ExprValue::getRep(), and CVCL::Expr::isNull(). Referenced by CVCL::Theory::rewriteCC(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryArray::update(), and CVCL::Theory::updateCC().

void CVCL::Expr::setSig (  const Theorem &  e  )  const [inline, inherited]

Definition at line 1282 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprManager::getCurrentContext(), CVCL::Expr::getEM(), CVCL::ExprValue::getSig(), IF_DEBUG(), CVCL::Expr::isNull(), CVCL::CDO< T >::set(), CVCL::ExprValue::setSig(), and CVCL::Expr::toString(). Referenced by CVCL::TheoryArray::setup(), CVCL::Theory::setupCC(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryArray::update(), and CVCL::Theory::updateCC().

void CVCL::Expr::setRep (  const Theorem &  e  )  const [inline, inherited]

Definition at line 1293 of file expr.h. References CVCL::Expr::d_expr, CVCL::ExprManager::getCurrentContext(), CVCL::Expr::getEM(), CVCL::ExprValue::getRep(), IF_DEBUG(), CVCL::Expr::isNull(), CVCL::CDO< T >::set(), CVCL::ExprValue::setRep(), and CVCL::Expr::toString(). Referenced by CVCL::TheoryArray::setup(), CVCL::Theory::setupCC(), CVCL::TheoryDatatypeLazy::update(), CVCL::TheoryDatatype::update(), CVCL::TheoryArray::update(), and CVCL::Theory::updateCC().

---

Variable Documentation

Expr CVCL::Expr::s_null [static, private, inherited]

Convenient null expr. Definition at line 176 of file expr.h. Referenced by CVCL::Expr::getType(), CVCL::Expr::lookupTCC(), and CVCL::Expr::lookupType().

ExprValue* CVCL::Expr::d_expr [private, inherited]

The value. This is the only data member in this class. Definition at line 182 of file expr.h. Referenced by CVCL::Expr::addToNotify(), CVCL::Expr::arity(), CVCL::Expr::clearRewriteNormal(), CVCL::compare(), CVCL::Expr::computeTransClosure(), CVCL::Expr::Expr(), CVCL::Expr::getBody(), CVCL::Expr::getBoundIndex(), CVCL::Expr::getEM(), CVCL::Expr::getExistential(), CVCL::Expr::getExprValue(), CVCL::Expr::getFind(), CVCL::Expr::getFlag(), CVCL::Expr::getHeight(), CVCL::Expr::getHighestKid(), CVCL::Expr::getIndex(), CVCL::Expr::getIsAtomicFlag(), CVCL::Expr::getKids(), CVCL::Expr::getKind(), CVCL::Expr::getMMIndex(), CVCL::Expr::getName(), CVCL::Expr::getNotify(), CVCL::Expr::getOp(), CVCL::Expr::getRational(), CVCL::Expr::getRep(), CVCL::Expr::getSig(), CVCL::Expr::getSimpCache(), CVCL::Expr::getSimpFrom(), CVCL::Expr::getString(), CVCL::Expr::getType(), CVCL::Expr::getUid(), CVCL::Expr::getVars(), CVCL::DecisionEngineMBTF::goalSatisfied(), CVCL::DecisionEngineCaching::goalSatisfied(), CVCL::Expr::hasFind(), CVCL::ExprManager::hash(), CVCL::Expr::hasLastIndex(), CVCL::Expr::hasRep(), CVCL::Expr::hasSig(), CVCL::Expr::hasSimpFrom(), CVCL::Expr::isApply(), CVCL::Expr::isClosure(), CVCL::Expr::isFinite(), CVCL::Expr::isImpliedLiteral(), CVCL::Expr::isInitialized(), CVCL::Expr::isIntAssumption(), CVCL::Expr::isJustified(), CVCL::Expr::isNull(), CVCL::Expr::isRewriteNormal(), CVCL::Expr::isSelected(), CVCL::Expr::isString(), CVCL::Expr::isSymbol(), CVCL::Expr::isTranslated(), CVCL::Expr::isUserAssumption(), CVCL::Expr::isUserRegisteredAtom(), CVCL::Expr::isValidType(), CVCL::Expr::isVar(), CVCL::Expr::isWellFounded(), CVCL::Expr::lookupSubtypePred(), CVCL::Expr::lookupTCC(), CVCL::Expr::lookupType(), CVCL::Expr::operator=(), CVCL::operator==(), CVCL::Expr::operator[](), CVCL::ExprManager::rebuildRec(), CVCL::Expr::setComputeTransClosure(), CVCL::Expr::setFind(), CVCL::Expr::setFinite(), CVCL::Expr::setFlag(), CVCL::Expr::setImpliedLiteral(), CVCL::Expr::setIntAssumption(), CVCL::Expr::setIsAtomicFlag(), CVCL::Expr::setJustified(), CVCL::Expr::setRep(), CVCL::Expr::setRewriteNormal(), CVCL::Expr::setSelected(), CVCL::Expr::setSig(), CVCL::Expr::setSimpCache(), CVCL::Expr::setSimpFrom(), CVCL::Expr::setSubtypePred(), CVCL::Expr::setTCC(), CVCL::Expr::setTranslated(), CVCL::Expr::setType(), CVCL::Expr::setUserAssumption(), CVCL::Expr::setUserRegisteredAtom(), CVCL::Expr::setValidType(), CVCL::Expr::setWellFounded(), CVCL::Expr::validIsAtomicFlag(), CVCL::Expr::validSimpCache(), and CVCL::Expr::~Expr().

---