CVC3  2.4.1
Classes | Typedefs | Enumerations | Functions | Variables
CVC3 Namespace Reference

Classes

Typedefs

Enumerations

Functions

Variables


Typedef Documentation

Definition at line 78 of file cvc_util.h.

typedef long unsigned CVC3::ExprIndex

Expression index type.

Definition at line 87 of file expr.h.

Definition at line 402 of file theorem.h.

typedef struct CVC3::dynTrig CVC3::dynTrig

Enumeration Type Documentation

Different types of command line flags.

Enumerator:
CLFLAG_NULL 
CLFLAG_BOOL 
CLFLAG_INT 
CLFLAG_STRING 
CLFLAG_STRVEC 

Vector of pair<string, bool>

Definition at line 34 of file command_line_flags.h.

Type ID of each ExprValue subclass.

It is defined in expr.h, so that ExprManager can use it before loading expr_value.h

Enumerator:
EXPR_VALUE 
EXPR_NODE 
EXPR_APPLY 

Application of functions and predicates.

EXPR_STRING 
EXPR_RATIONAL 
EXPR_SKOLEM 
EXPR_UCONST 
EXPR_SYMBOL 
EXPR_BOUND_VAR 
EXPR_CLOSURE 
EXPR_VALUE_TYPE_LAST 

Definition at line 65 of file expr.h.

Enum for cardinality of types.

Enumerator:
CARD_FINITE 
CARD_INFINITE 
CARD_UNKNOWN 

Definition at line 80 of file expr.h.

Enumerator:
TRUE_VAL 
FALSE_VAL 
UNKNOWN_VAL 

Definition at line 31 of file formula_value.h.

Different input languages.

Enumerator:
PRESENTATION_LANG 

Nice SAL-like language for manually written specs.

SMTLIB_LANG 

SMT-LIB format.

LISP_LANG 

Lisp-like format for automatically generated specs.

AST_LANG 
SIMPLIFY_LANG 

for output into Simplify format

TPTP_LANG 

for output in TPTP format

SPASS_LANG 

for output in SPASS format

SMTLIB_V2_LANG 

SMT-LIB v2 format.

Definition at line 30 of file lang.h.

Enumerator:
SATISFIABLE 
INVALID 
VALID 
UNSATISFIABLE 
ABORT 
UNKNOWN 

Definition at line 32 of file queryresult.h.

Enumerator:
REAL_CONST 
NEGINF 
POSINF 
REAL 
INT 
SUBRANGE 
UMINUS 
PLUS 
MINUS 
MULT 
DIVIDE 
POW 
INTDIV 
MOD 
LT 
LE 
GT 
GE 
IS_INTEGER 
DARK_SHADOW 
GRAY_SHADOW 

Definition at line 31 of file theory_arith.h.

Enumerator:
ARRAY 
READ 
WRITE 
ARRAY_LITERAL 

Definition at line 30 of file theory_array.h.

Enumerator:
BVCONST 
BITVECTOR 
CONCAT 
EXTRACT 
BOOLEXTRACT 
LEFTSHIFT 
CONST_WIDTH_LEFTSHIFT 
RIGHTSHIFT 
BVSHL 
BVLSHR 
BVASHR 
SX 
BVREPEAT 
BVZEROEXTEND 
BVROTL 
BVROTR 
BVAND 
BVOR 
BVXOR 
BVXNOR 
BVNEG 
BVNAND 
BVNOR 
BVCOMP 
BVUMINUS 
BVPLUS 
BVSUB 
BVMULT 
BVUDIV 
BVSDIV 
BVUREM 
BVSREM 
BVSMOD 
BVLT 
BVLE 
BVGT 
BVGE 
BVSLT 
BVSLE 
BVSGT 
BVSGE 
INTTOBV 
BVTOINT 
BVTYPEPRED 

Definition at line 32 of file theory_bitvector.h.

Local kinds for datatypes.

Enumerator:
DATATYPE_DECL 
DATATYPE 
CONSTRUCTOR 
SELECTOR 
TESTER 

Definition at line 33 of file theory_datatype.h.

Enumerator:
Ukn 
Pos 
Neg 
PosNeg 

Definition at line 48 of file theory_quant.h.

