CVC3 Namespace Reference

Classes

Typedefs

Enumerations

Functions

Variables


Typedef Documentation

typedef long unsigned CVC3::ExprIndex

Expression index type.

Definition at line 87 of file expr.h.

typedef enum CVC3::FormulaValue CVC3::FormulaValue

typedef enum CVC3::QueryResult CVC3::QueryResult

typedef unsigned long CVC3::Unsigned

Definition at line 198 of file rational.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

enum CVC3::CLFlagType

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.

enum CVC3::ExprValueType

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 CVC3::Cardinality

Enum for cardinality of types.

Enumerator:
CARD_FINITE 
CARD_INFINITE 
CARD_UNKNOWN 

Definition at line 80 of file expr.h.

enum CVC3::FormulaValue

Enumerator:
TRUE_VAL 
FALSE_VAL 
UNKNOWN_VAL 

Definition at line 31 of file formula_value.h.

enum CVC3::Kind

Enumerator:
NULL_KIND 
TRUE_EXPR 
FALSE_EXPR 
RATIONAL_EXPR 
STRING_EXPR 
MAX_CONST 
RAW_LIST  May have any number of children >= 0
ID  Identifier is (ID (STRING_EXPR "name")).
BOOLEAN 
ANY_TYPE 
ARROW 
TYPE 
TYPEDECL 
TYPEDEF 
EQ 
NEQ 
DISTINCT 
NOT 
AND 
OR 
XOR 
IFF 
IMPLIES 
AND_R 
IFF_R 
ITE_R 
ITE 
FORALL 
EXISTS 
UFUNC 
APPLY 
ASSERT 
QUERY 
CHECKSAT 
CONTINUE 
RESTART 
DBG 
TRACE 
UNTRACE 
OPTION 
HELP 
TRANSFORM 
PRINT 
CALL 
ECHO 
INCLUDE 
DUMP_PROOF 
DUMP_ASSUMPTIONS 
DUMP_SIG 
DUMP_TCC 
DUMP_TCC_ASSUMPTIONS 
DUMP_TCC_PROOF 
DUMP_CLOSURE 
DUMP_CLOSURE_PROOF 
WHERE 
ASSERTIONS 
ASSUMPTIONS 
COUNTEREXAMPLE 
COUNTERMODEL 
PUSH 
POP 
POPTO 
PUSH_SCOPE 
POP_SCOPE 
POPTO_SCOPE 
RESET 
CONTEXT 
FORGET 
GET_TYPE 
CHECK_TYPE 
GET_CHILD 
SUBSTITUTE 
SEQ 
ARITH_VAR_ORDER 
TCC 
VARDECL 
VARDECLS 
BOUND_VAR 
BOUND_ID 
SUBTYPE 
IF 
IFTHEN 
ELSE 
COND 
LET 
LETDECLS 
LETDECL 
LAMBDA 
SIMULATE 
CONST 
VARLIST 
UCONST 
DEFUN 
PF_APPLY 
PF_HOLE 
SKOLEM_VAR 
THEOREM_KIND 
LAST_KIND  Must always be the last kind.

Definition at line 29 of file kinds.h.

enum CVC3::InputLanguage

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 
TPTP_LANG  for output in TPTP format

Definition at line 30 of file lang.h.

enum CVC3::QueryResult

Enumerator:
SATISFIABLE 
INVALID 
VALID 
UNSATISFIABLE 
ABORT 
UNKNOWN 

Definition at line 32 of file queryresult.h.

enum CVC3::ArithKinds

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.

enum CVC3::ArrayKinds

Enumerator:
ARRAY 
READ 
WRITE 
ARRAY_LITERAL 

Definition at line 30 of file theory_array.h.

enum CVC3::BVKinds

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.

enum CVC3::DatatypeKinds

Local kinds for datatypes.

Enumerator:
DATATYPE_DECL 
DATATYPE 
CONSTRUCTOR 
SELECTOR 
TESTER 

