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
• 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 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
• 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 Engine. 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 long unsigned ExprIndex

  Expression index type.
  

• typedef enum CVC3::FormulaValue FormulaValue
• typedef enum CVC3::QueryResult QueryResult
• typedef unsigned long Unsigned
• typedef std::map< Theorem,
  bool, TheoremLess > TheoremMap
• typedef 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 Kind {
    NULL_KIND = 0, TRUE_EXPR = 1, FALSE_EXPR = 2, RATIONAL_EXPR = 3,
    STRING_EXPR = 4, MAX_CONST = 100, RAW_LIST, ID,
    BOOLEAN, ANY_TYPE, ARROW, TYPE,
    TYPEDECL, TYPEDEF, EQ, NEQ,
    DISTINCT, NOT, AND, OR,
    XOR, IFF, IMPLIES, AND_R,
    IFF_R, ITE_R, ITE, FORALL,
    EXISTS, UFUNC, APPLY, ASSERT,
    QUERY, CHECKSAT, CONTINUE, RESTART,
    DBG, TRACE, UNTRACE, OPTION,
    HELP, TRANSFORM, PRINT, CALL,
    ECHO, INCLUDE, DUMP_PROOF, DUMP_ASSUMPTIONS,
    DUMP_SIG, DUMP_TCC, DUMP_TCC_ASSUMPTIONS, DUMP_TCC_PROOF,
    DUMP_CLOSURE, DUMP_CLOSURE_PROOF, WHERE, ASSERTIONS,
    ASSUMPTIONS, COUNTEREXAMPLE, COUNTERMODEL, PUSH,
    POP, POPTO, PUSH_SCOPE, POP_SCOPE,
    POPTO_SCOPE, RESET, CONTEXT, FORGET,
    GET_TYPE, CHECK_TYPE, GET_CHILD, SUBSTITUTE,
    SEQ, ARITH_VAR_ORDER, TCC, VARDECL,
    VARDECLS, BOUND_VAR, BOUND_ID, SUBTYPE,
    IF, IFTHEN, ELSE, COND,
    LET, LETDECLS, LETDECL, LAMBDA,
    SIMULATE, CONST, VARLIST, UCONST,
    DEFUN, PF_APPLY, PF_HOLE, SKOLEM_VAR,
    THEOREM_KIND, LAST_KIND
  }
• enum InputLanguage {
    PRESENTATION_LANG, SMTLIB_LANG, LISP_LANG, AST_LANG,
    SIMPLIFY_LANG, TPTP_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)
• ExprStream & operator<< (ExprStream &os, ExprStream &(*manip)(ExprStream &))

  Use manipulators which are functions over ExprStream&.
  

• ExprStream & operator<< (ExprStream &os, const Expr &e)

  Print Expr.
  

• ExprStream & operator<< (ExprStream &os, const Type &t)

  Print Type.
  

• ExprStream & operator<< (ExprStream &os, const string &s)

  Print string.
  

• ExprStream & operator<< (ExprStream &os, const char *s)

  Print char* string.
  

• ExprStream & operator<< (ExprStream &os, const Rational &r)

  Print Rational.
  

• ExprStream & operator<< (ExprStream &os, int i)

  Print int.
  

• ExprStream & push (ExprStream &os)

  Set the indentation to the current position.
  

• ExprStream & pop (ExprStream &os)

  Restore the indentation to the previous position.
  

• ExprStream & popSave (ExprStream &os)

  Remember the current indentation and pop to the previous position.
  

• ExprStream & pushRestore (ExprStream &os)

  Set the indentation to the position saved by popSave().
  

• ExprStream & reset (ExprStream &os)

  Reset the indentation to the default at this level.
  

• ExprStream & space (ExprStream &os)

  Insert a single white space separator.
  

• ExprStream & nodag (ExprStream &os)
• ExprStream & pushdag (ExprStream &os)
• ExprStream & popdag (ExprStream &os)
• 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)
• 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)
• 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
• ParserTemp * parserTemp

---

Typedef Documentation