Enumerator:
RECORD 
RECORD_SELECT 
RECORD_UPDATE 
RECORD_TYPE 
TUPLE 
TUPLE_SELECT 
TUPLE_UPDATE 
TUPLE_TYPE 

Definition at line 29 of file theory_records.h.

Local kinds for transitive closure of binary relations.

Enumerator:
TRANS_CLOSURE 
OLD_ARROW 

Definition at line 32 of file theory_uf.h.

Used to keep track of which subset of arith is being used.

Enumerator:
NOT_USED 
TERMS_ONLY 
DIFF_ONLY 
LINEAR 
NONLINEAR 

Definition at line 51 of file translator.h.


Function Documentation

static bool CVC3::subExprRec ( const Expr &  e1,
const Expr &  e2 
) [static]
int CVC3::compare ( const Expr &  e1,
const Expr &  e2 
)
ostream& CVC3::operator<< ( std::ostream os,
const Expr &  e 
)
static bool CVC3::isTrivialExpr ( const Expr &  e) [static]

Definition at line 49 of file expr_stream.cpp.

References CVC3::Expr::arity(), and CVC3::Expr::isClosure().

Referenced by CVC3::ExprStream::collectShared().

std::string CVC3::to_upper ( const std::string src) [inline]

Definition at line 30 of file cvc_util.h.

Referenced by CVC3::ExprStream::collectShared(), and CVC3::TheoryCore::print().

std::string CVC3::to_lower ( const std::string src) [inline]

Definition at line 38 of file cvc_util.h.

Referenced by CVC3::TheoryCore::print(), and CVC3::TheoryUF::print().

std::string CVC3::int2string ( int  n) [inline]

Definition at line 46 of file cvc_util.h.

