Expression Package
[Building Blocks]

Collaboration diagram for Expression Package:

Modules

• Smart Pointer Functionality in Expr
• Private methods

Classes

• class CVC3::Expr

  Data structure of expressions in CVC3. More...
  

• class CVC3::Expr::iterator

Enumerations

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

  bit-masks for static flags More...
  

• enum CVC3::Expr::DynamicFlagsEnum {
    CVC3::Expr::IMPLIED_LITERAL = 0x10, CVC3::Expr::IS_USER_ASSUMPTION = 0x20, CVC3::Expr::IS_INT_ASSUMPTION = 0x40, CVC3::Expr::IS_JUSTIFIED = 0x80,
    CVC3::Expr::IS_TRANSLATED = 0x100, CVC3::Expr::IS_USER_REGISTERED_ATOM = 0x200, CVC3::Expr::IS_SELECTED = 0x2000, CVC3::Expr::IS_STORED_PREDICATE = 0x4000,
    CVC3::Expr::IS_REGISTERED_ATOM = 0x8000, CVC3::Expr::IN_USER_ASSUMPTION = 0x00010000
  }

  bit-masks for dynamic flags More...
  

Functions

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

  Private constructor, simply wraps around the pointer.
  

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

  Default constructor creates the Null Expr.
  

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

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

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

  Assignment operator: take care of the refcounting and GC.
  

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

  Destructor.
  

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

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

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

  Rebuild Expr with a new ExprManager.
  

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

  Expr represents a type.
  

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

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

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

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

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

  Test if e is atomic.
  

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

  Test if e is an atomic formula.
  

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

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

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

  Test if e is a literal.
  

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

  Test if e is an abstract literal.
  

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

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

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

  True iff expr is not a Bool connective.
  

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

  PropAtom or negation of PropAtom.
  

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

  For BOUND_VAR, get the UID.
  

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

  Get bound variables from a closure Expr.
  

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

  Get the existential axiom expression for skolem constant.
  

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

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

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

  Get the body of the closure Expr.
  

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

  Get the Rational value out of RATIONAL_EXPR.
  

• const Theorem & CVC3::Expr::getTheorem () const

  Get theorem from THEOREM_EXPR.
  

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

  Make the expr into an operator.
  

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

  Get operator from expression.
  

• Expr CVC3::Expr::getOpExpr () const

  Get expression of operator (for APPLY Exprs only).
  

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

  Get kind of operator (for APPLY Exprs only).
  

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

  Remove leading NOT if any.
  

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

  Begin iterator.
  

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

  End iterator.
  

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

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

• bool CVC3::Expr::hasFind () const
• const Theorem & CVC3::Expr::getFind () const
• int CVC3::Expr::getFindLevel () const
• NotifyList * CVC3::Expr::getNotify () const
• const Type CVC3::Expr::getType () const

  Get the type. Recursively compute if necessary.
  

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

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

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

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

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

  Check if the generic flag is set.
  

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

  Set the generic flag.
  

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

  Clear the generic flag in all Exprs.
  

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

  Print the expression to a string.
  

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

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

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

  Print the expression in the specified format.
  

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

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

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

  Print the expression as AST without dagifying.
  

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

  Pretty-print the expression.
  

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

  Pretty-print without dagifying.
  

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

  Print a leaf node.
  

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

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

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

  Set initial indentation to n.
  

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

  Set the find attribute to e.
  

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

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

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

  Set the cached type.
  

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

  Set the translated flag for this Expr.
  

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

  Set the UserRegisteredAtom flag for this Expr.
  

• void CVC3::Expr::setRegisteredAtom () const

  Set the RegisteredAtom flag for this Expr.
  

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

  Set the Selected flag for this Expr.
  

• void CVC3::Expr::setStoredPredicate () const

  Set the Stored Predicate flag for this Expr.
  

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

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

• bool CVC3::Expr::hasSig () const
• bool CVC3::Expr::hasRep () const
• const Theorem & CVC3::Expr::getSig () const
• const Theorem & CVC3::Expr::getRep () const
• void CVC3::Expr::setSig (const Theorem &e) const
• void CVC3::Expr::setRep (const Theorem &e) const

Variables

• static Expr CVC3::Expr::s_null

  Convenient null expr.
  

• ExprValue * CVC3::Expr::d_expr

---

Enumeration Type Documentation

enum CVC3::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).
CONTAINS_BOUND_VAR	Whether expr contains a bounded variable (for quantifier instantiation).

Definition at line 140 of file expr.h.

enum CVC3::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
IS_STORED_PREDICATE
IS_REGISTERED_ATOM
IN_USER_ASSUMPTION

Definition at line 161 of file expr.h.

---

Function Documentation

CVC3::Expr::Expr

(

ExprValue *

expr

)

[inline, private, inherited]

Private constructor, simply wraps around the pointer.

Definition at line 727 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::incRefcount().

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

Definition at line 45 of file expr.cpp.

References CVC3::Expr::begin(), CVC3::ExprHashMap< Data >::begin(), CVC3::ExprHashMap< Data >::clear(), CVC3::Expr::clearFlags(), CVC3::ExprHashMap< Data >::count(), CVC3::Debug::counter(), CVC3::debugger, CVC3::Expr::end(), CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::erase(), CVC3::Expr::Expr(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Expr::getFlag(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), CVC3::Expr::getVars(), IF_DEBUG, CVC3::ExprHashMap< Data >::insert(), CVC3::Expr::isClosure(), CVC3::ExprManager::newClosureExpr(), CVC3::Expr::recursiveSubst(), and CVC3::Expr::setFlag().

Referenced by CVC3::Expr::recursiveSubst(), and CVC3::Expr::substExpr().

CVC3::Expr::Expr

(

)

[inline, inherited]

Default constructor creates the Null Expr.

Definition at line 266 of file expr.h.

Referenced by CVC3::Expr::andExpr(), CVC3::Expr::eqExpr(), CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), CVC3::Expr::iteExpr(), CVC3::Expr::notExpr(), CVC3::Expr::orExpr(), and CVC3::Expr::recursiveSubst().

CVC3::Expr::Expr

(

const Expr &

e

)

[inline, inherited]

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

Definition at line 729 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::incRefcount().

Expr & CVC3::Expr::operator=

(

const Expr &

e

)

[inline, inherited]

Assignment operator: take care of the refcounting and GC.

Definition at line 733 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::decRefcount(), and CVC3::ExprValue::incRefcount().

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

Definition at line 752 of file expr.h.

References CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::Op::getExpr(), CVC3::ExprNode::getKids1(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), CVC3::Expr::isNull(), and CVC3::ExprManager::newExprValue().

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

Definition at line 768 of file expr.h.

References CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::Op::getExpr(), CVC3::ExprNode::getKids1(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), CVC3::Expr::isNull(), and CVC3::ExprManager::newExprValue().

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

Definition at line 786 of file expr.h.

References CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::Op::getExpr(), CVC3::ExprNode::getKids1(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), CVC3::Expr::isNull(), and CVC3::ExprManager::newExprValue().

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

Definition at line 807 of file expr.h.

References CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::Op::getExpr(), CVC3::ExprNode::getKids1(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), CVC3::Expr::isNull(), and CVC3::ExprManager::newExprValue().

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

Definition at line 830 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getEM(), CVC3::Op::getExpr(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), CVC3::Expr::isNull(), and CVC3::ExprManager::newExprValue().

CVC3::Expr::~Expr

(

)

[inline, inherited]

Destructor.

Definition at line 903 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::decRefcount().

Expr CVC3::Expr::eqExpr

(

const Expr &

right

)

const [inline, inherited]

Definition at line 851 of file expr.h.

