CVC3 2.2
|
Different types of command line flags.
More...Type ID of each ExprValue subclass.
More...Enum for cardinality of types.
More...Different input languages.
More...Local kinds for datatypes.
More...Local kinds for transitive closure of binary relations.
More...Used to keep track of which subset of arith is being used.
More...typedef std::pair<std::string,std::string> CVC3::StrPair |
Definition at line 78 of file cvc_util.h.
typedef long unsigned CVC3::ExprIndex |
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 |
typedef struct CVC3::dynTrig CVC3::dynTrig |
enum CVC3::CLFlagType |
Different types of command line flags.
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.
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
enum CVC3::Cardinality |
enum CVC3::FormulaValue |
Definition at line 31 of file formula_value.h.
enum CVC3::Kind |
enum CVC3::InputLanguage |
enum CVC3::QueryResult |
Definition at line 32 of file queryresult.h.
enum CVC3::ArithKinds |
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 |
Definition at line 30 of file theory_array.h.
enum CVC3::BVKinds |
Definition at line 32 of file theory_bitvector.h.
enum CVC3::DatatypeKinds |
Local kinds for datatypes.
Definition at line 33 of file theory_datatype.h.
enum CVC3::Polarity |
Definition at line 48 of file theory_quant.h.
enum CVC3::RecordKinds |
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.
Definition at line 31 of file theory_uf.h.
enum CVC3::ArithLang |
Used to keep track of which subset of arith is being used.
Definition at line 49 of file translator.h.
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(), CVC3::ExprStream::os(), 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().
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::TheoryArithOld::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().
T CVC3::abs | ( | T | t | ) |
Definition at line 53 of file cvc_util.h.
Referenced by CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), SAT::Lit::isTrue(), operator<(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), and CVC3::TheoryArith3::pickIntEqMonomial().
T CVC3::max | ( | T | a, |
T | b | ||
) |
Definition at line 56 of file cvc_util.h.
Referenced by CVC3::TheoryArithOld::fixCurrentMaxCoefficient(), CVC3::TheoryArith3::fixCurrentMaxCoefficient(), SAT::Clause::getMaxVar(), and MiniSat::malloc_clause().
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().
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 942 of file expr.h.
References AND, and DebugAssert.
Referenced by CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andIntro(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), 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(), and CVC3::BitvectorTheoremProducer::zeroBVOR().
Expr CVC3::orExpr | ( | const std::vector< Expr > & | children | ) | [inline] |
Definition at line 952 of file expr.h.
References DebugAssert, 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(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), and CVC3::VCL::tryModelGeneration().
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] |
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(), 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 abs(), 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] |
bool CVC3::operator<= | ( | const Theorem & | t1, |
const Theorem & | t2 | ||
) | [inline] |
bool CVC3::operator> | ( | const Theorem & | t1, |
const Theorem & | t2 | ||
) | [inline] |
bool CVC3::operator>= | ( | const Theorem & | t1, |
const Theorem & | t2 | ||
) | [inline] |
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 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 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 MINUS.
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 MULT.
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.
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.
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 LT.
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.
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.
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.
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 plusExpr().
Expr CVC3::operator- | ( | const Expr & | left, |
const Expr & | right | ||
) | [inline] |
Definition at line 233 of file theory_arith.h.
References minusExpr().
Expr CVC3::operator* | ( | const Expr & | left, |
const Expr & | right | ||
) | [inline] |
Definition at line 235 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 237 of file theory_arith.h.
References divideExpr().
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().
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::dataType(), 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 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 | ||
) |
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(), 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::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 | ||
) |
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().
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().