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

Classes

class  Assumptions
class  CDFlags
class  CDList
class  CDOmap
class  CDMapData
class  CDMap
class  CDOmapOrdered
class  CDMapOrderedData
class  CDMapOrdered
class  CDO
class  Circuit
class  ClauseValue
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  CompactClause
class  CLException
class  CLFlag
class  CLFlags
class  CommonProofRules
class  Scope
class  ContextObjChain
class  ContextObj
class  Context
class  ContextManager
 Manager for multiple contexts. Also holds current context. More...
class  ContextNotifyObj
struct  ltstr
class  StrPairLess
class  ScopeWatcher
 A class which sets a boolean value to true when created, and resets to false when deleted. More...
class  MemoryTracker
class  DebugException
class  EvalException
class  ResetException
class  Exception
class  Expr
 Data structure of expressions in CVC3. More...
class  ExprManager
class  ExprManagerNotifyObj
 Notifies ExprManager before and after each pop() More...
class  ExprMap
class  ExprHashMap
class  Op
class  ExprStream
 Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING! More...
class  ExprTransform
class  ExprValue
 The base class for holding the actual data in expressions. More...
class  ExprNode
class  ExprNodeTmp
class  ExprApplyTmp
class  ExprApply
class  ExprString
class  ExprSkolem
class  ExprRational
class  ExprVar
class  ExprSymbol
class  ExprBoundVar
class  ExprClosure
 A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers. More...
class  MemoryManager
class  MemoryManagerChunks
class  ContextMemoryManager
 ContextMemoryManager. More...
class  MemoryManagerMalloc
class  NotifyList
class  Parser
class  ParserException
class  PrettyPrinter
 Abstract API to a pretty-printer for Expr. More...
class  Proof
class  Rational
class  Unsigned
class  SearchEngine
 API to to a generic proof search engine. More...
class  SearchEngineFast
 Implementation of a faster search engine, using newer techniques. More...
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  SearchSimple
 Implementation of the simple search engine. More...
class  SmartCDO
 SmartCDO. More...
class  SmtlibException
class  SoundException
class  StatFlag
class  StatCounter
class  Statistics
class  Theorem
class  Theorem3
 Theorem3. More...
class  TheoremLess
 "Less" comparator for theorems by TheoremValue pointers More...
class  TheoremManager
class  TheoremProducer
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  Trigger
struct  dynTrig
class  CompleteInstPreProcessor
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  Type
 MS C++ specific settings. More...
class  TypecheckException
class  Variable
class  Literal
class  VariableValue
class  VariableManager
class  VariableManagerNotifyObj
 Notifies VariableManager before and after each pop() More...
class  ValidityChecker
 Generic API for a validity checker. More...
class  VCCmd
class  VCL
class  ParserTemp
class  CNF_Rules
 API to the CNF proof rules. More...
class  CNF_TheoremProducer
class  DecisionEngine
class  DecisionEngineCaching
class  DecisionEngineDFS
 Decision Engine for use with the Search EngineAuthor: Clark Barrett. More...
class  DecisionEngineMBTF
class  CoreSatAPI_implBase
class  SearchEngineRules
 API to the proof rules for the Search Engines. More...
class  SearchSatCoreSatAPI
class  SearchSatTheoryAPI
class  SearchSatDecider
class  SearchSatCNFCallback
class  SearchEngineTheoremProducer
class  CommonTheoremProducer
class  TheoremValue
class  RegTheoremValue
class  RWTheoremValue
class  ArithException
class  ArithProofRules
class  ArithTheoremProducer
class  ArithTheoremProducer3
class  ArithTheoremProducerOld
class  ArrayProofRules
class  ArrayTheoremProducer
class  BitvectorException
class  BVConstExpr
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  CoreProofRules
class  CoreTheoremProducer
class  PrettyPrinterCore
 Implementation of PrettyPrinter class. More...