References CVC3::EQ, CVC3::Expr::Expr(), and MiniSat::right().

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryArray::computeModel(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::VCL::eqExpr(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::RWTheoremValue::getExpr(), CVC3::Theorem::getExpr(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::typePredBit(), and CVC3::CommonTheoremProducer::varIntroRule().

Expr CVC3::Expr::notExpr

(

)

const [inline, inherited]

Definition at line 855 of file expr.h.

References CVC3::Expr::Expr(), and CVC3::NOT.

Referenced by CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::Expr::negate(), and CVC3::QuantTheoremProducer::pullVarOut().

Expr CVC3::Expr::negate

(

)

const [inline, inherited]

Definition at line 859 of file expr.h.

References CVC3::Expr::isNot(), and CVC3::Expr::notExpr().

Referenced by CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::VCL::checkUnsat(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::Circuit::Circuit(), SAT::CNF_Manager::cons(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::Translator::finish(), CVC3::VariableValue::getNegExpr(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::DecisionEngine::pushDecision(), and CVC3::CoreTheoremProducer::rewriteIteToIff().

Expr CVC3::Expr::andExpr

(

const Expr &

right

)

const [inline, inherited]

Definition at line 863 of file expr.h.

References CVC3::AND, CVC3::Expr::Expr(), and MiniSat::right().

Referenced by CVC3::BitvectorTheoremProducer::computeCarry(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryDatatype::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryArithOld::computeTCC(), CVC3::TheoryArithNew::computeTCC(), CVC3::VCL::createOp(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::signBVLTRule(), and CVC3::QuantTheoremProducer::universalInst().

Expr CVC3::Expr::orExpr

(

const Expr &

right

)

const [inline, inherited]

Definition at line 873 of file expr.h.

References CVC3::Expr::Expr(), CVC3::OR, and MiniSat::right().

Referenced by CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::CommonTheoremProducer::excludedMiddle(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::CoreTheoremProducer::rewriteIteBool(), and CVC3::BitvectorTheoremProducer::signBVLTRule().

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

Definition at line 883 of file expr.h.

References CVC3::Expr::Expr(), and CVC3::ITE.

Referenced by CVC3::CoreTheoremProducer::AndToIte(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::VCL::iteExpr(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::Translator::preprocessRec(), CVC3::TheoryCore::processCond(), CVC3::CoreTheoremProducer::rewriteIteBool(), and CVC3::ArrayTheoremProducer::rewriteReadWrite().

Expr CVC3::Expr::iffExpr

(

const Expr &

right

)

const [inline, inherited]

Definition at line 887 of file expr.h.

References CVC3::Expr::Expr(), CVC3::IFF, and MiniSat::right().

Referenced by CVC3::TheoryCore::assignValue(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::RWTheoremValue::getExpr(), CVC3::Theorem::getExpr(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::VCCmd::skolemizeAx(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), and CVC3::CommonTheoremProducer::varIntroRule().

Expr CVC3::Expr::impExpr

(

const Expr &

right

)

const [inline, inherited]

Definition at line 891 of file expr.h.

References CVC3::Expr::Expr(), CVC3::IMPLIES, and MiniSat::right().

Referenced by CVC3::VCL::impliesExpr(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::ArrayTheoremProducer::rewriteSameStore(), and CVC3::QuantTheoremProducer::universalInst().

Expr CVC3::Expr::skolemExpr

(

int

i

)

const [inline, inherited]

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

Definition at line 895 of file expr.h.

References CVC3::Expr::getEM(), and CVC3::ExprManager::newSkolemExpr().

Referenced by CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::CommonTheoremProducer::skolemize(), CVC3::VCCmd::skolemizeAx(), and CVC3::CommonTheoremProducer::skolemizeRewriteVar().

Expr CVC3::Expr::rebuild

(

ExprManager *

em

)

const [inline, inherited]

Rebuild Expr with a new ExprManager.

Definition at line 899 of file expr.h.

References CVC3::ExprManager::rebuild().

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

Definition at line 149 of file expr.cpp.

References CVC3::Expr::clearFlags(), DebugAssert, CVC3::ExprHashMap< Data >::insert(), and CVC3::Expr::recursiveSubst().

Referenced by CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::CommonTheoremProducer::skolemize(), CVC3::VCCmd::skolemizeAx(), and CVC3::QuantTheoremProducer::universalInst().

Expr CVC3::Expr::substExpr

(

const ExprHashMap< Expr > &

oldToNew

)

const [inherited]

Definition at line 170 of file expr.cpp.

References CVC3::Expr::clearFlags(), CVC3::Expr::recursiveSubst(), and CVC3::ExprHashMap< Data >::size().

Expr CVC3::Expr::operator!

(

)

const [inline, inherited]

Definition at line 310 of file expr.h.

Expr CVC3::Expr::operator &&

(

const Expr &

right

)

const [inline, inherited]

Definition at line 311 of file expr.h.

References CVC3::andExpr(), and MiniSat::right().

Expr CVC3::Expr::operator||

(

const Expr &

right

)

const [inline, inherited]

Definition at line 312 of file expr.h.

References CVC3::orExpr(), and MiniSat::right().

size_t CVC3::Expr::hash

(

const Expr &

e

)

[inline, static, inherited]

Definition at line 909 of file expr.h.

References CVC3::Expr::getEM(), and CVC3::ExprManager::hash().

Referenced by CVC3::ExprSkolem::computeHash(), CVC3::ExprApplyTmp::computeHash(), CVC3::ExprClosure::computeHash(), CVC3::VariableManager::HashLV::operator()(), and Hash::hash< CVC3::Expr >::operator()().

size_t CVC3::Expr::hash

(

)

const [inline, inherited]

Definition at line 915 of file expr.h.

References CVC3::Expr::getEM(), and CVC3::ExprManager::hash().

Referenced by CVC3::Expr::print().

bool CVC3::Expr::isFalse

(

)

const [inline, inherited]

Definition at line 328 of file expr.h.

References CVC3::FALSE_EXPR.

Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::SearchSat::check(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::SearchSimple::checkValidRec(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryQuant::enqueueInst(), CVC3::BitvectorTheoremProducer::generalIneqn(), SAT::CNF_Manager::getCNFLit(), CVC3::CommonTheoremProducer::iffFalseElim(), CVC3::CNF_TheoremProducer::learnedClause(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::SearchImplBase::processResult(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::TheoryCore::registerAtom(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplifyOp(), SAT::CNF_Manager::translateExprRec(), and CVC3::TheoryCore::update().

bool CVC3::Expr::isTrue

(

)

const [inline, inherited]

Definition at line 329 of file expr.h.

References CVC3::TRUE_EXPR.

Referenced by CVC3::TheoryCore::assertFactCore(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::SearchSat::check(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::TheoryQuant::enqueueInst(), CVC3::BitvectorTheoremProducer::generalIneqn(), SAT::CNF_Manager::getCNFLit(), CVC3::CommonTheoremProducer::iffTrueElim(), CVC3::SearchSat::newUserAssumptionInt(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryCore::registerAtom(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplifyOp(), CVC3::SearchEngineFast::split(), SAT::CNF_Manager::translateExprRec(), and CVC3::TheoryUF::update().

bool CVC3::Expr::isBoolConst

(

)

const [inline, inherited]

Definition at line 330 of file expr.h.

Referenced by CVC3::Theory::addSplitter(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryBitvector::comparebv(), CVC3::Expr::isAtomic(), and CVC3::SearchEngineFast::split().

bool CVC3::Expr::isVar

(

)

const [inline, inherited]

Definition at line 922 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::isVar().

Referenced by CVC3::TypeComputerCore::computeType(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::Theory::getTCC(), CVC3::Theory::isLeaf(), CVC3::Expr::printAST(), recursiveGetSubTrig(), CVC3::TheoryCore::simplify(), and CVC3::Theory::theoryOf().

bool CVC3::Expr::isBoundVar

(

)

const [inline, inherited]

Definition at line 332 of file expr.h.

References CVC3::BOUND_VAR.

bool CVC3::Expr::isString

(

)

const [inline, inherited]

Definition at line 923 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::isString().

Referenced by CVC3::TheoryDatatype::checkType(), CVC3::Expr::getString(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::PrettyPrinterCore::print(), and CVC3::Expr::printAST().

bool CVC3::Expr::isClosure

(

)

const [inline, inherited]

Definition at line 924 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::isClosure().

Referenced by CVC3::TheoryArray::computeType(), CVC3::VCCmd::findAxioms(), CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::isArrayLiteral(), CVC3::Expr::isLambda(), CVC3::Expr::isQuantifier(), CVC3::isTrivialExpr(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::Expr::printAST(), recGetSubTerms(), recursiveExprScore(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), and CVC3::Expr::recursiveSubst().

bool CVC3::Expr::isQuantifier

(

)

const [inline, inherited]

Definition at line 925 of file expr.h.

References CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getKind(), and CVC3::Expr::isClosure().

Referenced by CVC3::TheoryQuant::computeTCC(), hasBoundVarRec(), CVC3::TheoryQuant::print(), and CVC3::Expr::print().

bool CVC3::Expr::isLambda

(

)

const [inline, inherited]

Definition at line 928 of file expr.h.

References CVC3::Expr::getKind(), CVC3::Expr::isClosure(), and CVC3::LAMBDA.

Referenced by CVC3::Theory::newSubtypeExpr(), and CVC3::TheoryUF::print().

bool CVC3::Expr::isApply

(

)

const [inline, inherited]

Definition at line 931 of file expr.h.

References CVC3::APPLY, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getKind(), and CVC3::ExprValue::isApply().

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::UFTheoremProducer::applyLambda(), CVC3::TheoryUF::assertFact(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryCore::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::getConstructor(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryRecords::getField(), CVC3::TheoryRecords::getFields(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::TheoryRecords::getIndex(), CVC3::Expr::getOp(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::TheoryBitvector::getSXIndex(), CVC3::TheoryBitvector::getTypePredType(), CVC3::isConstructor(), CVC3::TheoryRecords::isRecord(), CVC3::TheoryRecords::isRecordAccess(), CVC3::TheoryRecords::isRecordType(), CVC3::isSelector(), CVC3::isTester(), CVC3::TheoryRecords::isTuple(), CVC3::TheoryRecords::isTupleAccess(), CVC3::TheoryRecords::isTupleType(), CVC3::TheoryCore::parseExpr(), CVC3::Translator::preprocess2Rec(), CVC3::TheoryUF::print(), CVC3::PrettyPrinterCore::print(), CVC3::TheoryBitvector::print(), CVC3::Expr::printAST(), recursiveGetSubTrig(), CVC3::UFTheoremProducer::relToClosure(), CVC3::TheoryUF::rewrite(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::Theory::theoryOf(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().

bool CVC3::Expr::isSymbol

(

)

const [inline, inherited]

Definition at line 935 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::isSymbol().

Referenced by CVC3::TheoryUF::assertFact(), CVC3::TheoryUF::computeType(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::Expr::print(), and CVC3::Expr::printAST().

bool CVC3::Expr::isTheorem

(

)

const [inline, inherited]

Definition at line 936 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::isTheorem().

Referenced by CVC3::Expr::getTheorem(), and CVC3::Expr::printAST().

bool CVC3::Expr::isType

(

)

const [inline, inherited]

Expr represents a type.

Definition at line 937 of file expr.h.

References CVC3::Expr::getEM(), CVC3::Expr::getOpKind(), and CVC3::ExprManager::isTypeKind().

Referenced by CVC3::TypeComputerCore::checkType().

const ExprValue * CVC3::Expr::getExprValue

(

)

const [inline, inherited]

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

Definition at line 917 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::getExprValue().

Referenced by CVC3::computeBVConst(), CVC3::TheoryBitvector::getBVConstSize(), and CVC3::TheoryBitvector::getBVConstValue().

bool CVC3::Expr::isTerm

(

)

const [inline, inherited]

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

Definition at line 938 of file expr.h.

References CVC3::Expr::getType(), and CVC3::Type::isBool().

Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::Theorem::getExpr(), CVC3::TheoryArithOld::isStale(), CVC3::ExprTransform::pushNegation(), CVC3::ExprTransform::pushNegationRec(), recursiveGetSubTrig(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryRecords::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryDatatype::solve(), CVC3::TheoryArithOld::solve(), and CVC3::TheoryArithNew::solve().

bool CVC3::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 368 of file expr.cpp.

References CVC3::Expr::arity(), CVC3::Expr::getIsAtomicFlag(), CVC3::Expr::getType(), CVC3::Expr::isBoolConst(), CVC3::Expr::setIsAtomicFlag(), and CVC3::Expr::validIsAtomicFlag().

Referenced by SAT::CNF_Manager::replaceITErec(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArray::setup(), CVC3::TheoryCore::setupSubFormulas(), and CVC3::TheoryArray::update().

bool CVC3::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 394 of file expr.cpp.

References CVC3::AND, CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::IFF, CVC3::IMPLIES, CVC3::ITE, CVC3::NOT, CVC3::OR, and CVC3::XOR.

Referenced by CVC3::TheoryQuant::recSynMatch(), and CVC3::TheoryBitvector::setup().

bool CVC3::Expr::isAbsAtomicFormula

(

)

const [inline, inherited]

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

Definition at line 366 of file expr.h.

Referenced by CVC3::SearchSat::findSplitterRec(), CVC3::DecisionEngineMBTF::goalSatisfied(), CVC3::DecisionEngineCaching::goalSatisfied(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryArithNew::registerAtom(), CVC3::TheoryCore::setupSubFormulas(), and SAT::CNF_Manager::translateExprRec().

bool CVC3::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 371 of file expr.h.

bool CVC3::Expr::isAbsLiteral

(

)

const [inline, inherited]

Test if e is an abstract literal.

Definition at line 374 of file expr.h.

Referenced by CVC3::SearchSat::addLemma(), CVC3::Theory::addSplitter(), CVC3::SearchImplBase::addSplitter(), CVC3::SearchEngineFast::addSplitter(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::SearchEngineFast::bcp(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::Theorem::isAbsLiteral(), CVC3::SearchImplBase::isClause(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchEngineFast::propagate(), CVC3::DecisionEngine::pushDecision(), CVC3::SearchImplBase::replaceITE(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryCore::rewriteLiteral(), and CVC3::TheoryCore::setupTerm().

bool CVC3::Expr::isBoolConnective

(

)

const [inline, inherited]

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

Definition at line 939 of file expr.h.

References CVC3::AND, CVC3::Expr::getKind(), CVC3::Expr::getType(), CVC3::IFF, CVC3::IMPLIES, CVC3::ITE, CVC3::NOT, CVC3::OR, and CVC3::XOR.

bool CVC3::Expr::isPropAtom

(

)

const [inline, inherited]

True iff expr is not a Bool connective.

Definition at line 379 of file expr.h.

bool CVC3::Expr::isPropLiteral

(

)

const [inline, inherited]

PropAtom or negation of PropAtom.

Definition at line 381 of file expr.h.

Referenced by CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::isPropClause(), and CVC3::SearchImplBase::replaceITE().

bool CVC3::Expr::isEq

(

)

const [inline, inherited]

Definition at line 384 of file expr.h.

References CVC3::EQ.

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::compare(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), isSysPred(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewriteCore(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryArray::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::setup(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::TheoryCore::solve(), CVC3::TheoryArray::solve(), CVC3::Theory::theoryOf(), and usefulInMatch().

bool CVC3::Expr::isNot

(

)

const [inline, inherited]

Definition at line 385 of file expr.h.

References CVC3::NOT.

Referenced by CVC3::SearchImplBase::addToCNFCache(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::SearchSat::check(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), SAT::CNF_Manager::getCNFLit(), CVC3::SearchImplBase::isGoodSplitter(), CVC3::Expr::negate(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchImplBase::newIntAssumption(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::SearchImplBase::processResult(), CVC3::ExprTransform::pushNegation1(), CVC3::Theorem::refutes(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryCore::rewriteLiteral(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CoreTheoremProducer::rewriteNotIff(), CVC3::CoreTheoremProducer::rewriteNotIte(), CVC3::CommonTheoremProducer::rewriteNotNot(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryArray::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::setup(), CVC3::SearchEngineFast::split(), CVC3::Theory::theoryOf(), SAT::CNF_Manager::translateExprRec(), CVC3::SearchEngineTheoremProducer::unitProp(), and CVC3::TheoryCore::update().

bool CVC3::Expr::isAnd

(

)

const [inline, inherited]

Definition at line 386 of file expr.h.

References CVC3::AND.

Referenced by CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andElim(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), and CVC3::CoreTheoremProducer::rewriteNotAnd().

bool CVC3::Expr::isOr

(

)

const [inline, inherited]

Definition at line 387 of file expr.h.

References CVC3::OR.

Referenced by CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::ClauseValue::ClauseValue(), SAT::CNF_Manager::convertLemma(), CVC3::SearchImplBase::isClause(), CVC3::SearchImplBase::isPropClause(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::TheoryCore::rewrite(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CommonTheoremProducer::rewriteOr(), and CVC3::CoreTheoremProducer::rewriteOrSubterms().

bool CVC3::Expr::isITE

(

)

const [inline, inherited]

Definition at line 388 of file expr.h.

References CVC3::ITE.

Referenced by CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CoreTheoremProducer::rewriteIteTrue(), and CVC3::CoreTheoremProducer::rewriteNotIte().

bool CVC3::Expr::isIff

(

)

const [inline, inherited]

Definition at line 389 of file expr.h.

References CVC3::IFF.

Referenced by CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::compare(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteNotIff(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), and CVC3::CommonTheoremProducer::skolemizeRewriteVar().

bool CVC3::Expr::isImpl

(

)

const [inline, inherited]

Definition at line 390 of file expr.h.

References CVC3::IMPLIES.

Referenced by CVC3::TheoryQuant::assertFact(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implMP(), CVC3::CoreTheoremProducer::ImpToIte(), and CVC3::CoreTheoremProducer::rewriteImplies().

bool CVC3::Expr::isXor

(

)

const [inline, inherited]

Definition at line 391 of file expr.h.

References CVC3::XOR.

Referenced by CVC3::CommonTheoremProducer::xorToIff().

bool CVC3::Expr::isForall

(

)

const [inline, inherited]

Definition at line 393 of file expr.h.

References CVC3::FORALL.

Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::TheoryQuant::assertFact(), CVC3::QuantTheoremProducer::boundVarElim(), hasMoreBVs(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), and CVC3::QuantTheoremProducer::universalInst().

bool CVC3::Expr::isExists

(

)

const [inline, inherited]

Definition at line 394 of file expr.h.

References CVC3::EXISTS.

Referenced by CVC3::TheoryQuant::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::SearchEngineFast::bcp(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::skolemize(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), and CVC3::CommonTheoremProducer::varIntroSkolem().

bool CVC3::Expr::isRational

(

)

const [inline, inherited]

Definition at line 396 of file expr.h.

References CVC3::RATIONAL_EXPR.

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::Expr::getRational(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::isIntegerConst(), isIntx(), CVC3::isRational(), CVC3::TheoryArith::isSyntacticRational(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::separateMonomial(), and usefulInMatch().

bool CVC3::Expr::isSkolem

(

)

const [inline, inherited]

Definition at line 397 of file expr.h.

References CVC3::SKOLEM_VAR.

Referenced by CVC3::VCCmd::findAxioms(), CVC3::Expr::getBoundIndex(), CVC3::Expr::getExistential(), and CVC3::TheoryArray::renameExpr().

const std::string & CVC3::Expr::getName

(

)

const [inline, inherited]

Definition at line 959 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getName(), and CVC3::Expr::isNull().

Referenced by CVC3::TheoryUF::assertFact(), CVC3::TheoryUF::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryRecords::getField(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::UFTheoremProducer::relToClosure(), and CVC3::UFTheoremProducer::relTrans().

const std::string & CVC3::Expr::getUid

(

)

const [inline, inherited]

For BOUND_VAR, get the UID.

Definition at line 1011 of file expr.h.

References CVC3::AST_LANG, CVC3::BOUND_VAR, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getKind(), CVC3::ExprValue::getUid(), and CVC3::Expr::toString().

Referenced by CVC3::TheoryCore::print(), CVC3::Expr::print(), and CVC3::Expr::printAST().

const std::string & CVC3::Expr::getString

(

)

const [inline, inherited]

Definition at line 964 of file expr.h.

References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getString(), CVC3::Expr::isString(), and CVC3::Expr::toString().

Referenced by CVC3::RecordsTheoremProducer::expandRecord(), CVC3::TheoryRecords::getField(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryUF::print(), CVC3::TheoryCore::print(), CVC3::Expr::print(), and CVC3::Expr::printAST().

const std::vector< Expr > & CVC3::Expr::getVars

(

)

const [inline, inherited]

Get bound variables from a closure Expr.

Definition at line 971 of file expr.h.

References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getVars(), CVC3::Expr::isClosure(), and CVC3::Expr::toString().

Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheoryArray::computeType(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::TheoryQuant::enqueueInst(), hasMoreBVs(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryQuant::print(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::TheoryQuant::recInstantiate(), CVC3::Expr::recursiveSubst(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::TheoryQuant::setupTriggers(), CVC3::CommonTheoremProducer::skolemize(), CVC3::VCCmd::skolemizeAx(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::QuantTheoremProducer::universalInst(), and CVC3::CommonTheoremProducer::varIntroSkolem().

const Expr & CVC3::Expr::getExistential

(

)

const [inline, inherited]

Get the existential axiom expression for skolem constant.

Definition at line 985 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getExistential(), and CVC3::Expr::isSkolem().

Referenced by CVC3::VCCmd::findAxioms(), and CVC3::Expr::printAST().

int CVC3::Expr::getBoundIndex

(

)

const [inline, inherited]

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

Definition at line 990 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getBoundIndex(), and CVC3::Expr::isSkolem().

const Expr & CVC3::Expr::getBody

(

)

const [inline, inherited]

Get the body of the closure Expr.

Definition at line 978 of file expr.h.

References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getBody(), CVC3::Expr::isClosure(), and CVC3::Expr::toString().

Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::ExprSkolem::computeHash(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryArray::computeType(), CVC3::VCCmd::findAxioms(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryQuant::print(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::QuantTheoremProducer::recFindBoundVars(), recGetSubTerms(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::TheoryQuant::recursiveMap(), CVC3::Expr::recursiveSubst(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::skolemize(), CVC3::VCCmd::skolemizeAx(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), and CVC3::QuantTheoremProducer::universalInst().

const Rational & CVC3::Expr::getRational

(

)

const [inline, inherited]

Get the Rational value out of RATIONAL_EXPR.

Definition at line 997 of file expr.h.

References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getRational(), CVC3::Expr::isRational(), and CVC3::Expr::toString().

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultPowLeaf(), CVC3::ArithTheoremProducer::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowPow(), CVC3::ArithTheoremProducer::canonMultPowPow(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithNew::checkSatSimplex(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::TheoryArithNew::findCoefficient(), CVC3::TheoryArithOld::findRationalBound(), CVC3::TheoryArithNew::findRationalBound(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::TheoryRecords::getIndex(), CVC3::TheoryBitvector::getSXIndex(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::isIntegerConst(), isIntx(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith::isSyntacticRational(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::Translator::preprocessRec(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::TheoryArithNew::registerAtom(), CVC3::TheoryArith::rewriteToDiff(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::TheoryArithOld::updateStats(), CVC3::TheoryArithNew::updateStats(), and CVC3::TheoryArithOld::updateSubsumptionDB().

const Theorem & CVC3::Expr::getTheorem

(

)

const [inline, inherited]

Get theorem from THEOREM_EXPR.

Definition at line 1004 of file expr.h.

References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getTheorem(), CVC3::Expr::isTheorem(), and CVC3::Expr::toString().

Referenced by CVC3::Expr::printAST().

ExprManager * CVC3::Expr::getEM

(

)

const [inline, inherited]

Definition at line 1018 of file expr.h.

References CVC3::ExprValue::d_em, CVC3::Expr::d_expr, and DebugAssert.

Referenced by CVC3::ExprStream::addLetHeader(), CVC3::Expr::addToNotify(), CVC3::arrayLiteral(), CVC3::Expr::begin(), CVC3::Expr::clearFlags(), CVC3::TheoryCore::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryArithNew::computeTypePred(), CVC3::Theory::computeTypePred(), CVC3::Expr::end(), CVC3::Expr::Expr(), CVC3::Expr::getFlag(), CVC3::Expr::getKids(), CVC3::Expr::getType(), hasBoundVar(), CVC3::Expr::hash(), CVC3::Expr::indent(), CVC3::Expr::isType(), CVC3::ExprManager::newLeafExpr(), CVC3::ExprManager::newSkolemExpr(), CVC3::operator<<(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::Expr::pprint(), CVC3::Expr::pprintnodag(), CVC3::Theorem::print(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::ExprManager::rebuild(), CVC3::Expr::recursiveSubst(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::Expr::setFind(), CVC3::Expr::setFlag(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), CVC3::Expr::setSimpCache(), CVC3::Expr::skolemExpr(), CVC3::Expr::toString(), CVC3::Type::Type(), CVC3::QuantTheoremProducer::universalInst(), and CVC3::Expr::validSimpCache().

const std::vector< Expr > & CVC3::Expr::getKids

(

)

const [inline, inherited]

Definition at line 1024 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getEM(), CVC3::ExprManager::getEmptyVector(), CVC3::ExprValue::getKids(), and CVC3::Expr::isNull().

Referenced by CVC3::CoreTheoremProducer::AndToIte(), CVC3::UFTheoremProducer::applyLambda(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::TheoryRecords::getFields(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::Translator::preprocessRec(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::TheoryArithOld::separateMonomial(), and CVC3::TheoryArithNew::separateMonomial().

int CVC3::Expr::getKind

(

)

const [inline, inherited]

Definition at line 1030 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_kind, and CVC3::NULL_KIND.

Referenced by CVC3::Theory::addBoundVar(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::BitvectorTheoremProducer::andOne(), CVC3::TheoryUF::assertFact(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), canGetHead(), CVC3::TheoryQuant::canMatch(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonInvert(), CVC3::ArithTheoremProducer::canonInvert(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultPlusPlus(), CVC3::ArithTheoremProducer::canonMultPlusPlus(), CVC3::ArithTheoremProducerOld::canonMultPowLeaf(), CVC3::ArithTheoremProducer::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowPow(), CVC3::ArithTheoremProducer::canonMultPowPow(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryUF::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryCore::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), CVC3::computeBVConst(), CVC3::TheoryBitvector::computeBVConst(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArray::computeModelTerm(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryBitvector::computeNegBVConst(), CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryCore::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryCore::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryArithNew::computeTypePred(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::Translator::containsArray(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::Translator::dump(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::SearchSat::findSplitterRec(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::TheoryDatatype::getConsForTester(), CVC3::TheoryDatatype::getConsPos(), getHeadExpr(), getLeft(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), getRight(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::Theory::getTCC(), CVC3::Theory::getTypePred(), CVC3::Expr::getUid(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), hasBoundVarRec(), CVC3::Expr::isApply(), CVC3::isArray(), CVC3::isArrayLiteral(), CVC3::TheoryArith::isAtomicArithFormula(), CVC3::TheoryArith::isAtomicArithTerm(), CVC3::Expr::isAtomicFormula(), CVC3::Expr::isBoolConnective(), CVC3::isConstructor(), CVC3::isDarkShadow(), CVC3::isDatatype(), CVC3::isDivide(), CVC3::isGE(), CVC3::isGrayShadow(), CVC3::isGT(), CVC3::isInt(), CVC3::isIntPred(), CVC3::Expr::isLambda(), CVC3::isLE(), CVC3::isLT(), CVC3::isMinus(), CVC3::isMult(), CVC3::TheoryArithOld::isolateVariable(), CVC3::isPlus(), CVC3::isPow(), CVC3::Expr::isQuantifier(), CVC3::isRead(), CVC3::isReal(), CVC3::TheoryArith::isSyntacticRational(), CVC3::isUMinus(), CVC3::isWrite(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ExprManager::newBoundVarExpr(), CVC3::Theory::newFunction(), CVC3::Theory::newVar(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::TheoryArithNew::ExprBoundInfo::operator<(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::operator<<(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryUF::parseExprOp(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheorySimulate::print(), CVC3::TheoryQuant::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryArray::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryArithNew::print(), CVC3::Expr::print(), CVC3::Translator::printArrayExpr(), CVC3::Expr::printAST(), CVC3::TheoryCore::processEquality(), CVC3::Translator::processType(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::QuantTheoremProducer::recFindBoundVars(), CVC3::TheoryQuant::recGeneralTrig(), CVC3::TheoryQuant::recSynMatch(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::TheoryQuant::recursiveMap(), CVC3::Expr::recursiveSubst(), CVC3::TheoryArithNew::registerAtom(), CVC3::Theory::resolveID(), CVC3::TheoryUF::rewrite(), CVC3::TheorySimulate::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::TheoryCore::rewriteLitCore(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::TheoryArith::rewriteToDiff(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rewriteXOR(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::TheoryUF::setup(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryDatatype::setup(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::Theory::theoryOf(), and SAT::CNF_Manager::translateExprRec().

ExprIndex CVC3::Expr::getIndex

(

)

const [inline, inherited]

Definition at line 1035 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::d_index.

Referenced by CVC3::compare(), CVC3::Expr::hasLastIndex(), CVC3::TheoryCore::print(), CVC3::Expr::printAST(), and CVC3::RegTheoremValue::RegTheoremValue().

bool CVC3::Expr::hasLastIndex

(

)

const [inline, inherited]

Definition at line 1037 of file expr.h.

References CVC3::ExprValue::d_em, CVC3::Expr::d_expr, CVC3::Expr::getIndex(), and CVC3::ExprManager::lastIndex().

Op CVC3::Expr::mkOp

(

)

const [inline, inherited]

Make the expr into an operator.

Definition at line 1040 of file expr.h.

References DebugAssert, CVC3::Expr::isNull(), and CVC3::Expr::Op.

Referenced by CVC3::TheoryUF::computeTCC(), CVC3::VCL::createOp(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::VCL::lambdaExpr(), CVC3::Theory::newFunction(), CVC3::Theory::newSubtypeExpr(), CVC3::TheoryCore::parseExpr(), and CVC3::TheoryUF::parseExprOp().

Op CVC3::Expr::getOp

(

)

const [inline, inherited]

Get operator from expression.

Definition at line 1045 of file expr.h.

References CVC3::Expr::arity(), CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getKind(), CVC3::ExprValue::getOp(), CVC3::Expr::isApply(), CVC3::Expr::isNull(), and CVC3::Expr::Op.

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::BitvectorTheoremProducer::andOne(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryDatatype::computeType(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::extractBitwise(), getHeadExpr(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryBitvector::print(), CVC3::Expr::printAST(), CVC3::Translator::processType(), CVC3::ExprTransform::pushNegation1(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryQuant::recGeneralTrig(), CVC3::Expr::recursiveSubst(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), and CVC3::CommonTheoremProducer::substitutivityRule().

Expr CVC3::Expr::getOpExpr

(

)

const [inline, inherited]

Get expression of operator (for APPLY Exprs only).

Definition at line 1053 of file expr.h.

References DebugAssert, CVC3::Op::getExpr(), CVC3::Expr::getOp(), and CVC3::Expr::isApply().

Referenced by CVC3::UFTheoremProducer::applyLambda(), CVC3::TheoryUF::assertFact(), CVC3::TheoryCore::computeType(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::getConstructor(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryRecords::getField(), CVC3::TheoryRecords::getFields(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::TheoryRecords::getIndex(), CVC3::TheoryBitvector::getSXIndex(), CVC3::TheoryBitvector::getTypePredType(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::UFTheoremProducer::relTrans(), CVC3::TheoryUF::rewrite(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().

int CVC3::Expr::getOpKind

(

)

const [inline, inherited]

Get kind of operator (for APPLY Exprs only).

Definition at line 1058 of file expr.h.

References CVC3::Op::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), and CVC3::Expr::isApply().

Referenced by CVC3::BitvectorTheoremProducer::andOne(), CVC3::BitvectorTheoremProducer::andZero(), CVC3::UFTheoremProducer::applyLambda(), CVC3::TheoryUF::assertFact(), CVC3::TheoryRecords::assertFact(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::TheoryBitvector::BVSize(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::TheoryRecords::checkType(), CVC3::TheoryBitvector::checkType(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryBitvector::computeModelTerm(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryRecords::computeTypePred(), CVC3::TheoryBitvector::computeTypePred(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::TheoryBitvector::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryRecords::getField(), CVC3::TheoryRecords::getFields(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::TheoryRecords::getIndex(), CVC3::TheoryBitvector::getSXIndex(), CVC3::TheoryBitvector::getTypePredExpr(), CVC3::TheoryBitvector::getTypePredType(), CVC3::isConstructor(), CVC3::TheoryRecords::isRecord(), CVC3::TheoryRecords::isRecordAccess(), CVC3::TheoryRecords::isRecordType(), CVC3::isSelector(), CVC3::isTester(), CVC3::TheoryRecords::isTuple(), CVC3::TheoryRecords::isTupleAccess(), CVC3::TheoryRecords::isTupleType(), CVC3::Expr::isType(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVCompExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVIndexExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVNandExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVNorExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::BitvectorTheoremProducer::orOne(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::TheoryBitvector::pad(), CVC3::BitvectorTheoremProducer::pad(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryBitvector::parseExprOp(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryRecords::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryBitvector::pushNegation(), CVC3::UFTheoremProducer::relTrans(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryBitvector::rewriteConst(), CVC3::RecordsTheoremProducer::rewriteLitSelect(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::RecordsTheoremProducer::rewriteUpdateSelect(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::sameKidCheck(), CVC3::TheoryRecords::setup(), CVC3::TheoryBitvector::setup(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryBitvector::signExtendBVLT(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::TheoryCore::simplify(), CVC3::TheoryBitvector::simplifyOp(), CVC3::Theory::theoryOf(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::TheoryUF::update(), CVC3::TheoryRecords::update(), CVC3::TheoryBitvector::update(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

int CVC3::Expr::arity

(

)

const [inline, inherited]

Definition at line 1063 of file expr.h.

References CVC3::ExprValue::arity(), CVC3::Expr::d_expr, and CVC3::Expr::isNull().

Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andElim(), CVC3::BitvectorTheoremProducer::andOne(), CVC3::BitvectorTheoremProducer::andZero(), CVC3::SearchImplBase::applyCNFRules(), CVC3::UFTheoremProducer::applyLambda(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryUF::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::TheoryArithNew::boundsAsString(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::TheoryDatatype::canCollapse(), CVC3::TheoryQuant::canMatch(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithNew::checkSatSimplex(), CVC3::TheoryUF::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryCore::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::Circuit::Circuit(), CVC3::ClauseValue::ClauseValue(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheorySimulate::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryRecords::computeTypePred(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), constantKids(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), SAT::CNF_Manager::convertLemma(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::Translator::dump(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::VCCmd::findAxioms(), CVC3::TheoryArithNew::findCoefficient(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::TheoryDatatype::getConstant(), getLeft(), CVC3::TheoryArithNew::getLowerBoundExplanation(), CVC3::Expr::getOp(), getRight(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), hasBoundVarRec(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implMP(), CVC3::Expr::isAtomic(), CVC3::TheoryArith::isAtomicArithTerm(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), isSimpleTrig(), isSuperSimpleTrig(), CVC3::isTrivialExpr(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::TheoryArithNew::kidsCanonical(), CVC3::Theory::leavesAreSimp(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::TheoryQuant::matchChild(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::TheoryQuant::newTopMatch(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::Expr::operator[](), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::orOne(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryUF::parseExprOp(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheorySimulate::print(), CVC3::TheoryRecords::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryArray::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryArithNew::print(), CVC3::Expr::print(), CVC3::TheoryCore::processCond(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::Translator::processType(), CVC3::Circuit::propagate(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryQuant::recSynMatch(), recursiveExprScore(), recursiveGetPartTriggers(), CVC3::TheoryQuant::recursiveMap(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBV(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::TheoryArith::rewriteToDiff(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rewriteXOR(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::separateMonomial(), setRecursiveInUserAssumption(), CVC3::TheoryArray::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::setup(), CVC3::Theory::setupCC(), CVC3::TheoryArithOld::setupRec(), CVC3::TheoryArithNew::setupRec(), CVC3::TheoryCore::setupSubFormulas(), CVC3::TheoryCore::setupTerm(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), CVC3::Theory::updateCC(), CVC3::TheoryArithNew::updateDependencies(), CVC3::Theory::updateHelper(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArithNew::updateValue(), usefulInMatch(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), and CVC3::BitvectorTheoremProducer::zeroLeq().

const Expr & CVC3::Expr::operator[]

(

int

i

)

const [inline, inherited]

Definition at line 1068 of file expr.h.

References CVC3::Expr::arity(), CVC3::Expr::d_expr, DebugAssert, and CVC3::ExprValue::getKids().

const Expr& CVC3::Expr::unnegate

(

)

const [inline, inherited]

Remove leading NOT if any.

Definition at line 461 of file expr.h.

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

Expr::iterator CVC3::Expr::begin

(

)

const [inline, inherited]

Begin iterator.

Definition at line 1073 of file expr.h.

References CVC3::ExprValue::arity(), CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::ExprValue::getKids(), and CVC3::Expr::isNull().

Referenced by CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::addToBuffer(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultPlusPlus(), CVC3::ArithTheoremProducer::canonMultPlusPlus(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryUF::checkType(), CVC3::TheoryRecords::checkType(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::ExprStream::collectShared(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryBitvector::computeModelTerm(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryCore::computeTCC(), CVC3::Theory::computeTCC(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::BitvectorTheoremProducer::concatFlatten(), constantKids(), CVC3::Translator::containsArray(), SAT::CNF_Manager::convertLemma(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::VCCmd::findAxioms(), CVC3::Theory::findReduced(), CVC3::TheoryBitvector::flattenBVPlus(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::Expr::isAtomicFormula(), CVC3::SearchImplBase::isClause(), CVC3::Theory::isLeafIn(), CVC3::SearchImplBase::isPropClause(), CVC3::TheoryArithOld::isStale(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryBitvector::print(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::QuantTheoremProducer::recFindBoundVars(), CVC3::TheoryQuant::recGeneralTrig(), recGetSubTerms(), CVC3::TheoryRecords::recordExpr(), CVC3::TheoryArith::recursiveCanonSimpCheck(), recursiveExprScore(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::TheoryQuant::recursiveMap(), CVC3::Expr::recursiveSubst(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::subExprRec(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithNew::updateDependenciesAdd(), CVC3::TheoryArithNew::updateDependenciesRemove(), and CVC3::TheoryArithOld::updateSubsumptionDB().

Expr::iterator CVC3::Expr::end

(

)

const [inline, inherited]

End iterator.

Definition at line 1079 of file expr.h.

References CVC3::ExprValue::arity(), CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::ExprValue::getKids(), and CVC3::Expr::isNull().

Referenced by CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::addToBuffer(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultPlusPlus(), CVC3::ArithTheoremProducer::canonMultPlusPlus(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryUF::checkType(), CVC3::TheoryRecords::checkType(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::ExprStream::collectShared(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryBitvector::computeModelTerm(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryCore::computeTCC(), CVC3::Theory::computeTCC(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::BitvectorTheoremProducer::concatFlatten(), constantKids(), CVC3::Translator::containsArray(), SAT::CNF_Manager::convertLemma(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::VCCmd::findAxioms(), CVC3::Theory::findReduced(), CVC3::TheoryBitvector::flattenBVPlus(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::Expr::isAtomicFormula(), CVC3::SearchImplBase::isClause(), CVC3::Theory::isLeafIn(), CVC3::SearchImplBase::isPropClause(), CVC3::TheoryArithOld::isStale(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryBitvector::print(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::QuantTheoremProducer::recFindBoundVars(), CVC3::TheoryQuant::recGeneralTrig(), recGetSubTerms(), CVC3::TheoryArith::recursiveCanonSimpCheck(), recursiveExprScore(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::TheoryQuant::recursiveMap(), CVC3::Expr::recursiveSubst(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::subExprRec(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithNew::updateDependenciesAdd(), CVC3::TheoryArithNew::updateDependenciesRemove(), and CVC3::TheoryArithOld::updateSubsumptionDB().

bool CVC3::Expr::isNull

(

)

const [inline, inherited]

Definition at line 1085 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_kind, and CVC3::NULL_KIND.

Referenced by CVC3::Expr::addToNotify(), CVC3::Expr::arity(), CVC3::TheoryUF::assertFact(), CVC3::SearchSat::assertLit(), CVC3::Expr::begin(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::SearchSimple::checkValidRec(), CVC3::ExprManager::clear(), CVC3::Expr::clearFlags(), CVC3::Expr::clearRewriteNormal(), CVC3::TheoryArray::computeModel(), CVC3::TypeComputerCore::computeType(), CVC3::ExprManager::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::Expr::end(), CVC3::VCCmd::evaluateCommand(), CVC3::Expr::Expr(), CVC3::ExprApply::ExprApply(), CVC3::ExprApplyTmp::ExprApplyTmp(), CVC3::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineDFS::findSplitter(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::DecisionEngine::findSplitterRec(), CVC3::SearchEngineFast::fixConflict(), CVC3::Theory::getBaseType(), CVC3::TheoryDatatype::getConstant(), CVC3::RWTheoremValue::getExpr(), CVC3::Expr::getFlag(), CVC3::Expr::getKids(), CVC3::Expr::getMMIndex(), CVC3::Expr::getName(), CVC3::VariableValue::getNegExpr(), CVC3::Expr::getNotify(), CVC3::Expr::getOp(), CVC3::Expr::getRep(), CVC3::Expr::getSig(), CVC3::Expr::getType(), CVC3::Expr::hasFind(), CVC3::ExprManager::hash(), CVC3::Expr::hasRep(), CVC3::Expr::hasSig(), CVC3::Expr::indent(), CVC3::Proof::isNull(), CVC3::Expr::lookupType(), CVC3::Expr::mkOp(), CVC3::ExprManager::newLeafExpr(), CVC3::Theory::newSubtypeExpr(), CVC3::Theory::newTypeExpr(), CVC3::Theory::newVar(), CVC3::Op::Op(), CVC3::operator<<(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryUF::parseExprOp(), CVC3::Expr::pprint(), CVC3::Expr::pprintnodag(), CVC3::Expr::print(), CVC3::Expr::printAST(), CVC3::ExprManager::rebuild(), CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::setFind(), CVC3::Expr::setFinite(), CVC3::Expr::setFlag(), CVC3::Expr::setImpliedLiteral(), CVC3::Expr::setIntAssumption(), CVC3::Expr::setInUserAssumption(), CVC3::Expr::setIsAtomicFlag(), CVC3::Expr::setJustified(), CVC3::Expr::setRegisteredAtom(), CVC3::Expr::setRep(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::Expr::setSig(), CVC3::Expr::setSimpCache(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTranslated(), CVC3::Expr::setType(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setValidType(), CVC3::Expr::setWellFounded(), CVC3::SearchEngineFast::split(), CVC3::Theory::theoryOf(), CVC3::Expr::toString(), CVC3::Type::Type(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().

bool CVC3::Expr::isInitialized

(

)

const [inline, inherited]

Definition at line 473 of file expr.h.

size_t CVC3::Expr::getMMIndex

(

)

const [inline, inherited]

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

Definition at line 1089 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getMMIndex(), and CVC3::Expr::isNull().

bool CVC3::Expr::hasFind

(

)

const [inline, inherited]

Definition at line 1094 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_find, DebugAssert, and CVC3::Expr::isNull().

Referenced by CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::SearchSimple::checkValidRec(), CVC3::Theory::find(), CVC3::Theory::findExpr(), CVC3::Theory::findReduced(), CVC3::Theory::findRef(), CVC3::Expr::getFind(), CVC3::Expr::getFindLevel(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::TheoryCore::getTheoremForTerm(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::Theory::leavesAreSimp(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArith::recursiveCanonSimpCheck(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryArithOld::setupRec(), CVC3::TheoryArithNew::setupRec(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplify(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryRecords::update(), CVC3::TheoryCore::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().

const Theorem & CVC3::Expr::getFind

(

)

const [inline, inherited]

Definition at line 1099 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_find, DebugAssert, and CVC3::Expr::hasFind().

Referenced by CVC3::Theory::find(), CVC3::Theory::findReduced(), CVC3::Theory::findRef(), CVC3::Theory::leavesAreSimp(), and CVC3::TheoryRecords::rewriteAux().

int CVC3::Expr::getFindLevel

(

)

const [inline, inherited]

Definition at line 1104 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_find, DebugAssert, and CVC3::Expr::hasFind().

NotifyList * CVC3::Expr::getNotify

(

)

const [inline, inherited]

Definition at line 1109 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_notifyList, and CVC3::Expr::isNull().

Referenced by CVC3::Expr::addToNotify(), CVC3::TheoryCore::assertEqualities(), and CVC3::TheoryCore::setFindLiteral().

const Type CVC3::Expr::getType

(

)

const [inline, inherited]

Get the type. Recursively compute if necessary.

Definition at line 1114 of file expr.h.

References CVC3::ExprManager::computeType(), CVC3::Expr::d_expr, CVC3::ExprValue::d_type, CVC3::Expr::getEM(), CVC3::Type::isNull(), CVC3::Expr::isNull(), and CVC3::Expr::s_null.

Referenced by CVC3::CoreTheoremProducer::AndToIte(), CVC3::VCL::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::SearchSat::check(), CVC3::TheoryCore::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryUF::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryBitvector::computeModelTerm(), CVC3::TheoryUF::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::ExprManager::computeType(), CVC3::VCL::createOp(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), findPolarity(), CVC3::Translator::finish(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::Theory::getBaseType(), CVC3::RWTheoremValue::getExpr(), CVC3::VCL::getType(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::Expr::isAtomic(), CVC3::Expr::isAtomicFormula(), CVC3::Expr::isBoolConnective(), CVC3::isConstructor(), CVC3::TheoryArithOld::isIntegerThm(), CVC3::TheoryArithNew::isIntegerThm(), CVC3::Expr::isTerm(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVCompExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVIndexExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVNandExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVNorExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::Theory::newSubtypeExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::TheoryQuant::newTopMatch(), CVC3::Theory::newVar(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::TheoryBitvector::pad(), CVC3::BitvectorTheoremProducer::pad(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryBitvector::parseExprOp(), CVC3::Translator::preprocess2Rec(), CVC3::TheoryCore::print(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryBitvector::pushNegation(), CVC3::VCL::query(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryUF::rewrite(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryQuant::setupTriggers(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::VCL::simplifyThm(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CoreTheoremProducer::typePred(), CVC3::TheoryUF::update(), CVC3::Theory::updateCC(), CVC3::VCL::varExpr(), CVC3::CommonTheoremProducer::varIntroRule(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

const Type CVC3::Expr::lookupType

(

)

const [inline, inherited]

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

Definition at line 1120 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_type, CVC3::Expr::isNull(), and CVC3::Expr::s_null.

Referenced by CVC3::TheoryDatatype::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryCore::computeTypePred(), CVC3::Theory::getBaseType(), CVC3::Theory::lookupVar(), and CVC3::ExprManager::newBoundVarExpr().

bool CVC3::Expr::validSimpCache

(

)

const [inline, inherited]

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

Definition at line 1125 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_simpCacheTag, CVC3::Expr::getEM(), and CVC3::ExprManager::getSimpCacheTag().

Referenced by CVC3::TheoryCore::simplify(), and CVC3::ExprTransform::smartSimplify().

const Theorem & CVC3::Expr::getSimpCache

(

)

const [inline, inherited]

Definition at line 1129 of file expr.h.

References CVC3::Expr::d_expr, and CVC3::ExprValue::d_simpCache.

Referenced by CVC3::TheoryCore::simplify().

bool CVC3::Expr::isValidType

(

)

const [inline, inherited]

Definition at line 1133 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::VALID_TYPE.

Referenced by CVC3::ExprManager::checkType().

bool CVC3::Expr::validIsAtomicFlag

(

)

const [inline, inherited]

Definition at line 1137 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::VALID_IS_ATOMIC.

Referenced by CVC3::Expr::isAtomic().

bool CVC3::Expr::getIsAtomicFlag

(

)

const [inline, inherited]

Definition at line 1141 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_ATOMIC.

Referenced by CVC3::Expr::isAtomic().

bool CVC3::Expr::isRewriteNormal

(

)

const [inline, inherited]

Definition at line 1145 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::REWRITE_NORMAL.

Referenced by CVC3::TheoryCore::rewriteCore().

bool CVC3::Expr::isFinite

(

)

const [inline, inherited]

Definition at line 1149 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_FINITE.

Referenced by CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), and CVC3::TheoryDatatype::instantiate().

bool CVC3::Expr::isWellFounded

(

)

const [inline, inherited]

Definition at line 1153 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::WELL_FOUNDED.

bool CVC3::Expr::computeTransClosure

(

)

const [inline, inherited]

Definition at line 1157 of file expr.h.

References CVC3::Expr::COMPUTE_TRANS_CLOSURE, CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, and CVC3::CDFlags::get().

Referenced by CVC3::TheoryUF::assertFact(), and CVC3::TheoryUF::update().

bool CVC3::Expr::containsBoundVar

(

)

const [inline, inherited]

Definition at line 1161 of file expr.h.

References CVC3::Expr::CONTAINS_BOUND_VAR, CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, and CVC3::CDFlags::get().

Referenced by CVC3::TheoryQuant::recGeneralTrig(), CVC3::TheoryQuant::recSynMatch(), and recursiveGetBoundVars().

bool CVC3::Expr::isImpliedLiteral

(

)

const [inline, inherited]

Definition at line 1165 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IMPLIED_LITERAL.

Referenced by CVC3::TheoryCore::setFindLiteral(), and CVC3::TheoryCore::update().

bool CVC3::Expr::isUserAssumption

(

)

const [inline, inherited]

Definition at line 1169 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_USER_ASSUMPTION.

Referenced by CVC3::SearchSat::getAssumptions(), and CVC3::SearchSat::isAssumption().

bool CVC3::Expr::inUserAssumption

(

)

const [inline, inherited]

Definition at line 1173 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IN_USER_ASSUMPTION.

Referenced by setRecursiveInUserAssumption().

bool CVC3::Expr::isIntAssumption

(

)

const [inline, inherited]

Definition at line 1177 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_INT_ASSUMPTION.

Referenced by CVC3::SearchSat::assertLit(), and CVC3::SearchSat::isAssumption().

bool CVC3::Expr::isJustified

(

)

const [inline, inherited]

Definition at line 1181 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_JUSTIFIED.

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

bool CVC3::Expr::isTranslated

(

)

const [inline, inherited]

Definition at line 1185 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_TRANSLATED.

Referenced by SAT::CNF_Manager::getCNFLit(), CVC3::TheoryDatatypeLazy::instantiate(), and SAT::CNF_Manager::translateExprRec().

bool CVC3::Expr::isUserRegisteredAtom

(

)

const [inline, inherited]

Definition at line 1189 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_USER_REGISTERED_ATOM.

Referenced by CVC3::SearchSat::getImplication(), CVC3::SearchSat::getImpliedLiteral(), and SAT::CNF_Manager::registerAtom().

bool CVC3::Expr::isRegisteredAtom

(

)

const [inline, inherited]

Definition at line 1193 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_REGISTERED_ATOM.

Referenced by CVC3::TheoryCore::registerAtom(), CVC3::SearchSat::registerAtom(), SAT::CNF_Manager::registerAtom(), CVC3::TheoryCore::setFindLiteral(), and CVC3::TheoryCore::update().

bool CVC3::Expr::isSelected

(

)

const [inline, inherited]

Definition at line 1197 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_SELECTED.

Referenced by CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), and CVC3::TheoryDatatype::update().

bool CVC3::Expr::isStoredPredicate

(

)

const [inline, inherited]

Definition at line 1201 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_STORED_PREDICATE.

Referenced by CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::TheoryCore::getTheoremForTerm(), and CVC3::TheoryCore::setupTerm().

bool CVC3::Expr::getFlag

(

)

const [inline, inherited]

Check if the generic flag is set.

Definition at line 1205 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_flag, DebugAssert, CVC3::Expr::getEM(), and CVC3::Expr::isNull().

Referenced by hasBoundVarRec(), recGetSubTerms(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::Expr::recursiveSubst(), and CVC3::subExprRec().

void CVC3::Expr::setFlag

(

)

const [inline, inherited]

Set the generic flag.

Definition at line 1210 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_flag, DebugAssert, CVC3::Expr::getEM(), CVC3::ExprManager::getFlag(), and CVC3::Expr::isNull().

Referenced by hasBoundVarRec(), recGetSubTerms(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::Expr::recursiveSubst(), and CVC3::subExprRec().

void CVC3::Expr::clearFlags

(

)

const [inline, inherited]

Clear the generic flag in all Exprs.

Definition at line 1215 of file expr.h.

References CVC3::ExprManager::clearFlags(), DebugAssert, CVC3::Expr::getEM(), and CVC3::Expr::isNull().

Referenced by getBoundVars(), getPartTriggers(), CVC3::TheoryQuant::getSubTerms(), getSubTrig(), CVC3::Expr::recursiveSubst(), CVC3::Expr::subExprOf(), and CVC3::Expr::substExpr().

string CVC3::Expr::toString

(

)

const [inherited]

Print the expression to a string.

Definition at line 187 of file expr.cpp.

References CVC3::PRESENTATION_LANG.

Referenced by CVC3::Theory::addBoundVar(), CVC3::TheoryArithOld::VarOrderGraph::addEdge(), CVC3::TheoryCore::addFact(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::SearchSat::addLemma(), CVC3::TheoryBitvector::addSharedTerm(), CVC3::SearchImplBase::addSplitter(), CVC3::SearchEngineFast::addSplitter(), CVC3::SearchImplBase::addToCNFCache(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::BitvectorTheoremProducer::andOne(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::BitvectorTheoremProducer::andZero(), CVC3::SearchImplBase::applyCNFRules(), CVC3::UFTheoremProducer::applyLambda(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryUF::assertFact(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::TheoryArithNew::assertLower(), CVC3::TheoryBitvector::assertTypePred(), CVC3::TheoryArithNew::assertUpper(), CVC3::TheoryCore::assignValue(), CVC3::Theory::assignValue(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bitwiseConcat(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::TheoryArithNew::boundsAsString(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryCore::buildModel(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::TheoryBitvector::BVSize(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithNew::canon(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonInvert(), CVC3::ArithTheoremProducer::canonInvert(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultTerm1Term2(), CVC3::ArithTheoremProducer::canonMultTerm1Term2(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArithNew::canonSimplify(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::SearchSat::check(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::VCL::checkTCC(), CVC3::TheoryUF::checkType(), CVC3::TheoryRecords::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryCore::checkType(), CVC3::TypeComputerCore::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::Theory::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryCore::computeBaseType(), CVC3::computeBVConst(), CVC3::TheoryBitvector::computeBVConst(), CVC3::TheoryUF::computeModel(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryBitvector::computeNegBVConst(), CVC3::TheoryUF::computeTCC(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryCore::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::VCL::createOp(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::TheoryArithNew::deriveGomoryCut(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::TheoryCore::enqueueFact(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::VCCmd::evaluateCommand(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::RecordsTheoremProducer::expandRecord(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::RecordsTheoremProducer::expandTuple(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::TheoryArithNew::findCoefficient(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::TheoryArithOld::findRationalBound(), CVC3::TheoryArithNew::findRationalBound(), CVC3::SearchEngineFast::findSplitter(), CVC3::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::TheoryBitvector::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::TheoryArithOld::freeConstIneq(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::Expr::getBody(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::SearchEngine::getConcreteModel(), CVC3::TheoryDatatype::getConsForTester(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryRecords::getField(), CVC3::TheoryRecords::getFieldIndex(), CVC3::TheoryRecords::getFields(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::TheoryArithNew::getLowerBoundThm(), CVC3::Theory::getModelTerm(), CVC3::Expr::getRational(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::Expr::getString(), getSubTrig(), CVC3::TheoryBitvector::getSXIndex(), CVC3::Expr::getTheorem(), CVC3::TheoryBitvector::getTypePredExpr(), CVC3::TheoryBitvector::getTypePredType(), CVC3::Expr::getUid(), CVC3::TheoryArithNew::getUpperBoundThm(), CVC3::Expr::getVars(), CVC3::TheoryQuant::goodSynMatch(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::CoreTheoremProducer::IffToIte(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::implMP(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::RWTheoremValue::init(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryArithOld::isolateVariable(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::TheoryArithOld::lessThanVar(), CVC3::TheoryArithNew::lessThanVar(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newBVAndExpr(), CVC3::TheoryBitvector::newBVCompExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVIndexExpr(), CVC3::TheoryBitvector::newBVLEExpr(), CVC3::TheoryBitvector::newBVLTExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVNandExpr(), CVC3::TheoryBitvector::newBVNegExpr(), CVC3::TheoryBitvector::newBVNorExpr(), CVC3::TheoryBitvector::newBVOrExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::SearchImplBase::newIntAssumption(), CVC3::Theory::newSubtypeExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::TheoryBitvector::normalizeConcat(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::orOne(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::BitvectorTheoremProducer::orZero(), CVC3::QuantTheoremProducer::packVar(), CVC3::TheoryBitvector::pad(), CVC3::BitvectorTheoremProducer::pad(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::pivotAndUpdate(), CVC3::TheoryArithNew::pivotRule(), CVC3::Translator::preprocess(), CVC3::Translator::preprocess2(), CVC3::Translator::preprocess2Rec(), CVC3::TheoryCore::print(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryCore::processCond(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::propagateTheory(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::ExprManager::rebuildRec(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::TheoryQuant::recSynMatch(), CVC3::TheoryCore::refineCounterExample(), CVC3::TheoryArithNew::registerAtom(), CVC3::RegTheoremValue::RegTheoremValue(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::TheoryBitvector::rewriteAtomic(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CoreTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CoreTheoremProducer::rewriteIteTrue(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::TheoryCore::rewriteLiteral(), CVC3::RecordsTheoremProducer::rewriteLitSelect(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::RecordsTheoremProducer::rewriteUpdateSelect(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryCore::setFindLiteral(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), CVC3::TheoryBitvector::setup(), CVC3::TheoryQuant::setupTriggers(), CVC3::VariableValue::setValue(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::TheoryBitvector::signExtendBVLT(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::simplifyOp(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::TheoryCore::solve(), CVC3::TheoryArray::solve(), CVC3::SearchEngineFast::split(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::TheoremValue::toString(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::QuantTheoremProducer::universalInst(), CVC3::TheoryBitvector::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArithNew::updateDependencies(), CVC3::TheoryArithNew::updateDependenciesAdd(), CVC3::TheoryArithNew::updateDependenciesRemove(), CVC3::TheoryArithOld::updateSubsumptionDB(), usefulInMatch(), CVC3::CommonTheoremProducer::varIntroSkolem(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().

string CVC3::Expr::toString

(

InputLanguage

lang

)

const [inherited]

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

Definition at line 195 of file expr.cpp.

References CVC3::Expr::getEM(), CVC3::Expr::isNull(), CVC3::ExprStream::lang(), and CVC3::ExprStream::os().

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

Print the expression in the specified format.

Definition at line 205 of file expr.cpp.

References CVC3::ExprStream::dagFlag(), std::endl(), CVC3::Expr::getEM(), CVC3::Expr::isNull(), and CVC3::ExprStream::lang().

Referenced by CVC3::TheoryUF::print(), CVC3::TheoryQuant::print(), CVC3::TheoryCore::print(), CVC3::PrettyPrinterCore::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryArithNew::print(), and CVC3::Theorem::printx().

void CVC3::Expr::print

(

)

const [inline, inherited]

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

Definition at line 575 of file expr.h.

References CVC3::AST_LANG.

Referenced by CVC3::Expr::printnodag().

void CVC3::Expr::printnodag

(

)

const [inherited]

Print the expression as AST without dagifying.

Definition at line 237 of file expr.cpp.

References CVC3::AST_LANG, and CVC3::Expr::print().

Referenced by CVC3::Theorem::printxnodag().

void CVC3::Expr::pprint

(

)

const [inherited]

Pretty-print the expression.

Definition at line 216 of file expr.cpp.

References std::endl(), CVC3::Expr::getEM(), and CVC3::Expr::isNull().

Referenced by CVC3::Theorem::pprintx().

void CVC3::Expr::pprintnodag

(

)

const [inherited]

Pretty-print without dagifying.

Definition at line 226 of file expr.cpp.

References CVC3::ExprStream::dagFlag(), std::endl(), CVC3::Expr::getEM(), and CVC3::Expr::isNull().

Referenced by CVC3::Theorem::pprintxnodag().

ExprStream & CVC3::Expr::print

(

ExprStream &

os

)

const [inherited]

Print a leaf node.

Definition at line 301 of file expr.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::BOUND_VAR, DebugAssert, CVC3::Expr::end(), std::endl(), CVC3::EXISTS, CVC3::FALSE_EXPR, CVC3::FORALL, CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Expr::getKind(), CVC3::ExprManager::getKindName(), CVC3::Expr::getName(), CVC3::Expr::getRational(), CVC3::Expr::getString(), CVC3::Expr::getUid(), CVC3::Expr::getVars(), CVC3::Expr::hash(), CVC3::Expr::isNull(), CVC3::Expr::isQuantifier(), CVC3::Expr::isSymbol(), CVC3::NULL_KIND, CVC3::pop(), CVC3::push(), CVC3::RATIONAL_EXPR, CVC3::RAW_LIST, CVC3::ExprStream::resetIndent(), CVC3::SKOLEM_VAR, CVC3::space(), CVC3::STRING_EXPR, CVC3::TRUE_EXPR, and CVC3::UCONST.

ExprStream & CVC3::Expr::printAST

(

ExprStream &

os

)

const [inherited]

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

Definition at line 243 of file expr.cpp.

References CVC3::Expr::begin(), CVC3::BOUND_VAR, DebugAssert, CVC3::Expr::end(), std::endl(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Expr::getExistential(), CVC3::Op::getExpr(), CVC3::Expr::getIndex(), CVC3::Expr::getKind(), CVC3::ExprManager::getKindName(), CVC3::Expr::getName(), CVC3::Expr::getOp(), CVC3::Expr::getRational(), CVC3::Expr::getString(), CVC3::Expr::getTheorem(), CVC3::Expr::getUid(), CVC3::Expr::getVars(), CVC3::Expr::isApply(), CVC3::Expr::isClosure(), CVC3::Expr::isNull(), CVC3::Expr::isString(), CVC3::Expr::isSymbol(), CVC3::Expr::isTheorem(), CVC3::Expr::isVar(), CVC3::LETDECL, CVC3::nodag(), CVC3::pop(), CVC3::push(), CVC3::RATIONAL_EXPR, CVC3::ExprStream::resetIndent(), CVC3::SKOLEM_VAR, CVC3::space(), CVC3::STRING_EXPR, CVC3::THEOREM_KIND, CVC3::Theorem::toString(), and CVC3::UCONST.

Referenced by CVC3::operator<<(), CVC3::TheoryUF::print(), CVC3::TheorySimulate::print(), CVC3::TheoryRecords::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryArray::print(), and CVC3::Theory::print().

Expr & CVC3::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 353 of file expr.cpp.

References DebugAssert, CVC3::Expr::getEM(), CVC3::ExprManager::indent(), and CVC3::Expr::isNull().

void CVC3::Expr::setFind

(

const Theorem &

e

)

const [inline, inherited]

Set the find attribute to e.

Definition at line 1220 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_find, DebugAssert, CVC3::Expr::getEM(), CVC3::Theorem::getLHS(), IF_DEBUG, CVC3::Expr::isNull(), and CVC3::ContextObj::setName().

Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::Theory::findRef(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryArithOld::setupRec(), and CVC3::TheoryArithNew::setupRec().

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

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

Definition at line 360 of file expr.cpp.

References CVC3::NotifyList::add(), CVC3::Expr::d_expr, CVC3::ExprValue::d_notifyList, DebugAssert, CVC3::Expr::getEM(), CVC3::Expr::getNotify(), and CVC3::Expr::isNull().

Referenced by CVC3::TheoryDatatype::addSharedTerm(), CVC3::TheoryBitvector::addSharedTerm(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::processUpdates(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryArray::setup(), CVC3::TheoryCore::setupSubFormulas(), CVC3::TheoryCore::update(), and CVC3::TheoryArray::update().

void CVC3::Expr::setType

(

const Type &

t

)

const [inline, inherited]

Set the cached type.

Definition at line 1231 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_type, DebugAssert, and CVC3::Expr::isNull().

Referenced by CVC3::TheoryQuant::checkSat(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryUF::computeType(), CVC3::TheorySimulate::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ExprManager::ExprManager(), and CVC3::ExprManager::newBoundVarExpr().

void CVC3::Expr::setSimpCache

(

const Theorem &

e

)

const [inline, inherited]

Definition at line 1236 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::d_simpCache, CVC3::ExprValue::d_simpCacheTag, DebugAssert, CVC3::Expr::getEM(), CVC3::ExprManager::getSimpCacheTag(), and CVC3::Expr::isNull().

Referenced by CVC3::TheoryCore::simplify().

void CVC3::Expr::setValidType

(

)

const [inline, inherited]

Definition at line 1242 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), CVC3::CDFlags::set(), and CVC3::Expr::VALID_TYPE.

void CVC3::Expr::setIsAtomicFlag

(

bool

value

)

const [inline, inherited]

Definition at line 1247 of file expr.h.

References CVC3::CDFlags::clear(), CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_ATOMIC, CVC3::Expr::isNull(), CVC3::CDFlags::set(), and CVC3::Expr::VALID_IS_ATOMIC.

Referenced by CVC3::Expr::isAtomic().

void CVC3::Expr::setRewriteNormal

(

)

const [inline, inherited]

Definition at line 1254 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), CVC3::Expr::REWRITE_NORMAL, CVC3::CDFlags::set(), and CVC3::TRACE.

Referenced by CVC3::TheoryUF::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::rewrite(), and CVC3::TheoryCore::rewriteCore().

void CVC3::Expr::clearRewriteNormal

(

)

const [inline, inherited]

Definition at line 1330 of file expr.h.

References CVC3::CDFlags::clear(), CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), and CVC3::Expr::REWRITE_NORMAL.

Referenced by CVC3::TheoryCore::rewriteCore().

void CVC3::Expr::setFinite

(

)

const [inline, inherited]

Definition at line 1260 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_FINITE, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

void CVC3::Expr::setWellFounded

(

)

const [inline, inherited]

Definition at line 1265 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), CVC3::CDFlags::set(), and CVC3::Expr::WELL_FOUNDED.

Referenced by CVC3::TheoryDatatype::dataType().

void CVC3::Expr::setComputeTransClosure

(

)

const [inline, inherited]

Definition at line 1270 of file expr.h.

References CVC3::Expr::COMPUTE_TRANS_CLOSURE, CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

void CVC3::Expr::setContainsBoundVar

(

)

const [inline, inherited]

Definition at line 1275 of file expr.h.

References CVC3::Expr::CONTAINS_BOUND_VAR, CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

Referenced by recursiveGetBoundVars().

void CVC3::Expr::setImpliedLiteral

(

)

const [inline, inherited]

Definition at line 1280 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IMPLIED_LITERAL, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

Referenced by CVC3::TheoryCore::setFindLiteral().

void CVC3::Expr::setUserAssumption

(

int

scope = -1

)

const [inline, inherited]

Definition at line 1285 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_USER_ASSUMPTION, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

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

void CVC3::Expr::setInUserAssumption

(

int

scope = -1

)

const [inline, inherited]

Definition at line 1290 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IN_USER_ASSUMPTION, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

Referenced by setRecursiveInUserAssumption().

void CVC3::Expr::setIntAssumption

(

)

const [inline, inherited]

Definition at line 1295 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_INT_ASSUMPTION, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

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

void CVC3::Expr::setJustified

(

)

const [inline, inherited]

Definition at line 1300 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_JUSTIFIED, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

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

void CVC3::Expr::setTranslated

(

int

scope = -1

)

const [inline, inherited]

Set the translated flag for this Expr.

Definition at line 1305 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_TRANSLATED, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

Referenced by CVC3::TheoryDatatypeLazy::instantiate(), and SAT::CNF_Manager::translateExprRec().

void CVC3::Expr::setUserRegisteredAtom

(

)

const [inline, inherited]

Set the UserRegisteredAtom flag for this Expr.

Definition at line 1310 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_USER_REGISTERED_ATOM, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

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

void CVC3::Expr::setRegisteredAtom

(

)

const [inline, inherited]

Set the RegisteredAtom flag for this Expr.

Definition at line 1315 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_REGISTERED_ATOM, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

Referenced by CVC3::TheoryCore::registerAtom().

void CVC3::Expr::setSelected

(

)

const [inline, inherited]

Set the Selected flag for this Expr.

Definition at line 1320 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_SELECTED, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

Referenced by CVC3::TheoryDatatypeLazy::checkSat(), and CVC3::TheoryDatatype::update().

void CVC3::Expr::setStoredPredicate

(

)

const [inline, inherited]

Set the Stored Predicate flag for this Expr.

Definition at line 1325 of file expr.h.

References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::IS_STORED_PREDICATE, CVC3::Expr::isNull(), and CVC3::CDFlags::set().

Referenced by CVC3::TheoryCore::setupTerm().

bool CVC3::Expr::subExprOf

(

const Expr &

e

)

const [inherited]

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

Definition at line 140 of file expr.cpp.

References CVC3::Expr::clearFlags(), and CVC3::subExprRec().

bool CVC3::Expr::hasSig

(

)

const [inline, inherited]

Definition at line 1335 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::getSig(), and CVC3::Expr::isNull().

bool CVC3::Expr::hasRep

(

)

const [inline, inherited]

Definition at line 1341 of file expr.h.

References CVC3::Expr::d_expr, CVC3::ExprValue::getRep(), and CVC3::Expr::isNull().

const Theorem & CVC3::Expr::getSig

(

)

const [inline, inherited]

Definition at line 1347 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getSig(), and CVC3::Expr::isNull().

Referenced by CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), and CVC3::Theory::updateCC().

const Theorem & CVC3::Expr::getRep

(

)

const [inline, inherited]

Definition at line 1356 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getRep(), and CVC3::Expr::isNull().

Referenced by CVC3::Theory::rewriteCC(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), and CVC3::Theory::updateCC().

void CVC3::Expr::setSig

(

const Theorem &

e

)

const [inline, inherited]

Definition at line 1365 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getEM(), CVC3::ExprValue::getSig(), IF_DEBUG, CVC3::Expr::isNull(), CVC3::CDO< T >::set(), CVC3::ContextObj::setName(), CVC3::ExprValue::setSig(), and CVC3::Expr::toString().

Referenced by CVC3::TheoryArray::setup(), CVC3::Theory::setupCC(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), and CVC3::Theory::updateCC().

void CVC3::Expr::setRep

(

const Theorem &

e

)

const [inline, inherited]

Definition at line 1376 of file expr.h.

References CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getEM(), CVC3::ExprValue::getRep(), IF_DEBUG, CVC3::Expr::isNull(), CVC3::CDO< T >::set(), CVC3::ContextObj::setName(), CVC3::ExprValue::setRep(), and CVC3::Expr::toString().

Referenced by CVC3::TheoryArray::setup(), CVC3::Theory::setupCC(), CVC3::TheoryUF::update(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArray::update(), and CVC3::Theory::updateCC().

---

Variable Documentation

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

Convenient null expr.

Definition at line 176 of file expr.h.

Referenced by CVC3::Expr::getType(), and CVC3::Expr::lookupType().

ExprValue* CVC3::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 CVC3::Expr::addToNotify(), CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::Expr::clearRewriteNormal(), CVC3::compare(), CVC3::Expr::computeTransClosure(), CVC3::Expr::containsBoundVar(), CVC3::Expr::end(), CVC3::Expr::Expr(), CVC3::Expr::getBody(), CVC3::Expr::getBoundIndex(), CVC3::Expr::getEM(), CVC3::Expr::getExistential(), CVC3::Expr::getExprValue(), CVC3::Expr::getFind(), CVC3::Expr::getFindLevel(), CVC3::Expr::getFlag(), CVC3::Expr::getIndex(), CVC3::Expr::getIsAtomicFlag(), CVC3::Expr::getKids(), CVC3::Expr::getKind(), CVC3::Expr::getMMIndex(), CVC3::Expr::getName(), CVC3::Expr::getNotify(), CVC3::Expr::getOp(), CVC3::Expr::getRational(), CVC3::Expr::getRep(), CVC3::Expr::getSig(), CVC3::Expr::getSimpCache(), CVC3::Expr::getString(), CVC3::Expr::getTheorem(), CVC3::Expr::getType(), CVC3::Expr::getUid(), CVC3::Expr::getVars(), CVC3::DecisionEngineMBTF::goalSatisfied(), CVC3::DecisionEngineCaching::goalSatisfied(), CVC3::Expr::hasFind(), CVC3::ExprManager::hash(), CVC3::Expr::hasLastIndex(), CVC3::Expr::hasRep(), CVC3::Expr::hasSig(), CVC3::Expr::inUserAssumption(), CVC3::Expr::isApply(), CVC3::Expr::isClosure(), CVC3::Expr::isFinite(), CVC3::Expr::isImpliedLiteral(), CVC3::Expr::isIntAssumption(), CVC3::Expr::isJustified(), CVC3::Expr::isNull(), CVC3::Expr::isRegisteredAtom(), CVC3::Expr::isRewriteNormal(), CVC3::Expr::isSelected(), CVC3::Expr::isStoredPredicate(), CVC3::Expr::isString(), CVC3::Expr::isSymbol(), CVC3::Expr::isTheorem(), CVC3::Expr::isTranslated(), CVC3::Expr::isUserAssumption(), CVC3::Expr::isUserRegisteredAtom(), CVC3::Expr::isValidType(), CVC3::Expr::isVar(), CVC3::Expr::isWellFounded(), CVC3::Expr::lookupType(), CVC3::Expr::operator=(), CVC3::operator==(), CVC3::Expr::operator[](), CVC3::ExprManager::rebuildRec(), CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::setFind(), CVC3::Expr::setFinite(), CVC3::Expr::setFlag(), CVC3::Expr::setImpliedLiteral(), CVC3::Expr::setIntAssumption(), CVC3::Expr::setInUserAssumption(), CVC3::Expr::setIsAtomicFlag(), CVC3::Expr::setJustified(), CVC3::Expr::setRegisteredAtom(), CVC3::Expr::setRep(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::Expr::setSig(), CVC3::Expr::setSimpCache(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTranslated(), CVC3::Expr::setType(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setValidType(), CVC3::Expr::setWellFounded(), CVC3::Expr::validIsAtomicFlag(), CVC3::Expr::validSimpCache(), and CVC3::Expr::~Expr().

---