typedef long unsigned CVC3::ExprIndex

Expression index type.

Definition at line 87 of file expr.h.

typedef enum CVC3::FormulaValue CVC3::FormulaValue

typedef enum CVC3::QueryResult CVC3::QueryResult

typedef unsigned long CVC3::Unsigned

Definition at line 198 of file rational.h.

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

Definition at line 402 of file theorem.h.

typedef struct CVC3::dynTrig CVC3::dynTrig

---

Enumeration Type Documentation

enum CVC3::CLFlagType

Different types of command line flags.

Enumerator:

CLFLAG_NULL
CLFLAG_BOOL
CLFLAG_INT
CLFLAG_STRING
CLFLAG_STRVEC	Vector of pair<string, bool>.

Definition at line 34 of file command_line_flags.h.

enum CVC3::ExprValueType

Type ID of each ExprValue subclass.

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

Enumerator:

EXPR_VALUE
EXPR_NODE
EXPR_APPLY	Application of functions and predicates.
EXPR_STRING
EXPR_RATIONAL
EXPR_SKOLEM
EXPR_UCONST
EXPR_SYMBOL
EXPR_BOUND_VAR
EXPR_CLOSURE
EXPR_VALUE_TYPE_LAST

Definition at line 65 of file expr.h.

enum CVC3::Cardinality

Enum for cardinality of types.

Enumerator:

CARD_FINITE
CARD_INFINITE
CARD_UNKNOWN

Definition at line 80 of file expr.h.

enum CVC3::FormulaValue

Enumerator:

TRUE_VAL
FALSE_VAL
UNKNOWN_VAL

Definition at line 31 of file formula_value.h.

enum CVC3::Kind

Enumerator:

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

Definition at line 29 of file kinds.h.

enum CVC3::InputLanguage

Different input languages.

Enumerator:

PRESENTATION_LANG	Nice SAL-like language for manually written specs.
SMTLIB_LANG	SMT-LIB format.
LISP_LANG	Lisp-like format for automatically generated specs.
AST_LANG
SIMPLIFY_LANG
TPTP_LANG	for output in TPTP format

Definition at line 30 of file lang.h.

enum CVC3::QueryResult

Enumerator:

SATISFIABLE
INVALID
VALID
UNSATISFIABLE
ABORT
UNKNOWN

Definition at line 32 of file queryresult.h.

enum CVC3::ArithKinds

Enumerator:

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

Definition at line 31 of file theory_arith.h.

enum CVC3::ArrayKinds

Enumerator:

ARRAY
READ
WRITE
ARRAY_LITERAL

Definition at line 30 of file theory_array.h.

enum CVC3::BVKinds

Enumerator:

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

Definition at line 32 of file theory_bitvector.h.

enum CVC3::DatatypeKinds

Local kinds for datatypes.

Enumerator:

DATATYPE_DECL
DATATYPE
CONSTRUCTOR
SELECTOR
TESTER

Definition at line 33 of file theory_datatype.h.

enum CVC3::Polarity

Enumerator:

Ukn
Pos
Neg
PosNeg

Definition at line 48 of file theory_quant.h.

enum CVC3::RecordKinds

Enumerator:

RECORD
RECORD_SELECT
RECORD_UPDATE
RECORD_TYPE
TUPLE
TUPLE_SELECT
TUPLE_UPDATE
TUPLE_TYPE

Definition at line 29 of file theory_records.h.

enum CVC3::UFKinds

Local kinds for transitive closure of binary relations.

Enumerator:

TRANS_CLOSURE
OLD_ARROW

Definition at line 31 of file theory_uf.h.

enum CVC3::ArithLang

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

Enumerator:

NOT_USED
TERMS_ONLY
DIFF_ONLY
LINEAR
NONLINEAR

Definition at line 49 of file translator.h.

---

Function Documentation

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

Definition at line 132 of file expr.cpp.

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

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

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

Definition at line 556 of file expr.cpp.

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

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

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

Definition at line 580 of file expr.cpp.

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