class  TypeComputerCore
class  DatatypeProofRules
class  DatatypeTheoremProducer
class  QuantProofRules
class  QuantTheoremProducer
class  RecordsProofRules
class  RecordsTheoremProducer
class  SimulateProofRules
class  SimulateTheoremProducer
class  UFProofRules
class  UFTheoremProducer

Typedefs

typedef std::pair< std::string,
std::string > 
StrPair
typedef long unsigned ExprIndex
 Expression index type.
typedef enum CVC3::FormulaValue FormulaValue
typedef enum CVC3::QueryResult QueryResult
typedef std::map< Theorem,
bool, TheoremLess
TheoremMap
typedef struct CVC3::dynTrig dynTrig

Enumerations

enum  CLFlagType {
  CLFLAG_NULL, CLFLAG_BOOL, CLFLAG_INT, CLFLAG_STRING,
  CLFLAG_STRVEC
}
 Different types of command line flags. More...
enum  ExprValueType {
  EXPR_VALUE, EXPR_NODE, EXPR_APPLY, EXPR_STRING,
  EXPR_RATIONAL, EXPR_SKOLEM, EXPR_UCONST, EXPR_SYMBOL,
  EXPR_BOUND_VAR, EXPR_CLOSURE, EXPR_VALUE_TYPE_LAST
}
 Type ID of each ExprValue subclass. More...
enum  Cardinality { CARD_FINITE, CARD_INFINITE, CARD_UNKNOWN }
 Enum for cardinality of types. More...
enum  FormulaValue { TRUE_VAL, FALSE_VAL, UNKNOWN_VAL }
enum  InputLanguage {
  PRESENTATION_LANG, SMTLIB_LANG, LISP_LANG, AST_LANG,
  SIMPLIFY_LANG, TPTP_LANG, SPASS_LANG, SMTLIB_V2_LANG
}
 Different input languages. More...
enum  QueryResult {
  SATISFIABLE = 0, INVALID = 0, VALID = 1, UNSATISFIABLE = 1,
  ABORT, UNKNOWN
}
enum  ArithKinds {
  REAL_CONST = 30, NEGINF = 31, POSINF = 32, REAL = 3000,
  INT, SUBRANGE, UMINUS, PLUS,
  MINUS, MULT, DIVIDE, POW,
  INTDIV, MOD, LT, LE,
  GT, GE, IS_INTEGER, DARK_SHADOW,
  GRAY_SHADOW
}
enum  ArrayKinds { ARRAY = 2000, READ, WRITE, ARRAY_LITERAL }
enum  BVKinds {
  BVCONST = 80, BITVECTOR = 8000, CONCAT, EXTRACT,
  BOOLEXTRACT, LEFTSHIFT, CONST_WIDTH_LEFTSHIFT, RIGHTSHIFT,
  BVSHL, BVLSHR, BVASHR, SX,
  BVREPEAT, BVZEROEXTEND, BVROTL, BVROTR,
  BVAND, BVOR, BVXOR, BVXNOR,
  BVNEG, BVNAND, BVNOR, BVCOMP,
  BVUMINUS, BVPLUS, BVSUB, BVMULT,
  BVUDIV, BVSDIV, BVUREM, BVSREM,
  BVSMOD, BVLT, BVLE, BVGT,
  BVGE, BVSLT, BVSLE, BVSGT,
  BVSGE, INTTOBV, BVTOINT, BVTYPEPRED
}
enum  DatatypeKinds {
  DATATYPE_DECL = 600, DATATYPE, CONSTRUCTOR, SELECTOR,
  TESTER
}
 Local kinds for datatypes. More...
enum  Polarity { Ukn, Pos, Neg, PosNeg }
enum  RecordKinds {
  RECORD = 2500, RECORD_SELECT, RECORD_UPDATE, RECORD_TYPE,
  TUPLE, TUPLE_SELECT, TUPLE_UPDATE, TUPLE_TYPE
}
enum  UFKinds { TRANS_CLOSURE = 500, OLD_ARROW }
 Local kinds for transitive closure of binary relations. More...
