CVC3
Classes | Typedefs | Enumerations | Functions | Variables

CVC3 Namespace Reference

Classes

Typedefs

Enumerations

Functions

Variables


Typedef Documentation

typedef std::pair<std::string,std::string> CVC3::StrPair

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.

typedef std::map<Theorem,bool, TheoremLess> CVC3::TheoremMap

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 35 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::TheoryUF::print(), and CVC3::TheoryCore::print().

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

Definition at line 46 of file cvc_util.h.

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

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::recordExpr(), and CVC3::VCL::recordType().

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.

References CVC3::Exception::toString().

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

Definition at line 945 of file expr.h.

References AND, and DebugAssert.

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

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.

References CVC3::Proof::getExpr().

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

Definition at line 61 of file proof.h.

References CVC3::Proof::getExpr().

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.

References CVC3::StatFlag::d_flag.

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

Definition at line 69 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 72 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 122 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 125 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 128 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 131 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 134 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 137 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 140 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

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

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

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::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CompleteInstPreProcessor::isGoodQuant(), isIneq(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryArith3::isStale(), isSysPred(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::updateSubsumptionDB(), and CVC3::TheoryArith3::updateSubsumptionDB().

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::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CompleteInstPreProcessor::isGoodQuant(), isIneq(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), isSysPred(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::updateSubsumptionDB(), and CVC3::TheoryArith3::updateSubsumptionDB().

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 isGE(), isGT(), isLE(), and isLT().

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::TheoryArithOld::freeConstIneq(), CVC3::TheoryArith3::freeConstIneq(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), 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::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::TheoryArithNew::setup(), and CVC3::ArithTheoremProducerOld::simpleIneqInt().

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::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), operator+(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryArithOld::updateSubsumptionDB(), and CVC3::TheoryArith3::updateSubsumptionDB().

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 ARRAY_LITERAL, CVC3::Expr::getKind(), and CVC3::Expr::isClosure().

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.

References CVC3::Literal::getVar(), and CVC3::Literal::isNegative().

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 46 of file theorem.cpp.

References compare().

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

Definition at line 66 of file theorem.cpp.

References CVC3::Expr::isEq(), and CVC3::Expr::isIff().

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

Definition at line 84 of file theorem.cpp.

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