static bool CVC3::isTrivialExpr

(

const Expr &

e

)

[static]

Definition at line 49 of file expr_stream.cpp.

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

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

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

Function for fatal exit.

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

Definition at line 35 of file debug.cpp.

References std::endl().

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

Definition at line 52 of file exception.h.

References CVC3::Exception::toString().

Expr CVC3::andExpr

(

const std::vector< Expr > &

children

)

[inline]

Definition at line 942 of file expr.h.

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

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

Expr CVC3::orExpr

(

const std::vector< Expr > &

children

)

[inline]

Definition at line 952 of file expr.h.

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

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

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

Definition at line 1597 of file expr.h.

References CVC3::Expr::d_expr.

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

Definition at line 1602 of file expr.h.

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

Definition at line 1607 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1609 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1611 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1613 of file expr.h.

References CVC3::Expr::compare.

InputLanguage CVC3::getLanguage

(

const std::string &

lang

)

[inline]

Definition at line 47 of file lang.h.

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

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

std::ostream& CVC3::operator<<	(	std::ostream &	os,
		const Proof &	pf
	)			[inline]

Definition at line 57 of file proof.h.

References CVC3::Proof::getExpr().

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

Definition at line 61 of file proof.h.

References CVC3::Proof::getExpr().

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

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

Definition at line 153 of file rational.h.

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

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

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

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

Definition at line 166 of file rational.h.

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

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

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

Definition at line 183 of file rational.h.

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

Definition at line 184 of file rational.h.

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

Definition at line 186 of file rational.h.

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

Definition at line 188 of file rational.h.

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

Definition at line 190 of file rational.h.

void CVC3::printRational

(

const Rational &

x

)

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

Definition at line 311 of file search_sat.h.

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

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

Definition at line 66 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 69 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 72 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 122 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 125 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 128 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 131 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 134 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 137 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 140 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 427 of file theorem.h.

References compare().

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

Definition at line 429 of file theorem.h.

References compare().

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

Definition at line 431 of file theorem.h.

References compare().

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

Definition at line 433 of file theorem.h.

References compare().

bool CVC3::isReal

(

Type

t

)

[inline]

Definition at line 172 of file theory_arith.h.

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

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

bool CVC3::isInt

(

Type

t

)

[inline]

Definition at line 173 of file theory_arith.h.

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

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

bool CVC3::isRational

(

const Expr &

e

)

[inline]

Definition at line 176 of file theory_arith.h.

References CVC3::Expr::isRational().

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

bool CVC3::isIntegerConst

(

const Expr &

e

)

[inline]

Definition at line 177 of file theory_arith.h.

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

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

bool CVC3::isUMinus

(

const Expr &

e

)

[inline]

Definition at line 179 of file theory_arith.h.

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

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

bool CVC3::isPlus

(

const Expr &

e

)

[inline]

Definition at line 180 of file theory_arith.h.

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

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

bool CVC3::isMinus

(

const Expr &

e

)

[inline]

Definition at line 181 of file theory_arith.h.

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

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

bool CVC3::isMult

(

const Expr &

e

)

[inline]

Definition at line 182 of file theory_arith.h.

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

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

bool CVC3::isDivide

(

const Expr &

e

)

[inline]

Definition at line 183 of file theory_arith.h.

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

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

bool CVC3::isPow

(

const Expr &

e

)

[inline]

Definition at line 184 of file theory_arith.h.

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

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

bool CVC3::isLT

(

const Expr &

e

)

[inline]