enum  ArithLang {
  NOT_USED = 0, TERMS_ONLY, DIFF_ONLY, LINEAR,
  NONLINEAR
}
 Used to keep track of which subset of arith is being used. More...

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)
ExprStreamoperator<< (ExprStream &os, ExprStream &(*manip)(ExprStream &))
 Use manipulators which are functions over ExprStream&.
ExprStreamoperator<< (ExprStream &os, const Expr &e)
 Print Expr.
ExprStreamoperator<< (ExprStream &os, const Type &t)
 Print Type.
ExprStreamoperator<< (ExprStream &os, const string &s)
 Print string.
ExprStreamoperator<< (ExprStream &os, const char *s)
 Print char* string.
ExprStreamoperator<< (ExprStream &os, const Rational &r)
 Print Rational.
ExprStreamoperator<< (ExprStream &os, int i)
 Print int.
ExprStreampush (ExprStream &os)
 Set the indentation to the current position.
ExprStreampop (ExprStream &os)
 Restore the indentation.
ExprStreampopSave (ExprStream &os)
 Remember the current indentation and pop to the previous position.
ExprStreampushRestore (ExprStream &os)
 Set the indentation to the position saved by popSave()
ExprStreamreset (ExprStream &os)
 Reset the indentation to the default at this level.
ExprStreamspace (ExprStream &os)
 Insert a single white space separator.
ExprStreamnodag (ExprStream &os)
ExprStreampushdag (ExprStream &os)
ExprStreampopdag (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 >
abs (T t)
template<class 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.
CVC_DLL void fatalError (const std::string &file, int line, const std::string &cond, const std::string &msg)
 Function for fatal exit.
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)
Rational ratRoot (const Rational &base, unsigned long int n)
 take nth root of base, return result if it is exact, 0 otherwise
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)
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
Expr powExpr (const Expr &pow, const Expr &base)
 Power (x^n, or base^{pow}) expressions.
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.
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.
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
ParserTempparserTemp

Typedef Documentation

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

Definition at line 78 of file cvc_util.h.

typedef long unsigned CVC3::ExprIndex

Expression index type.

Definition at line 87 of file expr.h.

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

Definition at line 402 of file theorem.h.

typedef struct CVC3::dynTrig CVC3::dynTrig

Enumeration Type Documentation

Different types of command line flags.

Enumerator:
CLFLAG_NULL 
CLFLAG_BOOL 
CLFLAG_INT 
CLFLAG_STRING 
CLFLAG_STRVEC 

Vector of pair<string, bool>

Definition at line 34 of file command_line_flags.h.

Type ID of each ExprValue subclass.

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

Enumerator:
EXPR_VALUE 
EXPR_NODE 
EXPR_APPLY 

Application of functions and predicates.

EXPR_STRING 
EXPR_RATIONAL 
EXPR_SKOLEM 
EXPR_UCONST 
EXPR_SYMBOL 
EXPR_BOUND_VAR 
EXPR_CLOSURE 
EXPR_VALUE_TYPE_LAST 

Definition at line 65 of file expr.h.

Enum for cardinality of types.

Enumerator:
CARD_FINITE 
CARD_INFINITE 
CARD_UNKNOWN 

Definition at line 80 of file expr.h.

Enumerator:
TRUE_VAL 
FALSE_VAL 
UNKNOWN_VAL 

Definition at line 31 of file formula_value.h.

Different input languages.

Enumerator:
PRESENTATION_LANG 

Nice SAL-like language for manually written specs.

SMTLIB_LANG 

SMT-LIB format.

LISP_LANG 

Lisp-like format for automatically generated specs.

AST_LANG 
SIMPLIFY_LANG 

for output into Simplify format

TPTP_LANG 

for output in TPTP format

SPASS_LANG 

for output in SPASS format

SMTLIB_V2_LANG 

SMT-LIB v2 format.

Definition at line 30 of file lang.h.

Enumerator:
SATISFIABLE 
INVALID 
VALID 
UNSATISFIABLE 
ABORT 
UNKNOWN 

Definition at line 32 of file queryresult.h.

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

Definition at line 31 of file theory_arith.h.