Definition at line 33 of file theory_datatype.h.

enum CVC3::Polarity

Enumerator:
Ukn 
Pos 
Neg 
PosNeg 

Definition at line 48 of file theory_quant.h.

enum CVC3::RecordKinds

Enumerator:
RECORD 
RECORD_SELECT 
RECORD_UPDATE 
RECORD_TYPE 
TUPLE 
TUPLE_SELECT 
TUPLE_UPDATE 
TUPLE_TYPE 

Definition at line 29 of file theory_records.h.

enum CVC3::UFKinds

Local kinds for transitive closure of binary relations.

Enumerator:
TRANS_CLOSURE 
OLD_ARROW 

Definition at line 31 of file theory_uf.h.

enum CVC3::ArithLang

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

Enumerator:
NOT_USED 
TERMS_ONLY 
DIFF_ONLY 
LINEAR 
NONLINEAR 

Definition at line 49 of file translator.h.


Function Documentation

static bool CVC3::subExprRec ( const Expr &  e1,
const Expr &  e2 
) [static]

Definition at line 132 of file expr.cpp.

References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::getFlag(), and CVC3::Expr::setFlag().

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

int CVC3::compare ( const Expr &  e1,
const Expr &  e2 
)

Definition at line 556 of file expr.cpp.

References CVC3::Expr::d_expr, CVC3::Expr::getIndex(), and CVC3::Expr::isConstant().

Referenced by CVC3::Assumptions::add(), CVC3::Assumptions::Assumptions(), compare(), CVC3::Assumptions::find(), CVC3::TheoryArithNew::findCoefficient(), CVC3::Assumptions::findTheorem(), operator<(), operator<=(), operator>(), operator>=(), and CVC3::TheoryArithNew::substAndCanonizeTableaux().

ostream& CVC3::operator<< ( std::ostream &  os,
const Expr &  e 
)

Definition at line 580 of file expr.cpp.

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

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().

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 942 of file expr.h.

References AND, DebugAssert, and CVC3::Expr::Expr().