Definition at line 185 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CompleteInstPreProcessor::isGoodQuant(), isIneq(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), CVC3::TheoryArithOld::isStale(), CVC3::TheoryArith3::isStale(), isSysPred(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::updateSubsumptionDB(), and CVC3::TheoryArith3::updateSubsumptionDB().

bool CVC3::isLE

(

const Expr &

e

)

[inline]

Definition at line 186 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer3::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::CompleteInstPreProcessor::collect_forall_index(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::CompleteInstPreProcessor::isGoodQuant(), isIneq(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArith3::isolateVariable(), isSysPred(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatchNoSig(), CVC3::TheoryQuant::newTopMatchSig(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArith3::normalizeProjectIneqs(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArith3::processFiniteInterval(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArith3::projectInequalities(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer3::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::ArithTheoremProducerOld::realShadowEq(), CVC3::ArithTheoremProducer3::realShadowEq(), CVC3::ArithTheoremProducer::realShadowEq(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArith3::setup(), CVC3::TheoryArithOld::updateSubsumptionDB(), and CVC3::TheoryArith3::updateSubsumptionDB().

bool CVC3::isGT

(

const Expr &

e

)

[inline]

Definition at line 187 of file theory_arith.h.

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

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

bool CVC3::isGE

(

const Expr &

e

)

[inline]

Definition at line 188 of file theory_arith.h.

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

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

bool CVC3::isDarkShadow

(

const Expr &

e

)

[inline]

Definition at line 189 of file theory_arith.h.

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

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

bool CVC3::isGrayShadow

(

const Expr &

e

)

[inline]

Definition at line 190 of file theory_arith.h.

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

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

bool CVC3::isIneq

(

const Expr &

e

)

[inline]

Definition at line 191 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArithNew::assertFact(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::TheoryArithOld::freeConstIneq(), CVC3::TheoryArith3::freeConstIneq(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer3::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryArithOld::normalize(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArith3::normalize(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::TheoryArithOld::registerAtom(), CVC3::TheoryArithOld::rewrite(), CVC3::TheoryArith3::rewrite(), CVC3::TheoryArithOld::setup(), CVC3::TheoryArithNew::setup(), CVC3::TheoryArithOld::update(), CVC3::TheoryArithNew::update(), and CVC3::TheoryArith3::update().

bool CVC3::isIntPred

(

const Expr &

e

)

[inline]

Definition at line 193 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer3::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer3::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer3::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducerOld::intEqIrrational(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer3::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::lessThanToLERewrite(), CVC3::ArithTheoremProducer3::lessThanToLERewrite(), CVC3::ArithTheoremProducer::lessThanToLERewrite(), CVC3::TheoryArithNew::setup(), and CVC3::ArithTheoremProducerOld::simpleIneqInt().

Expr CVC3::uminusExpr

(

const Expr &

child

)

[inline]

Definition at line 196 of file theory_arith.h.

References UMINUS.

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

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

Definition at line 198 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer3::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducer3::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer3::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer3::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer3::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer3::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer3::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), operator+(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArith3::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::TheoryArithOld::rafineInequalityToInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer3::substitute(), CVC3::ArithTheoremProducer::substitute(), CVC3::TheoryArithOld::tryPropagate(), CVC3::TheoryArithOld::updateSubsumptionDB(), and CVC3::TheoryArith3::updateSubsumptionDB().

Expr CVC3::plusExpr

(

const std::vector< Expr > &

children

)

[inline]

Definition at line 200 of file theory_arith.h.

References DebugAssert, and PLUS.

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

Definition at line 204 of file theory_arith.h.

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

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

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

Definition at line 206 of file theory_arith.h.

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

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

Expr CVC3::multExpr

(

const std::vector< Expr > &

children

)

[inline]

a Mult expr with two or more children

Definition at line 210 of file theory_arith.h.

References DebugAssert, and MULT.

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

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

Definition at line 215 of file theory_arith.h.

References pow(), and POW.

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

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

Definition at line 218 of file theory_arith.h.

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

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

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

Definition at line 220 of file theory_arith.h.

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

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

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

Definition at line 222 of file theory_arith.h.

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

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

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

Definition at line 224 of file theory_arith.h.

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

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

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

Definition at line 226 of file theory_arith.h.

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

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

Expr CVC3::operator-

(

const Expr &

child

)

[inline]

Definition at line 229 of file theory_arith.h.

References uminusExpr().

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

Definition at line 231 of file theory_arith.h.

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

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

Definition at line 233 of file theory_arith.h.

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

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

Definition at line 235 of file theory_arith.h.

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

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

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

Definition at line 237 of file theory_arith.h.

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

bool CVC3::isArray

(

const Type &

t

)

[inline]

Definition at line 109 of file theory_array.h.

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

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

bool CVC3::isRead

(

const Expr &

e

)

[inline]

Definition at line 110 of file theory_array.h.

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

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

bool CVC3::isWrite

(

const Expr &

e

)

[inline]

Definition at line 111 of file theory_array.h.

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

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

bool CVC3::isArrayLiteral

(

const Expr &

e

)

[inline]

Definition at line 112 of file theory_array.h.

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

Type CVC3::arrayType	(	const Type &	type1,
		const Type &	type2
	)			[inline]

Definition at line 116 of file theory_array.h.

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

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

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

Definition at line 1181 of file theory_array.cpp.

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

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

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

Printing NotifyList class.

Definition at line 97 of file theory_core.cpp.

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

bool CVC3::isDatatype

(

const Type &

t

)

[inline]

Definition at line 133 of file theory_datatype.h.

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

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

bool CVC3::isConstructor

(

const Expr &

e

)

[inline]

Definition at line 136 of file theory_datatype.h.

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

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

bool CVC3::isSelector

(

const Expr &

e

)

[inline]

Definition at line 140 of file theory_datatype.h.

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

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

bool CVC3::isTester

(

const Expr &

e

)

[inline]

Definition at line 143 of file theory_datatype.h.

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

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

Expr CVC3::getConstructor

(

const Expr &

e

)

[inline]

Definition at line 146 of file theory_datatype.h.

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

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

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

Definition at line 168 of file type.h.

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

Definition at line 171 of file type.h.

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

Definition at line 175 of file type.h.

Literal CVC3::operator!

(

const Variable &

v

)

[inline]

Definition at line 188 of file variable.h.

Literal CVC3::operator!

(

const Literal &

l

)

[inline]

Definition at line 192 of file variable.h.

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

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

Definition at line 217 of file variable.cpp.

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

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

Definition at line 135 of file clause.cpp.

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

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

Definition at line 157 of file clause.cpp.

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

Referenced by operator<<().

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

Definition at line 164 of file clause.cpp.

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

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

Definition at line 202 of file variable.cpp.

References CVC3::Variable::d_val.

ostream& CVC3::operator<<	(	std::ostream &	os,
		const VariableValue &	v
	)

Definition at line 337 of file variable.cpp.

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

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

Definition at line 301 of file assumptions.cpp.

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

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

Definition at line 311 of file assumptions.cpp.

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

ostream& CVC3::operator<<	(	std::ostream &	os,
		const Assumptions &	assump
	)

Definition at line 321 of file assumptions.cpp.

References CVC3::Assumptions::d_vector.

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

Compare Theorems by their expressions. Return -1, 0, or 1.

This is an arbitrary total ordering on Theorems. For simplicity, we define rewrite theorems (e1 = e2 or e1 <=> e2) to be smaller than other theorems.

Definition at line 45 of file theorem.cpp.

References compare(), CVC3::Theorem::d_thm, CVC3::Theorem::getExpr(), CVC3::Theorem::isNull(), and CVC3::Theorem::isRewrite().

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

Definition at line 65 of file theorem.cpp.

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

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

Definition at line 83 of file theorem.cpp.

References CVC3::Theorem::d_thm.

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

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

Definition at line 44 of file theory_arith3.cpp.

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

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

Definition at line 54 of file theory_arith3.cpp.

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

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

Definition at line 44 of file theory_arith_new.cpp.

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

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

Definition at line 54 of file theory_arith_new.cpp.

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

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

Definition at line 46 of file theory_arith_old.cpp.

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

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

Definition at line 56 of file theory_arith_old.cpp.

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

---

Variable Documentation

const unsigned CVC3::chunkSizeBytes = 16384

Definition at line 30 of file memory_manager_context.h.

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

ParserTemp* CVC3::parserTemp

---