Enumerator:
ARRAY 
READ 
WRITE 
ARRAY_LITERAL 

Definition at line 30 of file theory_array.h.

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

Definition at line 32 of file theory_bitvector.h.

Local kinds for datatypes.

Enumerator:
DATATYPE_DECL 
DATATYPE 
CONSTRUCTOR 
SELECTOR 
TESTER 

Definition at line 33 of file theory_datatype.h.

Enumerator:
Ukn 
Pos 
Neg 
PosNeg 

Definition at line 48 of file theory_quant.h.

Enumerator:
RECORD 
RECORD_SELECT 
RECORD_UPDATE 
RECORD_TYPE 
TUPLE 
TUPLE_SELECT 
TUPLE_UPDATE 
TUPLE_TYPE 

Definition at line 29 of file theory_records.h.

Local kinds for transitive closure of binary relations.

Enumerator:
TRANS_CLOSURE 
OLD_ARROW 

Definition at line 32 of file theory_uf.h.

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

Enumerator:
NOT_USED 
TERMS_ONLY 
DIFF_ONLY 
LINEAR 
NONLINEAR 

Definition at line 51 of file translator.h.


Function Documentation

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

Definition at line 49 of file expr_stream.cpp.

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

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

std::string CVC3::to_upper ( const std::string &  src)
inline

Definition at line 30 of file cvc_util.h.

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

std::string CVC3::to_lower ( const std::string &  src)
inline

Definition at line 38 of file cvc_util.h.

Referenced by CVC3::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::TheoryArith3::assertFact(), CVC3::TheoryArithOld::assertFact(), CVC3::CDList< SmartCDO< Theorem > >::at(), CVC3::CDList< SmartCDO< Theorem > >::back(), CVC3::SearchEngineFast::bcp(), CVC3::BitvectorTheoremProducer::bitBlastDisEqnRule(), CVC3::BitvectorTheoremProducer::bitBlastEqnRule(), CVC3::TheoryBitvector::bitBlastTerm(), CVC3::BitvectorTheoremProducer::bitExtractBitwise(), CVC3::BitvectorTheoremProducer::bitExtractBVASHR(), CVC3::BitvectorTheoremProducer::bitExtractBVLSHR(), CVC3::BitvectorTheoremProducer::bitExtractBVMult(), CVC3::BitvectorTheoremProducer::bitExtractBVPlus(), CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed(), CVC3::BitvectorTheoremProducer::bitExtractBVSHL(), CVC3::BitvectorTheoremProducer::bitExtractConcatenation(), CVC3::BitvectorTheoremProducer::bitExtractConstant(), CVC3::BitvectorTheoremProducer::bitExtractConstBVMult(), CVC3::BitvectorTheoremProducer::bitExtractExtraction(), CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVC3::BitvectorTheoremProducer::bitExtractNot(), CVC3::BitvectorTheoremProducer::bitExtractRewrite(), CVC3::BitvectorTheoremProducer::bitwiseConst(), CVC3::BitvectorTheoremProducer::bitwiseConstElim(), CVC3::BVConstExpr::BVConstExpr(), CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::TheoryArray::checkSat(), CVC3::TheoryUF::computeModel(), CVC3::TheoryArray::computeModel(), CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheorySimulate::computeType(), CVC3::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< SmartCDO< Theorem > >::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().

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

Definition at line 74 of file cvc_util.h.

Referenced by IF_DEBUG(), and sort2().

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

Sort two vectors based on the first vector.

Definition at line 82 of file cvc_util.h.

References DebugAssert, and strPair().

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

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

Function for fatal exit.

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

Definition at line 35 of file debug.cpp.

References std::endl().

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

Definition at line 52 of file exception.h.

References CVC3::Exception::toString().

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

Definition at line 945 of file expr.h.

References AND, and DebugAssert.

