CVC3
2.4.1
|
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, CVC3::Expr::USES_CC = 0x00080000, CVC3::Expr::VALID_TERMINALS_CONST = 0x00100000, CVC3::Expr::TERMINALS_CONST = 0x00200000 } |
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, CVC3::Expr::NOT_ARRAY_NORMALIZED = 0x00040000 } |
bit-masks for dynamic flags More... | |
Functions | |
CVC3::Expr::Expr (ExprValue *expr) | |
Private constructor, simply wraps around the pointer. More... | |
Expr | CVC3::Expr::recursiveSubst (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const |
Expr | CVC3::Expr::recursiveQuantSubst (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const |
std::vector< std::vector< Expr > > | CVC3::Expr::substTriggers (const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited) const |
CVC3::Expr::Expr () | |
Default constructor creates the Null Expr. More... | |
CVC3::Expr::Expr (const Expr &e) | |
Copy constructor and assignment (copy the pointer and take care of the refcount) More... | |
Expr & | CVC3::Expr::operator= (const Expr &e) |
Assignment operator: take care of the refcounting and GC. More... | |
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. More... | |
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::xorExpr (const Expr &right) const |
Expr | CVC3::Expr::skolemExpr (int i) const |
Create a Skolem constant for the i'th variable of an existential (*this) More... | |
Expr | CVC3::Expr::rebuild (ExprManager *em) const |
Create a Boolean variable out of the expression. More... | |
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::substExprQuant (const std::vector< Expr > &oldTerms, const std::vector< Expr > &newTerms) const |
Expr | CVC3::Expr::substExprQuant (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::isConstant () const |
bool | CVC3::Expr::isRawList () const |
bool | CVC3::Expr::isType () const |
Expr represents a type. More... | |
const ExprValue * | CVC3::Expr::getExprValue () const |
Provide access to ExprValue for client subclasses of ExprValue only More... | |
bool | CVC3::Expr::isTerm () const |
Test if e is a term (as opposed to a predicate/formula) More... | |
bool | CVC3::Expr::isAtomic () const |
Test if e is atomic. More... | |
bool | CVC3::Expr::isAtomicFormula () const |
Test if e is an atomic formula. More... | |
bool | CVC3::Expr::isAbsAtomicFormula () const |
An abstract atomic formua is an atomic formula or a quantified formula. More... | |
bool | CVC3::Expr::isLiteral () const |
Test if e is a literal. More... | |
bool | CVC3::Expr::isAbsLiteral () const |
Test if e is an abstract literal. More... | |
bool | CVC3::Expr::isBoolConnective () const |
A Bool connective is one of NOT,AND,OR,IMPLIES,IFF,XOR,ITE (with type Bool) More... | |
bool | CVC3::Expr::isPropAtom () const |
True iff expr is not a Bool connective. More... | |
bool | CVC3::Expr::isPropLiteral () const |
PropAtom or negation of PropAtom. More... | |
bool | CVC3::Expr::containsTermITE () const |
Return whether Expr contains a non-bool type ITE as a sub-term. More... | |
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. More... | |
const std::string & | CVC3::Expr::getString () const |
const std::vector< Expr > & | CVC3::Expr::getVars () const |
Get bound variables from a closure Expr. More... | |
const Expr & | CVC3::Expr::getExistential () const |
Get the existential axiom expression for skolem constant. More... | |
int | CVC3::Expr::getBoundIndex () const |
Get the index of the bound var that skolem constant comes from. More... | |
const Expr & | CVC3::Expr::getBody () const |
Get the body of the closure Expr. More... | |
void | CVC3::Expr::setTriggers (const std::vector< std::vector< Expr > > &triggers) const |
Set the triggers for a closure Expr. More... | |
void | CVC3::Expr::setTriggers (const std::vector< Expr > &triggers) const |
void | CVC3::Expr::setTrigger (const Expr &trigger) const |
void | CVC3::Expr::setMultiTrigger (const std::vector< Expr > &multiTrigger) const |
const std::vector< std::vector < Expr > > & | CVC3::Expr::getTriggers () const |
Get the manual triggers of the closure Expr. More... | |
const Rational & | CVC3::Expr::getRational () const |
Get the Rational value out of RATIONAL_EXPR. More... | |
const Theorem & | CVC3::Expr::getTheorem () const |
Get theorem from THEOREM_EXPR. More... | |
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. More... | |
Op | CVC3::Expr::getOp () const |
Get operator from expression. More... | |
Expr | CVC3::Expr::getOpExpr () const |
Get expression of operator (for APPLY Exprs only) More... | |
int | CVC3::Expr::getOpKind () const |
Get kind of operator (for APPLY Exprs only) More... | |
int | CVC3::Expr::arity () const |
const Expr & | CVC3::Expr::operator[] (int i) const |
const Expr & | CVC3::Expr::unnegate () const |
Remove leading NOT if any. More... | |
iterator | CVC3::Expr::begin () const |
Begin iterator. More... | |
iterator | CVC3::Expr::end () const |
End iterator. More... | |
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) More... | |
bool | CVC3::Expr::hasFind () const |
const Theorem & | CVC3::Expr::getFind () const |
int | CVC3::Expr::getFindLevel () const |
const Theorem & | CVC3::Expr::getEqNext () const |
NotifyList * | CVC3::Expr::getNotify () const |
Type | CVC3::Expr::getType () const |
Get the type. Recursively compute if necessary. More... | |
Type | CVC3::Expr::lookupType () const |
Look up the current type. Do not recursively compute (i.e. may be NULL) More... | |
Cardinality | CVC3::Expr::typeCard () const |
Return cardinality of type. More... | |
Expr | CVC3::Expr::typeEnumerateFinite (Unsigned n) const |
Return nth (starting with 0) element in a finite type. More... | |
Unsigned | CVC3::Expr::typeSizeFinite () const |
Return size of a finite type; returns 0 if size cannot be determined. More... | |
bool | CVC3::Expr::validSimpCache () const |
Return true if there is a valid cached value for calling simplify on this Expr. More... | |
const Theorem & | CVC3::Expr::getSimpCache () const |
bool | CVC3::Expr::isValidType () const |
bool | CVC3::Expr::validIsAtomicFlag () const |
bool | CVC3::Expr::validTerminalsConstFlag () const |
bool | CVC3::Expr::getIsAtomicFlag () const |
bool | CVC3::Expr::getTerminalsConstFlag () 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::usesCC () const |
bool | CVC3::Expr::notArrayNormalized () 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. More... | |
void | CVC3::Expr::setFlag () const |
Set the generic flag. More... | |
void | CVC3::Expr::clearFlags () const |
Clear the generic flag in all Exprs. More... | |
std::string | CVC3::Expr::toString () const |
Print the expression to a string. More... | |
std::string | CVC3::Expr::toString (InputLanguage lang) const |
Print the expression to a string using the given output language. More... | |
void | CVC3::Expr::print (InputLanguage lang, bool dagify=true) const |
Print the expression in the specified format. More... | |
void | CVC3::Expr::print () const |
Print the expression as AST (lisp-like format) More... | |
void | CVC3::Expr::printnodag () const |
Print the expression as AST without dagifying. More... | |
void | CVC3::Expr::pprint () const |
Pretty-print the expression. More... | |
void | CVC3::Expr::pprintnodag () const |
Pretty-print without dagifying. More... | |
ExprStream & | CVC3::Expr::print (ExprStream &os) const |
Print a leaf node. More... | |
ExprStream & | CVC3::Expr::printAST (ExprStream &os) const |
Print the top node and then recurse through the children */. More... | |
Expr & | CVC3::Expr::indent (int n, bool permanent=false) |
Set initial indentation to n. More... | |
void | CVC3::Expr::setFind (const Theorem &e) const |
Set the find attribute to e. More... | |
void | CVC3::Expr::setEqNext (const Theorem &e) const |
Set the eqNext attribute to e. More... | |
void | CVC3::Expr::addToNotify (Theory *i, const Expr &e) const |
Add (e,i) to the notify list of this expression. More... | |
void | CVC3::Expr::setType (const Type &t) const |
Set the cached type. More... | |
void | CVC3::Expr::setSimpCache (const Theorem &e) const |
void | CVC3::Expr::setValidType () const |
void | CVC3::Expr::setIsAtomicFlag (bool value) const |
void | CVC3::Expr::setTerminalsConstFlag (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::setUsesCC () const |
void | CVC3::Expr::setNotArrayNormalized () 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. More... | |
void | CVC3::Expr::setUserRegisteredAtom () const |
Set the UserRegisteredAtom flag for this Expr. More... | |
void | CVC3::Expr::setRegisteredAtom () const |
Set the RegisteredAtom flag for this Expr. More... | |
void | CVC3::Expr::setSelected () const |
Set the Selected flag for this Expr. More... | |
void | CVC3::Expr::setStoredPredicate () const |
Set the Stored Predicate flag for this Expr. More... | |
bool | CVC3::Expr::subExprOf (const Expr &e) const |
Check if the current Expr (*this) is a subexpression of e. More... | |
Unsigned | CVC3::Expr::getSize () const |
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. More... | |
ExprValue * | CVC3::Expr::d_expr |
The value. This is the only data member in this class. More... | |
Friends | |
CVC_DLL std::ostream & | CVC3::Expr::operator<< (std::ostream &os, const Expr &e) |
int | CVC3::Expr::compare (const Expr &e1, const Expr &e2) |
bool | CVC3::Expr::operator== (const Expr &e1, const Expr &e2) |
bool | CVC3::Expr::operator!= (const Expr &e1, const Expr &e2) |
bool | CVC3::Expr::operator< (const Expr &e1, const Expr &e2) |
bool | CVC3::Expr::operator<= (const Expr &e1, const Expr &e2) |
bool | CVC3::Expr::operator> (const Expr &e1, const Expr &e2) |
bool | CVC3::Expr::operator>= (const Expr &e1, const Expr &e2) |
|
private |
bit-masks for static flags
|
private |
bit-masks for dynamic flags
|
inlineprivate |
Private constructor, simply wraps around the pointer.
Definition at line 807 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::incRefcount().
|
private |
Definition at line 63 of file expr.cpp.
References CVC3::ExprHashMap< Data >::begin(), CVC3::ExprHashMap< Data >::clear(), CVC3::ExprHashMap< Data >::count(), CVC3::ExprHashMap< Data >::end(), CVC3::Expr::getIndex(), IF_DEBUG, CVC3::ExprHashMap< Data >::insert(), CVC3::Expr::isNull(), CVC3::Expr::mkOp(), and CVC3::Expr::recursiveSubst().
Referenced by CVC3::Expr::recursiveSubst().
|
private |
Definition at line 260 of file expr.cpp.
References BOUND_VAR, CVC3::ExprHashMap< Data >::end(), CVC3::ExprHashMap< Data >::find(), and CVC3::Expr::recursiveQuantSubst().
Referenced by CVC3::Expr::recursiveQuantSubst().
|
private |
|
inline |
Default constructor creates the Null Expr.
Definition at line 287 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(), CVC3::Expr::typeEnumerateFinite(), and CVC3::Expr::xorExpr().
|
inline |
Copy constructor and assignment (copy the pointer and take care of the refcount)
Definition at line 809 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::incRefcount().
|
inline |
Assignment operator: take care of the refcounting and GC.
Definition at line 813 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::decRefcount(), and CVC3::ExprValue::incRefcount().
Definition at line 830 of file expr.h.
References APPLY, CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::ExprNode::getKids1(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), and CVC3::ExprManager::newExprValue().
Definition at line 846 of file expr.h.
References APPLY, CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::ExprNode::getKids1(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), and CVC3::ExprManager::newExprValue().
|
inline |
Definition at line 864 of file expr.h.
References APPLY, CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::ExprNode::getKids1(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), and CVC3::ExprManager::newExprValue().
|
inline |
Definition at line 885 of file expr.h.
References APPLY, CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::ExprNode::getKids1(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), and CVC3::ExprManager::newExprValue().
|
inline |
Definition at line 908 of file expr.h.
References APPLY, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getEM(), CVC3::Op::getExpr(), CVC3::Op::getKind(), CVC3::ExprValue::incRefcount(), and CVC3::ExprManager::newExprValue().
|
inline |
Destructor.
Definition at line 985 of file expr.h.
References CVC3::ExprValue::d_em, CVC3::Expr::d_expr, CVC3::ExprValue::d_refcount, FatalAssert, CVC3::ExprManager::gc(), and IF_DEBUG.
|
inline |
Definition at line 929 of file expr.h.
References EQ, and CVC3::Expr::Expr().
Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryArray::computeModel(), CVC3::TheoryBitvector::computeTCC(), CVC3::ExprTransform::ConstrainedConstraints(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::ArithTheoremProducer3::divideEqnNonConst(), CVC3::ArithTheoremProducerOld::divideEqnNonConst(), CVC3::ArithTheoremProducer::divideEqnNonConst(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducerOld::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducerOld::elimPowerConst(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::VCL::eqExpr(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::TheoryArithOld::findRationalBound(), CVC3::Theorem::getExpr(), CVC3::RWTheoremValue::getExpr(), CVC3::ExprTransform::GetPEqs(), CVC3::ArithTheoremProducerOld::implyEqualities(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::ExprTransform::ITE_generator(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer3::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multEqZero(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::BitvectorTheoremProducer::notBVEQ1Rule(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::TheoryCore::parseExprOp(), CVC3::ArithTheoremProducer3::powEqZero(), CVC3::ArithTheoremProducerOld::powEqZero(), CVC3::ArithTheoremProducer::powEqZero(), CVC3::ExprTransform::PredConstrainer(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::ArrayTheoremProducer::propagateIndexDiseq(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::ExprTransform::simplifyWithCare(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::ArrayTheoremProducer::splitOnConstants(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::CommonTheoremProducer::varIntroRule(), and CVC3::BitvectorTheoremProducer::zeroBVOR().
|
inline |
Definition at line 933 of file expr.h.
References CVC3::Expr::Expr(), and NOT.
Referenced by CVC3::ExprTransform::ConstrainedConstraints(), CVC3::ExprTransform::dobryant(), CVC3::ExprTransform::GetPEqs(), CVC3::ArithTheoremProducerOld::implyNegatedInequalityDiffLogic(), CVC3::Expr::negate(), CVC3::ExprTransform::PredConstrainer(), CVC3::TheoryCore::print(), CVC3::ArrayTheoremProducer::propagateIndexDiseq(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::CompleteInstPreProcessor::recRewriteNot(), and CVC3::ArrayTheoremProducer::splitOnConstants().
|
inline |
Definition at line 937 of file expr.h.
References CVC3::Expr::isNot(), and CVC3::Expr::notExpr().
Referenced by CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::VCL::checkUnsat(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::Circuit::Circuit(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::Translator::finish(), CVC3::VariableValue::getNegExpr(), CVC3::CommonTheoremProducer::iffContrapositive(), CVC3::SearchEngineTheoremProducer::iffToClauses(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::ExprTransform::newPPrec(), CVC3::TheoryCore::print(), CVC3::DecisionEngine::pushDecision(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), and CVC3::CommonTheoremProducer::rewriteOr().
|
inline |
Definition at line 941 of file expr.h.
References AND, and CVC3::Expr::Expr().
Referenced by CVC3::TheoryDatatype::assertFact(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), recCompleteInster::build_tree(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::BitvectorTheoremProducer::computeCarry(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryDatatype::computeTCC(), CVC3::TheoryArithNew::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryArith3::computeTCC(), CVC3::TheoryArithOld::computeTCC(), CVC3::ExprTransform::ConstrainedConstraints(), CVC3::VCL::createOp(), CVC3::ExprTransform::ITE_generator(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::signBVLTRule(), and CVC3::QuantTheoremProducer::universalInst().
|
inline |
Definition at line 951 of file expr.h.
References CVC3::Expr::Expr(), and OR.
Referenced by CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducerOld::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducerOld::elimPowerConst(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::CommonTheoremProducer::excludedMiddle(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::CoreTheoremProducer::rewriteIteBool(), and CVC3::BitvectorTheoremProducer::signBVLTRule().
Definition at line 961 of file expr.h.
References CVC3::Expr::Expr(), and ITE.
Referenced by CVC3::CoreTheoremProducer::AndToIte(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::CNF_TheoremProducer::CNFITEtranslate(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::ExprTransform::ITE_generator(), CVC3::VCL::iteExpr(), CVC3::CommonTheoremProducer::liftOneITE(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::TheoryCore::parseExprOp(), CVC3::Translator::preprocessRec(), CVC3::TheoryCore::processCond(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), and CVC3::ArrayTheoremProducer::rewriteReadWrite2().
|
inline |
Definition at line 965 of file expr.h.
References CVC3::Expr::Expr(), and IFF.
Referenced by CVC3::TheoryCore::assignValue(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ExprTransform::dobryant(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::Theorem::getExpr(), CVC3::RWTheoremValue::getExpr(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::VCL::iffExpr(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::TheoryCore::parseExprOp(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::ExprTransform::simplifyWithCare(), CVC3::VCCmd::skolemizeAx(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::TheoryQuant::theoryPreprocess(), SAT::CNF_Manager::translateExprRec(), CVC3::CommonTheoremProducer::varIntroRule(), and LFSCObj::what_is_proven().
|
inline |
Definition at line 969 of file expr.h.
References CVC3::Expr::Expr(), and IMPLIES.
Referenced by CVC3::TheoryDatatype::assertFact(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ExprTransform::dobryant(), CVC3::VCL::impliesExpr(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::VCL::query(), CVC3::ArrayTheoremProducer::rewriteSameStore(), SAT::CNF_Manager::translateExprRec(), CVC3::QuantTheoremProducer::universalInst(), and LFSCObj::what_is_proven().
|
inline |
Definition at line 973 of file expr.h.
References CVC3::Expr::Expr(), and XOR.
Referenced by SAT::CNF_Manager::translateExprRec().
|
inline |
Create a Skolem constant for the i'th variable of an existential (*this)
Definition at line 977 of file expr.h.
References CVC3::Expr::getEM(), and CVC3::ExprManager::newSkolemExpr().
Referenced by CVC3::CommonTheoremProducer::skolemize(), CVC3::VCCmd::skolemizeAx(), and CVC3::CommonTheoremProducer::skolemizeRewriteVar().
|
inline |
Create a Boolean variable out of the expression.
Rebuild Expr with a new ExprManager
Definition at line 981 of file expr.h.
References CVC3::ExprManager::rebuild().
Referenced by CVC3::VCL::importExpr().
Expr CVC3::Expr::substExpr | ( | const std::vector< Expr > & | oldTerms, |
const std::vector< Expr > & | newTerms | ||
) | const |
Definition at line 178 of file expr.cpp.
References DebugAssert, and CVC3::ExprHashMap< Data >::insert().
Referenced by CVC3::ExprTransform::dobryant(), CVC3::CompleteInstPreProcessor::inst(), recCompleteInster::inst_helper(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::CommonTheoremProducer::skolemize(), CVC3::VCCmd::skolemizeAx(), CVC3::CompleteInstPreProcessor::substMacro(), and CVC3::QuantTheoremProducer::universalInst().
Expr CVC3::Expr::substExpr | ( | const ExprHashMap< Expr > & | oldToNew) | const |
Definition at line 199 of file expr.cpp.
References CVC3::ExprHashMap< Data >::begin(), CVC3::ExprHashMap< Data >::end(), and CVC3::ExprHashMap< Data >::size().
Expr CVC3::Expr::substExprQuant | ( | const std::vector< Expr > & | oldTerms, |
const std::vector< Expr > & | newTerms | ||
) | const |
Definition at line 217 of file expr.cpp.
References DebugAssert, and CVC3::ExprHashMap< Data >::insert().
Expr CVC3::Expr::substExprQuant | ( | const ExprHashMap< Expr > & | oldToNew) | const |
|
inline |
Definition at line 338 of file expr.h.
References CVC3::andExpr().
|
inline |
Definition at line 339 of file expr.h.
References CVC3::orExpr().
|
inlinestatic |
Definition at line 992 of file expr.h.
References CVC3::Expr::getEM(), and CVC3::ExprManager::hash().
Referenced by CVC3::ExprApplyTmp::computeHash(), CVC3::ExprSkolem::computeHash(), Hash::hash< CVC3::Expr >::operator()(), and CVC3::VariableManager::HashLV::operator()().
|
inline |
Definition at line 998 of file expr.h.
References CVC3::Expr::getEM(), and CVC3::ExprManager::hash().
|
inline |
Definition at line 355 of file expr.h.
References FALSE_EXPR.
Referenced by SAT::CNF_Manager::addAssumption(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::SearchSat::check(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArray::checkSat(), CVC3::SearchSimple::checkValidRec(), SAT::CNF_Manager::concreteExpr(), CVC3::SearchEngineTheoremProducer::conflictClause(), LFSCConvert::cvc3_to_lfsc(), CVC3::TheoryArithOld::doSolve(), CVC3::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVC3::TheoryQuant::enqueueInst(), CVC3::DecisionEngine::findSplitterRec(), CVC3::BitvectorTheoremProducer::generalIneqn(), SAT::CNF_Manager::getCNFLit(), CVC3::CNF_TheoremProducer::getSmartClauses(), LFSCObj::getY(), CVC3::CommonTheoremProducer::iffFalseElim(), LFSCObj::isFormula(), CVC3::CNF_TheoremProducer::learnedClauses(), LFSCPrinter::LFSCPrinter(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchSat::newUserAssumptionInt(), TReturn::normalize_tr(), CVC3::TheoryQuant::notifyInconsistent(), LFSCPrinter::print_formula_h(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processIntEq(), CVC3::SearchImplBase::processResult(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::SearchEngineTheoremProducer::proofByContradiction(), CVC3::TheoryCore::registerAtom(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CommonTheoremProducer::rewriteNotFalse(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplifyOp(), SAT::CNF_Manager::translateExprRec(), CVC3::VCL::tryModelGeneration(), and CVC3::TheoryCore::update().
|
inline |
Definition at line 356 of file expr.h.
References TRUE_EXPR.
Referenced by SAT::CNF_Manager::addAssumption(), CVC3::TheoryCore::assertFactCore(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::SearchSat::check(), CVC3::TheoryArray::checkSat(), CVC3::SearchEngineFast::checkValidMain(), CVC3::SearchSimple::checkValidRec(), CVC3::TheoryBitvector::computeModel(), SAT::CNF_Manager::concreteExpr(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryQuant::enqueueInst(), CVC3::SearchEngineFast::findSplitter(), CVC3::DecisionEngine::findSplitterRec(), CVC3::BitvectorTheoremProducer::generalIneqn(), SAT::CNF_Manager::getCNFLit(), LFSCObj::getY(), CVC3::CommonTheoremProducer::iffTrueElim(), LFSCObj::isFormula(), CVC3::SearchSat::newUserAssumptionInt(), TReturn::normalize_tr(), LFSCPrinter::print_formula_h(), CVC3::TheoryArith3::processBuffer(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryCore::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::CommonTheoremProducer::rewriteNotTrue(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplifyOp(), CVC3::SearchEngineFast::split(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryUF::update(), and CVC3::TheoryCore::update().
|
inline |
Definition at line 357 of file expr.h.
Referenced by CVC3::Theory::addSplitter(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::BitvectorTheoremProducer::bitExtractAllToConstEq(), CVC3::TheoryArray::checkSat(), CVC3::TheoryCore::checkSolved(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryBitvector::computeModel(), CVC3::SearchEngineFast::findSplitter(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryCore::solve(), and CVC3::SearchEngineFast::split().
|
inline |
Definition at line 1005 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::isVar().
Referenced by CVC3::ExprTransform::BuildBryantMaps(), LFSCObj::can_pnorm(), CVC3::TheoryBitvector::check_linear(), CVC3::TheoryBitvector::computeTCC(), CVC3::TypeComputerCore::computeType(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::Theory::getTCC(), CVC3::Theory::isLeaf(), CVC3::TheoremProducer::newPf(), CVC3::Translator::preprocessRec(), LFSCPrinter::print_poly_norm(), LFSCPrinter::print_terms_h(), recursiveGetSubTrig(), CVC3::TheoryArray::rewrite(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::TheoryCore::simplify(), and CVC3::Theory::theoryOf().
|
inline |
Definition at line 359 of file expr.h.
References BOUND_VAR.
Referenced by CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::CompleteInstPreProcessor::hasShieldVar(), CVC3::CompleteInstPreProcessor::isGoodQuant(), and CVC3::CompleteInstPreProcessor::isShield().
|
inline |
Definition at line 1006 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::isString().
Referenced by CVC3::TheoryDatatype::checkType(), CVC3::Expr::getString(), CVC3::PrettyPrinterCore::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), and CVC3::TheoryUF::printSmtLibShared().
|
inline |
Definition at line 1007 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::isClosure().
Referenced by CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::TheoryArray::computeType(), containsRec(), CVC3::VCCmd::findAxioms(), findPolarity(), findPolarityAtomic(), CVC3::Expr::getBody(), CVC3::Expr::getTriggers(), CVC3::Expr::getVars(), CVC3::isArrayLiteral(), CVC3::Expr::isLambda(), CVC3::Expr::isQuantifier(), CVC3::isTrivialExpr(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::ArrayTheoremProducer::readArrayLiteral(), recGetSubTerms(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), recursiveExprScore(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::Expr::setMultiTrigger(), CVC3::Expr::setTrigger(), CVC3::Expr::setTriggers(), and CVC3::CompleteInstPreProcessor::simplifyEq().
|
inline |
Definition at line 1008 of file expr.h.
References EXISTS, FORALL, CVC3::Expr::getKind(), and CVC3::Expr::isClosure().
Referenced by CVC3::TheoryQuant::computeTCC(), hasBoundVarRec(), and CVC3::TheoryQuant::print().
|
inline |
Definition at line 1011 of file expr.h.
References CVC3::Expr::getKind(), CVC3::Expr::isClosure(), and LAMBDA.
Referenced by CVC3::TheoryUF::checkSat(), CVC3::Theory::newSubtypeExpr(), and CVC3::TheoryUF::print().
|
inline |
Definition at line 1014 of file expr.h.
References 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::ExprTransform::BuildBryantMaps(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryDatatype::computeTCC(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryQuant::debug(), 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(), isUniterpFunc(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::TheoryCore::parseExpr(), CVC3::ExprTransform::PredConstrainer(), CVC3::Translator::preprocess2Rec(), CVC3::PrettyPrinterCore::print(), CVC3::TheoryUF::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryBitvector::printSmtLibShared(), recursiveGetSubTrig(), CVC3::UFTheoremProducer::relToClosure(), CVC3::ExprTransform::RemoveFunctionApps(), CVC3::TheoryUF::rewrite(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::Theory::theoryOf(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), and CVC3::TheoryDatatype::update().
|
inline |
Definition at line 1018 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::isSymbol().
Referenced by CVC3::TheoryUF::computeType(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), and CVC3::TheoryUF::printSmtLibShared().
|
inline |
Definition at line 1019 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::isTheorem().
Referenced by CVC3::Expr::getTheorem().
|
inline |
|
inline |
|
inline |
Expr represents a type.
Definition at line 1020 of file expr.h.
References CVC3::Expr::getEM(), CVC3::Expr::getOpKind(), and CVC3::ExprManager::isTypeKind().
Referenced by CVC3::TypeComputerCore::checkType(), CVC3::TypeComputerCore::finiteTypeInfo(), and CVC3::Theory::lookupTypeExpr().
|
inline |
Provide access to ExprValue for client subclasses of ExprValue only
Definition at line 1000 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::getExprValue().
Referenced by CVC3::TheoryBitvector::getBVConstSize(), and CVC3::TheoryBitvector::getBVConstValue().
|
inline |
Test if e is a term (as opposed to a predicate/formula)
Definition at line 1021 of file expr.h.
References CVC3::Expr::getType(), and CVC3::Type::isBool().
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::ExprTransform::BuildBryantMaps(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::Theorem::getAssumptionsAndCongRec(), CVC3::Theorem::getExpr(), CVC3::ExprTransform::GetSub_vec(), CVC3::TheoryArith3::isStale(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryArith::leavesAreNumConst(), CVC3::ExprTransform::PredConstrainer(), CVC3::ExprTransform::pushNegation(), CVC3::ExprTransform::pushNegationRec(), recursiveGetSubTrig(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryUF::setup(), CVC3::TheoryRecords::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryBitvector::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryDatatype::solve(), CVC3::TheoryArithNew::solve(), CVC3::TheoryBitvector::solve(), CVC3::TheoryArith3::solve(), CVC3::TheoryArithOld::solve(), CVC3::TheoryCore::solve(), and CVC3::VCL::value().
bool CVC3::Expr::isAtomic | ( | ) | const |
Test if e is atomic.
An atomic expression is TRUE or FALSE or one that does not contain a formula (including not being a formula itself).
Definition at line 550 of file expr.cpp.
Referenced by CVC3::TheoryArray::checkSat(), CVC3::DecisionEngine::findSplitterRec(), CVC3::Theorem::getAssumptionsAndCongRec(), CVC3::ArithTheoremProducerOld::getLeaves(), CVC3::TheoryArith::leavesAreNumConst(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArray::setup(), CVC3::TheoryCore::setupSubFormulas(), CVC3::ExprTransform::simplifyWithCare(), CVC3::ExprTransform::specialSimplify(), CVC3::ExprTransform::substitute(), CVC3::TheoryArray::update(), CVC3::TheoryBitvector::update(), and CVC3::TheoryArithOld::update().
bool CVC3::Expr::isAtomicFormula | ( | ) | const |
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 571 of file expr.cpp.
References AND, EXISTS, FORALL, IFF, IMPLIES, ITE, NOT, OR, and XOR.
Referenced by CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::CompleteInstPreProcessor::collectIndex(), findPolarity(), findPolarityAtomic(), CVC3::Theorem::getAssumptionsAndCongRec(), CVC3::TheoryQuant::multMatchChild(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::CompleteInstPreProcessor::simplifyEq(), and CVC3::ExprTransform::simplifyWithCare().
|
inline |
An abstract atomic formua is an atomic formula or a quantified formula.
Definition at line 398 of file expr.h.
Referenced by CVC3::TheoryArray::checkSat(), CVC3::CompleteInstPreProcessor::collectHeads(), findAtom(), CVC3::DecisionEngine::findSplitterRec(), CVC3::TheoryCore::processUpdates(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArithNew::registerAtom(), CVC3::TheoryCore::setupSubFormulas(), CVC3::CompleteInstPreProcessor::simplifyEq(), and SAT::CNF_Manager::translateExprRec().
|
inline |
|
inline |
Test if e is an abstract literal.
Definition at line 406 of file expr.h.
Referenced by CVC3::SearchImplBase::addSplitter(), CVC3::SearchEngineFast::addSplitter(), CVC3::Theory::addSplitter(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::SearchEngineFast::bcp(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::Theorem::GetSatAssumptionsRec(), CVC3::Theorem::isAbsLiteral(), CVC3::SearchImplBase::isClause(), CVC3::SearchEngineFast::newIntAssumption(), CVC3::SearchEngineFast::propagate(), CVC3::DecisionEngine::pushDecision(), CVC3::SearchImplBase::replaceITE(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewriteLiteral(), CVC3::TheoryCore::setupTerm(), and CVC3::SearchEngineFast::updateLitCounts().
|
inline |
|
inline |
True iff expr is not a Bool connective.
Definition at line 411 of file expr.h.
Referenced by CVC3::TheoryArith::leavesAreNumConst(), CVC3::ExprTransform::newPPrec(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithOld::rewrite(), CVC3::ArithTheoremProducerOld::rewriteLeavesConst(), and CVC3::ExprTransform::simplifyWithCare().
|
inline |
PropAtom or negation of PropAtom.
Definition at line 413 of file expr.h.
Referenced by CVC3::SearchImplBase::applyCNFRules(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::isPropClause(), and CVC3::SearchImplBase::replaceITE().
bool CVC3::Expr::containsTermITE | ( | ) | const |
Return whether Expr contains a non-bool type ITE as a sub-term.
Definition at line 525 of file expr.cpp.
Referenced by CVC3::CommonTheoremProducer::findITE(), CVC3::CommonTheoremProducer::liftOneITE(), CVC3::ExprTransform::newPPrec(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithOld::rewrite(), and CVC3::ExprTransform::simplifyWithCare().
|
inline |
Definition at line 419 of file expr.h.
References EQ.
Referenced by CVC3::SearchSat::addSplitter(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::SearchSat::check(), CVC3::TheoryCore::checkEquation(), CVC3::TheoryQuant::checkSat(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::compare(), CVC3::BitvectorTheoremProducer::constEq(), LFSCObj::define_skolem_vars(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducerOld::elimPowerConst(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducerOld::evenPowerEqNegConst(), CVC3::ArithTheoremProducer3::evenPowerEqNegConst(), CVC3::ArithTheoremProducer::evenPowerEqNegConst(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::ExprTransform::GetFormulaMap(), CVC3::ExprTransform::GetPEqs(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::TheoryArithOld::isNonlinearEq(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), isSysPred(), CVC3::BitvectorTheoremProducer::MarkNonSolvableEq(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::TheoryBitvector::multiply_coeff(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::ArithTheoremProducerOld::powEqZero(), CVC3::ArithTheoremProducer3::powEqZero(), CVC3::ArithTheoremProducer::powEqZero(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewriteCore(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryArray::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArith3::setup(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::TheoryArray::solve(), CVC3::TheoryCore::solve(), CVC3::Theorem::Theorem(), CVC3::Theory::theoryOf(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithOld::update(), CVC3::TheoryCore::update(), usefulInMatch(), and CVC3::BitvectorTheoremProducer::zeroBVOR().
|
inline |
Definition at line 420 of file expr.h.
References NOT.
Referenced by SAT::CNF_Manager::addAssumption(), CVC3::SearchImplBase::addToCNFCache(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitExtractToExtract(), CVC3::SearchSat::check(), CVC3::Circuit::Circuit(), SAT::CNF_Manager::concreteExpr(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), findPolarity(), findPolarityAtomic(), flatAnds(), SAT::CNF_Manager::getCNFLit(), CVC3::ExprTransform::GetFormulaMap(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::Theorem::GetSatAssumptionsRec(), LFSCObj::isFormula(), CVC3::SearchImplBase::isGoodSplitter(), LFSCBoolRes::Make(), LFSCLraPoly::Make(), LFSCProof::Make_not_not_elim(), CVC3::Expr::negate(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::SearchEngineTheoremProducer::negIntro(), CVC3::SearchImplBase::newIntAssumption(), CVC3::CommonTheoremProducer::notNotElim(), CVC3::CommonTheoremProducer::notToIff(), CVC3::CoreTheoremProducer::NotToIte(), CVC3::SearchEngineTheoremProducer::opCNFRule(), LFSCPrinter::print_formula_h(), CVC3::SearchImplBase::processResult(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::ExprTransform::pushNegation1(), LFSCObj::queryAtomic(), LFSCObj::queryElimNotNot(), LFSCObj::queryM(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::Theorem::refutes(), CVC3::TheoryQuant::rewrite(), 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::TheoryArithNew::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::setup(), CVC3::SearchEngineFast::split(), CVC3::Theory::theoryOf(), SAT::CNF_Manager::translateExprRec(), CVC3::SearchEngineTheoremProducer::unitProp(), and CVC3::TheoryCore::update().
|
inline |
Definition at line 421 of file expr.h.
References AND.
Referenced by CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andElim(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::SearchImplBase::applyCNFRules(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryCore::assertFactCore(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryCore::checkSolved(), CVC3::SearchImplBase::enqueueCNFrec(), findPolarity(), findPolarityAtomic(), flatAnds(), LFSCObj::isFormula(), CVC3::TheoryArith3::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::SearchSat::newUserAssumptionIntHelper(), CVC3::CoreTheoremProducer::orDistributivityRule(), LFSCPrinter::print_formula_h(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::CoreTheoremProducer::rewriteNotAnd(), and CVC3::TheoryCore::solve().
|
inline |
Definition at line 422 of file expr.h.
References OR.
Referenced by SAT::CNF_Manager::addAssumption(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::ClauseValue::ClauseValue(), CVC3::CNF_TheoremProducer::CNFConvert(), SAT::CNF_Manager::convertLemma(), findPolarity(), findPolarityAtomic(), CVC3::SearchEngineFast::fixConflict(), flatAnds(), CVC3::SearchImplBase::isClause(), LFSCObj::isFormula(), CVC3::SearchImplBase::isPropClause(), LFSCBoolRes::MakeC(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::CoreTheoremProducer::OrToIte(), LFSCPrinter::print_formula_h(), CVC3::TheoryCore::rewrite(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CommonTheoremProducer::rewriteOr(), and CVC3::CoreTheoremProducer::rewriteOrSubterms().
|
inline |
Definition at line 423 of file expr.h.
References ITE.
Referenced by CVC3::CommonTheoremProducer::findITE(), findPolarity(), findPolarityAtomic(), CVC3::DecisionEngine::findSplitterRec(), CVC3::ArithTheoremProducerOld::getLeaves(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::TheoryArith::leavesAreNumConst(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CommonTheoremProducer::rewriteIteTrue(), and CVC3::CoreTheoremProducer::rewriteNotIte().
|
inline |
Definition at line 424 of file expr.h.
References IFF.
Referenced by CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitvectorFalseRule(), CVC3::BitvectorTheoremProducer::bitvectorTrueRule(), CVC3::compare(), findPolarity(), findPolarityAtomic(), CVC3::TheoryCore::getQuantLevelForTerm(), LFSCObj::getY(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::CoreTheoremProducer::IffToIte(), LFSCObj::isFormula(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), TReturn::normalize_tr(), CVC3::SearchEngineTheoremProducer::opCNFRule(), LFSCPrinter::print_formula_h(), CVC3::CommonTheoremProducer::rewriteIff(), CVC3::CoreTheoremProducer::rewriteNotIff(), CVC3::CommonTheoremProducer::rewriteReflexivity(), CVC3::CommonTheoremProducer::rewriteUsingSymmetry(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), and CVC3::Theorem::Theorem().
|
inline |
Definition at line 425 of file expr.h.
References IMPLIES.
Referenced by findPolarity(), findPolarityAtomic(), LFSCObj::getY(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implMP(), CVC3::CoreTheoremProducer::ImpToIte(), LFSCObj::isFormula(), TReturn::normalize_tr(), LFSCPrinter::print_formula_h(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), and CVC3::CoreTheoremProducer::rewriteImplies().
|
inline |
Definition at line 426 of file expr.h.
References XOR.
Referenced by findPolarity(), findPolarityAtomic(), and CVC3::CommonTheoremProducer::xorToIff().
|
inline |
Definition at line 428 of file expr.h.
References FORALL.
Referenced by CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::TheoryQuant::assertFact(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchSat::check(), CVC3::CompleteInstPreProcessor::collectIndex(), hasMoreBVs(), CVC3::CompleteInstPreProcessor::inst(), CVC3::CompleteInstPreProcessor::isGood(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::TheoryQuant::rewrite(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::CompleteInstPreProcessor::simplifyQuant(), and CVC3::QuantTheoremProducer::universalInst().
|
inline |
Definition at line 429 of file expr.h.
References EXISTS.
Referenced by CVC3::TheoryQuant::assertFact(), CVC3::SearchEngineFast::bcp(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::SearchSat::check(), CVC3::CompleteInstPreProcessor::collectIndex(), CVC3::CompleteInstPreProcessor::inst(), CVC3::CompleteInstPreProcessor::isGood(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::TheoryQuant::rewrite(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::CommonTheoremProducer::skolemize(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), and CVC3::CommonTheoremProducer::varIntroSkolem().
|
inline |
Definition at line 431 of file expr.h.
References RATIONAL_EXPR.
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArith3::assignVariables(), CVC3::TheoryArithOld::assignVariables(), LFSCObj::can_pnorm(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithOld::checkSat(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::ArithTheoremProducer3::evenPowerEqNegConst(), CVC3::ArithTheoremProducer::evenPowerEqNegConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::getLeaves(), CVC3::TheoryArithOld::getLowerBound(), getRat(), CVC3::Expr::getRational(), CVC3::TheoryArithOld::getUpperBound(), CVC3::TheoryArithOld::DifferenceLogicGraph::getValuation(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer3::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), CVC3::isIntegerConst(), isIntx(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::isRational(), CVC3::TheoryArith::isSyntacticRational(), CVC3::TheoryArithOld::isUnconstrained(), CVC3::TheoryArith::leavesAreNumConst(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer3::multEqn(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducerOld::multEqZero(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::ArithTheoremProducer3::multIneqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::ArithTheoremProducer3::oneElimination(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryArith3::pickMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::ArithTheoremProducer3::powEqZero(), CVC3::ArithTheoremProducerOld::powEqZero(), CVC3::ArithTheoremProducer::powEqZero(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), LFSCPrinter::print_poly_norm(), LFSCPrinter::print_terms_h(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArithOld::separateMonomial(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer3::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), CVC3::ArithTheoremProducer3::sumMulF(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithOld::updateConstrained(), CVC3::TheoryArithOld::updateStats(), and usefulInMatch().
|
inline |
Definition at line 432 of file expr.h.
References SKOLEM_VAR.
Referenced by CVC3::VCCmd::findAxioms(), CVC3::Expr::getBoundIndex(), CVC3::Expr::getExistential(), and CVC3::Theory::renameExpr().
|
inline |
Definition at line 1050 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::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::Translator::printArrayExpr(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryCore::printSmtLibShared(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), and CVC3::VCL::transClosure().
|
inline |
For BOUND_VAR, get the UID.
Definition at line 1149 of file expr.h.
References CVC3::AST_LANG, BOUND_VAR, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::getKind(), CVC3::ExprValue::getUid(), and CVC3::Expr::toString().
|
inline |
Definition at line 1055 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::TheoryArithOld::extractTermsFromInequality(), CVC3::Translator::finish(), CVC3::TheoryRecords::getField(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryCore::print(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryCore::processCond(), and CVC3::ArithTheoremProducerOld::rafineStrictInteger().
|
inline |
Get bound variables from a closure Expr.
Definition at line 1062 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::UFTheoremProducer::applyLambda(), CVC3::TheoryQuant::assertFact(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryQuant::enqueueInst(), hasMoreBVs(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::Theory::newSubtypeExpr(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryQuant::print(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::TheoryQuant::recInstantiate(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::TheoryQuant::setupTriggers(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::CommonTheoremProducer::skolemize(), CVC3::VCCmd::skolemizeAx(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::CompleteInstPreProcessor::substMacro(), CVC3::QuantTheoremProducer::universalInst(), and CVC3::CommonTheoremProducer::varIntroSkolem().
|
inline |
Get the existential axiom expression for skolem constant.
Definition at line 1123 of file expr.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getExistential(), and CVC3::Expr::isSkolem().
Referenced by CVC3::VCCmd::findAxioms().
|
inline |
Get the index of the bound var that skolem constant comes from.
Definition at line 1128 of file expr.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getBoundIndex(), and CVC3::Expr::isSkolem().
|
inline |
Get the body of the closure Expr.
Definition at line 1069 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::CompleteInstPreProcessor::collectHeads(), CVC3::ExprSkolem::computeHash(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryUF::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryQuant::computeType(), containsRec(), CVC3::VCCmd::findAxioms(), findPolarity(), CVC3::CompleteInstPreProcessor::inst(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::Theory::newSubtypeExpr(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::QuantTheoremProducer::packVar(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryArray::print(), CVC3::TheoryQuant::print(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::QuantTheoremProducer::recFindBoundVars(), recGetSubTerms(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recSkolemize(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::TheoryQuant::recursiveMap(), CVC3::CommonTheoremProducer::rewriteNotExists(), CVC3::CommonTheoremProducer::rewriteNotForall(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::CommonTheoremProducer::skolemize(), CVC3::VCCmd::skolemizeAx(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), and CVC3::QuantTheoremProducer::universalInst().
|
inline |
Set the triggers for a closure Expr.
Definition at line 1076 of file expr.h.
References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isClosure(), CVC3::ExprValue::setTriggers(), and CVC3::Expr::toString().
Referenced by CVC3::ExprManager::newClosureExpr(), CVC3::Expr::setMultiTrigger(), CVC3::Expr::setTrigger(), and CVC3::VCL::setTriggers().
|
inline |
Definition at line 1083 of file expr.h.
References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isClosure(), CVC3::ExprValue::setTriggers(), and CVC3::Expr::toString().
|
inline |
Definition at line 1096 of file expr.h.
References CVC3::AST_LANG, DebugAssert, CVC3::Expr::isClosure(), CVC3::Expr::setTriggers(), and CVC3::Expr::toString().
Referenced by CVC3::ExprManager::newClosureExpr(), and CVC3::VCL::setTrigger().
|
inline |
Definition at line 1107 of file expr.h.
References CVC3::AST_LANG, DebugAssert, CVC3::Expr::isClosure(), CVC3::Expr::setTriggers(), and CVC3::Expr::toString().
Referenced by CVC3::VCL::setMultiTrigger().
|
inline |
Get the manual triggers of the closure Expr.
Definition at line 1116 of file expr.h.
References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getTriggers(), CVC3::Expr::isClosure(), and CVC3::Expr::toString().
Referenced by CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::TheoryQuant::print(), and CVC3::TheoryQuant::setupTriggers().
|
inline |
Get the Rational value out of RATIONAL_EXPR.
Definition at line 1135 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::addToBuffer(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducer3::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducer3::canonDivideVar(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonInvertConst(), CVC3::ArithTheoremProducer3::canonInvertConst(), CVC3::ArithTheoremProducer::canonInvertConst(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer3::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer3::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultPowLeaf(), CVC3::ArithTheoremProducer3::canonMultPowLeaf(), CVC3::ArithTheoremProducer::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowPow(), CVC3::ArithTheoremProducer3::canonMultPowPow(), CVC3::ArithTheoremProducer::canonMultPowPow(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithNew::checkSatSimplex(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryArith3::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducer3::constPredicate(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::ArithTheoremProducerOld::elimPower(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducerOld::elimPowerConst(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::evenPowerEqNegConst(), CVC3::ArithTheoremProducer::evenPowerEqNegConst(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::TheoryArithNew::findCoefficient(), CVC3::TheoryArithNew::findRationalBound(), CVC3::TheoryArith3::findRationalBound(), CVC3::TheoryArithOld::findRationalBound(), CVC3::TheoryArithNew::finiteTypeInfo(), CVC3::TheoryArith3::finiteTypeInfo(), CVC3::TheoryArithOld::finiteTypeInfo(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryArith3::getFactors(), CVC3::TheoryArithOld::getFactors(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::TheoryRecords::getIndex(), CVC3::ArithTheoremProducerOld::getLeaves(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithNew::getLowerBoundExplanation(), getRat(), CVC3::TheoryBitvector::getSXIndex(), CVC3::TheoryArithOld::getUpperBound(), CVC3::TheoryArithNew::getUpperBoundExplanation(), CVC3::TheoryArithOld::DifferenceLogicGraph::getValuation(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducer3::greaterthan(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::isIntegerConst(), isIntx(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::TheoryArith::isSyntacticRational(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducerOld::multEqn(), CVC3::ArithTheoremProducer3::multEqn(), CVC3::ArithTheoremProducer::multEqn(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducerOld::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::ArithTheoremProducer3::multIneqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::ArithTheoremProducer3::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::ArithTheoremProducerOld::powEqZero(), CVC3::ArithTheoremProducer3::powEqZero(), CVC3::ArithTheoremProducer::powEqZero(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithNew::print(), CVC3::TheoryArith3::print(), CVC3::TheoryArithOld::print(), LFSCPrinter::print_poly_norm(), LFSCPrinter::print_terms_h(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArithNew::registerAtom(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArith::rewriteToDiff(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer3::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer3::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), CVC3::TheoryArithOld::termDegree(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithOld::updateConstrained(), CVC3::TheoryArithNew::updateStats(), CVC3::TheoryArith3::updateStats(), CVC3::TheoryArithOld::updateStats(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArithNew::updateValue(), and LFSCObj::what_is_proven().
|
inline |
Get theorem from THEOREM_EXPR.
Definition at line 1142 of file expr.h.
References CVC3::AST_LANG, CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getTheorem(), CVC3::Expr::isTheorem(), and CVC3::Expr::toString().
|
inline |
Definition at line 1156 of file expr.h.
References CVC3::ExprValue::d_em, CVC3::Expr::d_expr, and DebugAssert.
Referenced by CVC3::ExprStream::addLetHeader(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::arrayLiteral(), CVC3::Expr::begin(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::Expr::clearFlags(), CVC3::TheoryArithNew::computeTypePred(), CVC3::Theory::computeTypePred(), CVC3::TheoryBitvector::computeTypePred(), CVC3::TheoryArith3::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryCore::computeTypePred(), LFSCConvert::cvc3_to_lfsc(), CVC3::Expr::end(), CVC3::Expr::Expr(), CVC3::Expr::getFlag(), CVC3::Expr::getKids(), CVC3::Expr::getType(), LFSCObj::getY(), CVC3::Expr::hash(), IF_DEBUG(), LFSCObj::initialize(), CVC3::Expr::isType(), CVC3::ExprManager::newLeafExpr(), CVC3::ExprManager::newSkolemExpr(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::operator<<(), CVC3::QuantTheoremProducer::packVar(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::Theorem::print(), CVC3::QuantTheoremProducer::pullVarOut(), LFSCObj::queryAtomic(), CVC3::ExprManager::rebuild(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::QuantTheoremProducer::rewriteNotExists(), CVC3::QuantTheoremProducer::rewriteNotForall(), CVC3::Expr::setEqNext(), CVC3::Expr::setFind(), CVC3::Expr::setFlag(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), CVC3::Expr::setSimpCache(), CVC3::Expr::skolemExpr(), CVC3::Type::Type(), CVC3::Expr::typeCard(), CVC3::Expr::typeEnumerateFinite(), CVC3::Expr::typeSizeFinite(), CVC3::QuantTheoremProducer::universalInst(), CVC3::Expr::validSimpCache(), and LFSCObj::what_is_proven().
|
inline |
Definition at line 1162 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::BitvectorTheoremProducer::chopConcat(), CVC3::TheoryUF::computeTCC(), CVC3::BitvectorTheoremProducer::distributive_rule(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::TheoryRecords::getFields(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::Translator::preprocessRec(), LFSCPrinter::print_terms_h(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), and CVC3::TheoryArithOld::separateMonomial().
|
inline |
Definition at line 1168 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::d_kind, and NULL_KIND.
Referenced by CVC3::Theory::addBoundVar(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArithOld::addToBuffer(), CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryUF::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryCore::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractAllToConstEq(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), LFSCObj::can_pnorm(), canGetHead(), CVC3::TheoryQuant::canMatch(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArith3::canon(), CVC3::TheoryArithOld::canon(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonInvert(), CVC3::ArithTheoremProducer3::canonInvert(), CVC3::ArithTheoremProducer::canonInvert(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer3::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer3::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonMultPlusPlus(), CVC3::ArithTheoremProducer3::canonMultPlusPlus(), CVC3::ArithTheoremProducer::canonMultPlusPlus(), CVC3::ArithTheoremProducer3::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowLeaf(), CVC3::ArithTheoremProducer::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowPow(), CVC3::ArithTheoremProducer3::canonMultPowPow(), CVC3::ArithTheoremProducer::canonMultPowPow(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer3::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), LFSCObj::cascade_expr(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryBitvector::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryUF::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryArith3::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryCore::checkType(), CVC3::CompleteInstPreProcessor::collect_shield_index(), LFSCObj::collect_vars(), CVC3::TheoryBitvector::comparebv(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithNew::computeBaseType(), CVC3::TheoryArith3::computeBaseType(), CVC3::TheoryArithOld::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryBitvector::computeBVConst(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArray::computeModelTerm(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryArith3::computeModelTerm(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::TheoryBitvector::computeNegBVConst(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryDatatype::computeTCC(), CVC3::TheoryArithNew::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryArith3::computeTCC(), CVC3::TheoryArithOld::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheorySimulate::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryUF::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryArithNew::computeTypePred(), CVC3::TheoryArith3::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryCore::computeTypePred(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer3::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::Translator::containsArray(), CVC3::SearchEngineTheoremProducer::convertToCNF(), LFSCConvert::cvc3_to_lfsc(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), LFSCObj::define_skolem_vars(), CVC3::Translator::dump(), CVC3::VCCmd::evaluateCommand(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::VCL::exprFromString(), CVC3::Translator::finish(), CVC3::TheoryUF::finiteTypeInfo(), CVC3::TheoryArray::finiteTypeInfo(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::TheoryArithNew::finiteTypeInfo(), CVC3::TheoryBitvector::finiteTypeInfo(), CVC3::TheoryArith3::finiteTypeInfo(), CVC3::TheoryArithOld::finiteTypeInfo(), CVC3::TheoryCore::finiteTypeInfo(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::TheoryArray::getBaseArray(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::TheoryBitvector::getBVConstSize(), CVC3::TheoryBitvector::getBVConstValue(), CVC3::TheoryDatatype::getConsForTester(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryArith3::getFactors(), CVC3::TheoryArithOld::getFactors(), CVC3::TheoryQuant::getHeadExpr(), getLeft(), CVC3::Expr::getOp(), CVC3::Expr::getOpKind(), getRat(), getRight(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::Theory::getTCC(), CVC3::Theory::getTypePred(), CVC3::Expr::getUid(), LFSCObj::getY(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer3::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), hasBoundVarRec(), CVC3::CompleteInstPreProcessor::hasShieldVar(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::Expr::isApply(), CVC3::isArray(), CVC3::isArrayLiteral(), CVC3::TheoryArith::isAtomicArithFormula(), CVC3::TheoryArith::isAtomicArithTerm(), CVC3::Expr::isBoolConnective(), CVC3::isConstructor(), CVC3::isDarkShadow(), CVC3::isDatatype(), CVC3::isDivide(), isFlat(), LFSCObj::isFormula(), CVC3::isGE(), CVC3::isGrayShadow(), CVC3::isGT(), CVC3::isInt(), CVC3::ArithTheoremProducer3::IsIntegerElim(), CVC3::ArithTheoremProducerOld::IsIntegerElim(), CVC3::ArithTheoremProducer::IsIntegerElim(), CVC3::isIntPred(), CVC3::Expr::isLambda(), CVC3::isLE(), CVC3::isLT(), CVC3::isMinus(), CVC3::isMult(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::isPlus(), CVC3::isPow(), CVC3::Expr::isQuantifier(), CVC3::isRead(), CVC3::isReal(), CVC3::CompleteInstPreProcessor::isShield(), isSuperSimpleTrig(), CVC3::TheoryArith::isSyntacticRational(), CVC3::isUMinus(), LFSCObj::isVar(), CVC3::isWrite(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer3::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::Theory::lookupTypeExpr(), LFSCBoolRes::Make(), LFSCLraPoly::Make(), LFSCProof::Make_CNF(), make_flatten_expr_h(), LFSCClausify::Make_i(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer3::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryQuant::multMatchChild(), CVC3::ExprManager::newBoundVarExpr(), CVC3::Theory::newFunction(), CVC3::Theory::newVar(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), TReturn::normalize_to_tf(), TReturn::normalize_tr(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::BitvectorTheoremProducer::notBVEQ1Rule(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::TheoryArithNew::BoundInfo::operator<(), CVC3::TheoryArithNew::ExprBoundInfo::operator<(), CVC3::operator<<(), CVC3::TheoryCore::parseExpr(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::PrettyPrinterCore::print(), CVC3::TheorySimulate::print(), CVC3::TheoryUF::print(), CVC3::TheoryArray::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryArithNew::print(), CVC3::TheoryArith3::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryCore::print(), CVC3::TheoryQuant::print(), LFSCPrinter::print_formula_h(), LFSCPrinter::print_poly_norm(), LFSCPrinter::print_terms_h(), CVC3::Translator::printArrayExpr(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryCore::printSmtLibShared(), CVC3::VCCmd::printSymbols(), CVC3::TheoryCore::processCond(), CVC3::Translator::processType(), CVC3::Circuit::propagate(), CVC3::TheoryArithNew::propagateTheory(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::QuantTheoremProducer::recFindBoundVars(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::TheoryQuant::recursiveMap(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArithNew::registerAtom(), SAT::CNF_Manager::replaceITErec(), CVC3::Theory::resolveID(), CVC3::TheorySimulate::rewrite(), CVC3::TheoryUF::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::TheoryBitvector::rewriteBV(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::ArithTheoremProducerOld::rewriteLeavesConst(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::TheoryCore::rewriteLitCore(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::TheoryArith::rewriteToDiff(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::ArithTheoremProducer3::rightMinusLeft(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryUF::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryQuant::setupTriggers(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryBitvector::simplifyPendingEq(), CVC3::ExprTransform::simplifyWithCare(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::Theory::theoryOf(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithOld::tryPropagate(), and CVC3::TheoryArithOld::update().
|
inline |
Definition at line 1173 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::d_index.
Referenced by cmpExpr(), CVC3::compare(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::Expr::hasLastIndex(), CVC3::TheoryCore::print(), CVC3::Expr::recursiveSubst(), CVC3::TheoryCore::setupTerm(), and CVC3::TheoryQuant::setupTriggers().
|
inline |
Definition at line 1175 of file expr.h.
References CVC3::ExprValue::d_em, CVC3::Expr::d_expr, CVC3::Expr::getIndex(), and CVC3::ExprManager::lastIndex().
|
inline |
Make the expr into an operator.
Definition at line 1178 of file expr.h.
References DebugAssert, CVC3::Expr::isNull(), and CVC3::Expr::Op.
Referenced by CVC3::TheoryUF::computeTCC(), CVC3::TheoryCore::computeTypePred(), CVC3::VCL::createOp(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::Theory::lookupFunction(), CVC3::Theory::newFunction(), CVC3::Theory::newSubtypeExpr(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryUF::parseExprOp(), CVC3::Expr::recursiveSubst(), and CVC3::UFTheoremProducer::rewriteOpDef().
|
inline |
Get operator from expression.
Definition at line 1183 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::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryUF::checkSat(), CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryDatatype::computeType(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::CommonTheoremProducer::findITE(), CVC3::TheoryQuant::getHeadExpr(), CVC3::Expr::getOpExpr(), CVC3::Expr::getOpKind(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CompleteInstPreProcessor::inst(), CVC3::CompleteInstPreProcessor::isMacro(), CVC3::ArithTheoremProducerOld::leftMinusRight(), CVC3::ArithTheoremProducer3::leftMinusRight(), CVC3::ArithTheoremProducer::leftMinusRight(), CVC3::ArithTheoremProducer3::multIneqn(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryBitvector::printSmtLibShared(), CVC3::Translator::processType(), CVC3::ExprTransform::pushNegation1(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::TheoryBitvector::rewriteBV(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::ArithTheoremProducer3::rightMinusLeft(), CVC3::ArithTheoremProducerOld::rightMinusLeft(), CVC3::ArithTheoremProducer::rightMinusLeft(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::CommonTheoremProducer::substitutivityRule(), and CVC3::CompleteInstPreProcessor::substMacro().
|
inline |
Get expression of operator (for APPLY Exprs only)
Definition at line 1191 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::TheoryDatatype::assertFact(), CVC3::ExprTransform::BuildBryantMaps(), CVC3::TheoryDatatype::canCollapse(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryDatatype::computeTCC(), 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::ExprTransform::ITE_generator(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::ExprTransform::PredConstrainer(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::VCCmd::printSymbols(), CVC3::UFTheoremProducer::relTrans(), CVC3::TheoryUF::rewrite(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), and CVC3::TheoryDatatype::update().
|
inline |
Get kind of operator (for APPLY Exprs only)
Definition at line 1196 of file expr.h.
References CVC3::Op::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOp(), and CVC3::Expr::isApply().
Referenced by CVC3::UFTheoremProducer::applyLambda(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryUF::assertFact(), CVC3::TheoryArray::assertFact(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), 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::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::ExprTransform::BuildBryantMaps(), CVC3::BitvectorTheoremProducer::buildPlusTerm(), CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvShiftZero(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::TheoryBitvector::BVSize(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::BitvectorTheoremProducer::canonBVPlus(), CVC3::BitvectorTheoremProducer::canonBVUMinus(), CVC3::TheoryBitvector::canSolveFor(), CVC3::TheoryBitvector::check_linear(), CVC3::TheoryUF::checkSat(), CVC3::TheoryRecords::checkType(), CVC3::TheoryBitvector::checkType(), CVC3::BitvectorTheoremProducer::chopConcat(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryBitvector::computeModelTerm(), CVC3::TheoryRecords::computeTCC(), 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::TheoryBitvector::countTermIn(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::BitvectorTheoremProducer::distributive_rule(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::TheoryBitvector::extract_vars(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractBVPlus(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::TheoryBitvector::generalBitBlast(), 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::BitvectorTheoremProducer::getPlusTerms(), CVC3::TheoryBitvector::getSXIndex(), CVC3::TheoryBitvector::getTypePredExpr(), CVC3::TheoryBitvector::getTypePredType(), CVC3::isConstructor(), CVC3::TheoryBitvector::isLinearTerm(), CVC3::BitvectorTheoremProducer::isolate_var(), 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(), isUniterpFunc(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::TheoryBitvector::multiply_coeff(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negElim(), 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::newBVPlusExpr(), CVC3::TheoryBitvector::newBVSDivExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSModExpr(), CVC3::TheoryBitvector::newBVSRemExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::TheoryBitvector::Odd_coeff(), CVC3::BitvectorTheoremProducer::okToSplit(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), 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::ExprTransform::PredConstrainer(), CVC3::Translator::preprocessRec(), CVC3::TheoryRecords::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryBitvector::printSmtLibShared(), CVC3::BitvectorTheoremProducer::processExtract(), CVC3::TheoryBitvector::pushNegation(), CVC3::UFTheoremProducer::relTrans(), CVC3::ExprTransform::RemoveFunctionApps(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::RecordsTheoremProducer::rewriteLitSelect(), CVC3::RecordsTheoremProducer::rewriteLitUpdate(), CVC3::RecordsTheoremProducer::rewriteUpdateSelect(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::BitvectorTheoremProducer::sameKidCheck(), CVC3::TheoryRecords::setup(), CVC3::BitvectorTheoremProducer::signBVLTRule(), 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::zeroExtendRule(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().
|
inline |
Definition at line 1201 of file expr.h.
References CVC3::ExprValue::arity(), CVC3::Expr::d_expr, and CVC3::Expr::isNull().
Referenced by CVC3::CommonTheoremProducer::ackermann(), CVC3::TheoryQuant::add_parent(), SAT::CNF_Manager::addAssumption(), CVC3::TheoryArray::addSharedTerm(), CVC3::TheoryArithOld::addToBuffer(), ajr_debug_print(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andElim(), CVC3::SearchImplBase::applyCNFRules(), CVC3::UFTheoremProducer::applyLambda(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryUF::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractAllToConstEq(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), 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::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::TheoryArithNew::boundsAsString(), CVC3::ExprTransform::BuildBryantMaps(), CVC3::BitvectorTheoremProducer::buildPlusTerm(), CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvShiftZero(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::TheoryDatatype::canCollapse(), CVC3::TheoryQuant::canMatch(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArith3::canon(), CVC3::TheoryArithOld::canon(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer3::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithNew::canonPred(), CVC3::TheoryArith3::canonPred(), CVC3::TheoryArithOld::canonPred(), CVC3::TheoryArithNew::canonPredEquiv(), CVC3::TheoryArith3::canonPredEquiv(), CVC3::TheoryArithOld::canonPredEquiv(), CVC3::TheoryArith::canonRec(), CVC3::TheoryArith::canonSimp(), CVC3::TheoryArithOld::canPickEqMonomial(), LFSCObj::cascade_expr(), CVC3::TheoryBitvector::check_linear(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArithNew::checkSatSimplex(), CVC3::TheoryCore::checkSolved(), CVC3::TheoryUF::checkType(), CVC3::TheoryArray::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryArith3::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryCore::checkType(), CVC3::BitvectorTheoremProducer::chopConcat(), CVC3::Circuit::Circuit(), CVC3::ClauseValue::ClauseValue(), CVC3::CompleteInstPreProcessor::collect_shield_index(), LFSCObj::collect_vars(), CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryDatatype::computeTCC(), CVC3::TheoryArithNew::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryArith3::computeTCC(), CVC3::TheoryArithOld::computeTCC(), CVC3::TheorySimulate::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryRecords::computeTypePred(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), constantKids(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer3::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::ExprTransform::CountSubTerms(), CVC3::TheoryBitvector::countTermIn(), LFSCConvert::cvc3_to_lfsc(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::TheoryDatatype::dataType(), CVC3::VCL::dataType(), CVC3::DatatypeTheoremProducer::decompose(), LFSCObj::define_skolem_vars(), LFSCConvert::do_bso(), CVC3::TheoryArith3::doSolve(), CVC3::Translator::dump(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::VCCmd::evaluateCommand(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::VCL::exprFromString(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractBVMult(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::extractConst(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractWhole(), findAtom(), CVC3::VCCmd::findAxioms(), CVC3::TheoryArithNew::findCoefficient(), CVC3::CommonTheoremProducer::findITE(), findPolarity(), findPolarityAtomic(), CVC3::Theory::findReduce(), CVC3::DecisionEngine::findSplitterRec(), CVC3::Translator::finish(), CVC3::TheoryDatatype::finiteTypeInfo(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::TheoryBitvector::generalBitBlast(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryArith3::getFactors(), CVC3::TheoryArithOld::getFactors(), CVC3::ExprTransform::GetFormulaMap(), CVC3::ArithTheoremProducerOld::getLeaves(), getLeft(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithNew::getLowerBoundExplanation(), LFSCObj::getNumNodes(), CVC3::Expr::getOp(), CVC3::ExprTransform::GetPEqs(), CVC3::BitvectorTheoremProducer::getPlusTerms(), getRight(), CVC3::ExprTransform::GetSub_vec(), CVC3::TheoryArithOld::getUpperBound(), CVC3::TheoryArithNew::getUpperBoundExplanation(), LFSCObj::getY(), CVC3::ArithTheoremProducer3::greaterthan(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), hasBoundVarRec(), CVC3::CompleteInstPreProcessor::hasShieldVar(), CVC3::CoreTheoremProducer::iffAndDistrib(), CVC3::CoreTheoremProducer::iffOrDistrib(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CoreTheoremProducer::ifLiftUnaryRule(), CVC3::CommonTheoremProducer::implContrapositive(), CVC3::CommonTheoremProducer::implMP(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::CompleteInstPreProcessor::inst(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryArith::isAtomicArithTerm(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), isFlat(), CVC3::TheoryArith3::isIntegerDerive(), CVC3::TheoryArithNew::isIntegerDerive(), CVC3::TheoryArithOld::isIntegerDerive(), CVC3::TheoryArithOld::isNonlinearEq(), CVC3::TheoryArithOld::isNonlinearSumTerm(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::CompleteInstPreProcessor::isShield(), isSimpleTrig(), isSuperSimpleTrig(), CVC3::isTrivialExpr(), CVC3::TheoryArithOld::isUnconstrained(), CVC3::ExprTransform::ITE_generator(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::TheoryArithNew::kidsCanonical(), CVC3::TheoryArith3::kidsCanonical(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::TheoryArith::leavesAreNumConst(), CVC3::Theory::leavesAreSimp(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), LFSCClausify::Make(), LFSCProof::Make_and_elim(), LFSCProof::Make_CNF(), LFSCPrinter::make_let_map(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::TheoryBitvector::multiply_coeff(), CVC3::TheoryQuant::multMatchChild(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negElim(), CVC3::BitvectorTheoremProducer::negNeg(), CVC3::ExprTransform::newPPrec(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::SearchSat::newUserAssumptionIntHelper(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::ArithTheoremProducer3::oneElimination(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::Expr::operator[](), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVMult(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::TheoryCore::parseExpr(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pivotRule(), CVC3::ArithTheoremProducerOld::powEqZero(), CVC3::ArithTheoremProducer3::powEqZero(), CVC3::ArithTheoremProducer::powEqZero(), CVC3::ExprTransform::PredConstrainer(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheorySimulate::print(), CVC3::TheoryRecords::print(), CVC3::TheoryUF::print(), CVC3::TheoryArray::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryArithNew::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryArith3::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryCore::print(), LFSCPrinter::print_poly_norm(), LFSCPrinter::print_terms_h(), CVC3::Translator::printArrayExpr(), CVC3::TheoryUF::printSmtLibShared(), CVC3::TheoryBitvector::printSmtLibShared(), CVC3::TheoryCore::printSmtLibShared(), CVC3::TheoryCore::processCond(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::Translator::processType(), CVC3::Circuit::propagate(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), recursiveExprScore(), recursiveGetPartTriggers(), CVC3::TheoryQuant::recursiveMap(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::ExprTransform::RemoveFunctionApps(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBV(), CVC3::BitvectorTheoremProducer::rewriteBVCOMP(), CVC3::BitvectorTheoremProducer::rewriteBVSub(), CVC3::CoreTheoremProducer::rewriteDistinct(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::UFTheoremProducer::rewriteOpDef(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::TheoryArith::rewriteToDiff(), CVC3::BitvectorTheoremProducer::rewriteXNOR(), CVC3::BitvectorTheoremProducer::rightShiftToConcat(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArithOld::separateMonomial(), setRecursiveInUserAssumption(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryArray::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryBitvector::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::setup(), CVC3::Theory::setupCC(), CVC3::TheoryArithNew::setupRec(), CVC3::TheoryArith3::setupRec(), CVC3::TheoryArithOld::setupRec(), CVC3::TheoryCore::setupSubFormulas(), CVC3::TheoryCore::setupTerm(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::TheoryCore::simplify(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::TheoryBitvector::simplifyOp(), CVC3::Theory::simplifyOp(), CVC3::TheoryCore::simplifyOp(), CVC3::ExprTransform::simplifyWithCare(), CVC3::TheoryQuant::simpRAWList(), CVC3::ExprTransform::smartSimplify(), CVC3::ExprTransform::specialSimplify(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::TheoryArithNew::substAndCanonizeTableaux(), CVC3::ExprTransform::substitute(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::TheoryArithOld::termDegree(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), CVC3::Theory::updateCC(), CVC3::TheoryArithOld::updateConstrained(), CVC3::TheoryArithNew::updateDependencies(), CVC3::Theory::updateHelper(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryBitvector::updateSubterms(), CVC3::TheoryArithNew::updateValue(), usefulInMatch(), LFSCObj::what_is_proven(), CVC3::CommonTheoremProducer::xorToIff(), CVC3::BitvectorTheoremProducer::zeroBVOR(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), and CVC3::BitvectorTheoremProducer::zeroLeq().
|
inline |
Definition at line 1206 of file expr.h.
References CVC3::Expr::arity(), CVC3::Expr::d_expr, DebugAssert, and CVC3::ExprValue::getKids().
|
inline |
Remove leading NOT if any.
Definition at line 506 of file expr.h.
Referenced by CVC3::TheoryCore::assertFact(), CVC3::SearchSat::getImplication(), and CVC3::SearchSat::getImpliedLiteral().
|
inline |
Begin iterator.
Definition at line 1211 of file expr.h.
References CVC3::ExprValue::arity(), CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::ExprManager::getEmptyVector(), CVC3::ExprValue::getKids(), and CVC3::Expr::isNull().
Referenced by CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::TheoryArithOld::addToBuffer(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultPlusPlus(), CVC3::ArithTheoremProducer3::canonMultPlusPlus(), CVC3::ArithTheoremProducer::canonMultPlusPlus(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer3::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryRecords::checkType(), CVC3::TheoryUF::checkType(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::ExprStream::collectShared(), CVC3::TheoryArithNew::collectVars(), CVC3::TheoryArith3::collectVars(), CVC3::TheoryArithOld::collectVars(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithOld::DifferenceLogicGraph::computeModel(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryBitvector::computeModelTerm(), CVC3::TheoryArith3::computeModelTerm(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::Theory::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::BitvectorTheoremProducer::concatFlatten(), constantKids(), CVC3::Translator::containsArray(), containsRec(), SAT::CNF_Manager::convertLemma(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::TheoryArith3::doSolve(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::VCCmd::findAxioms(), CVC3::Theory::findReduced(), CVC3::TheoryUF::finiteTypeInfo(), flatAnds(), CVC3::TheoryArith3::getFactors(), CVC3::TheoryArithOld::getFactors(), CVC3::ArithTheoremProducer3::greaterthan(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::SearchImplBase::isClause(), CVC3::Theory::isLeafIn(), CVC3::SearchImplBase::isPropClause(), CVC3::TheoryArith3::isStale(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryBitvector::isTermIn(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducerOld::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::TheoryCore::parseExpr(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArith3::pickMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryArithNew::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryArith3::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryCore::print(), CVC3::TheoryCore::printSmtLibShared(), CVC3::VCCmd::printSymbols(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::QuantTheoremProducer::recFindBoundVars(), recGetSubTerms(), CVC3::TheoryArith::recursiveCanonSimpCheck(), recursiveExprScore(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::TheoryQuant::recursiveMap(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryArithOld::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryRecords::setup(), CVC3::subExprRec(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducer3::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer3::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithNew::updateDependenciesAdd(), CVC3::TheoryArithNew::updateDependenciesRemove(), CVC3::TheoryArith3::updateSubsumptionDB(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
End iterator.
Definition at line 1217 of file expr.h.
References CVC3::ExprValue::arity(), CVC3::Expr::d_expr, CVC3::Expr::getEM(), CVC3::ExprManager::getEmptyVector(), CVC3::ExprValue::getKids(), and CVC3::Expr::isNull().
Referenced by CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::TheoryArithOld::addToBuffer(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::canonMult(), CVC3::ArithTheoremProducer::canonMult(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonMultConstPlus(), CVC3::ArithTheoremProducer3::canonMultConstPlus(), CVC3::ArithTheoremProducer::canonMultConstPlus(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducer::canonMultLeafOrPowOrMultPlus(), CVC3::ArithTheoremProducerOld::canonMultPlusPlus(), CVC3::ArithTheoremProducer3::canonMultPlusPlus(), CVC3::ArithTheoremProducer::canonMultPlusPlus(), CVC3::ArithTheoremProducerOld::canonPlus(), CVC3::ArithTheoremProducer3::canonPlus(), CVC3::ArithTheoremProducer::canonPlus(), CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::TheoryRecords::checkType(), CVC3::TheoryUF::checkType(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::ExprStream::collectShared(), CVC3::TheoryArithNew::collectVars(), CVC3::TheoryArith3::collectVars(), CVC3::TheoryArithOld::collectVars(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryRecords::computeBaseType(), CVC3::TheoryUF::computeBaseType(), CVC3::TheoryArray::computeBaseType(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryBitvector::computeModelTerm(), CVC3::TheoryArith3::computeModelTerm(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::Theory::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryRecords::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::BitvectorTheoremProducer::concatFlatten(), constantKids(), CVC3::Translator::containsArray(), containsRec(), SAT::CNF_Manager::convertLemma(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::TheoryArith3::doSolve(), CVC3::BitvectorTheoremProducer::extractBitwise(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::VCCmd::findAxioms(), CVC3::Theory::findReduced(), CVC3::TheoryUF::finiteTypeInfo(), flatAnds(), CVC3::TheoryArith3::getFactors(), CVC3::TheoryArithOld::getFactors(), CVC3::ArithTheoremProducerOld::greaterthan(), CVC3::ArithTheoremProducer3::greaterthan(), CVC3::ArithTheoremProducer::greaterthan(), CVC3::SearchImplBase::isClause(), CVC3::Theory::isLeafIn(), CVC3::SearchImplBase::isPropClause(), CVC3::TheoryArith3::isStale(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryBitvector::isTermIn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducerOld::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::BitvectorTheoremProducer::padBVPlus(), CVC3::TheoryCore::parseExpr(), CVC3::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArith3::pickMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::Translator::preprocessRec(), CVC3::TheoryUF::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryArithNew::print(), CVC3::TheoryBitvector::print(), CVC3::TheoryArith3::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryCore::print(), CVC3::TheoryCore::printSmtLibShared(), CVC3::VCCmd::printSymbols(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryBitvector::pushNegationRec(), CVC3::QuantTheoremProducer::recFindBoundVars(), recGetSubTerms(), CVC3::TheoryArith::recursiveCanonSimpCheck(), recursiveExprScore(), recursiveGetBoundVars(), recursiveGetPartTriggers(), recursiveGetSubTrig(), CVC3::TheoryQuant::recursiveMap(), SAT::CNF_Manager::replaceITErec(), CVC3::TheoryArithOld::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::TheoryBitvector::rewriteBoolean(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::TheoryRecords::setup(), CVC3::subExprRec(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducer3::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer3::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), SAT::CNF_Manager::translateExprRec(), CVC3::TheoryArithNew::updateDependenciesAdd(), CVC3::TheoryArithNew::updateDependenciesRemove(), CVC3::TheoryArith3::updateSubsumptionDB(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
Definition at line 1223 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::d_kind, and NULL_KIND.
Referenced by CVC3::Expr::arity(), CVC3::TheoryDatatype::assertFact(), CVC3::SearchSat::assertLit(), CVC3::Expr::begin(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::BitvectorTheoremProducer::buildPlusTerm(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::SearchSimple::checkValidRec(), CVC3::BitvectorTheoremProducer::chopConcat(), CVC3::ExprManager::clear(), CVC3::Expr::clearFlags(), CVC3::Expr::clearRewriteNormal(), cmpExpr(), CVC3::TheoryBitvector::comparebv(), 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::ExprApply::ExprApply(), CVC3::ExprApplyTmp::ExprApplyTmp(), CVC3::VCL::exprFromString(), findAtom(), CVC3::DecisionEngineDFS::findSplitter(), CVC3::DecisionEngine::findSplitterRec(), CVC3::SearchEngineFast::fixConflict(), CVC3::BitvectorTheoremProducer::generalIneqn(), CVC3::Theory::getBaseType(), CVC3::TheoryDatatype::getConstant(), CVC3::Expr::getEqNext(), 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::Proof::isNull(), CVC3::ExprTransform::ITE_generator(), CVC3::Expr::lookupType(), CVC3::Theory::lookupTypeExpr(), CVC3::Expr::mkOp(), CVC3::Theory::newSubtypeExpr(), CVC3::Theory::newTypeExpr(), CVC3::Theory::newVar(), CVC3::Op::Op(), CVC3::operator<<(), CVC3::TheoryCore::parseExpr(), CVC3::TheoryUF::parseExprOp(), CVC3::ExprManager::rebuild(), CVC3::Expr::recursiveSubst(), CVC3::ArithTheoremProducerOld::rewriteLeavesConst(), CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::setEqNext(), 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::setNotArrayNormalized(), CVC3::Expr::setRegisteredAtom(), CVC3::Expr::setRep(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::Expr::setSig(), CVC3::Expr::setSimpCache(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTerminalsConstFlag(), CVC3::Expr::setTranslated(), CVC3::Expr::setType(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setUsesCC(), CVC3::Expr::setValidType(), CVC3::Expr::setWellFounded(), CVC3::SearchEngineFast::split(), CVC3::Theory::theoryOf(), CVC3::Type::Type(), CVC3::Expr::typeCard(), CVC3::Expr::typeEnumerateFinite(), CVC3::Expr::typeSizeFinite(), CVC3::QuantTheoremProducer::universalInst(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and CVC3::TheoryBitvector::update().
|
inline |
Definition at line 518 of file expr.h.
Referenced by LFSCObj::queryM().
|
inline |
Get the memory manager index (it uniquely identifies the subclass)
Definition at line 1227 of file expr.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getMMIndex(), and CVC3::Expr::isNull().
|
inline |
Definition at line 1232 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::d_find, DebugAssert, and CVC3::Expr::isNull().
Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith3::canonSimplify(), CVC3::TheoryArithOld::canonSimplify(), CVC3::TheoryArith3::checkAssertEqInvariant(), CVC3::TheoryArithOld::checkAssertEqInvariant(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::SearchSimple::checkValidRec(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::Theory::find(), CVC3::Theory::findExpr(), CVC3::Theory::findReduce(), CVC3::Theory::findReduced(), CVC3::Theory::findRef(), CVC3::Expr::getEqNext(), CVC3::Expr::getFind(), CVC3::Expr::getFindLevel(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::TheoryArithOld::isStale(), CVC3::Theory::leavesAreSimp(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryDatatypeLazy::mergeLabels(), CVC3::TheoryDatatype::mergeLabels(), CVC3::TheoryQuant::multMatchChild(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryArith::recursiveCanonSimpCheck(), CVC3::TheoryRecords::rewriteAux(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryArithNew::setupRec(), CVC3::TheoryArith3::setupRec(), CVC3::TheoryArithOld::setupRec(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryCore::simplify(), CVC3::ExprTransform::smartSimplify(), CVC3::TheoryRecords::update(), CVC3::TheoryArray::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryCore::update().
|
inline |
Definition at line 1237 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(), CVC3::TheoryQuant::matchListOld(), and CVC3::TheoryRecords::rewriteAux().
|
inline |
Definition at line 1242 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::d_find, DebugAssert, and CVC3::Expr::hasFind().
|
inline |
Definition at line 1247 of file expr.h.
References CVC3::ExprValue::d_eqNext, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::hasFind(), and CVC3::Expr::isNull().
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryQuant::multMatchChild(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), and CVC3::TheoryQuant::synNewInst().
|
inline |
Definition at line 1254 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::d_notifyList, and CVC3::Expr::isNull().
Referenced by CVC3::TheoryCore::assertEqualities(), and CVC3::TheoryCore::setFindLiteral().
|
inline |
Get the type. Recursively compute if necessary.
Definition at line 1259 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::CompleteInstPreProcessor::addIndex(), CVC3::TheoryArithOld::addPairToArithOrder(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::VCL::assertFormula(), CVC3::TheoryCore::assignValue(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::ExprTransform::BuildBryantMaps(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivConst(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::bvURemConst(), CVC3::SearchSat::check(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryCore::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::CompleteInstPreProcessor::collectHeads(), CVC3::ExprStream::collectShared(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryRecords::computeModelTerm(), CVC3::TheoryArray::computeModelTerm(), CVC3::TheoryBitvector::computeModelTerm(), CVC3::TheoryRecords::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryRecords::computeType(), CVC3::TheoryUF::computeType(), CVC3::TheoryArray::computeType(), CVC3::ExprManager::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryQuant::computeType(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::VCL::createOp(), CVC3::TheoryArithOld::currentMaxCoefficient(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::CommonTheoremProducer::findITE(), findPolarity(), findPolarityAtomic(), CVC3::Translator::finish(), CVC3::TheoryDatatype::finiteTypeInfo(), 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::isBoolConnective(), CVC3::isConstructor(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArith3::isIntegerThm(), CVC3::TheoryArithNew::isIntegerThm(), CVC3::TheoryArithOld::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::newBVPlusExpr(), CVC3::TheoryBitvector::newBVSDivExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSModExpr(), CVC3::TheoryBitvector::newBVSRemExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::TheoremProducer::newPf(), CVC3::ExprTransform::newPP(), CVC3::ExprTransform::newPPrec(), CVC3::Theory::newSubtypeExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), 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::TheoryCore::parseExprOp(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryCore::print(), CVC3::TheoryCore::processUpdates(), CVC3::VCL::query(), CVC3::CompleteInstPreProcessor::recInstMacros(), CVC3::CompleteInstPreProcessor::recRewriteNot(), CVC3::CompleteInstPreProcessor::recSkolemize(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::BitvectorTheoremProducer::repeatRule(), SAT::CNF_Manager::replaceITErec(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryUF::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryUF::setup(), CVC3::TheoryArray::setup(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::setupTriggers(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::CompleteInstPreProcessor::simplifyEq(), CVC3::VCL::simplifyThm(), CVC3::ExprTransform::simplifyWithCare(), CVC3::TheoryArithNew::solve(), CVC3::TheoryArith3::solve(), CVC3::ExprTransform::specialSimplify(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate(), CVC3::CoreTheoremProducer::typePred(), CVC3::TheoryUF::update(), CVC3::Theory::updateCC(), CVC3::TheoryArithOld::updateStats(), CVC3::VCL::varExpr(), CVC3::CommonTheoremProducer::varIntroRule(), CVC3::BitvectorTheoremProducer::zeroExtendRule(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().
|
inline |
Look up the current type. Do not recursively compute (i.e. may be NULL)
Definition at line 1265 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::d_type, CVC3::Expr::isNull(), and CVC3::Expr::s_null.
Referenced by CVC3::TypeComputerCore::computeType(), CVC3::TheoryCore::computeTypePred(), CVC3::Theory::getBaseType(), CVC3::Theory::lookupFunction(), CVC3::Theory::lookupVar(), and CVC3::ExprManager::newBoundVarExpr().
|
inline |
Return cardinality of type.
Definition at line 1270 of file expr.h.
References DebugAssert, CVC3::ExprManager::finiteTypeInfo(), CVC3::Expr::getEM(), and CVC3::Expr::isNull().
|
inline |
Return nth (starting with 0) element in a finite type.
Returns NULL Expr if unable to compute nth element
Definition at line 1277 of file expr.h.
References CVC3::CARD_FINITE, DebugAssert, CVC3::Expr::Expr(), CVC3::ExprManager::finiteTypeInfo(), CVC3::Expr::getEM(), and CVC3::Expr::isNull().
Referenced by CVC3::Type::enumerateFinite(), and CVC3::TheoryDatatype::finiteTypeInfo().
|
inline |
Return size of a finite type; returns 0 if size cannot be determined.
Definition at line 1285 of file expr.h.
References CVC3::CARD_FINITE, DebugAssert, CVC3::ExprManager::finiteTypeInfo(), CVC3::Expr::getEM(), and CVC3::Expr::isNull().
Referenced by CVC3::TheoryDatatype::finiteTypeInfo().
|
inline |
Return true if there is a valid cached value for calling simplify on this Expr.
Definition at line 1294 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().
|
inline |
Definition at line 1298 of file expr.h.
References CVC3::Expr::d_expr, and CVC3::ExprValue::d_simpCache.
Referenced by CVC3::TheoryCore::simplify().
|
inline |
Definition at line 1302 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().
|
inline |
Definition at line 1306 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::VALID_IS_ATOMIC.
|
inline |
Definition at line 1310 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::VALID_TERMINALS_CONST.
Referenced by CVC3::TheoryArith::leavesAreNumConst().
|
inline |
Definition at line 1314 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IS_ATOMIC.
|
inline |
Definition at line 1318 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::TERMINALS_CONST.
Referenced by CVC3::TheoryArith::leavesAreNumConst().
|
inline |
Definition at line 1322 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().
|
inline |
Definition at line 1326 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::dataType(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), and CVC3::TheoryDatatype::instantiate().
|
inline |
Definition at line 1330 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::WELL_FOUNDED.
Referenced by CVC3::TheoryDatatype::dataType().
|
inline |
Definition at line 1334 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().
|
inline |
Definition at line 1338 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::CompleteInstPreProcessor::collectIndex(), CVC3::CompleteInstPreProcessor::isGoodQuant(), isGround(), isSimpleTrig(), CVC3::TheoryQuant::multMatchChild(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), recursiveGetBoundVars(), and CVC3::TheoryQuant::theoryPreprocess().
|
inline |
Definition at line 1342 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::USES_CC.
Referenced by CVC3::TheoryCore::simplify().
|
inline |
Definition at line 1346 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::NOT_ARRAY_NORMALIZED.
Referenced by CVC3::TheoryArray::addSharedTerm(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::setup(), and CVC3::TheoryArray::update().
|
inline |
Definition at line 1350 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().
|
inline |
Definition at line 1354 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().
|
inline |
Definition at line 1358 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, CVC3::CDFlags::get(), and CVC3::Expr::IN_USER_ASSUMPTION.
Referenced by CVC3::TheoryCore::getQuantLevelForTerm(), and setRecursiveInUserAssumption().
|
inline |
Definition at line 1362 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().
|
inline |
Definition at line 1366 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().
|
inline |
Definition at line 1370 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().
|
inline |
Definition at line 1374 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().
|
inline |
Definition at line 1378 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::Theorem::GetSatAssumptionsRec(), SAT::CNF_Manager::registerAtom(), CVC3::SearchSat::registerAtom(), CVC3::TheoryCore::registerAtom(), CVC3::TheoryCore::setFindLiteral(), and CVC3::TheoryCore::update().
|
inline |
Definition at line 1382 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().
|
inline |
Definition at line 1386 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::setupTerm().
|
inline |
Check if the generic flag is set.
Definition at line 1390 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(), and CVC3::subExprRec().
|
inline |
Set the generic flag.
Definition at line 1395 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(), and CVC3::subExprRec().
|
inline |
Clear the generic flag in all Exprs.
Definition at line 1400 of file expr.h.
References CVC3::ExprManager::clearFlags(), DebugAssert, CVC3::Expr::getEM(), and CVC3::Expr::isNull().
Referenced by getBoundVars(), getPartTriggers(), CVC3::Expr::getSize(), CVC3::TheoryQuant::getSubTerms(), and getSubTrig().
string CVC3::Expr::toString | ( | ) | const |
Print the expression to a string.
Definition at line 344 of file expr.cpp.
References CVC3::PRESENTATION_LANG.
Referenced by SAT::CNF_Manager::addAssumption(), CVC3::Theory::addBoundVar(), CVC3::TheoryArith3::VarOrderGraph::addEdge(), CVC3::TheoryArithOld::VarOrderGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryCore::addFact(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::SearchSat::addLemma(), CVC3::TheoryArithOld::addPairToArithOrder(), CVC3::TheoryArray::addSharedTerm(), CVC3::SearchImplBase::addSplitter(), CVC3::SearchEngineFast::addSplitter(), CVC3::TheoryArithOld::addToBuffer(), CVC3::SearchImplBase::addToCNFCache(), CVC3::QuantTheoremProducer::adjustVarUniv(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::SearchImplBase::applyCNFRules(), CVC3::UFTheoremProducer::applyLambda(), CVC3::TheoryCore::assertEqualities(), CVC3::TheoryRecords::assertFact(), CVC3::TheoryUF::assertFact(), CVC3::TheoryArray::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryBitvector::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryQuant::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchSat::assertLit(), CVC3::TheoryArithNew::assertLower(), CVC3::TheoryBitvector::assertTypePred(), CVC3::TheoryArithNew::assertUpper(), CVC3::Theory::assignValue(), CVC3::TheoryCore::assignValue(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bitblastBVPlus(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastIneqn(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), 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::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::bitwiseFlatten(), CVC3::TheoryArithNew::boundsAsString(), CVC3::QuantTheoremProducer::boundVarElim(), CVC3::TheoryCore::buildModel(), CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::bvConstIneqn(), CVC3::BitvectorTheoremProducer::bvConstMultAssocRule(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::BVMult_order_subterms(), CVC3::BitvectorTheoremProducer::bvMultAssocRule(), CVC3::BitvectorTheoremProducer::bvmultBVUminus(), CVC3::BitvectorTheoremProducer::bvmultConst(), CVC3::BitvectorTheoremProducer::bvMultDistRule(), CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule(), CVC3::BitvectorTheoremProducer::bvSDivRewrite(), CVC3::BitvectorTheoremProducer::bvShiftZero(), CVC3::BitvectorTheoremProducer::bvshlSplit(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::TheoryBitvector::BVSize(), CVC3::BitvectorTheoremProducer::bvSModRewrite(), CVC3::BitvectorTheoremProducer::bvSRemRewrite(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::bvuminusBVConst(), CVC3::BitvectorTheoremProducer::bvuminusBVMult(), CVC3::BitvectorTheoremProducer::bvuminusBVUminus(), CVC3::BitvectorTheoremProducer::bvuminusToBVPlus(), CVC3::BitvectorTheoremProducer::bvuminusVar(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArith3::canon(), CVC3::TheoryArithOld::canon(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::BitvectorTheoremProducer::canonBVPlus(), CVC3::BitvectorTheoremProducer::canonBVUMinus(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::canonDivide(), CVC3::ArithTheoremProducerOld::canonDivide(), CVC3::ArithTheoremProducer::canonDivide(), CVC3::ArithTheoremProducer3::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer3::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducer3::canonDivideVar(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonInvert(), CVC3::ArithTheoremProducerOld::canonInvert(), CVC3::ArithTheoremProducer::canonInvert(), CVC3::ArithTheoremProducerOld::canonInvertConst(), CVC3::ArithTheoremProducer3::canonInvertConst(), CVC3::ArithTheoremProducer::canonInvertConst(), CVC3::ArithTheoremProducerOld::canonInvertMult(), CVC3::ArithTheoremProducer3::canonInvertMult(), CVC3::ArithTheoremProducer::canonInvertMult(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer3::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonMultTerm1Term2(), CVC3::ArithTheoremProducerOld::canonMultTerm1Term2(), CVC3::ArithTheoremProducer::canonMultTerm1Term2(), CVC3::ArithTheoremProducer3::canonMultTermConst(), CVC3::ArithTheoremProducerOld::canonMultTermConst(), CVC3::ArithTheoremProducer::canonMultTermConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithNew::canonSimplify(), CVC3::TheoryArith3::canonSimplify(), CVC3::TheoryArithOld::canonSimplify(), CVC3::SearchEngineTheoremProducer::caseSplit(), CVC3::SearchSat::check(), CVC3::TheoryBitvector::check_linear(), CVC3::TheoryCore::checkEquation(), CVC3::TheoryDatatypeLazy::checkSat(), CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryArithOld::checkSat(), CVC3::SearchEngineTheoremProducer::checkSoundNoSkolems(), CVC3::VCL::checkTCC(), CVC3::TheoryRecords::checkType(), CVC3::TypeComputerCore::checkType(), CVC3::TheoryUF::checkType(), CVC3::TheoryDatatype::checkType(), CVC3::Theory::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryArith3::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::TheoryCore::checkType(), CVC3::SearchSimple::checkValidInternal(), CVC3::SearchEngineFast::checkValidInternal(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::BitvectorTheoremProducer::collectLikeTermsOfPlus(), CVC3::BitvectorTheoremProducer::combineLikeTermsRule(), CVC3::TheoryCore::computeBaseType(), CVC3::TheoryBitvector::computeBVConst(), CVC3::TheoryRecords::computeModel(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryBitvector::computeModel(), CVC3::TheoryArith3::computeModel(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithNew::computeModelTerm(), CVC3::TheoryArith3::computeModelTerm(), CVC3::TheoryArithOld::computeModelTerm(), CVC3::TheoryBitvector::computeNegBVConst(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryDatatype::computeTCC(), CVC3::TheoryQuant::computeTCC(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheorySimulate::computeType(), CVC3::TypeComputerCore::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryUF::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryQuant::computeType(), CVC3::BitvectorTheoremProducer::concatConst(), CVC3::BitvectorTheoremProducer::concatFlatten(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::constEq(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer3::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducer3::create_t(), CVC3::BitvectorTheoremProducer::createNewPlusCollection(), CVC3::VCL::createOp(), CVC3::TheoryArithOld::currentMaxCoefficient(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::TheoryDatatype::datatypeConsExpr(), CVC3::TheoryDatatype::datatypeSelExpr(), CVC3::TheoryDatatype::datatypeTestExpr(), CVC3::TheoryArithNew::deriveGomoryCut(), CVC3::TheoryArithOld::VarOrderGraph::dfs(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::BitvectorTheoremProducer::distributive_rule(), CVC3::TheoryArith3::doSolve(), CVC3::ArithTheoremProducerOld::elimPower(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducerOld::elimPowerConst(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::BitvectorTheoremProducer::eqConst(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::VCCmd::evaluateCommand(), CVC3::ArithTheoremProducerOld::evenPowerEqNegConst(), CVC3::ArithTheoremProducer3::evenPowerEqNegConst(), CVC3::ArithTheoremProducer::evenPowerEqNegConst(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), 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::TheoryArithOld::extractTermsFromInequality(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::TheoryArithNew::findCoefficient(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), findPolarityAtomic(), CVC3::TheoryArithNew::findRationalBound(), CVC3::TheoryArith3::findRationalBound(), CVC3::TheoryArithOld::findRationalBound(), CVC3::SearchEngineFast::findSplitter(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::BitvectorTheoremProducer::flattenBVPlus(), CVC3::BitvectorTheoremProducer::flipBVMult(), CVC3::ArithTheoremProducerOld::flipInequality(), CVC3::ArithTheoremProducer3::flipInequality(), CVC3::ArithTheoremProducer::flipInequality(), CVC3::TheoryArith3::freeConstIneq(), 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::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryArith3::getFactors(), CVC3::TheoryArithOld::getFactors(), CVC3::TheoryRecords::getField(), CVC3::TheoryRecords::getFieldIndex(), CVC3::TheoryRecords::getFields(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithNew::getLowerBoundThm(), CVC3::Theory::getModelTerm(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::Expr::getRational(), CVC3::TheoryDatatype::getSelectorInfo(), CVC3::Expr::getString(), getSubTrig(), CVC3::TheoryBitvector::getSXIndex(), CVC3::Expr::getTheorem(), CVC3::Expr::getTriggers(), CVC3::TheoryBitvector::getTypePredExpr(), CVC3::TheoryBitvector::getTypePredType(), CVC3::Expr::getUid(), CVC3::TheoryArithOld::getUpperBound(), CVC3::TheoryArithNew::getUpperBoundThm(), CVC3::TheoryArithOld::DifferenceLogicGraph::getValuation(), CVC3::SearchSat::getValue(), CVC3::Expr::getVars(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::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::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CoreTheoremProducer::ImpToIte(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryArithOld::isBounded(), CVC3::TheoryArithOld::isConstrained(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::TheoryArithOld::isNonlinearEq(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::BitvectorTheoremProducer::iteBVnegRule(), CVC3::BitvectorTheoremProducer::iteExtractRule(), CVC3::SearchEngineTheoremProducer::iteToClauses(), CVC3::BitvectorTheoremProducer::leftShiftToConcat(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::TheoryArithNew::lessThanVar(), CVC3::TheoryArith3::lessThanVar(), CVC3::TheoryArithOld::lessThanVar(), CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVC3::BitvectorTheoremProducer::lhsMinusRhsRule(), CVC3::BitvectorTheoremProducer::liftConcatBVMult(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::CommonTheoremProducer::liftOneITE(), CVC3::ArrayTheoremProducer::liftReadIte(), CVC3::BitvectorTheoremProducer::MarkNonSolvableEq(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::ArithTheoremProducerOld::multIneqn(), CVC3::ArithTheoremProducer3::multIneqn(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::BitvectorTheoremProducer::negBVand(), CVC3::BitvectorTheoremProducer::negBVor(), CVC3::BitvectorTheoremProducer::negBVxnor(), CVC3::BitvectorTheoremProducer::negBVxor(), CVC3::BitvectorTheoremProducer::negConcat(), CVC3::BitvectorTheoremProducer::negConst(), CVC3::BitvectorTheoremProducer::negElim(), 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::newBVPlusExpr(), CVC3::TheoryBitvector::newBVSDivExpr(), CVC3::TheoryBitvector::newBVSLEExpr(), CVC3::TheoryBitvector::newBVSLTExpr(), CVC3::TheoryBitvector::newBVSModExpr(), CVC3::TheoryBitvector::newBVSRemExpr(), CVC3::TheoryBitvector::newBVSubExpr(), CVC3::TheoryBitvector::newBVUDivExpr(), CVC3::TheoryBitvector::newBVUminusExpr(), CVC3::TheoryBitvector::newBVURemExpr(), CVC3::TheoryBitvector::newBVXnorExpr(), CVC3::TheoryBitvector::newBVXorExpr(), CVC3::TheoryBitvector::newConcatExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::SearchImplBase::newIntAssumption(), CVC3::TheoremProducer::newPf(), CVC3::Theory::newSubtypeExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::BitvectorTheoremProducer::notBVEQ1Rule(), CVC3::BitvectorTheoremProducer::notBVLTRule(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::BitvectorTheoremProducer::oneCoeffBVMult(), CVC3::ArithTheoremProducer3::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::CoreTheoremProducer::OrToIte(), 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::TheorySimulate::parseExprOp(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryUF::parseExprOp(), CVC3::TheoryArray::parseExprOp(), CVC3::TheoryDatatype::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryCore::parseExprOp(), CVC3::TheoryQuant::parseExprOp(), CVC3::QuantTheoremProducer::partialUniversalInst(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArith3::pickMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArithNew::pivot(), CVC3::TheoryArithNew::pivotAndUpdate(), CVC3::TheoryArithNew::pivotRule(), CVC3::ArithTheoremProducer3::powEqZero(), CVC3::ArithTheoremProducerOld::powEqZero(), CVC3::ArithTheoremProducer::powEqZero(), CVC3::ArithTheoremProducerOld::powerOfOne(), CVC3::Translator::preprocess(), CVC3::Translator::preprocess2(), CVC3::Translator::preprocess2Rec(), CVC3::TheoryArithOld::print(), CVC3::TheoryCore::print(), CVC3::TheoryCore::printSmtLibShared(), CVC3::TheoryArith3::processBuffer(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryCore::processCond(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processIntEq(), CVC3::TheoryArith3::processIntEq(), CVC3::TheoryArithOld::processIntEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::propagateTheory(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::ExprTransform::pushNegation1(), CVC3::ExprTransform::pushNegationRec(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArrayTheoremProducer::readArrayLiteral(), CVC3::ExprManager::rebuildRec(), CVC3::TheoryQuant::recGoodSemMatch(), CVC3::TheoryQuant::recMultMatch(), CVC3::TheoryQuant::recMultMatchDebug(), CVC3::TheoryQuant::recMultMatchOldWay(), CVC3::TheoryQuant::recursiveMap(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryCore::refineCounterExample(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArithNew::registerAtom(), CVC3::UFTheoremProducer::relToClosure(), CVC3::UFTheoremProducer::relTrans(), CVC3::BitvectorTheoremProducer::repeatRule(), CVC3::SearchSimple::restartInternal(), CVC3::SearchEngineFast::restartInternal(), CVC3::TheoryRecords::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryCore::rewriteCore(), CVC3::CoreTheoremProducer::rewriteIteBool(), CVC3::CoreTheoremProducer::rewriteIteCond(), CVC3::CoreTheoremProducer::rewriteIteElse(), CVC3::CommonTheoremProducer::rewriteIteFalse(), CVC3::CommonTheoremProducer::rewriteIteSame(), CVC3::CoreTheoremProducer::rewriteIteThen(), CVC3::CoreTheoremProducer::rewriteIteToAnd(), CVC3::CoreTheoremProducer::rewriteIteToIff(), CVC3::CoreTheoremProducer::rewriteIteToImp(), CVC3::CoreTheoremProducer::rewriteIteToNot(), CVC3::CoreTheoremProducer::rewriteIteToOr(), CVC3::CommonTheoremProducer::rewriteIteTrue(), CVC3::CoreTheoremProducer::rewriteLetDecl(), CVC3::TheoryCore::rewriteLitCore(), 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::BitvectorTheoremProducer::rotlRule(), CVC3::BitvectorTheoremProducer::rotrRule(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryCore::setFindLiteral(), CVC3::Expr::setMultiTrigger(), CVC3::Expr::setRep(), CVC3::Expr::setSig(), CVC3::Expr::setTrigger(), CVC3::Expr::setTriggers(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::setupTriggers(), CVC3::VariableValue::setValue(), CVC3::BitvectorTheoremProducer::signBVLTRule(), CVC3::BitvectorTheoremProducer::signExtendRule(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::simplifyOp(), CVC3::CommonTheoremProducer::skolemizeRewrite(), CVC3::CommonTheoremProducer::skolemizeRewriteVar(), CVC3::TheoryArray::solve(), CVC3::BitvectorTheoremProducer::solveExtractOverlap(), CVC3::SearchEngineFast::split(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::TheoryArithNew::substAndCanonize(), CVC3::TheoryArith3::substAndCanonize(), CVC3::TheoryArithOld::substAndCanonize(), CVC3::TheoryArithNew::substAndCanonizeModTableaux(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::CommonTheoremProducer::symmetryRule(), CVC3::TheoryQuant::synCheckSat(), CVC3::TheoremValue::toString(), CVC3::CommonTheoremProducer::transitivityRule(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate(), CVC3::BitvectorTheoremProducer::typePredBit(), CVC3::SearchEngineFast::unitPropagation(), CVC3::QuantTheoremProducer::universalInst(), CVC3::TheoryArray::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryBitvector::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::updateDependencies(), CVC3::TheoryArithNew::updateDependenciesAdd(), CVC3::TheoryArithNew::updateDependenciesRemove(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArithOld::updateSubsumptionDB(), usefulInMatch(), CVC3::CommonTheoremProducer::varIntroSkolem(), CVC3::TheoryArithOld::DifferenceLogicGraph::writeGraph(), CVC3::BitvectorTheoremProducer::zeroBVOR(), CVC3::BitvectorTheoremProducer::zeroCoeffBVMult(), CVC3::BitvectorTheoremProducer::zeroExtendRule(), CVC3::BitvectorTheoremProducer::zeroLeq(), and CVC3::BitvectorTheoremProducer::zeroPaddingRule().
string CVC3::Expr::toString | ( | InputLanguage | lang) | const |
Print the expression to a string using the given output language.
Definition at line 352 of file expr.cpp.
References CVC3::ExprStream::lang(), and CVC3::ExprStream::os().
void CVC3::Expr::print | ( | InputLanguage | lang, |
bool | dagify = true |
||
) | const |
Print the expression in the specified format.
Definition at line 362 of file expr.cpp.
References CVC3::ExprStream::dagFlag(), std::endl(), and CVC3::ExprStream::lang().
Referenced by ajr_debug_print(), CVC3::PrettyPrinterCore::print(), CVC3::TheoryUF::print(), CVC3::TheoryArithNew::print(), CVC3::TheoryArith3::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryCore::print(), CVC3::TheoryQuant::print(), CVC3::TheoryCore::printSmtLibShared(), and CVC3::Theorem::printx().
|
inline |
Print the expression as AST (lisp-like format)
Definition at line 640 of file expr.h.
References CVC3::AST_LANG, and CVC3::Expr::print().
Referenced by CVC3::Expr::print().
void CVC3::Expr::printnodag | ( | ) | const |
Print the expression as AST without dagifying.
Definition at line 394 of file expr.cpp.
References CVC3::AST_LANG.
Referenced by CVC3::Theorem::printxnodag().
void CVC3::Expr::pprint | ( | ) | const |
Pretty-print the expression.
Definition at line 373 of file expr.cpp.
References std::endl().
Referenced by CVC3::Theorem::pprintx().
void CVC3::Expr::pprintnodag | ( | ) | const |
Pretty-print without dagifying.
Definition at line 383 of file expr.cpp.
References CVC3::ExprStream::dagFlag(), and std::endl().
Referenced by CVC3::Theorem::pprintxnodag().
ExprStream & CVC3::Expr::print | ( | ExprStream & | os) | const |
Print a leaf node.
Definition at line 458 of file expr.cpp.
References BOUND_VAR, std::endl(), EXISTS, FALSE_EXPR, FORALL, NULL_KIND, CVC3::pop(), CVC3::push(), RATIONAL_EXPR, RAW_LIST, CVC3::ExprStream::resetIndent(), RESTART, SKOLEM_VAR, CVC3::space(), STRING_EXPR, TRUE_EXPR, and UCONST.
ExprStream & CVC3::Expr::printAST | ( | ExprStream & | os) | const |
Print the top node and then recurse through the children */.
Definition at line 400 of file expr.cpp.
References BOUND_VAR, DebugAssert, std::endl(), LETDECL, CVC3::nodag(), CVC3::pop(), CVC3::push(), RATIONAL_EXPR, CVC3::ExprStream::resetIndent(), SKOLEM_VAR, CVC3::space(), STRING_EXPR, THEOREM_KIND, and UCONST.
Referenced by CVC3::operator<<(), CVC3::TheorySimulate::print(), CVC3::TheoryRecords::print(), CVC3::TheoryUF::print(), CVC3::TheoryArray::print(), CVC3::TheoryDatatype::print(), CVC3::TheoryArithNew::print(), CVC3::TheoryBitvector::print(), CVC3::Theory::print(), CVC3::TheoryArith3::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryCore::print(), CVC3::TheoryBitvector::printSmtLibShared(), and CVC3::TheoryCore::printSmtLibShared().
Expr & CVC3::Expr::indent | ( | int | n, |
bool | permanent = false |
||
) |
Set initial indentation to n.
The indentation will be reset to default unless the second argument is true.
The indentation will be reset to default unless the second argument is true. This setting only takes effect when printing to std::ostream. When printing to ExprStream, the indentation can be set directly in the ExprStream.
Definition at line 510 of file expr.cpp.
References DebugAssert.
|
inline |
Set the find attribute to e.
Definition at line 1405 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::d_find, DebugAssert, CVC3::ExprManager::getCurrentContext(), CVC3::Expr::getEM(), CVC3::Theorem::getLHS(), IF_DEBUG, and CVC3::Expr::isNull().
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::Theory::find(), CVC3::Theory::findRef(), CVC3::TheoryCore::setFindLiteral(), CVC3::TheoryArithNew::setupRec(), CVC3::TheoryArith3::setupRec(), CVC3::TheoryArithOld::setupRec(), and CVC3::TheoryCore::setupTerm().
|
inline |
Set the eqNext attribute to e.
Definition at line 1416 of file expr.h.
References CVC3::ExprValue::d_eqNext, CVC3::Expr::d_expr, DebugAssert, CVC3::ExprManager::getCurrentContext(), CVC3::Expr::getEM(), CVC3::Theorem::getLHS(), IF_DEBUG, and CVC3::Expr::isNull().
Referenced by CVC3::TheoryCore::assertEqualities(), CVC3::TheoryArithNew::setupRec(), CVC3::TheoryArith3::setupRec(), CVC3::TheoryArithOld::setupRec(), and CVC3::TheoryCore::setupTerm().
Add (e,i) to the notify list of this expression.
Definition at line 517 of file expr.cpp.
References DebugAssert.
Referenced by CVC3::TheoryArray::addSharedTerm(), CVC3::TheoryDatatype::addSharedTerm(), CVC3::TheoryDatatype::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFormula(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryArray::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryBitvector::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::setup(), CVC3::Theory::setupCC(), CVC3::TheoryCore::setupSubFormulas(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), CVC3::TheoryArithOld::update(), CVC3::TheoryCore::update(), and CVC3::Theory::updateCC().
|
inline |
Set the cached type.
Definition at line 1427 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::TheorySimulate::computeType(), CVC3::TheoryRecords::computeType(), CVC3::TheoryUF::computeType(), CVC3::TheoryArray::computeType(), CVC3::TheoryDatatype::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryCore::computeType(), CVC3::TheoryQuant::computeType(), CVC3::TheoryDatatype::dataType(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ExprManager::ExprManager(), CVC3::Theory::getBaseType(), CVC3::ExprManager::newBoundVarExpr(), and CVC3::QuantTheoremProducer::normalizeQuant().
|
inline |
Definition at line 1432 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().
|
inline |
Definition at line 1438 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.
Referenced by CVC3::TypeComputerCore::checkType().
|
inline |
Definition at line 1443 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.
|
inline |
Definition at line 1450 of file expr.h.
References CVC3::CDFlags::clear(), CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), CVC3::CDFlags::set(), CVC3::Expr::TERMINALS_CONST, and CVC3::Expr::VALID_TERMINALS_CONST.
Referenced by CVC3::TheoryArith::leavesAreNumConst().
|
inline |
Definition at line 1457 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 TRACE.
Referenced by CVC3::TheoryUF::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryCore::rewrite(), CVC3::TheoryBitvector::rewriteBV(), and CVC3::TheoryCore::rewriteCore().
|
inline |
Definition at line 1543 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().
|
inline |
Definition at line 1463 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().
Referenced by CVC3::TheoryDatatype::dataType().
|
inline |
Definition at line 1468 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().
|
inline |
Definition at line 1473 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().
|
inline |
Definition at line 1478 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().
|
inline |
Definition at line 1483 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), CVC3::CDFlags::set(), and CVC3::Expr::USES_CC.
Referenced by CVC3::TheoryArray::setup(), and CVC3::Theory::setupCC().
|
inline |
Definition at line 1488 of file expr.h.
References CVC3::ExprValue::d_dynamicFlags, CVC3::Expr::d_expr, DebugAssert, CVC3::Expr::isNull(), CVC3::Expr::NOT_ARRAY_NORMALIZED, and CVC3::CDFlags::set().
Referenced by CVC3::TheoryArray::setup(), and CVC3::TheoryArray::update().
|
inline |
Definition at line 1493 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().
|
inline |
Definition at line 1498 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().
|
inline |
Definition at line 1503 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().
|
inline |
Definition at line 1508 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().
|
inline |
Definition at line 1513 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().
|
inline |
Set the translated flag for this Expr.
Definition at line 1518 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().
|
inline |
Set the UserRegisteredAtom flag for this Expr.
Definition at line 1523 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().
|
inline |
Set the RegisteredAtom flag for this Expr.
Definition at line 1528 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().
|
inline |
Set the Selected flag for this Expr.
Definition at line 1533 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(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryDatatype::setup(), and CVC3::TheoryDatatype::update().
|
inline |
Set the Stored Predicate flag for this Expr.
Definition at line 1538 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 |
Check if the current Expr (*this) is a subexpression of e.
Definition at line 169 of file expr.cpp.
References CVC3::subExprRec().
Referenced by CVC3::TheoryQuant::setupTriggers().
|
inline |
Definition at line 1030 of file expr.h.
References CVC3::Expr::clearFlags(), CVC3::Expr::d_expr, CVC3::ExprValue::d_size, and CVC3::ExprValue::getSize().
Referenced by CVC3::ExprTransform::newPP(), and CVC3::TheoryArithOld::rewrite().
|
inline |
Definition at line 1548 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::getSig(), and CVC3::Expr::isNull().
Referenced by CVC3::TheoryQuant::debug(), CVC3::TheoryQuant::newTopMatch(), and CVC3::TheoryQuant::newTopMatchSig().
|
inline |
Definition at line 1554 of file expr.h.
References CVC3::Expr::d_expr, CVC3::ExprValue::getRep(), and CVC3::Expr::isNull().
Referenced by CVC3::TheoryArray::checkSat(), and CVC3::TheoryQuant::debug().
|
inline |
Definition at line 1560 of file expr.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getSig(), and CVC3::Expr::isNull().
Referenced by CVC3::TheoryUF::checkSat(), CVC3::TheoryArray::checkSat(), CVC3::TheoryQuant::debug(), CVC3::TheoryQuant::matchListNew(), CVC3::TheoryQuant::matchListOld(), CVC3::TheoryQuant::multMatchChild(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and CVC3::Theory::updateCC().
|
inline |
Definition at line 1569 of file expr.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprValue::getRep(), and CVC3::Expr::isNull().
Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryQuant::debug(), CVC3::TheoryArray::rewrite(), CVC3::Theory::rewriteCC(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and CVC3::Theory::updateCC().
|
inline |
Definition at line 1578 of file expr.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprManager::getCurrentContext(), CVC3::Expr::getEM(), CVC3::ExprValue::getSig(), IF_DEBUG, CVC3::Expr::isNull(), CVC3::CDO< T >::set(), CVC3::ExprValue::setSig(), and CVC3::Expr::toString().
Referenced by CVC3::TheoryArray::setup(), CVC3::Theory::setupCC(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and CVC3::Theory::updateCC().
|
inline |
Definition at line 1589 of file expr.h.
References CVC3::Expr::d_expr, DebugAssert, CVC3::ExprManager::getCurrentContext(), CVC3::Expr::getEM(), CVC3::ExprValue::getRep(), IF_DEBUG, CVC3::Expr::isNull(), CVC3::CDO< T >::set(), CVC3::ExprValue::setRep(), and CVC3::Expr::toString().
Referenced by CVC3::TheoryArray::setup(), CVC3::Theory::setupCC(), CVC3::TheoryDatatypeLazy::update(), CVC3::TheoryUF::update(), CVC3::TheoryArray::update(), CVC3::TheoryDatatype::update(), and CVC3::Theory::updateCC().
|
staticprivate |
Convenient null expr.
Definition at line 191 of file expr.h.
Referenced by CVC3::Expr::getType(), and CVC3::Expr::lookupType().
|
private |
The value. This is the only data member in this class.
Definition at line 197 of file expr.h.
Referenced by CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::Expr::clearRewriteNormal(), CVC3::compare(), CVC3::ExprClosure::computeSize(), CVC3::Expr::computeTransClosure(), CVC3::Expr::containsBoundVar(), CVC3::Expr::end(), CVC3::Expr::Expr(), CVC3::Expr::getBody(), CVC3::Expr::getBoundIndex(), CVC3::Expr::getEM(), CVC3::Expr::getEqNext(), 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::getSize(), CVC3::Expr::getString(), CVC3::Expr::getTerminalsConstFlag(), CVC3::Expr::getTheorem(), CVC3::Expr::getTriggers(), CVC3::Expr::getType(), CVC3::Expr::getUid(), CVC3::Expr::getVars(), 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::notArrayNormalized(), CVC3::Expr::operator=(), CVC3::operator==(), CVC3::Expr::operator[](), CVC3::ExprManager::rebuildRec(), CVC3::Expr::setComputeTransClosure(), CVC3::Expr::setContainsBoundVar(), CVC3::Expr::setEqNext(), 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::setNotArrayNormalized(), CVC3::Expr::setRegisteredAtom(), CVC3::Expr::setRep(), CVC3::Expr::setRewriteNormal(), CVC3::Expr::setSelected(), CVC3::Expr::setSig(), CVC3::Expr::setSimpCache(), CVC3::Expr::setStoredPredicate(), CVC3::Expr::setTerminalsConstFlag(), CVC3::Expr::setTranslated(), CVC3::Expr::setTriggers(), CVC3::Expr::setType(), CVC3::Expr::setUserAssumption(), CVC3::Expr::setUserRegisteredAtom(), CVC3::Expr::setUsesCC(), CVC3::Expr::setValidType(), CVC3::Expr::setWellFounded(), CVC3::Theorem::Theorem(), CVC3::Expr::usesCC(), CVC3::Expr::validIsAtomicFlag(), CVC3::Expr::validSimpCache(), CVC3::Expr::validTerminalsConstFlag(), and CVC3::Expr::~Expr().
Definition at line 597 of file expr.cpp.
Referenced by CVC3::operator<(), CVC3::operator<=(), CVC3::operator>(), and CVC3::operator>=().