CVC3
2.4.1
|
Classes | |
class | ArithException |
class | ArithProofRules |
class | ArithTheoremProducer |
class | ArithTheoremProducer3 |
class | ArithTheoremProducerOld |
class | ArrayProofRules |
class | ArrayTheoremProducer |
class | Assumptions |
class | BitvectorException |
class | BitvectorProofRules |
class | BitvectorTheoremProducer |
This class implements proof rules for bitvector normalizers (concatenation normal form, bvplus normal form), bitblaster rules, other relevant rewrite rules for bv arithmetic and word-level operators. More... | |
class | BVConstExpr |
An expression subclass for bitvector constants. More... | |
class | CDFlags |
class | CDList |
class | CDMap |
class | CDMapData |
class | CDMapOrdered |
class | CDMapOrderedData |
class | CDO |
class | CDOmap |
class | CDOmapOrdered |
class | Circuit |
class | Clause |
A class representing a CNF clause (a smart pointer) More... | |
class | ClauseOwner |
Same as class Clause, but when destroyed, marks the clause as deleted. More... | |
class | ClauseValue |
class | CLException |
class | CLFlag |
class | CLFlags |
class | CNF_Rules |
API to the CNF proof rules. More... | |
class | CNF_TheoremProducer |
class | CommonProofRules |
class | CommonTheoremProducer |
class | CompactClause |
class | CompleteInstPreProcessor |
class | Context |
class | ContextManager |
Manager for multiple contexts. Also holds current context. More... | |
class | ContextMemoryManager |
ContextMemoryManager. More... | |
class | ContextNotifyObj |
class | ContextObj |
class | ContextObjChain |
class | CoreProofRules |
class | CoreSatAPI_implBase |
class | CoreTheoremProducer |
class | DatatypeProofRules |
class | DatatypeTheoremProducer |
class | DebugException |
class | DecisionEngine |
class | DecisionEngineCaching |
class | DecisionEngineDFS |
Decision Engine for use with the Search EngineAuthor: Clark Barrett. More... | |
class | DecisionEngineMBTF |
struct | dynTrig |
class | EvalException |
class | Exception |
class | Expr |
Data structure of expressions in CVC3. More... | |
class | ExprApply |
class | ExprApplyTmp |
class | ExprBoundVar |
class | ExprClosure |
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers. More... | |
class | ExprHashMap |
class | ExprManager |
Expression Manager. More... | |
class | ExprManagerNotifyObj |
Notifies ExprManager before and after each pop() More... | |
class | ExprMap |
class | ExprNode |
class | ExprNodeTmp |
class | ExprRational |
class | ExprSkolem |
class | ExprStream |
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING! More... | |
class | ExprString |
class | ExprSymbol |
class | ExprTransform |
class | ExprValue |
The base class for holding the actual data in expressions. More... | |
class | ExprVar |
class | Literal |
struct | ltstr |
class | MemoryManager |
class | MemoryManagerChunks |
class | MemoryManagerMalloc |
class | MemoryTracker |
class | NotifyList |
class | Op |
class | Parser |
class | ParserException |
class | ParserTemp |
class | PrettyPrinter |
Abstract API to a pretty-printer for Expr. More... | |
class | PrettyPrinterCore |
Implementation of PrettyPrinter class. More... | |
class | Proof |
class | QuantProofRules |
class | QuantTheoremProducer |
class | Rational |
class | RecordsProofRules |
class | RecordsTheoremProducer |
class | RegTheoremValue |
class | ResetException |
class | RWTheoremValue |
class | Scope |
class | ScopeWatcher |
A class which sets a boolean value to true when created, and resets to false when deleted. More... | |
class | SearchEngine |
API to to a generic proof search engine. More... | |
class | SearchEngineFast |
Implementation of a faster search engine, using newer techniques. More... | |
class | SearchEngineRules |
API to the proof rules for the Search Engines. More... | |
class | SearchEngineTheoremProducer |
class | SearchImplBase |
API to to a generic proof search engine (a.k.a. SAT solver) More... | |
class | SearchSat |
Search engine that connects to a generic SAT reasoning module. More... | |
class | SearchSatCNFCallback |
class | SearchSatCoreSatAPI |
class | SearchSatDecider |
class | SearchSatTheoryAPI |
class | SearchSimple |
Implementation of the simple search engine. More... | |
class | SimulateProofRules |
class | SimulateTheoremProducer |
class | SmartCDO |
SmartCDO. More... | |
class | SmtlibException |
class | SoundException |
class | StatCounter |
class | StatFlag |
class | Statistics |
class | StrPairLess |
class | Theorem |
class | Theorem3 |
Theorem3. More... | |
class | TheoremLess |
"Less" comparator for theorems by TheoremValue pointers More... | |
class | TheoremManager |
class | TheoremProducer |
class | TheoremValue |
class | Theory |
Base class for theories. More... | |
class | TheoryArith |
This theory handles basic linear arithmetic. More... | |
class | TheoryArith3 |
class | TheoryArithNew |
class | TheoryArithOld |
class | TheoryArray |
This theory handles arrays. More... | |
class | TheoryBitvector |
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG) More... | |
class | TheoryCore |
This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories. More... | |
class | TheoryDatatype |
This theory handles datatypes. More... | |
class | TheoryDatatypeLazy |
This theory handles datatypes. More... | |
class | TheoryQuant |
This theory handles quantifiers. More... | |
class | TheoryRecords |
This theory handles records. More... | |
class | TheorySimulate |
"Theory" of symbolic simulation. More... | |
class | TheoryUF |
This theory handles uninterpreted functions. More... | |
class | Translator |
class | Trigger |
class | Type |
MS C++ specific settings. More... | |
class | TypecheckException |
class | TypeComputerCore |
class | UFProofRules |
class | UFTheoremProducer |
class | Unsigned |
class | ValidityChecker |
Generic API for a validity checker. More... | |
class | Variable |
class | VariableManager |
class | VariableManagerNotifyObj |
Notifies VariableManager before and after each pop() More... | |
class | VariableValue |
class | VCCmd |
class | VCL |
Typedefs | |
typedef std::pair< std::string, std::string > | StrPair |
typedef long unsigned | ExprIndex |
Expression index type. More... | |
typedef enum CVC3::FormulaValue | FormulaValue |
typedef enum CVC3::QueryResult | QueryResult |
typedef std::map< Theorem, bool, TheoremLess > | TheoremMap |
typedef struct CVC3::dynTrig | dynTrig |
Functions | |
static bool | subExprRec (const Expr &e1, const Expr &e2) |
int | compare (const Expr &e1, const Expr &e2) |
ostream & | operator<< (ostream &os, const Expr &e) |
static bool | isTrivialExpr (const Expr &e) |
ExprStream & | operator<< (ExprStream &os, ExprStream &(*manip)(ExprStream &)) |
Use manipulators which are functions over ExprStream&. More... | |
ExprStream & | operator<< (ExprStream &os, const Expr &e) |
Print Expr. More... | |
ExprStream & | operator<< (ExprStream &os, const Type &t) |
Print Type. More... | |
ExprStream & | operator<< (ExprStream &os, const string &s) |
Print string. More... | |
ExprStream & | operator<< (ExprStream &os, const char *s) |
Print char* string. More... | |
ExprStream & | operator<< (ExprStream &os, const Rational &r) |
Print Rational. More... | |
ExprStream & | operator<< (ExprStream &os, int i) |
Print int. More... | |
ExprStream & | push (ExprStream &os) |
Set the indentation to the current position. More... | |
ExprStream & | pop (ExprStream &os) |
Restore the indentation. More... | |
ExprStream & | popSave (ExprStream &os) |
Remember the current indentation and pop to the previous position. More... | |
ExprStream & | pushRestore (ExprStream &os) |
Set the indentation to the position saved by popSave() More... | |
ExprStream & | reset (ExprStream &os) |
Reset the indentation to the default at this level. More... | |
ExprStream & | space (ExprStream &os) |
Insert a single white space separator. More... | |
ExprStream & | nodag (ExprStream &os) |
ExprStream & | pushdag (ExprStream &os) |
ExprStream & | popdag (ExprStream &os) |
std::string | to_upper (const std::string &src) |
std::string | to_lower (const std::string &src) |
std::string | int2string (int n) |
template<class T > | |
T | abs (T t) |
template<class T > | |
T | max (T a, T b) |
template<class T > | |
std::pair< std::string, T > | strPair (const std::string &f, const T &t) |
template<class T > | |
void | sort2 (std::vector< std::string > &keys, std::vector< T > &vals) |
Sort two vectors based on the first vector. More... | |
CVC_DLL void | fatalError (const std::string &file, int line, const std::string &cond, const std::string &msg) |
Function for fatal exit. More... | |
std::ostream & | operator<< (std::ostream &os, const Exception &e) |
Expr | andExpr (const std::vector< Expr > &children) |
Expr | orExpr (const std::vector< Expr > &children) |
bool | operator== (const Expr &e1, const Expr &e2) |
bool | operator!= (const Expr &e1, const Expr &e2) |
bool | operator< (const Expr &e1, const Expr &e2) |
bool | operator<= (const Expr &e1, const Expr &e2) |
bool | operator> (const Expr &e1, const Expr &e2) |
bool | operator>= (const Expr &e1, const Expr &e2) |
bool | isPrefix (const std::string &prefix, const std::string &str) |
InputLanguage | getLanguage (const std::string &lang) |
std::ostream & | operator<< (std::ostream &os, const Proof &pf) |
bool | operator== (const Proof &pf1, const Proof &pf2) |
Rational | pow (Rational pow, const Rational &base) |
Raise 'base' into the power of 'pow' (pow must be an integer) More... | |
Rational | ratRoot (const Rational &base, unsigned long int n) |
take nth root of base, return result if it is exact, 0 otherwise More... | |
Rational | newRational (int n, int d=1) |
Rational | newRational (const char *n, int base=10) |
Rational | newRational (const std::string &n, int base=10) |
Rational | newRational (const char *n, const char *d, int base=10) |
Rational | newRational (const std::string &n, const std::string &d, int base=10) |
void | printRational (const Rational &x) |
Unsigned | pow (Unsigned pow, const Unsigned &base) |
Raise 'base' into the power of 'pow' (pow must be an integer) More... | |
Unsigned | newUnsigned (int n) |
Unsigned | newUnsigned (const char *n, int base=10) |
Unsigned | newUnsigned (const std::string &n, int base=10) |
void | printUnsigned (const Unsigned &x) |
bool | operator< (const SearchSat::LitPriorityPair &p1, const SearchSat::LitPriorityPair &p2) |
bool | operator== (const StatFlag &f1, const StatFlag &f2) |
bool | operator!= (const StatFlag &f1, const StatFlag &f2) |
std::ostream & | operator<< (std::ostream &os, const StatFlag &f) |
bool | operator== (const StatCounter &c1, const StatCounter &c2) |
bool | operator!= (const StatCounter &c1, const StatCounter &c2) |
bool | operator== (int c1, const StatCounter &c2) |
bool | operator!= (int c1, const StatCounter &c2) |
bool | operator== (const StatCounter &c1, int c2) |
bool | operator!= (const StatCounter &c1, int c2) |
std::ostream & | operator<< (std::ostream &os, const StatCounter &c) |
bool | operator< (const Theorem &t1, const Theorem &t2) |
bool | operator<= (const Theorem &t1, const Theorem &t2) |
bool | operator> (const Theorem &t1, const Theorem &t2) |
bool | operator>= (const Theorem &t1, const Theorem &t2) |
bool | isReal (Type t) |
bool | isInt (Type t) |
bool | isRational (const Expr &e) |
bool | isIntegerConst (const Expr &e) |
bool | isUMinus (const Expr &e) |
bool | isPlus (const Expr &e) |
bool | isMinus (const Expr &e) |
bool | isMult (const Expr &e) |
bool | isDivide (const Expr &e) |
bool | isPow (const Expr &e) |
bool | isLT (const Expr &e) |
bool | isLE (const Expr &e) |
bool | isGT (const Expr &e) |
bool | isGE (const Expr &e) |
bool | isDarkShadow (const Expr &e) |
bool | isGrayShadow (const Expr &e) |
bool | isIneq (const Expr &e) |
bool | isIntPred (const Expr &e) |
Expr | uminusExpr (const Expr &child) |
Expr | plusExpr (const Expr &left, const Expr &right) |
Expr | plusExpr (const std::vector< Expr > &children) |
Expr | minusExpr (const Expr &left, const Expr &right) |
Expr | multExpr (const Expr &left, const Expr &right) |
Expr | multExpr (const std::vector< Expr > &children) |
a Mult expr with two or more children More... | |
Expr | powExpr (const Expr &pow, const Expr &base) |
Power (x^n, or base^{pow}) expressions. More... | |
Expr | divideExpr (const Expr &left, const Expr &right) |
Expr | ltExpr (const Expr &left, const Expr &right) |
Expr | leExpr (const Expr &left, const Expr &right) |
Expr | gtExpr (const Expr &left, const Expr &right) |
Expr | geExpr (const Expr &left, const Expr &right) |
Expr | operator- (const Expr &child) |
Expr | operator+ (const Expr &left, const Expr &right) |
Expr | operator- (const Expr &left, const Expr &right) |
Expr | operator* (const Expr &left, const Expr &right) |
Expr | operator/ (const Expr &left, const Expr &right) |
bool | isArray (const Type &t) |
bool | isRead (const Expr &e) |
bool | isWrite (const Expr &e) |
bool | isArrayLiteral (const Expr &e) |
Type | arrayType (const Type &type1, const Type &type2) |
Expr | arrayLiteral (const Expr &ind, const Expr &body) |
std::ostream & | operator<< (std::ostream &os, const NotifyList &l) |
Printing NotifyList class. More... | |
bool | isDatatype (const Type &t) |
bool | isConstructor (const Expr &e) |
bool | isSelector (const Expr &e) |
bool | isTester (const Expr &e) |
Expr | getConstructor (const Expr &e) |
bool | operator== (const Type &t1, const Type &t2) |
bool | operator!= (const Type &t1, const Type &t2) |
std::ostream & | operator<< (std::ostream &os, const Type &t) |
Literal | operator! (const Variable &v) |
Literal | operator! (const Literal &l) |
std::ostream & | operator<< (std::ostream &os, const Literal &l) |
ostream & | operator<< (ostream &os, const Clause &c) |
static void | printLit (ostream &os, const Literal &l) |
ostream & | operator<< (std::ostream &os, const CompactClause &c) |
ostream & | operator<< (ostream &os, const Variable &l) |
ostream & | operator<< (ostream &os, const VariableValue &v) |
Assumptions | operator- (const Assumptions &a, const Expr &e) |
Assumptions | operator- (const Assumptions &a, const vector< Expr > &es) |
ostream & | operator<< (ostream &os, const Assumptions &assump) |
int | compare (const Theorem &t1, const Theorem &t2) |
Compare Theorems by their expressions. Return -1, 0, or 1. More... | |
int | compare (const Theorem &t1, const Expr &e2) |
int | compareByPtr (const Theorem &t1, const Theorem &t2) |
ostream & | operator<< (ostream &os, const TheoryArith3::FreeConst &fc) |
ostream & | operator<< (ostream &os, const TheoryArith3::Ineq &ineq) |
ostream & | operator<< (ostream &os, const TheoryArithNew::FreeConst &fc) |
ostream & | operator<< (ostream &os, const TheoryArithNew::Ineq &ineq) |
ostream & | operator<< (ostream &os, const TheoryArithOld::FreeConst &fc) |
ostream & | operator<< (ostream &os, const TheoryArithOld::Ineq &ineq) |
Variables | |
const unsigned | chunkSizeBytes = 16384 |
ParserTemp * | parserTemp |
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 std::map<Theorem,bool, TheoremLess> CVC3::TheoremMap |
typedef struct CVC3::dynTrig CVC3::dynTrig |
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 |
enum CVC3::Cardinality |
enum CVC3::FormulaValue |
Enumerator | |
---|---|
TRUE_VAL | |
FALSE_VAL | |
UNKNOWN_VAL |
Definition at line 31 of file formula_value.h.
enum CVC3::InputLanguage |
Different input languages.
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 |
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 32 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 51 of file translator.h.
|
static |
Definition at line 155 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 597 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 621 of file expr.cpp.
References CVC3::Expr::getEM(), CVC3::Expr::isNull(), CVC3::ExprStream::os(), and CVC3::ExprManager::restoreIndent().
|
static |
Definition at line 49 of file expr_stream.cpp.
References CVC3::Expr::arity(), and CVC3::Expr::isClosure().
Referenced by CVC3::ExprStream::collectShared().
|
inline |
Definition at line 30 of file cvc_util.h.
Referenced by CVC3::ExprStream::collectShared(), and CVC3::TheoryCore::print().
|
inline |
Definition at line 38 of file cvc_util.h.
Referenced by CVC3::TheoryUF::print(), and CVC3::TheoryCore::print().
|
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::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::at(), CVC3::CDList< CVC3::TheoryArith3::Ineq >::back(), CVC3::SearchEngineFast::bcp(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseConstElim(), CVC3::BVConstExpr::BVConstExpr(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::TheoryArray::checkSat(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheorySimulate::computeType(), CVC3::TheoryBitvector::computeType(), CVC3::TheoryCore::computeType(), CVC3::BitvectorTheoremProducer::concatMergeExtract(), CVC3::SearchEngineTheoremProducer::conflictRule(), CVC3::TheoryDatatype::dataType(), CVC3::Clause::dir(), CVC3::SearchImplBase::enqueueCNFrec(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::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(), IF_DEBUG(), CVC3::CNF_TheoremProducer::ifLiftRule(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::TheoryQuant::naiveCheckSat(), CVC3::TheoryBitvector::newBitvectorTypeExpr(), CVC3::TheoryBitvector::newBoolExtractExpr(), CVC3::ExprManager::newBoundVarExpr(), 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< CVC3::TheoryArith3::Ineq >::operator[](), CVC3::CoreTheoremProducer::OrToIte(), CVC3::TheoryBitvector::pad(), CVC3::BitvectorTheoremProducer::pad(), CVC3::BitvectorTheoremProducer::padBVLTRule(), CVC3::BitvectorTheoremProducer::padBVSLTRule(), parse_args(), CVC3::TheoryArith3::pickMonomial(), CVC3::TheoryArithOld::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::TheoryArithNew::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::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::TheoryArith3::updateSubsumptionDB(), CVC3::TheoryArithOld::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::TheoryArith3::computeNormalFactor(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::BitvectorTheoremProducer::constMultToPlus(), LFSCConvert::cvc3_to_lfsc(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), SAT::Lit::getVar(), SAT::Lit::isVar(), LFSCPfLet::LFSCPfLet(), LFSCProof::Make_CNF(), LFSCClausify::Make_i(), LFSCBoolRes::MakeC(), TReturn::normalize_to_tf(), TReturn::normalize_tr(), operator<(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickIntEqMonomial(), LFSCPrinter::print_LFSC(), print_mpq(), LFSCBoolRes::print_pf(), LFSCLem::print_pf(), LFSCClausify::print_pf(), LFSCAssume::print_pf(), and LFSCLraPoly::print_pf().
T CVC3::max | ( | T | a, |
T | b | ||
) |
Definition at line 56 of file cvc_util.h.
Referenced by MiniSat::Solver::assume(), CVC3::TheoryArith3::fixCurrentMaxCoefficient(), CVC3::TheoryArithOld::fixCurrentMaxCoefficient(), SAT::Clause::getMaxVar(), MiniSat::malloc_clause(), and MiniSat::Solver::setPushID().
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 IF_DEBUG(), and 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().
|
inline |
Definition at line 52 of file exception.h.
References CVC3::Exception::toString().
|
inline |
Definition at line 945 of file expr.h.
References AND, and DebugAssert.
Referenced by CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andIntro(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), recCompleteInster::build_tree(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::VCL::checkContinue(), CVC3::TheoryUF::computeModel(), CVC3::TheorySimulate::computeTCC(), CVC3::TheoryUF::computeTCC(), CVC3::TheoryArray::computeTCC(), CVC3::Theory::computeTCC(), CVC3::TheoryBitvector::computeTCC(), CVC3::TheoryCore::computeTCC(), CVC3::TheoryRecords::computeTypePred(), CVC3::TheoryArithNew::computeTypePred(), CVC3::TheoryArith3::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryCore::computeTypePred(), CVC3::SearchEngineTheoremProducer::convertToCNF(), CVC3::DatatypeTheoremProducer::decompose(), CVC3::BitvectorTheoremProducer::eqToBits(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::RecordsTheoremProducer::expandEq(), CVC3::BitvectorTheoremProducer::expandTypePred(), CVC3::CommonTheoremProducer::implIntro(), CVC3::CommonTheoremProducer::implIntro3(), CVC3::ArithTheoremProducerOld::implyEqualities(), CVC3::DatatypeTheoremProducer::noCycle(), CVC3::BitvectorTheoremProducer::oneBVAND(), CVC3::SearchEngineTheoremProducer::opCNFRule(), CVC3::Expr::operator&&(), CVC3::TheoryArithNew::rewrite(), CVC3::CommonTheoremProducer::rewriteAnd(), CVC3::BitvectorTheoremProducer::rewriteNAND(), CVC3::CoreTheoremProducer::rewriteNotOr(), CVC3::ArrayTheoremProducer::splitOnConstants(), and CVC3::BitvectorTheoremProducer::zeroBVOR().
|
inline |
Definition at line 955 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::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducerOld::divideEqnNonConst(), CVC3::ArithTheoremProducer3::divideEqnNonConst(), CVC3::ArithTheoremProducer::divideEqnNonConst(), CVC3::RecordsTheoremProducer::expandNeq(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::Expr::operator||(), CVC3::CoreTheoremProducer::orDistributivityRule(), CVC3::QuantTheoremProducer::pullVarOut(), CVC3::CompleteInstPreProcessor::pullVarOut(), CVC3::BitvectorTheoremProducer::rewriteNOR(), CVC3::CoreTheoremProducer::rewriteNotAnd(), CVC3::CommonTheoremProducer::rewriteOr(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), CVC3::ArrayTheoremProducer::splitOnConstants(), and CVC3::VCL::tryModelGeneration().
|
inline |
Definition at line 1600 of file expr.h.
References CVC3::Expr::d_expr.
|
inline |
|
inline |
Definition at line 1610 of file expr.h.
References CVC3::Expr::compare.
|
inline |
Definition at line 1612 of file expr.h.
References CVC3::Expr::compare.
|
inline |
Definition at line 1614 of file expr.h.
References CVC3::Expr::compare.
|
inline |
Definition at line 1616 of file expr.h.
References CVC3::Expr::compare.
|
inline |
Definition at line 56 of file lang.h.
Referenced by getLanguage().
|
inline |
Definition at line 61 of file lang.h.
References AST_LANG, isPrefix(), LISP_LANG, PRESENTATION_LANG, SIMPLIFY_LANG, SMTLIB_LANG, SMTLIB_V2_LANG, SPASS_LANG, and TPTP_LANG.
Referenced by CVC3::ExprManager::getInputLang(), CVC3::ExprManager::getOutputLang(), and main().
|
inline |
Definition at line 57 of file proof.h.
References CVC3::Proof::getExpr().
|
inline |
Definition at line 61 of file proof.h.
References CVC3::Proof::getExpr().
|
inline |
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition at line 159 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::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::BitvectorTheoremProducer::chopConcat(), CVC3::TheoryArith3::doSolve(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducerOld::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(), pow(), CVC3::Translator::preprocessRec(), CVC3::VCL::ratExpr(), and CVC3::TheoryBitvector::rewriteBV().
|
inline |
take nth root of base, return result if it is exact, 0 otherwise
Definition at line 172 of file rational.h.
References DebugAssert, CVC3::Rational::getDenominator(), and CVC3::Rational::getNumerator().
Referenced by CVC3::TheoryArith3::doSolve(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), and CVC3::TheoryArithOld::rewrite().
|
inline |
Definition at line 189 of file rational.h.
|
inline |
Definition at line 190 of file rational.h.
|
inline |
Definition at line 192 of file rational.h.
|
inline |
Definition at line 194 of file rational.h.
|
inline |
Definition at line 196 of file rational.h.
void CVC3::printRational | ( | const Rational & | x | ) |
|
inline |
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition at line 285 of file rational.h.
References pow().
|
inline |
Definition at line 293 of file rational.h.
|
inline |
Definition at line 294 of file rational.h.
|
inline |
Definition at line 296 of file rational.h.
void CVC3::printUnsigned | ( | const Unsigned & | x | ) |
|
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().
|
inline |
Definition at line 66 of file statistics.h.
References CVC3::StatFlag::d_flag.
|
inline |
Definition at line 69 of file statistics.h.
References CVC3::StatFlag::d_flag.
|
inline |
Definition at line 72 of file statistics.h.
References CVC3::StatFlag::d_flag.
|
inline |
Definition at line 122 of file statistics.h.
References CVC3::StatCounter::d_counter.
|
inline |
Definition at line 125 of file statistics.h.
References CVC3::StatCounter::d_counter.
|
inline |
Definition at line 128 of file statistics.h.
References CVC3::StatCounter::d_counter.
|
inline |
Definition at line 131 of file statistics.h.
References CVC3::StatCounter::d_counter.
|
inline |
Definition at line 134 of file statistics.h.
References CVC3::StatCounter::d_counter.
|
inline |
Definition at line 137 of file statistics.h.
References CVC3::StatCounter::d_counter.
|
inline |
Definition at line 140 of file statistics.h.
References CVC3::StatCounter::d_counter.
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Definition at line 173 of file theory_arith.h.
References CVC3::Type::getExpr(), CVC3::Expr::getKind(), and REAL.
Referenced by CVC3::TheoryArithOld::addPairToArithOrder(), CVC3::TheorySimulate::computeType(), CVC3::Translator::finish(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArith3::isIntegerThm(), CVC3::TheoryArithNew::isIntegerThm(), CVC3::TheoryArithOld::isIntegerThm(), CVC3::Translator::preprocess2Rec(), CVC3::TheoryCore::print(), CVC3::Translator::printArrayExpr(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::Translator::processType(), CVC3::TheoryArithNew::refineCounterExample(), CVC3::TheoryArith3::refineCounterExample(), and CVC3::TheoryArithOld::refineCounterExample().
|
inline |
Definition at line 174 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::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::CompleteInstPreProcessor::isGoodQuant(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::TheoryArithOld::isInteger(), CVC3::TheoryArithOld::isIntegerThm(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::Translator::preprocess2Rec(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithNew::print(), CVC3::TheoryArith3::print(), CVC3::TheoryArithOld::print(), CVC3::Translator::printArrayExpr(), CVC3::Translator::processType(), and CVC3::TheoryArith3::projectInequalities().
|
inline |
Definition at line 177 of file theory_arith.h.
References CVC3::Expr::isRational().
Referenced by CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithNew::canon(), CVC3::TheoryArith3::canon(), CVC3::TheoryArithOld::canon(), CVC3::ArithTheoremProducer3::canonDivideConst(), CVC3::ArithTheoremProducerOld::canonDivideConst(), CVC3::ArithTheoremProducer::canonDivideConst(), CVC3::ArithTheoremProducer3::canonDivideMult(), CVC3::ArithTheoremProducerOld::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::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducerOld::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::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::TheoryArithNew::computeModel(), CVC3::TheoryArith3::computeModel(), CVC3::TheoryArithOld::computeModel(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheorySimulate::computeType(), CVC3::ArithTheoremProducer3::constPredicate(), CVC3::ArithTheoremProducerOld::constPredicate(), CVC3::ArithTheoremProducer::constPredicate(), LFSCConvert::cvc3_to_lfsc(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::VCCmd::evaluateCommand(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::TheoryArithNew::findCoefficient(), CVC3::TheoryArithNew::findRationalBound(), CVC3::TheoryArith3::findRationalBound(), CVC3::TheoryArithOld::findRationalBound(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), getLeft(), getRight(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::TheoryArithOld::inequalityToFind(), CVC3::ArithTheoremProducerOld::intEqualityRationalConstant(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::TheoryArithNew::lessThanVar(), CVC3::TheoryArith3::lessThanVar(), CVC3::TheoryArithOld::lessThanVar(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::ArithTheoremProducerOld::powerOfOne(), CVC3::Translator::preprocessRec(), CVC3::TheoryArithOld::print(), LFSCPrinter::print_poly_norm(), LFSCPrinter::print_terms_h(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArith::rewriteToDiff(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithOld::update(), CVC3::TheoryArith3::updateSubsumptionDB(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
Definition at line 178 of file theory_arith.h.
References CVC3::Expr::getRational(), CVC3::Rational::isInteger(), and CVC3::Expr::isRational().
Referenced by CVC3::TheoryArithNew::checkType(), CVC3::TheoryArith3::checkType(), CVC3::TheoryArithOld::checkType(), CVC3::ArithTheoremProducer3::elimPower(), CVC3::ArithTheoremProducer::elimPower(), CVC3::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), CVC3::ArithTheoremProducer3::evenPowerEqNegConst(), CVC3::ArithTheoremProducer::evenPowerEqNegConst(), CVC3::TheoryArith3::getFactors(), CVC3::TheoryArithOld::getFactors(), CVC3::ArithTheoremProducer3::intEqIrrational(), and CVC3::ArithTheoremProducer::intEqIrrational().
|
inline |
Definition at line 180 of file theory_arith.h.
References CVC3::Expr::getKind(), and UMINUS.
Referenced by CVC3::TheoryArith::isSyntacticRational().
|
inline |
Definition at line 181 of file theory_arith.h.
References CVC3::Expr::getKind(), and PLUS.
Referenced by CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArith3::addToBuffer(), CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::assertFact(), canGetHead(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::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::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::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::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::TheoryArithOld::isUnconstrained(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArith3::pickMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArith3::processBuffer(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArithOld::separateMonomial(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::TheoryArithOld::updateConstrained(), CVC3::TheoryArith3::updateSubsumptionDB(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
Definition at line 182 of file theory_arith.h.
References CVC3::Expr::getKind(), and MINUS.
Referenced by canGetHead(), and CVC3::TheoryQuant::getHeadExpr().
|
inline |
Definition at line 183 of file theory_arith.h.
References CVC3::Expr::getKind(), and MULT.
Referenced by CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::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::TheoryArith3::computeNormalFactor(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::TheoryArithNew::findCoefficient(), CVC3::TheoryQuant::getHeadExpr(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithOld::getUpperBound(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryArithOld::isConstrainedAbove(), CVC3::TheoryArithOld::isConstrainedBelow(), CVC3::TheoryArithOld::isNonlinearSumTerm(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isPowerEquality(), CVC3::TheoryArithOld::isPowersEquality(), CVC3::TheoryArithOld::isUnconstrained(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducer::monomialMulF(), CVC3::ArithTheoremProducer3::monomialMulF(), CVC3::ArithTheoremProducer3::multEqZero(), CVC3::ArithTheoremProducer::multEqZero(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::ArithTheoremProducer3::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArith3::pickIntEqMonomial(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArith3::processRealEq(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArithOld::separateMonomial(), CVC3::ArithTheoremProducerOld::simpleIneqInt(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::TheoryArithOld::termDegree(), and CVC3::TheoryArithOld::updateConstrained().
|
inline |
Definition at line 184 of file theory_arith.h.
References DIVIDE, and CVC3::Expr::getKind().
Referenced by canGetHead(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::TheoryQuant::getHeadExpr(), and CVC3::TheoryArith::isSyntacticRational().
|
inline |
Definition at line 185 of file theory_arith.h.
References CVC3::Expr::getKind(), and POW.
Referenced by CVC3::TheoryArithOld::addToBuffer(), canGetHead(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::TheoryArith3::doSolve(), CVC3::TheoryArithOld::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::TheoryArith3::processSimpleIntEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), and CVC3::TheoryArithOld::termDegree().
|
inline |
Definition at line 186 of file theory_arith.h.
References CVC3::Expr::getKind(), and LT.
Referenced by CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithOld::findBounds(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CompleteInstPreProcessor::isGoodQuant(), isIneq(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isStale(), CVC3::TheoryArithOld::isStale(), isSysPred(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArith3::updateSubsumptionDB(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
Definition at line 187 of file theory_arith.h.
References CVC3::Expr::getKind(), and LE.
Referenced by CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::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::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isolateVariable(), isSysPred(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArith3::projectInequalities(), CVC3::TheoryArithOld::projectInequalities(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArith3::updateSubsumptionDB(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
Definition at line 188 of file theory_arith.h.
References CVC3::Expr::getKind(), and GT.
Referenced by CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::ArithTheoremProducerOld::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::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArith3::rewrite(), and CVC3::TheoryArithOld::rewrite().
|
inline |
Definition at line 189 of file theory_arith.h.
References GE, and CVC3::Expr::getKind().
Referenced by CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducerOld::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::TheoryArith3::rewrite(), and CVC3::TheoryArithOld::rewrite().
|
inline |
Definition at line 190 of file theory_arith.h.
References DARK_SHADOW, and CVC3::Expr::getKind().
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), and CVC3::TheoryArith3::setup().
|
inline |
Definition at line 191 of file theory_arith.h.
References CVC3::Expr::getKind(), and GRAY_SHADOW.
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadow0(), CVC3::ArithTheoremProducer::expandGrayShadow0(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::TheoryArith3::setup(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), and CVC3::ArithTheoremProducerOld::splitGrayShadowSmall().
|
inline |
Definition at line 192 of file theory_arith.h.
References isGE(), isGT(), isLE(), and isLT().
Referenced by CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::TheoryArith3::freeConstIneq(), CVC3::TheoryArithOld::freeConstIneq(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::update(), CVC3::TheoryArith3::update(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithOld::updateConstrained().
|
inline |
Definition at line 194 of file theory_arith.h.
References CVC3::Expr::getKind(), and IS_INTEGER.
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::TheoryArithNew::setup(), and CVC3::ArithTheoremProducerOld::simpleIneqInt().
|
inline |
Definition at line 197 of file theory_arith.h.
References UMINUS.
Referenced by operator-(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), and CVC3::TheoryArithOld::parseExprOp().
|
inline |
Definition at line 199 of file theory_arith.h.
References PLUS.
Referenced by CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducerOld::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::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), operator+(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryArith3::updateSubsumptionDB(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
Definition at line 201 of file theory_arith.h.
References DebugAssert, and PLUS.
|
inline |
Definition at line 205 of file theory_arith.h.
References MINUS.
Referenced by CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), operator-(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), and CVC3::TheoryArithOld::parseExprOp().
|
inline |
Definition at line 207 of file theory_arith.h.
References MULT.
Referenced by CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducer3::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::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducer3::monomialMulF(), CVC3::ArithTheoremProducer::monomialMulF(), operator*(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithNew::separateMonomial(), CVC3::TheoryArith3::separateMonomial(), CVC3::TheoryArithOld::separateMonomial(), CVC3::ArithTheoremProducerOld::simplifiedMultExpr(), CVC3::ArithTheoremProducer3::simplifiedMultExpr(), and CVC3::ArithTheoremProducer::simplifiedMultExpr().
|
inline |
a Mult expr with two or more children
Definition at line 211 of file theory_arith.h.
References DebugAssert, and MULT.
|
inline |
Power (x^n, or base^{pow}) expressions.
Definition at line 216 of file theory_arith.h.
References POW.
Referenced by CVC3::ArithTheoremProducer3::canonInvertLeaf(), CVC3::ArithTheoremProducerOld::canonInvertLeaf(), CVC3::ArithTheoremProducer::canonInvertLeaf(), CVC3::ArithTheoremProducerOld::canonInvertPow(), CVC3::ArithTheoremProducer3::canonInvertPow(), CVC3::ArithTheoremProducer::canonInvertPow(), CVC3::ArithTheoremProducer3::canonMultLeafLeaf(), CVC3::ArithTheoremProducerOld::canonMultLeafLeaf(), CVC3::ArithTheoremProducer::canonMultLeafLeaf(), CVC3::ArithTheoremProducerOld::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer::canonMultLeafOrPowMult(), CVC3::ArithTheoremProducer3::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowLeaf(), CVC3::ArithTheoremProducer::canonMultPowLeaf(), CVC3::ArithTheoremProducerOld::canonMultPowPow(), CVC3::ArithTheoremProducer3::canonMultPowPow(), CVC3::ArithTheoremProducer::canonMultPowPow(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), and CVC3::VCL::powExpr().
|
inline |
Definition at line 219 of file theory_arith.h.
References DIVIDE.
Referenced by CVC3::VCL::divideExpr(), operator/(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), and CVC3::TheoryArithOld::parseExprOp().
|
inline |
Definition at line 221 of file theory_arith.h.
References LT.
Referenced by CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::VCL::ltExpr(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), and CVC3::TheoryArithOld::parseExprOp().
|
inline |
Definition at line 223 of file theory_arith.h.
References LE.
Referenced by CVC3::TheoryBitvector::bitBlastTerm(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::TheoryArithNew::computeTypePred(), CVC3::TheoryArith3::computeTypePred(), CVC3::TheoryArithOld::computeTypePred(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducer3::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducerOld::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::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArith3::updateSubsumptionDB(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
Definition at line 225 of file theory_arith.h.
References GT.
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::VCL::gtExpr(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), and CVC3::TheoryArithOld::parseExprOp().
|
inline |
Definition at line 227 of file theory_arith.h.
References GE.
Referenced by CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::eqToIneq(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::VCL::geExpr(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithOld::parseExprOp(), and CVC3::TheoryArithNew::rewrite().
|
inline |
Definition at line 230 of file theory_arith.h.
References uminusExpr().
|
inline |
Definition at line 232 of file theory_arith.h.
References plusExpr().
|
inline |
Definition at line 234 of file theory_arith.h.
References minusExpr().
|
inline |
Definition at line 236 of file theory_arith.h.
References multExpr().
Referenced by CVC3::Expr::iterator::operator->().
|
inline |
Definition at line 238 of file theory_arith.h.
References divideExpr().
|
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().
|
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().
|
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().
|
inline |
Definition at line 112 of file theory_array.h.
References ARRAY_LITERAL, CVC3::Expr::getKind(), and CVC3::Expr::isClosure().
|
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 1261 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 98 of file theory_core.cpp.
References CVC3::NotifyList::getExpr(), CVC3::Theory::getName(), CVC3::NotifyList::getTheory(), and CVC3::NotifyList::size().
|
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().
|
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().
|
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().
|
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().
|
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().
|
inline |
Definition at line 83 of file type.h.
References CVC3::Type::getExpr().
|
inline |
Definition at line 86 of file type.h.
References CVC3::Type::getExpr().
|
inline |
Definition at line 90 of file type.h.
References CVC3::Type::getExpr().
|
inline |
Definition at line 188 of file variable.h.
|
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 |
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(), CVC3::Theorem::clearAllFlags(), 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(), CVC3::Theorem::clearAllFlags(), and CVC3::Assumptions::end().
ostream& CVC3::operator<< | ( | std::ostream & | os, |
const Assumptions & | assump | ||
) |
Definition at line 321 of file assumptions.cpp.
References CVC3::Assumptions::d_vector.
int CVC3::compare | ( | const Theorem & | t1, |
const Theorem & | t2 | ||
) |
Compare Theorems by their expressions. Return -1, 0, or 1.
This is an arbitrary total ordering on Theorems. For simplicity, we define rewrite theorems (e1 = e2 or e1 <=> e2) to be smaller than other theorems.
Definition at line 45 of file theorem.cpp.
References compare(), CVC3::Theorem::d_thm, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), 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().
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 |