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 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
Author: 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 unsigned long Unsigned
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 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.
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)
std::string to_upper (const std::string &src)
std::string to_lower (const std::string &src)
std::string int2string (int n)
template<class T > T abs (T t)
template<class T > T max (T a, T b)
template<class T > std::pair< std::string, T > strPair (const std::string &f, const T &t)
template<class T > void sort2 (std::vector< std::string > &keys, std::vector< T > &vals)
Sort two vectors based on the first vector.
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 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 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 into Simplify format 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().

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.

template<class T >

T CVC3::abs ( T t ) [inline]

Definition at line 53 of file cvc_util.h.

Referenced by CVC3::TheoryArithOld::canPickEqMonomial(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), SAT::Lit::getVar(), SAT::Lit::isVar(), operator<(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), and CVC3::TheoryArith3::pickIntEqMonomial().

template<class T >

T CVC3::max	(	T	a,
		T	b
	)			`[inline]`

Definition at line 56 of file cvc_util.h.

template<class T >

std::pair<std::string,T> CVC3::strPair	(	const std::string &	f,
		const T &	t
	)			`[inline]`

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
	)			`[inline]`

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

References AND, and DebugAssert.

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

References DebugAssert, and OR.

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

Definition at line 1563 of file expr.h.

References CVC3::Expr::d_expr.

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

Definition at line 1568 of file expr.h.

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

Definition at line 1573 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1575 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1577 of file expr.h.

References CVC3::Expr::compare.

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

Definition at line 1579 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().

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

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

Definition at line 166 of file rational.h.

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

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

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

Definition at line 183 of file rational.h.

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

Definition at line 184 of file rational.h.

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

Definition at line 186 of file rational.h.

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

Definition at line 188 of file rational.h.

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

Definition at line 190 of file rational.h.

void CVC3::printRational ( const Rational & x )

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

Definition at line 311 of file search_sat.h.

References abs(), CVC3::SearchSat::SearchSat::LitPriorityPair::d_lit, CVC3::SearchSat::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.

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

Definition at line 176 of file theory_arith.h.

References CVC3::Expr::isRational().

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.

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.

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.

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

Definition at line 185 of file theory_arith.h.

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

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

Definition at line 186 of file theory_arith.h.

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

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

Definition at line 187 of file theory_arith.h.

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

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

Definition at line 188 of file theory_arith.h.

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

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.

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

Definition at line 191 of file theory_arith.h.

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

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

Definition at line 193 of file theory_arith.h.

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

Expr CVC3::uminusExpr ( const Expr & child ) [inline]

Definition at line 196 of file theory_arith.h.

References UMINUS.

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

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

Definition at line 198 of file theory_arith.h.

References PLUS.

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

Definition at line 200 of file theory_arith.h.

References DebugAssert, and PLUS.

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

Definition at line 204 of file theory_arith.h.

References MINUS.

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

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

Definition at line 206 of file theory_arith.h.

References MULT.

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.

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

Definition at line 218 of file theory_arith.h.

References DIVIDE.

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

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

Definition at line 220 of file theory_arith.h.

References LT.

Referenced by CVC3::ArithTheoremProducerOld::canonMult(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::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.

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

Definition at line 224 of file theory_arith.h.

References GT.

Referenced by CVC3::TheoryArith3::assertFact(), CVC3::ArithTheoremProducerOld::diseqToIneq(), CVC3::ArithTheoremProducer3::diseqToIneq(), CVC3::ArithTheoremProducer::diseqToIneq(), CVC3::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.

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

Definition at line 229 of file theory_arith.h.

References uminusExpr().

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

Definition at line 231 of file theory_arith.h.

References plusExpr().

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

Definition at line 233 of file theory_arith.h.

References minusExpr().

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

Definition at line 235 of file theory_arith.h.

References multExpr().

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

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

Definition at line 237 of file theory_arith.h.

References divideExpr().

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

Definition at line 109 of file theory_array.h.

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

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

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

Definition at line 110 of file theory_array.h.

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

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

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

Definition at line 111 of file theory_array.h.

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

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

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

Definition at line 112 of file theory_array.h.

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

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

Definition at line 116 of file theory_array.h.

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

Referenced by CVC3::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::dataType(), CVC3::TheoryDatatype::getConsPos(), CVC3::TheoryDatatype::getConstant(), CVC3::TheoryDatatype::getReachablePredicate(), and CVC3::DatatypeTheoremProducer::noCycle().

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

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(), IF_DEBUG, CVC3::Clause::isNull(), CVC3::Clause::sat(), CVC3::Clause::size(), and CVC3::Clause::wp().

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

Definition at line 157 of file clause.cpp.

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

Referenced by operator<<().

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

Definition at line 164 of file clause.cpp.

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

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

Definition at line 202 of file variable.cpp.

References CVC3::Variable::d_val.

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

Definition at line 337 of file variable.cpp.

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

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

Definition at line 301 of file assumptions.cpp.

References CVC3::Assumptions::begin(), 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::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::getLHS(), CVC3::Theorem::getRHS(), CVC3::Theorem::isNull(), and CVC3::Theorem::isRewrite().

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

Definition at line 65 of file theorem.cpp.

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

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

Definition at line 83 of file theorem.cpp.

References CVC3::Theorem::d_thm.

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

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

Definition at line 44 of file theory_arith3.cpp.

References CVC3::TheoryArith3::TheoryArith3::FreeConst::getConst(), and CVC3::TheoryArith3::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::TheoryArith3::Ineq::getConst(), CVC3::Theorem::getExpr(), CVC3::TheoryArith3::TheoryArith3::Ineq::ineq(), and CVC3::TheoryArith3::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::TheoryArithNew::FreeConst::getConst(), and CVC3::TheoryArithNew::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::TheoryArithNew::Ineq::getConst(), CVC3::Theorem::getExpr(), CVC3::TheoryArithNew::TheoryArithNew::Ineq::ineq(), and CVC3::TheoryArithNew::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::TheoryArithOld::FreeConst::getConst(), and CVC3::TheoryArithOld::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::TheoryArithOld::Ineq::getConst(), CVC3::Theorem::getExpr(), CVC3::TheoryArithOld::TheoryArithOld::Ineq::ineq(), and CVC3::TheoryArithOld::TheoryArithOld::Ineq::varOnRHS().

Variable Documentation

const unsigned CVC3::chunkSizeBytes = 16384

Definition at line 29 of file memory_manager_context.h.

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

ParserTemp* CVC3::parserTemp