Referenced by CVC3::CoreTheoremProducer::andDistributivityRule(), CVC3::CommonTheoremProducer::andIntro(), CVC3::BitvectorTheoremProducer::bitblastBVMult(), recCompleteInster::build_tree(), CVC3::BitvectorTheoremProducer::bvUDivTheorem(), CVC3::VCL::checkContinue(), CVC3::TheoryUF::computeModel(), CVC3::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().

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

Definition at line 1600 of file expr.h.

References CVC3::Expr::d_expr.

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

Definition at line 1605 of file expr.h.

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

Definition at line 1610 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1612 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1614 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1616 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 56 of file lang.h.

Referenced by getLanguage().

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

Definition at line 57 of file proof.h.

References CVC3::Proof::getExpr().

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

Definition at line 61 of file proof.h.

References CVC3::Proof::getExpr().

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

Definition at line 189 of file rational.h.

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

Definition at line 190 of file rational.h.

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

Definition at line 192 of file rational.h.

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

Definition at line 194 of file rational.h.

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

Definition at line 196 of file rational.h.

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

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

Definition at line 285 of file rational.h.

References pow().

Unsigned CVC3::newUnsigned ( int  n)
inline

Definition at line 293 of file rational.h.

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

Definition at line 294 of file rational.h.

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

Definition at line 296 of file rational.h.

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

Definition at line 66 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 69 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 72 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 122 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 125 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 128 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 131 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 134 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 137 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 140 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 427 of file theorem.h.

References compare().

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

Definition at line 429 of file theorem.h.

References compare().

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

Definition at line 431 of file theorem.h.

References compare().

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

Definition at line 433 of file theorem.h.

References compare().

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

Definition at line 177 of file theory_arith.h.

References CVC3::Expr::isRational().

Referenced by CVC3::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().

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

Definition at line 180 of file theory_arith.h.

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

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

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

Definition at line 181 of file theory_arith.h.

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

Referenced by CVC3::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().

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

Definition at line 182 of file theory_arith.h.

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

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

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

Definition at line 183 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::addToBuffer(), CVC3::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().

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

Definition at line 186 of file theory_arith.h.

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

Referenced by CVC3::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().

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

Definition at line 187 of file theory_arith.h.

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

Referenced by CVC3::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().

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

Definition at line 192 of file theory_arith.h.

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

Referenced by CVC3::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().

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

Definition at line 194 of file theory_arith.h.

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

Referenced by CVC3::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().

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

Definition at line 199 of file theory_arith.h.

References PLUS.

Referenced by CVC3::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().

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

Definition at line 201 of file theory_arith.h.

References DebugAssert, and PLUS.

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

a Mult expr with two or more children

Definition at line 211 of file theory_arith.h.

References DebugAssert, and MULT.

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

Definition at line 230 of file theory_arith.h.

References uminusExpr().

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

Definition at line 232 of file theory_arith.h.

References plusExpr().

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

Definition at line 234 of file theory_arith.h.

References minusExpr().

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

Definition at line 236 of file theory_arith.h.

References multExpr().

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

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

Definition at line 238 of file theory_arith.h.

References divideExpr().

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

Definition at line 112 of file theory_array.h.

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

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

Definition at line 83 of file type.h.

References CVC3::Type::getExpr().

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

Definition at line 86 of file type.h.

References CVC3::Type::getExpr().

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

Definition at line 90 of file type.h.

References CVC3::Type::getExpr().

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

Definition at line 188 of file variable.h.

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

Definition at line 192 of file variable.h.

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

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

Definition at line 202 of file variable.cpp.

References CVC3::Variable::d_val.

ostream& CVC3::operator<< ( std::ostream &  os,
const VariableValue &  v 
)
Assumptions CVC3::operator- ( const Assumptions a,
const Expr e 
)
Assumptions CVC3::operator- ( const Assumptions a,
const vector< Expr > &  es 
)
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 
)
int CVC3::compareByPtr ( const Theorem &  t1,
const Theorem &  t2 
)

Definition at line 83 of file theorem.cpp.

References CVC3::Theorem::d_thm.

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

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

Variable Documentation

const unsigned CVC3::chunkSizeBytes = 16384
ParserTemp* CVC3::parserTemp