Referenced by CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::zeroPaddingRule(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::extractWhole(), CVC3::BitvectorTheoremProducer::extractExtract(), CVC3::BitvectorTheoremProducer::extractConcat(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseConstElim(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::BitvectorTheoremProducer::pad(), CVC3::CDList< SmartCDO< Theorem > >::operator[](), CVC3::CDList< SmartCDO< Theorem > >::at(), CVC3::CDList< SmartCDO< Theorem > >::back(), CVC3::ClauseValue::~ClauseValue(), CVC3::Clause::~Clause(), CVC3::Clause::operator=(), CVC3::Clause::getLiteral(), CVC3::Clause::wp(), CVC3::Clause::dir(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::andElim(), CVC3::CommonTheoremProducer::implIntro(), CVC3::ContextObj::update(), CVC3::CoreTheoremProducer::OrToIte(), CVC3::CoreTheoremProducer::AndToIte(), CVC3::CoreTheoremProducer::rewriteAndSubterms(), CVC3::CoreTheoremProducer::rewriteOrSubterms(), CVC3::ExprManager::newKind(), CVC3::ExprManager::getKindName(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprStream::popIndent(), CVC3::ExprValue::ExprValue(), printUsage(), parse_args(), CVC3::QuantTheoremProducer::normalizeQuant(), CVC3::SearchEngineFast::split(), CVC3::SearchEngineFast::updateLitScores(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::bcp(), CVC3::SearchEngineFast::propagate(), CVC3::SearchEngineFast::unitPropagation(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::SearchEngineFast::traceConflict(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::SearchImplBase::findInCNFCache(), CVC3::SearchEngineTheoremProducer::unitProp(), CVC3::SearchEngineTheoremProducer::propIffr(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::Theorem::Theorem(), CVC3::Theorem::~Theorem(), CVC3::Theory::addSplitter(), CVC3::Theory::registerKinds(), CVC3::Theory::unregisterKinds(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArith3::pickMonomial(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::getEdgeTheorems(), CVC3::TheoryArithOld::DifferenceLogicGraph::analyseConflict(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::computeModel(), CVC3::TheoryBitvector::pad(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::TheoryBitvector::rewriteBV(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryBitvector::newBitvectorTypeExpr(), CVC3::TheoryBitvector::newSXExpr(), CVC3::TheoryBitvector::newBVIndexExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::TheoryBitvector::newFixedLeftShiftExpr(), CVC3::TheoryBitvector::newFixedConstWidthLeftShiftExpr(), CVC3::TheoryBitvector::newFixedRightShiftExpr(), CVC3::TheoryBitvector::newBVMultExpr(), CVC3::TheoryBitvector::newBVZeroString(), CVC3::TheoryBitvector::newBVOneString(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::newBVExtractExpr(), CVC3::TheoryBitvector::newBVPlusExpr(), CVC3::BVConstExpr::BVConstExpr(), CVC3::TheoryCore::simplify(), CVC3::TheoryCore::processCond(), CVC3::TheoryCore::computeType(), CVC3::TheoryCore::print(), CVC3::TheoryCore::enqueueFact(), CVC3::TheoryDatatype::dataType(), CVC3::TheoryQuant::TheoryQuant(), CVC3::TheoryQuant::setupTriggers(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoryRecords::setup(), CVC3::TheorySimulate::computeType(), CVC3::TheoryUF::computeModel(), CVC3::VariableValue::setValue(), and CVC3::VCCmd::evaluateCommand().

template<class T >
T CVC3::abs ( t)
template<class T >
T CVC3::max ( a,
b 
)
template<class T >
std::pair<std::string,T> CVC3::strPair ( const std::string f,
const T &  t 
)

Definition at line 74 of file cvc_util.h.

Referenced by sort2().

template<class T >
void CVC3::sort2 ( std::vector< std::string > &  keys,
std::vector< T > &  vals 
)

Sort two vectors based on the first vector.

Definition at line 82 of file cvc_util.h.

References DebugAssert, and strPair().

Referenced by CVC3::VCL::recordType(), and CVC3::VCL::recordExpr().

CVC_DLL void CVC3::fatalError ( const std::string file,
int  line,
const std::string cond,
const std::string msg 
)

Function for fatal exit.

It just exits with code 1, but is provided here for the debugger to set a breakpoint to. For this reason, it is not inlined.

Definition at line 35 of file debug.cpp.

References std::endl().

std::ostream& CVC3::operator<< ( std::ostream os,
const Exception &  e 
) [inline]

Definition at line 52 of file exception.h.

Expr CVC3::andExpr ( const std::vector< Expr > &  children) [inline]

Definition at line 945 of file expr.h.

References DebugAssert, and AND.

Referenced by CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducerOld::implyEqualities(), CVC3::ArrayTheoremProducer::splitOnConstants(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::zeroBVOR(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::CommonTheoremProducer::andIntro(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::Expr::operator&&(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::Theory::computeTCC(), CVC3::TheoryArith3::computeTypePred(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArithNew::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryArray::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryCore::computeTypePred(), recCompleteInster::build_tree(), CVC3::TheoryRecords::computeTypePred(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::computeModel(), CVC3::TheoryUF::computeTCC(), and CVC3::VCL::checkContinue().

Expr CVC3::orExpr ( const std::vector< Expr > &  children) [inline]
bool CVC3::operator== ( const Expr &  e1,
const Expr &  e2 
) [inline]

Definition at line 1600 of file expr.h.

References CVC3::Expr::d_expr.

bool CVC3::operator!= ( const Expr &  e1,
const Expr &  e2 
) [inline]

Definition at line 1605 of file expr.h.

bool CVC3::operator< ( const Expr &  e1,
const Expr &  e2 
) [inline]

Definition at line 1610 of file expr.h.

References CVC3::Expr::compare.

bool CVC3::operator<= ( const Expr &  e1,
const Expr &  e2 
) [inline]

Definition at line 1612 of file expr.h.

References CVC3::Expr::compare.

bool CVC3::operator> ( const Expr &  e1,
const Expr &  e2 
) [inline]

Definition at line 1614 of file expr.h.

References CVC3::Expr::compare.

bool CVC3::operator>= ( const Expr &  e1,
const Expr &  e2 
) [inline]

Definition at line 1616 of file expr.h.

References CVC3::Expr::compare.

bool CVC3::isPrefix ( const std::string prefix,
const std::string str 
) [inline]

Definition at line 56 of file lang.h.

Referenced by getLanguage().

InputLanguage CVC3::getLanguage ( const std::string lang) [inline]
std::ostream& CVC3::operator<< ( std::ostream os,
const Proof &  pf 
) [inline]

Definition at line 57 of file proof.h.

bool CVC3::operator== ( const Proof &  pf1,
const Proof &  pf2 
) [inline]

Definition at line 61 of file proof.h.

Rational CVC3::pow ( Rational  pow,
const Rational &  base 
) [inline]
Rational CVC3::ratRoot ( const Rational &  base,
unsigned long int  n 
) [inline]
Rational CVC3::newRational ( int  n,
int  d = 1 
) [inline]

Definition at line 189 of file rational.h.

Rational CVC3::newRational ( const char *  n,
int  base = 10 
) [inline]

Definition at line 190 of file rational.h.

Rational CVC3::newRational ( const std::string n,
int  base = 10 
) [inline]

Definition at line 192 of file rational.h.

Rational CVC3::newRational ( const char *  n,
const char *  d,
int  base = 10 
) [inline]

Definition at line 194 of file rational.h.

Rational CVC3::newRational ( const std::string n,
const std::string d,
int  base = 10 
) [inline]

Definition at line 196 of file rational.h.

void CVC3::printRational ( const Rational &  x)
Unsigned CVC3::pow ( Unsigned  pow,
const Unsigned &  base 
) [inline]

Raise 'base' into the power of 'pow' (pow must be an integer)

Definition at line 285 of file rational.h.

References pow().

Unsigned CVC3::newUnsigned ( int  n) [inline]

Definition at line 293 of file rational.h.

Unsigned CVC3::newUnsigned ( const char *  n,
int  base = 10 
) [inline]

Definition at line 294 of file rational.h.

Unsigned CVC3::newUnsigned ( const std::string n,
int  base = 10 
) [inline]

Definition at line 296 of file rational.h.

void CVC3::printUnsigned ( const Unsigned &  x)
bool CVC3::operator< ( const SearchSat::LitPriorityPair &  p1,
const SearchSat::LitPriorityPair &  p2 
) [inline]
bool CVC3::operator== ( const StatFlag &  f1,
const StatFlag &  f2 
) [inline]

Definition at line 66 of file statistics.h.

bool CVC3::operator!= ( const StatFlag &  f1,
const StatFlag &  f2 
) [inline]

Definition at line 69 of file statistics.h.

std::ostream& CVC3::operator<< ( std::ostream os,
const StatFlag &  f 
) [inline]

Definition at line 72 of file statistics.h.

bool CVC3::operator== ( const StatCounter &  c1,
const StatCounter &  c2 
) [inline]

Definition at line 122 of file statistics.h.

bool CVC3::operator!= ( const StatCounter &  c1,
const StatCounter &  c2 
) [inline]

Definition at line 125 of file statistics.h.

bool CVC3::operator== ( int  c1,
const StatCounter &  c2 
) [inline]

Definition at line 128 of file statistics.h.

bool CVC3::operator!= ( int  c1,
const StatCounter &  c2 
) [inline]

Definition at line 131 of file statistics.h.

bool CVC3::operator== ( const StatCounter &  c1,
int  c2 
) [inline]

Definition at line 134 of file statistics.h.

bool CVC3::operator!= ( const StatCounter &  c1,
int  c2 
) [inline]

Definition at line 137 of file statistics.h.

std::ostream& CVC3::operator<< ( std::ostream os,
const StatCounter &  c 
) [inline]

Definition at line 140 of file statistics.h.

bool CVC3::operator< ( const Theorem &  t1,
const Theorem &  t2 
) [inline]

Definition at line 427 of file theorem.h.

References compare().

bool CVC3::operator<= ( const Theorem &  t1,
const Theorem &  t2 
) [inline]

Definition at line 429 of file theorem.h.

References compare().

bool CVC3::operator> ( const Theorem &  t1,
const Theorem &  t2 
) [inline]

Definition at line 431 of file theorem.h.

References compare().

bool CVC3::operator>= ( const Theorem &  t1,
const Theorem &  t2 
) [inline]

Definition at line 433 of file theorem.h.

References compare().

bool CVC3::isReal ( Type  t) [inline]
bool CVC3::isInt ( Type  t) [inline]
bool CVC3::isRational ( const Expr &  e) [inline]

Definition at line 177 of file theory_arith.h.

References CVC3::Expr::isRational().

Referenced by CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducer::canonDivideVar(), CVC3::ArithTheoremProducer::canonMultConstMult(), CVC3::ArithTheoremProducer::canonInvertConst(), CVC3::ArithTheoremProducer::canonMultTermConst(), CVC3::ArithTheoremProducer::canonMultConstConst(), CVC3::ArithTheoremProducer::canonMultConstTerm(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducer::constPredicate(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducer3::canonDivideConst(), CVC3::ArithTheoremProducer3::canonDivideMult(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDivideVar(), CVC3::ArithTheoremProducer3::canonMultConstMult(), CVC3::ArithTheoremProducer3::canonInvertConst(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer3::canonMultTermConst(), CVC3::ArithTheoremProducer3::canonMultConstConst(), CVC3::ArithTheoremProducer3::canonMultConstTerm(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducer3::constPredicate(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDivideVar(), CVC3::ArithTheoremProducerOld::canonMultConstMult(), CVC3::ArithTheoremProducerOld::canonInvertConst(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::canonMultTermConst(), CVC3::ArithTheoremProducerOld::canonMultConstConst(), CVC3::ArithTheoremProducerOld::canonMultConstTerm(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::ArithTheoremProducerOld::powerOfOne(), LFSCConvert::cvc3_to_lfsc(), LFSCPrinter::print_poly_norm(), LFSCPrinter::print_terms_h(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::TheoryArith::rewriteToDiff(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArith3::canon(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArith3::addToBuffer(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArith3::lessThanVar(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArith3::findRationalBound(), CVC3::TheoryArith3::computeModel(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheoryArithNew::lessThanVar(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithNew::findRationalBound(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArithNew::findCoefficient(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArithOld::canon(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::lessThanVar(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithOld::findRationalBound(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithOld::print(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryBitvector::parseExprOp(), getLeft(), getRight(), CVC3::TheorySimulate::computeType(), CVC3::Translator::preprocessRec(), and CVC3::VCCmd::evaluateCommand().

bool CVC3::isIntegerConst ( const Expr &  e) [inline]
bool CVC3::isUMinus ( const Expr &  e) [inline]

Definition at line 180 of file theory_arith.h.

References CVC3::Expr::getKind(), and UMINUS.

Referenced by CVC3::TheoryArith::isSyntacticRational().

bool CVC3::isPlus ( const Expr &  e) [inline]

Definition at line 181 of file theory_arith.h.

References CVC3::Expr::getKind(), and PLUS.

Referenced by CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducer::substitute(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::processBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArith3::pickMonomial(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArithNew::findCoefficient(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::getUpperBound(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), CVC3::TheoryArithOld::isUnconstrained(), CVC3::TheoryArithOld::updateConstrained(), canGetHead(), and CVC3::TheoryQuant::getHeadExpr().

bool CVC3::isMinus ( const Expr &  e) [inline]

Definition at line 182 of file theory_arith.h.

References CVC3::Expr::getKind(), and MINUS.

Referenced by canGetHead(), and CVC3::TheoryQuant::getHeadExpr().

bool CVC3::isMult ( const Expr &  e) [inline]

Definition at line 183 of file theory_arith.h.

References CVC3::Expr::getKind(), and MULT.

Referenced by CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducer::monomialMulF(), CVC3::ArithTheoremProducer::substitute(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::ArithTheoremProducer3::canonDivideMult(), CVC3::ArithTheoremProducer3::canonMultMtermMterm(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducer3::monomialMulF(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer3::oneElimination(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithNew::findCoefficient(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithOld::isNonlinearSumTerm(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::termDegree(), CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::TheoryArithOld::getUpperBound(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), CVC3::TheoryArithOld::isUnconstrained(), CVC3::TheoryArithOld::updateConstrained(), canGetHead(), and CVC3::TheoryQuant::getHeadExpr().

bool CVC3::isDivide ( const Expr &  e) [inline]
bool CVC3::isPow ( const Expr &  e) [inline]
bool CVC3::isLT ( const Expr &  e) [inline]

Definition at line 186 of file theory_arith.h.

References CVC3::Expr::getKind(), and LT.

Referenced by CVC3::ArithTheoremProducer::negatedInequality(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), isIneq(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArith3::isStale(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::setup(), isSysPred(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().

bool CVC3::isLE ( const Expr &  e) [inline]

Definition at line 187 of file theory_arith.h.

References CVC3::Expr::getKind(), and LE.

Referenced by CVC3::ArithTheoremProducer::negatedInequality(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducerOld::addInequalities(), isIneq(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithOld::setup(), isSysPred(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::TheoryQuant::newTopMatchNoSig(), and CVC3::TheoryQuant::newTopMatchSig().

bool CVC3::isGT ( const Expr &  e) [inline]
bool CVC3::isGE ( const Expr &  e) [inline]
bool CVC3::isDarkShadow ( const Expr &  e) [inline]
bool CVC3::isGrayShadow ( const Expr &  e) [inline]
bool CVC3::isIneq ( const Expr &  e) [inline]

Definition at line 192 of file theory_arith.h.

References isLT(), isLE(), isGT(), and isGE().

Referenced by CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::TheoryArith3::freeConstIneq(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArith3::update(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArithNew::update(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithOld::freeConstIneq(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithOld::registerAtom(), and CVC3::TheoryArithOld::updateConstrained().

bool CVC3::isIntPred ( const Expr &  e) [inline]

Definition at line 194 of file theory_arith.h.

References CVC3::Expr::getKind(), and IS_INTEGER.

Referenced by CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithNew::setup(), and CVC3::TheoryArithOld::assertFact().

Expr CVC3::uminusExpr ( const Expr &  child) [inline]
Expr CVC3::plusExpr ( const Expr &  left,
const Expr &  right 
) [inline]

Definition at line 199 of file theory_arith.h.

References PLUS.

Referenced by CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducer::substitute(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), operator+(), CVC3::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::updateSubsumptionDB(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::TheoryArithOld::parseExprOp(), and CVC3::TheoryArithOld::tryPropagate().

Expr CVC3::plusExpr ( const std::vector< Expr > &  children) [inline]

Definition at line 201 of file theory_arith.h.

References DebugAssert, and PLUS.

Expr CVC3::minusExpr ( const Expr &  left,
const Expr &  right 
) [inline]
Expr CVC3::multExpr ( const Expr &  left,
const Expr &  right 
) [inline]
Expr CVC3::multExpr ( const std::vector< Expr > &  children) [inline]

a Mult expr with two or more children

Definition at line 211 of file theory_arith.h.

References DebugAssert, and MULT.

Expr CVC3::powExpr ( const Expr &  pow,
const Expr &  base 
) [inline]
Expr CVC3::divideExpr ( const Expr &  left,
const Expr &  right 
) [inline]
Expr CVC3::ltExpr ( const Expr &  left,
const Expr &  right 
) [inline]
Expr CVC3::leExpr ( const Expr &  left,
const Expr &  right 
) [inline]
Expr CVC3::gtExpr ( const Expr &  left,
const Expr &  right 
) [inline]
Expr CVC3::geExpr ( const Expr &  left,
const Expr &  right 
) [inline]
Expr CVC3::operator- ( const Expr &  child) [inline]

Definition at line 230 of file theory_arith.h.

References uminusExpr().

Expr CVC3::operator+ ( const Expr &  left,
const Expr &  right 
) [inline]

Definition at line 232 of file theory_arith.h.

References plusExpr().

Expr CVC3::operator- ( const Expr &  left,
const Expr &  right 
) [inline]

Definition at line 234 of file theory_arith.h.

References minusExpr().

Expr CVC3::operator* ( const Expr &  left,
const Expr &  right 
) [inline]

Definition at line 236 of file theory_arith.h.

References multExpr().

Referenced by CVC3::Expr::iterator::operator->().

Expr CVC3::operator/ ( const Expr &  left,
const Expr &  right 
) [inline]

Definition at line 238 of file theory_arith.h.

References divideExpr().

bool CVC3::isArray ( const Type &  t) [inline]
bool CVC3::isRead ( const Expr &  e) [inline]
bool CVC3::isWrite ( const Expr &  e) [inline]
bool CVC3::isArrayLiteral ( const Expr &  e) [inline]

Definition at line 112 of file theory_array.h.

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

Type CVC3::arrayType ( const Type &  type1,
const Type &  type2 
) [inline]
Expr CVC3::arrayLiteral ( const Expr ind,
const Expr body 
)
ostream & CVC3::operator<< ( std::ostream os,
const NotifyList l 
)
bool CVC3::isDatatype ( const Type &  t) [inline]
bool CVC3::isConstructor ( const Expr &  e) [inline]
bool CVC3::isSelector ( const Expr &  e) [inline]
bool CVC3::isTester ( const Expr &  e) [inline]
Expr CVC3::getConstructor ( const Expr &  e) [inline]
bool CVC3::operator== ( const Type &  t1,
const Type &  t2 
) [inline]

Definition at line 83 of file type.h.

References CVC3::Type::getExpr().

bool CVC3::operator!= ( const Type &  t1,
const Type &  t2 
) [inline]

Definition at line 86 of file type.h.

References CVC3::Type::getExpr().

std::ostream& CVC3::operator<< ( std::ostream os,
const Type &  t 
) [inline]

Definition at line 90 of file type.h.

References CVC3::Type::getExpr().

Literal CVC3::operator! ( const Variable &  v) [inline]

Definition at line 188 of file variable.h.

Literal CVC3::operator! ( const Literal &  l) [inline]

Definition at line 192 of file variable.h.

ostream & CVC3::operator<< ( std::ostream os,
const Literal &  l 
)
ostream& CVC3::operator<< ( std::ostream os,
const Clause &  c 
)
static void CVC3::printLit ( ostream os,
const Literal &  l 
) [static]
ostream& CVC3::operator<< ( std::ostream os,
const CompactClause &  c 
)
ostream& CVC3::operator<< ( std::ostream os,
const Variable &  l 
)

Definition at line 202 of file variable.cpp.

References CVC3::Variable::d_val.

ostream& CVC3::operator<< ( std::ostream os,
const VariableValue &  v 
)
Assumptions CVC3::operator- ( const Assumptions a,
const Expr e 
)

Definition at line 301 of file assumptions.cpp.

References CVC3::Assumptions::begin(), and CVC3::Assumptions::end().

Assumptions CVC3::operator- ( const Assumptions a,
const vector< Expr > &  es 
)

Definition at line 311 of file assumptions.cpp.

References CVC3::Assumptions::begin(), and CVC3::Assumptions::end().

ostream& CVC3::operator<< ( std::ostream os,
const Assumptions assump 
)

Definition at line 321 of file assumptions.cpp.

References CVC3::Assumptions::d_vector.

int CVC3::compare ( const Theorem &  t1,
const Theorem &  t2 
)

Compare Theorems by their expressions. Return -1, 0, or 1.

This is an arbitrary total ordering on Theorems. For simplicity, we define rewrite theorems (e1 = e2 or e1 <=> e2) to be smaller than other theorems.

Definition at line 45 of file theorem.cpp.

References CVC3::Theorem::d_thm, CVC3::Theorem::isNull(), CVC3::Theorem::isRewrite(), compare(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), and CVC3::Theorem::getRHS().

int CVC3::compare ( const Theorem &  t1,
const Expr &  e2 
)
int CVC3::compareByPtr ( const Theorem &  t1,
const Theorem &  t2 
)

Definition at line 83 of file theorem.cpp.

References CVC3::Theorem::d_thm.

Referenced by CVC3::TheoremLess::operator()().

ostream& CVC3::operator<< ( std::ostream os,
const TheoryArith3::FreeConst fc 
)
ostream& CVC3::operator<< ( std::ostream os,
const TheoryArith3::Ineq ineq 
)
ostream& CVC3::operator<< ( std::ostream os,
const TheoryArithNew::FreeConst fc 
)
ostream& CVC3::operator<< ( std::ostream os,
const TheoryArithNew::Ineq ineq 
)
ostream& CVC3::operator<< ( std::ostream os,
const TheoryArithOld::FreeConst fc 
)
ostream& CVC3::operator<< ( std::ostream os,
const TheoryArithOld::Ineq ineq 
)

Variable Documentation

const unsigned CVC3::chunkSizeBytes = 16384