Referenced by CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andIntro(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), 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::CompleteInstPreProcessor::pullVarOut(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::TheoryArithNew::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::CoreTheoremProducer::rewriteNotOr(), and CVC3::BitvectorTheoremProducer::zeroBVOR().

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

Definition at line 952 of file expr.h.

References DebugAssert, CVC3::Expr::Expr(), and OR.

Referenced by CVC3::BitvectorTheoremProducer::bitblastBVMult(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::BitvectorTheoremProducer::computeCarry(), CVC3::BitvectorTheoremProducer::computeCarryPreComputed(), CVC3::TheoryCore::computeTCC(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::ArithTheoremProducerOld::divideEqnNonConst(), CVC3::ArithTheoremProducer3::divideEqnNonConst(), CVC3::ArithTheoremProducer::divideEqnNonConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::Expr::operator||(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::CommonTheoremProducer::rewriteOr(), and CVC3::ArithTheoremProducerOld::splitGrayShadowSmall().

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

Definition at line 1597 of file expr.h.

References CVC3::Expr::d_expr.

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

Definition at line 1602 of file expr.h.

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

Definition at line 1607 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1609 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1611 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1613 of file expr.h.

References CVC3::Expr::compare.

InputLanguage CVC3::getLanguage ( const std::string &  lang  )  [inline]

Definition at line 47 of file lang.h.

References AST_LANG, LISP_LANG, PRESENTATION_LANG, SIMPLIFY_LANG, SMTLIB_LANG, and TPTP_LANG.

Referenced by CVC3::ExprManager::getInputLang(), and CVC3::ExprManager::getOutputLang().

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]

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

Definition at line 153 of file rational.h.

References DebugAssert, FatalAssert, CVC3::Rational::isInteger(), and CVC3::Rational::toString().

Referenced by CVC3::BitvectorTheoremProducer::buildPlusTerm(), CVC3::BitvectorTheoremProducer::canonBVEQ(), CVC3::BitvectorTheoremProducer::canonBVMult(), CVC3::BitvectorTheoremProducer::canonBVUMinus(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::BitvectorTheoremProducer::chopConcat(), CVC3::TheoryArith3::doSolve(), CVC3::ArithTheoremProducerOld::elimPowerConst(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::TheoryBitvector::finiteTypeInfo(), CVC3::BitvectorTheoremProducer::getPlusTerms(), CVC3::BitvectorTheoremProducer::isolate_var(), CVC3::BitvectorTheoremProducer::liftConcatBVPlus(), CVC3::TheoryBitvector::multiplicative_inverse(), CVC3::BitvectorTheoremProducer::negElim(), CVC3::BitvectorTheoremProducer::oneBVAND(), powExpr(), CVC3::Translator::preprocessRec(), CVC3::VCL::ratExpr(), and CVC3::TheoryBitvector::rewriteBV().

Rational CVC3::ratRoot ( const Rational &  base,
unsigned long int  n 
) [inline]

take nth root of base, return result if it is exact, 0 otherwise

Definition at line 166 of file rational.h.

References DebugAssert, CVC3::Rational::getDenominator(), and CVC3::Rational::getNumerator().

Referenced by CVC3::TheoryArith3::doSolve(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), and CVC3::TheoryArithOld::rewrite().

Rational CVC3::newRational ( int  n,
int  d = 1 
) [inline]

Definition at line 183 of file rational.h.

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

Definition at line 184 of file rational.h.

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

Definition at line 186 of file rational.h.

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

Definition at line 188 of file rational.h.

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

Definition at line 190 of file rational.h.

void CVC3::printRational ( const Rational &  x  ) 

bool CVC3::operator< ( const SearchSat::LitPriorityPair &  p1,
const SearchSat::LitPriorityPair &  p2 
) [inline]

Definition at line 311 of file search_sat.h.

References CVC3::SearchSat::LitPriorityPair::d_lit, CVC3::SearchSat::LitPriorityPair::d_priority, and SAT::Lit::getID().

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]

Definition at line 172 of file theory_arith.h.

References CVC3::Type::getExpr(), CVC3::Expr::getKind(), and REAL.

Referenced by CVC3::TheoryArithOld::addPairToArithOrder(), CVC3::TheorySimulate::computeType(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArithOld::isIntegerThm(), CVC3::TheoryArithNew::isIntegerThm(), CVC3::TheoryArith3::isIntegerThm(), CVC3::Translator::printArrayExpr(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::Translator::processType(), CVC3::TheoryArithOld::refineCounterExample(), CVC3::TheoryArithNew::refineCounterExample(), and CVC3::TheoryArith3::refineCounterExample().

bool CVC3::isInt ( Type  t  )  [inline]

Definition at line 173 of file theory_arith.h.

References CVC3::Type::getExpr(), CVC3::Expr::getKind(), and INT.

Referenced by CVC3::CompleteInstPreProcessor::addIndex(), CVC3::TheoryArithOld::addPairToArithOrder(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryArith3::doSolve(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArithOld::isIntegerThm(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithOld::print(), CVC3::TheoryArithNew::print(), CVC3::TheoryArith3::print(), CVC3::Translator::printArrayExpr(), CVC3::Translator::processType(), and CVC3::TheoryArith3::projectInequalities().

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

Definition at line 176 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(), 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(), 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]

Definition at line 177 of file theory_arith.h.

References CVC3::Expr::getRational(), CVC3::Rational::isInteger(), and CVC3::Expr::isRational().

Referenced by CVC3::TheoryArithOld::checkType(), CVC3::TheoryArithNew::checkType(), CVC3::TheoryArith3::checkType(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::ArithTheoremProducer3::evenPowerEqNegConst(), CVC3::ArithTheoremProducer::evenPowerEqNegConst(), CVC3::TheoryArithOld::getFactors(), CVC3::TheoryArith3::getFactors(), CVC3::ArithTheoremProducer3::intEqIrrational(), and CVC3::ArithTheoremProducer::intEqIrrational().

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

Definition at line 179 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 180 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::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::updateSubsumptionDB(), and CVC3::TheoryArith3::updateSubsumptionDB().

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

Definition at line 181 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 182 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::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(), and CVC3::TheoryArithOld::termDegree().

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

Definition at line 183 of file theory_arith.h.

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

Referenced by canGetHead(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::TheoryQuant::getHeadExpr(), and CVC3::TheoryArith::isSyntacticRational().

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

Definition at line 184 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::addToBuffer(), canGetHead(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::ArithTheoremProducer3::evenPowerEqNegConst(), CVC3::ArithTheoremProducer::evenPowerEqNegConst(), CVC3::TheoryQuant::getHeadExpr(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::TheoryArithOld::isNonlinearSumTerm(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::ArithTheoremProducerOld::multEqZero(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::ArithTheoremProducerOld::powEqZero(), CVC3::ArithTheoremProducer3::powEqZero(), CVC3::ArithTheoremProducer::powEqZero(), CVC3::ArithTheoremProducerOld::powerOfOne(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), and CVC3::TheoryArithOld::termDegree().

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

Definition at line 185 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 186 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]

Definition at line 187 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducerOld::flipInequality(), CVC3::ArithTheoremProducer3::flipInequality(), CVC3::ArithTheoremProducer::flipInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), isIneq(), isSysPred(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::rewrite(), and CVC3::TheoryArith3::rewrite().

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

Definition at line 188 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducerOld::flipInequality(), CVC3::ArithTheoremProducer3::flipInequality(), CVC3::ArithTheoremProducer::flipInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), isIneq(), isSysPred(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::rewrite(), and CVC3::TheoryArith3::rewrite().

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

Definition at line 189 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), and CVC3::TheoryArith3::setup().

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

Definition at line 190 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::TheoryArith3::setup(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), and CVC3::ArithTheoremProducerOld::splitGrayShadowSmall().

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

Definition at line 191 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(), and CVC3::TheoryArith3::update().

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

Definition at line 193 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]

Definition at line 196 of file theory_arith.h.

References UMINUS.

Referenced by operator-(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), and CVC3::TheoryArith3::parseExprOp().

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

Definition at line 198 of file theory_arith.h.

References MiniSat::left(), PLUS, and MiniSat::right().

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::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 200 of file theory_arith.h.

References DebugAssert, and PLUS.

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

Definition at line 204 of file theory_arith.h.

References MiniSat::left(), MINUS, and MiniSat::right().

Referenced by CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), operator-(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), and CVC3::TheoryArith3::parseExprOp().

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

Definition at line 206 of file theory_arith.h.

References MiniSat::left(), MULT, and MiniSat::right().

Referenced by CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducer3::monomialMulF(), CVC3::ArithTheoremProducer::monomialMulF(), operator *(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::ArithTheoremProducerOld::simplifiedMultExpr(), CVC3::ArithTheoremProducer3::simplifiedMultExpr(), and CVC3::ArithTheoremProducer::simplifiedMultExpr().

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

a Mult expr with two or more children

Definition at line 210 of file theory_arith.h.

References DebugAssert, and MULT.

Expr CVC3::powExpr ( const Expr &  pow,
const Expr &  base 
) [inline]

Power (x^n, or base^{pow}) expressions.

Definition at line 215 of file theory_arith.h.

References pow(), and POW.

Referenced by CVC3::ArithTheoremProducerOld::canonInvertLeaf(), CVC3::ArithTheoremProducer3::canonInvertLeaf(), CVC3::ArithTheoremProducer::canonInvertLeaf(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer3::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducerOld::canonMultLeafLeaf(), CVC3::ArithTheoremProducer3::canonMultLeafLeaf(), CVC3::ArithTheoremProducer::canonMultLeafLeaf(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducerOld::canonMultPowLeaf(), CVC3::ArithTheoremProducer3::canonMultPowLeaf(), CVC3::ArithTheoremProducer::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowPow(), CVC3::ArithTheoremProducer3::canonMultPowPow(), CVC3::ArithTheoremProducer::canonMultPowPow(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), and CVC3::VCL::powExpr().

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

Definition at line 218 of file theory_arith.h.

References DIVIDE, MiniSat::left(), and MiniSat::right().

Referenced by CVC3::VCL::divideExpr(), operator/(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), and CVC3::TheoryArith3::parseExprOp().

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

Definition at line 220 of file theory_arith.h.

References MiniSat::left(), LT, and MiniSat::right().

Referenced by CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::VCL::ltExpr(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), and CVC3::TheoryArith3::parseExprOp().

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

Definition at line 222 of file theory_arith.h.

References LE, MiniSat::left(), and MiniSat::right().

Referenced by CVC3::TheoryBitvector::bitBlastTerm(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryArithNew::computeTypePred(), CVC3::TheoryArith3::computeTypePred(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::VCL::leExpr(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArithOld::updateSubsumptionDB(), and CVC3::TheoryArith3::updateSubsumptionDB().

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

Definition at line 224 of file theory_arith.h.

References GT, MiniSat::left(), and MiniSat::right().

Referenced by CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::VCL::gtExpr(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), and CVC3::TheoryArith3::parseExprOp().

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

Definition at line 226 of file theory_arith.h.

References GE, MiniSat::left(), and MiniSat::right().

Referenced by CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::VCL::geExpr(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), and CVC3::TheoryArithNew::rewrite().

Expr CVC3::operator- ( const Expr &  child  )  [inline]

Definition at line 229 of file theory_arith.h.

References uminusExpr().

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

Definition at line 231 of file theory_arith.h.

References MiniSat::left(), plusExpr(), and MiniSat::right().

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

Definition at line 233 of file theory_arith.h.

References MiniSat::left(), minusExpr(), and MiniSat::right().

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

Definition at line 235 of file theory_arith.h.

References MiniSat::left(), multExpr(), and MiniSat::right().

Referenced by Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::const_iterator::operator->(), Hash::hash_table< _Key, _Value, _HashFcn, _EqualKey, _ExtractKey >::iterator::operator->(), and CVC3::Expr::iterator< std::input_iterator_tag, Expr, ptrdiff_t >::operator->().

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

Definition at line 237 of file theory_arith.h.

References divideExpr(), MiniSat::left(), and MiniSat::right().

bool CVC3::isArray ( const Type &  t  )  [inline]

Definition at line 109 of file theory_array.h.

References ARRAY, CVC3::Type::getExpr(), and CVC3::Expr::getKind().

Referenced by CVC3::ArrayTheoremProducer::arrayNotEq(), CVC3::TheoryArray::assertFact(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArray::computeType(), CVC3::Translator::printArrayExpr(), CVC3::Translator::processType(), and CVC3::TheoryArray::rewrite().

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

Definition at line 110 of file theory_array.h.

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

Referenced by CVC3::TheoryArray::addSharedTerm(), CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArray::computeModelTerm(), CVC3::TheoryArray::rewrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::TheoryArray::setup(), and CVC3::TheoryArray::update().

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

Definition at line 111 of file theory_array.h.

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

Referenced by CVC3::TheoryArray::addSharedTerm(), CVC3::TheoryArray::assertFact(), CVC3::TheoryArray::checkSat(), CVC3::ArrayTheoremProducer::interchangeIndices(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArray::rewrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite(), CVC3::ArrayTheoremProducer::rewriteReadWrite2(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite1(), CVC3::ArrayTheoremProducer::rewriteRedundantWrite2(), CVC3::ArrayTheoremProducer::rewriteSameStore(), CVC3::ArrayTheoremProducer::rewriteWriteWrite(), CVC3::TheoryArray::setup(), CVC3::TheoryArray::solve(), and CVC3::TheoryArray::update().

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]

Definition at line 116 of file theory_array.h.

References ARRAY, and CVC3::Type::getExpr().

Referenced by CVC3::VCL::arrayType(), CVC3::TheoryArray::computeType(), and CVC3::Translator::finish().

Expr CVC3::arrayLiteral ( const Expr ind,
const Expr body 
)

Definition at line 1181 of file theory_array.cpp.

References ARRAY_LITERAL, CVC3::Expr::getEM(), and CVC3::ExprManager::newClosureExpr().

Referenced by CVC3::TheoryArray::computeModel(), and CVC3::TheoryArray::finiteTypeInfo().

ostream & CVC3::operator<< ( std::ostream &  os,
const NotifyList l 
)

Printing NotifyList class.

Definition at line 97 of file theory_core.cpp.

References CVC3::NotifyList::getExpr(), CVC3::Theory::getName(), CVC3::NotifyList::getTheory(), and CVC3::NotifyList::size().

bool CVC3::isDatatype ( const Type &  t  )  [inline]

Definition at line 133 of file theory_datatype.h.

References DATATYPE, CVC3::Type::getExpr(), and CVC3::Expr::getKind().

Referenced by CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryDatatype::getReachablePredicate(), and CVC3::DatatypeTheoremProducer::noCycle().

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

Definition at line 136 of file theory_datatype.h.

References CVC3::Type::arity(), CONSTRUCTOR, CVC3::Expr::getKind(), CVC3::Expr::getOpKind(), CVC3::Expr::getType(), and CVC3::Expr::isApply().

Referenced by CVC3::TheoryDatatype::canCollapse(), CVC3::DatatypeTheoremProducer::decompose(), getConstructor(), CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::TheoryDatatypeLazy::instantiate(), CVC3::TheoryDatatype::instantiate(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::TheoryDatatype::rewrite(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryDatatype::solve(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().

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

Definition at line 140 of file theory_datatype.h.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), and SELECTOR.

Referenced by CVC3::TheoryDatatype::canCollapse(), CVC3::TheoryDatatype::checkSat(), CVC3::TheoryDatatype::rewrite(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), CVC3::TheoryDatatypeLazy::setup(), CVC3::TheoryDatatype::setup(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().

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

Definition at line 143 of file theory_datatype.h.

References CVC3::Expr::getOpKind(), CVC3::Expr::isApply(), and TESTER.

Referenced by CVC3::TheoryDatatype::rewrite(), CVC3::DatatypeTheoremProducer::rewriteTestCons(), CVC3::TheoryDatatypeLazy::update(), and CVC3::TheoryDatatype::update().

Expr CVC3::getConstructor ( const Expr &  e  )  [inline]

Definition at line 146 of file theory_datatype.h.

References DebugAssert, CVC3::Expr::getOpExpr(), CVC3::Expr::isApply(), and isConstructor().

Referenced by CVC3::TheoryDatatypeLazy::initializeLabels(), CVC3::TheoryDatatype::initializeLabels(), CVC3::DatatypeTheoremProducer::rewriteSelCons(), and CVC3::DatatypeTheoremProducer::rewriteTestCons().

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

Definition at line 168 of file type.h.

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

Definition at line 171 of file type.h.

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

Definition at line 175 of file type.h.

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 
)

Definition at line 217 of file variable.cpp.

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

ostream& CVC3::operator<< ( std::ostream &  os,
const Clause &  c 
)

Definition at line 135 of file clause.cpp.

References CVC3::Clause::deleted(), CVC3::Clause::dir(), CVC3::Clause::getTheorem(), CVC3::Clause::id(), CVC3::Clause::IF_DEBUG(), CVC3::Clause::isNull(), CVC3::Clause::sat(), CVC3::Clause::size(), and CVC3::Clause::wp().

static void CVC3::printLit ( ostream &  os,
const Literal &  l 
) [static]

Definition at line 157 of file clause.cpp.

References CVC3::Variable::getExpr(), CVC3::Literal::getScope(), CVC3::Literal::getValue(), CVC3::Literal::getVar(), and CVC3::Literal::isNegative().

Referenced by operator<<().

ostream& CVC3::operator<< ( std::ostream &  os,
const CompactClause &  c 
)

Definition at line 164 of file clause.cpp.

References CVC3::CompactClause::d_clause, CVC3::Clause::deleted(), CVC3::Clause::getLiterals(), CVC3::Clause::owners(), printLit(), CVC3::Clause::size(), and CVC3::Clause::wp().

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 
)

Definition at line 337 of file variable.cpp.

References CVC3::VariableValue::getAntecedent(), CVC3::VariableValue::getAntecedentIdx(), CVC3::VariableValue::getExpr(), CVC3::VariableValue::getScope(), CVC3::VariableValue::getTheorem(), CVC3::VariableValue::getValue(), CVC3::Clause::isNull(), and CVC3::Theorem::isNull().

Assumptions CVC3::operator- ( const Assumptions a,
const Expr e 
)

Definition at line 301 of file assumptions.cpp.

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

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

Definition at line 311 of file assumptions.cpp.

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

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 compare(), CVC3::Theorem::d_thm, CVC3::Theorem::getExpr(), CVC3::Theorem::isNull(), and CVC3::Theorem::isRewrite().

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

Definition at line 65 of file theorem.cpp.

References compare(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), and CVC3::Theorem::isRewrite().

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 
)

Definition at line 44 of file theory_arith3.cpp.

References CVC3::TheoryArith3::FreeConst::getConst(), and CVC3::TheoryArith3::FreeConst::strict().

ostream& CVC3::operator<< ( std::ostream &  os,
const TheoryArith3::Ineq ineq 
)

Definition at line 54 of file theory_arith3.cpp.

References CVC3::TheoryArith3::Ineq::getConst(), CVC3::Theorem::getExpr(), CVC3::TheoryArith3::Ineq::ineq(), and CVC3::TheoryArith3::Ineq::varOnRHS().

ostream& CVC3::operator<< ( std::ostream &  os,
const TheoryArithNew::FreeConst fc 
)

Definition at line 44 of file theory_arith_new.cpp.

References CVC3::TheoryArithNew::FreeConst::getConst(), and CVC3::TheoryArithNew::FreeConst::strict().

ostream& CVC3::operator<< ( std::ostream &  os,
const TheoryArithNew::Ineq ineq 
)

Definition at line 54 of file theory_arith_new.cpp.

References CVC3::TheoryArithNew::Ineq::getConst(), CVC3::Theorem::getExpr(), CVC3::TheoryArithNew::Ineq::ineq(), and CVC3::TheoryArithNew::Ineq::varOnRHS().

ostream& CVC3::operator<< ( std::ostream &  os,
const TheoryArithOld::FreeConst fc 
)

Definition at line 46 of file theory_arith_old.cpp.

References CVC3::TheoryArithOld::FreeConst::getConst(), and CVC3::TheoryArithOld::FreeConst::strict().

ostream& CVC3::operator<< ( std::ostream &  os,
const TheoryArithOld::Ineq ineq 
)

Definition at line 56 of file theory_arith_old.cpp.

References CVC3::TheoryArithOld::Ineq::getConst(), CVC3::Theorem::getExpr(), CVC3::TheoryArithOld::Ineq::ineq(), and CVC3::TheoryArithOld::Ineq::varOnRHS().


Variable Documentation

const unsigned CVC3::chunkSizeBytes = 16384

Definition at line 30 of file memory_manager_context.h.

Referenced by CVC3::ContextMemoryManager::ContextMemoryManager(), CVC3::ContextMemoryManager::getMemory(), CVC3::ContextMemoryManager::getStaticMemory(), and CVC3::ContextMemoryManager::newChunk().

ParserTemp* CVC3::parserTemp


Generated on Wed Nov 18 16:14:22 2009 for CVC3 by  doxygen 1.5.2