CVCL Namespace Reference

Classes

class Assumptions
class AVHash
class AssumptionsValue
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 DebugException
Our exception to throw. More...
class DebugFlag
Boolean flag (can only be true or false). More...
class DebugCounter
Integer counter for debugging purposes. More...
class DebugTimer
Time counter. More...
class Debug
The heart of the Bug Extermination Kingdom. More...
class EvalException
class Exception
class Expr
Data structure of expressions in CVC Lite. 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 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 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 TheoryArray
This theory handles arrays. More...
class TheoryBitvector
Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG). More...
class TheoryCore
This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories. More...
class TheoryDatatype
This theory handles datatypes. More...
class TheoryDatatypeLazy
This theory handles datatypes. More...
class TheoryQuant
This theory handles quantifiers. More...
class TheoryRecords
This theory handles records. More...
class TheorySimulate
"Theory" of symbolic simulation. More...
class TheoryUF
This theory handles uninterpreted functions. More...
class Translator
class 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 SearchEngineTheoremProducer
class SVC_API_impl
class CommonTheoremProducer
class TheoremValue
class RWTheoremValue
class ReflexivityTheoremValue
A special subclass for reflexivity theorems: e = e and e <=> e. More...
class ArithException
class ArithProofRules
class ArithTheoremProducer
class RefinedArithTheoremProducer
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 Dict_Entry
class Dict
class Dict_Ptr
struct _Hashtable_iterator
struct _Hashtable_const_iterator
class Hash_Entry
class Hash_Table
class Hash_Ptr
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
class DebugTime

Typedefs

typedef std::pair< std::string,
std::string > StrPair
typedef long long unsigned ExprIndex
Expression index type.
typedef std::map< Theorem,
bool, TheoremLess > TheoremMap
typedef std::map< const std::string,
Expr, ltstr > Str_To_Expr
typedef void * void_ptr
typedef void * void_pointer

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 Kind {
  NULL_KIND = 0, RAW_LIST, ID, STRING_EXPR,
  RATIONAL_EXPR, TRUE, FALSE, BOOLEAN,
  ARROW, TYPE, TYPEDECL, TYPEDEF,
  EQ, NEQ, 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, CONTEXT, FORGET,
  GET_TYPE, CHECK_TYPE, GET_CHILD, SUBSTITUTE,
  SEQ, TCC, VARDECL, VARDECLS,
  BOUND_VAR, BOUND_ID, SUBTYPE, IF,
  IFTHEN, ELSE, COND, LET,
  LETDECLS, LETDECL, LAMBDA, SIMULATE,
  CONSTDEF, CONST, VARLIST, UCONST,
  DEFUN, PF_APPLY, PF_HOLE, SKOLEM_VAR,
  LAST_KIND
}
enum InputLanguage { PRESENTATION_LANG, SMTLIB_LANG, LISP_LANG, AST_LANG }
Different input languages. More...
enum ArithKinds {
  REAL = 3000, INT, SUBRANGE, UMINUS,
  PLUS, MINUS, MULT, DIVIDE,
  POW, INTDIV, MOD, LT,
  LE, GT, GE, IS_INTEGER,
  NEGINF, POSINF, DARK_SHADOW, GRAY_SHADOW
}
enum ArithLang {
NOT_USED = 0, TERMS_ONLY, DIFF_ONLY, LINEAR,
NONLINEAR
}
Used to keep track of which subset of arith is being used. More...
enum ArrayKinds { ARRAY = 2000, READ, WRITE, ARRAY_LITERAL }
enum BVKinds {
  BITVECTOR = 8000, BVCONST, HEXBVCONST, CONCAT,
  BVOR, BVAND, BVNEG, BVXOR,
  BVNAND, BVNOR, BVXNOR, EXTRACT,
  LEFTSHIFT, RIGHTSHIFT, VARSHIFT, BVPLUS,
  BVSUB, BVUMINUS, BVMULT, BOOLEXTRACT,
  BVLT, BVLE, BVGT, BVGE,
  SBVLT, SBVLE, SBVGT, SBVGE,
  SX, SRIGHTSHIFT, INTTOBV, BVTOINT,
  BVTYPEPRED, BVPARAMOP
}
enum DatatypeKinds { DATATYPE = 600, CONSTRUCTOR, SELECTOR, TESTER }
Local kinds for datatypes. More...
enum RecordKinds {
RECORD = 2500, RECORD_SELECT, RECORD_UPDATE, RECORD_TYPE,
TUPLE, TUPLE_SELECT, TUPLE_UPDATE, TUPLE_TYPE
}
enum UFKinds { TRANS_CLOSURE = 500, OLD_ARROW, ANY_TYPE }
Local kinds for transitive closure of binary relations. 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)
bool operator== (const AssumptionsValue &a1, const AssumptionsValue &a2)
bool operator!= (const AssumptionsValue &a1, const AssumptionsValue &a2)
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.
void fatalError (const std::string &file, int line, const std::string &cond, const std::string &msg)
Function for fatal exit.
void debugError (const std::string &file, int line, const std::string &cond, const std::string &msg) throw (Exception)
Similar to fatalError to raise an exception when DebugAssert fires.
bool operator== (const DebugFlag &f1, const DebugFlag &f2)
Checks if the *values* of the flags are equal.
bool operator!= (const DebugFlag &f1, const DebugFlag &f2)
Checks if the *values* of the flags are disequal.
std::ostream & operator<< (std::ostream &os, const DebugFlag &f)
Printing flags.
bool operator== (const DebugCounter &c1, const DebugCounter &c2)
bool operator!= (const DebugCounter &c1, const DebugCounter &c2)
bool operator== (int c1, const DebugCounter &c2)
bool operator!= (int c1, const DebugCounter &c2)
bool operator== (const DebugCounter &c1, int c2)
bool operator!= (const DebugCounter &c1, int c2)
std::ostream & operator<< (std::ostream &os, const DebugCounter &c)
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 (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 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 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)
Assumptions merge (const Theorem &t1, const Theorem &t2)
Assumptions merge (const Assumptions &a, const Theorem &t)
Assumptions merge (const Theorem &t, const Assumptions &a)
Assumptions merge (const std::vector< Theorem > &t)
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 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)
Rational computeBVConst (const Expr &e)
computes the integer value of a bitvector constant
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 Literal &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)
bool operator== (const Assumptions &a1, const Assumptions &a2)
bool operator!= (const Assumptions &a1, const Assumptions &a2)
ostream & operator<< (ostream &os, const AssumptionsValue &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 TheoryArith::FreeConst &fc)
ostream & operator<< (ostream &os, const TheoryArith::Ineq &ineq)
template<class _Key, class _Data> std::ostream & operator<< (std::ostream &cout, Dict_Entry< _Key, _Data > &element)
template<class _Key, class _Data> std::ostream & operator<< (std::ostream &cout, Dict< _Key, _Data > &dict)
template<class _Key> static size_t hash (_Key e)
template<class _Key> static size_t equal_to (_Key x, _Key y)
template<class InputIterator> void insert (InputIterator l, InputIterator r)
template<class _Key, class _Data> void HashUpdateIntData (Hash_Table< _Key, _Data > &t, _Key key, _Data i)
ostream & operator<< (ostream &os, const NotifyList &l)
DebugTime operator+ (const DebugTime &t1, const DebugTime &t2)
DebugTime operator- (const DebugTime &t1, const DebugTime &t2)
bool operator== (const DebugTime &t1, const DebugTime &t2)
bool operator!= (const DebugTime &t1, const DebugTime &t2)
bool operator== (const DebugTimer &t1, const DebugTimer &t2)
bool operator!= (const DebugTimer &t1, const DebugTimer &t2)
bool operator< (const DebugTimer &t1, const DebugTimer &t2)
bool operator> (const DebugTimer &t1, const DebugTimer &t2)
bool operator<= (const DebugTimer &t1, const DebugTimer &t2)
bool operator>= (const DebugTimer &t1, const DebugTimer &t2)
ostream & operator<< (ostream &os, const DebugTime &t)
ostream & operator<< (ostream &os, const DebugTimer &timer)
ostream & operator<< (ostream &os, const Rational &n)
static void checkInt (const Rational &n, const string &funName)
Rational gcd (const Rational &x, const Rational &y)
Rational gcd (const vector< Rational > &v)
Rational lcm (const Rational &x, const Rational &y)
Rational lcm (const vector< Rational > &v)
Rational abs (const Rational &x)
Rational floor (const Rational &x)
Rational ceil (const Rational &x)
Rational mod (const Rational &x, const Rational &y)
bool operator== (const Rational &n1, const Rational &n2)
bool operator< (const Rational &n1, const Rational &n2)
bool operator<= (const Rational &n1, const Rational &n2)
bool operator> (const Rational &n1, const Rational &n2)
bool operator>= (const Rational &n1, const Rational &n2)
bool operator!= (const Rational &n1, const Rational &n2)
Rational operator+ (const Rational &n1, const Rational &n2)
Rational operator- (const Rational &n1, const Rational &n2)
Rational operator * (const Rational &n1, const Rational &n2)
Rational operator/ (const Rational &n1, const Rational &n2)
Rational operator% (const Rational &n1, const Rational &n2)
static long int plus (long int x, long int y)
Add two integers and check for overflows.
static long int uminus (long int x)
Unary minus which checks for overflows.
static long int mult (long int x, long int y)
Multiply two integers and check for overflows.
static long int gcd (long int n1, long int n2)
Compute GCD using Euclid's algorithm (from Aaron Stump's code).
static long int lcm (long int n1, long int n2)
Compute LCM.

Variables

Typedef Documentation

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

Definition at line 53 of file cvclutil.h.

typedef long long unsigned CVCL::ExprIndex

Expression index type.

Definition at line 87 of file expr.h.

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

Definition at line 369 of file theorem.h.

typedef std::map<const std::string, Expr, ltstr> CVCL::Str_To_Expr

Definition at line 54 of file vcl.h.

typedef void* CVCL::void_ptr

Definition at line 22 of file dictionary.h.

typedef void* CVCL::void_pointer

Definition at line 30 of file hash.h.

Enumeration Type Documentation

enum CVCL::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 41 of file command_line_flags.h.

enum CVCL::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 72 of file expr.h.

enum CVCL::Kind

Enumerator:

NULL_KIND

RAW_LIST May have any number of children >= 0

ID Identifier is (ID (STRING_EXPR "name")).

STRING_EXPR

RATIONAL_EXPR

TRUE

FALSE

BOOLEAN

ARROW

TYPE

TYPEDECL

TYPEDEF

EQ

NEQ

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

CONTEXT

FORGET

GET_TYPE

CHECK_TYPE

GET_CHILD

SUBSTITUTE

SEQ

TCC

VARDECL

VARDECLS

BOUND_VAR

BOUND_ID

SUBTYPE

IF

IFTHEN

ELSE

COND

LET

LETDECLS

LETDECL

LAMBDA

SIMULATE

CONSTDEF

CONST

VARLIST

UCONST

DEFUN

PF_APPLY

PF_HOLE

SKOLEM_VAR

LAST_KIND Must always be the last kind.

Definition at line 37 of file kinds.h.

enum CVCL::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

Definition at line 38 of file lang.h.

enum CVCL::ArithKinds

Enumerator:

REAL

INT

SUBRANGE

UMINUS

PLUS

MINUS

MULT

DIVIDE

POW

INTDIV

MOD

LT

LE

GT

GE

IS_INTEGER

NEGINF

POSINF

DARK_SHADOW

GRAY_SHADOW

Definition at line 40 of file theory_arith.h.

enum CVCL::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 65 of file theory_arith.h.

enum CVCL::ArrayKinds

Enumerator:

ARRAY

READ

WRITE

ARRAY_LITERAL

Definition at line 38 of file theory_array.h.

enum CVCL::BVKinds

Enumerator:

BITVECTOR

BVCONST

HEXBVCONST

CONCAT

BVOR

BVAND

BVNEG

BVXOR

BVNAND

BVNOR

BVXNOR

EXTRACT

LEFTSHIFT

RIGHTSHIFT

VARSHIFT

BVPLUS

BVSUB

BVUMINUS

BVMULT

BOOLEXTRACT

BVLT

BVLE

BVGT

BVGE

SBVLT

SBVLE

SBVGT

SBVGE

SX

SRIGHTSHIFT

INTTOBV

BVTOINT

BVTYPEPRED

BVPARAMOP

Definition at line 40 of file theory_bitvector.h.

enum CVCL::DatatypeKinds

Local kinds for datatypes.

Enumerator:

DATATYPE

CONSTRUCTOR

SELECTOR

TESTER

Definition at line 41 of file theory_datatype.h.

enum CVCL::RecordKinds

Enumerator:

RECORD

RECORD_SELECT

RECORD_UPDATE

RECORD_TYPE

TUPLE

TUPLE_SELECT

TUPLE_UPDATE

TUPLE_TYPE

Definition at line 37 of file theory_records.h.

enum CVCL::UFKinds

Local kinds for transitive closure of binary relations.

Enumerator:

TRANS_CLOSURE

OLD_ARROW

ANY_TYPE

Definition at line 39 of file theory_uf.h.

Function Documentation

static bool CVCL::subExprRec ( const Expr & e1,

const Expr & e2

) [static]

Definition at line 134 of file expr.cpp.
References CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::getFlag(), and CVCL::Expr::setFlag().
Referenced by CVCL::Expr::subExprOf().

int CVCL::compare ( const Expr & e1,

const Expr & e2

)

Definition at line 422 of file expr.cpp.
References CVCL::Expr::d_expr, and CVCL::Expr::getIndex().
Referenced by CVCL::AssumptionsValue::add(), CVCL::AssumptionsValue::AssumptionsValue(), compare(), CVCL::AssumptionsValue::find(), CVCL::Assumptions::findTheorem(), operator<(), operator<=(), operator>(), and operator>=().

ostream& CVCL::operator<< ( ostream & os,

const Expr & e

)

Definition at line 463 of file expr.cpp.
References CVCL::Expr::getEM(), CVCL::Expr::isNull(), CVCL::ExprStream::os(), and CVCL::ExprManager::restoreIndent().

static bool CVCL::isTrivialExpr ( const Expr & e ) [static]

Definition at line 59 of file expr_stream.cpp.
References CVCL::Expr::arity(), CONSTDEF, DIVIDE, CVCL::Expr::getKind(), CVCL::Expr::isClosure(), MINUS, MULT, PLUS, RATIONAL_EXPR, and UMINUS.
Referenced by CVCL::ExprStream::collectShared().

bool CVCL::operator== ( const AssumptionsValue & a1,

const AssumptionsValue & a2

) [inline]

Definition at line 97 of file assumptions_value.h.
References CVCL::AssumptionsValue::d_vector.

bool CVCL::operator!= ( const AssumptionsValue & a1,

const AssumptionsValue & a2

) [inline]

Definition at line 101 of file assumptions_value.h.
References CVCL::AssumptionsValue::d_vector.

template<class T>

T CVCL::abs ( T t )

Definition at line 28 of file cvclutil.h.
Referenced by CVCL::TheoryArith::computeNormalFactor(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), SAT::Lit::getVar(), SAT::Lit::isVar(), and CVCL::TheoryArith::pickIntEqMonomial().

template<class T>

T CVCL::max ( T a,

T b

)

Definition at line 31 of file cvclutil.h.
Referenced by CVCL::Rational::Impl::getInt(), CVCL::Rational::Impl::getUnsigned(), and CVCL::DecisionEngineMBTF::goalSatisfied().

template<class T>

std::pair<std::string,T> CVCL::strPair ( const std::string & f,

const T & t

)

Definition at line 49 of file cvclutil.h.
Referenced by sort2().

template<class T>

void CVCL::sort2 ( std::vector< std::string > & keys,

std::vector< T > & vals

)

Sort two vectors based on the first vector.

Definition at line 57 of file cvclutil.h.
References strPair().

void CVCL::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 41 of file debug.cpp.
References std::endl().

void CVCL::debugError ( const std::string & file,

int line,

const std::string & cond,

const std::string & msg

) throw (Exception)

Similar to fatalError to raise an exception when DebugAssert fires.
This does not necessarily cause the program to quit.
Definition at line 58 of file debug.cpp.

bool CVCL::operator== ( const DebugFlag & f1,

const DebugFlag & f2

) [inline]

Checks if the *values* of the flags are equal.

Definition at line 158 of file debug.h.
References CVCL::DebugFlag::d_flag.

bool CVCL::operator!= ( const DebugFlag & f1,

const DebugFlag & f2

) [inline]

Checks if the *values* of the flags are disequal.

Definition at line 162 of file debug.h.
References CVCL::DebugFlag::d_flag.

std::ostream& CVCL::operator<< ( std::ostream & os,

const DebugFlag & f

) [inline]

Printing flags.

Definition at line 166 of file debug.h.
References CVCL::DebugFlag::d_flag.

bool CVCL::operator== ( const DebugCounter & c1,

const DebugCounter & c2

) [inline]

Definition at line 225 of file debug.h.
References CVCL::DebugCounter::d_counter.

bool CVCL::operator!= ( const DebugCounter & c1,

const DebugCounter & c2

) [inline]

Definition at line 228 of file debug.h.
References CVCL::DebugCounter::d_counter.

bool CVCL::operator== ( int c1,

const DebugCounter & c2

) [inline]

Definition at line 231 of file debug.h.
References CVCL::DebugCounter::d_counter.

bool CVCL::operator!= ( int c1,

const DebugCounter & c2

) [inline]

Definition at line 234 of file debug.h.
References CVCL::DebugCounter::d_counter.

bool CVCL::operator== ( const DebugCounter & c1,

int c2

) [inline]

Definition at line 237 of file debug.h.
References CVCL::DebugCounter::d_counter.

bool CVCL::operator!= ( const DebugCounter & c1,

int c2

) [inline]

Definition at line 240 of file debug.h.
References CVCL::DebugCounter::d_counter.

std::ostream& CVCL::operator<< ( std::ostream & os,

const DebugCounter & c

) [inline]

Definition at line 243 of file debug.h.
References CVCL::DebugCounter::d_counter.

std::ostream& CVCL::operator<< ( std::ostream & os,

const Exception & e

) [inline]

Definition at line 60 of file exception.h.
References CVCL::Exception::toString().

Expr CVCL::andExpr ( const std::vector< Expr > & children ) [inline]

Definition at line 825 of file expr.h.
References AND.
Referenced by CVCL::CoreTheoremProducer::andDistributivityRule(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::TheoryUF::computeModel(), CVCL::TheoryUF::computeTCC(), CVCL::TheorySimulate::computeTCC(), TheoryCore::computeTCC(), CVCL::TheoryArray::computeTCC(), CVCL::Theory::computeTCC(), CVCL::TheoryRecords::computeTypePred(), CVCL::TheoryArith::computeTypePred(), CVCL::SearchEngineTheoremProducer::convertToCNF(), CVCL::DatatypeTheoremProducer::decompose(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::CommonTheoremProducer::implIntro(), CVCL::DatatypeTheoremProducer::noCycle(), TheoryCore::rewrite(), CVCL::CommonTheoremProducer::rewriteAnd(), and CVCL::CoreTheoremProducer::rewriteNotOr().

Expr CVCL::orExpr ( const std::vector< Expr > & children ) [inline]

Definition at line 835 of file expr.h.
References OR.
Referenced by CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::computeCarry(), TheoryCore::computeTCC(), CVCL::SearchEngineTheoremProducer::convertToCNF(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::CoreTheoremProducer::orDistributivityRule(), TheoryCore::rewrite(), CVCL::CoreTheoremProducer::rewriteNotAnd(), and CVCL::CommonTheoremProducer::rewriteOr().

bool CVCL::operator== ( const Expr & e1,

const Expr & e2

) [inline]

Definition at line 1304 of file expr.h.
References CVCL::Expr::d_expr.

bool CVCL::operator!= ( const Expr & e1,

const Expr & e2

) [inline]

Definition at line 1309 of file expr.h.

bool CVCL::operator< ( const Expr & e1,

const Expr & e2

) [inline]

Definition at line 1314 of file expr.h.
References compare().

bool CVCL::operator<= ( const Expr & e1,

const Expr & e2

) [inline]

Definition at line 1316 of file expr.h.
References compare().

bool CVCL::operator> ( const Expr & e1,

const Expr & e2

) [inline]

Definition at line 1318 of file expr.h.
References compare().

bool CVCL::operator>= ( const Expr & e1,

const Expr & e2

) [inline]

Definition at line 1320 of file expr.h.
References compare().

InputLanguage CVCL::getLanguage ( std::string & lang ) [inline]

Definition at line 50 of file lang.h.
References AST_LANG, LISP_LANG, PRESENTATION_LANG, and SMTLIB_LANG.
Referenced by CVCL::ExprManager::getInputLang(), and CVCL::ExprManager::getOutputLang().

std::ostream& CVCL::operator<< ( std::ostream & os,

const Proof & pf

) [inline]

Definition at line 64 of file proof.h.
References CVCL::Proof::getExpr().

bool CVCL::operator== ( const Proof & pf1,

const Proof & pf2

) [inline]

Definition at line 68 of file proof.h.
References CVCL::Proof::getExpr().

Rational CVCL::pow ( Rational pow,

const Rational & base

) [inline]

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

Definition at line 159 of file rational.h.
References CVCL::Rational::isInteger(), and CVCL::Rational::toString().
Referenced by CVCL::ArithTheoremProducer::canonPowConst().

Rational CVCL::newRational ( int n,

int d = 1

) [inline]

Definition at line 173 of file rational.h.

Rational CVCL::newRational ( const char * n,

int base = 10

) [inline]

Definition at line 174 of file rational.h.

Rational CVCL::newRational ( const std::string & n,

int base = 10

) [inline]

Definition at line 176 of file rational.h.

Rational CVCL::newRational ( const char * n,

const char * d,

int base = 10

) [inline]

Definition at line 178 of file rational.h.

Rational CVCL::newRational ( const std::string & n,

const std::string & d,

int base = 10

) [inline]

Definition at line 180 of file rational.h.

void CVCL::printRational ( const Rational & x )

bool CVCL::operator== ( const StatFlag & f1,

const StatFlag & f2

) [inline]

Definition at line 74 of file statistics.h.
References CVCL::StatFlag::d_flag.

bool CVCL::operator!= ( const StatFlag & f1,

const StatFlag & f2

) [inline]

Definition at line 77 of file statistics.h.
References CVCL::StatFlag::d_flag.

std::ostream& CVCL::operator<< ( std::ostream & os,

const StatFlag & f

) [inline]

Definition at line 80 of file statistics.h.
References CVCL::StatFlag::d_flag.

bool CVCL::operator== ( const StatCounter & c1,

const StatCounter & c2

) [inline]

Definition at line 130 of file statistics.h.
References CVCL::StatCounter::d_counter.

bool CVCL::operator!= ( const StatCounter & c1,

const StatCounter & c2

) [inline]

Definition at line 133 of file statistics.h.
References CVCL::StatCounter::d_counter.

bool CVCL::operator== ( int c1,

const StatCounter & c2

) [inline]

Definition at line 136 of file statistics.h.
References CVCL::StatCounter::d_counter.

bool CVCL::operator!= ( int c1,

const StatCounter & c2

) [inline]

Definition at line 139 of file statistics.h.
References CVCL::StatCounter::d_counter.

bool CVCL::operator== ( const StatCounter & c1,

int c2

) [inline]

Definition at line 142 of file statistics.h.
References CVCL::StatCounter::d_counter.

bool CVCL::operator!= ( const StatCounter & c1,

int c2

) [inline]

Definition at line 145 of file statistics.h.
References CVCL::StatCounter::d_counter.

std::ostream& CVCL::operator<< ( std::ostream & os,

const StatCounter & c

) [inline]

Definition at line 148 of file statistics.h.
References CVCL::StatCounter::d_counter.

Assumptions CVCL::merge ( const Theorem & t1,

const Theorem & t2

) [inline]

Definition at line 384 of file theorem.h.
Referenced by CVCL::CommonTheoremProducer::contradictionRule(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::CommonTheoremProducer::iffMP(), CVCL::CommonTheoremProducer::implMP(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::CoreTheoremProducer::queryTCC(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::UFTheoremProducer::relTrans(), and CVCL::CommonTheoremProducer::transitivityRule().

Assumptions CVCL::merge ( const Assumptions & a,

const Theorem & t

) [inline]

Definition at line 387 of file theorem.h.
References CVCL::Assumptions::add(), and CVCL::Assumptions::copy().

Assumptions CVCL::merge ( const Theorem & t,

const Assumptions & a

) [inline]

Definition at line 392 of file theorem.h.
References CVCL::Assumptions::add(), and CVCL::Assumptions::copy().

Assumptions CVCL::merge ( const std::vector< Theorem > & t ) [inline]

Definition at line 397 of file theorem.h.

bool CVCL::operator< ( const Theorem & t1,

const Theorem & t2

) [inline]

Definition at line 401 of file theorem.h.
References compare().

bool CVCL::operator<= ( const Theorem & t1,

const Theorem & t2

) [inline]

Definition at line 403 of file theorem.h.
References compare().

bool CVCL::operator> ( const Theorem & t1,

const Theorem & t2

) [inline]

Definition at line 405 of file theorem.h.
References compare().

bool CVCL::operator>= ( const Theorem & t1,

const Theorem & t2

) [inline]

Definition at line 407 of file theorem.h.
References compare().

bool CVCL::isReal ( Type t ) [inline]

Definition at line 384 of file theory_arith.h.
References CVCL::Type::getExpr(), CVCL::Expr::getKind(), and REAL.
Referenced by CVCL::TheorySimulate::computeType(), CVCL::TheoryArith::isIntegerThm(), CVCL::TheoryArith::processRealEq(), and CVCL::TheoryArith::refineCounterExample().

bool CVCL::isInt ( Type t ) [inline]

Definition at line 385 of file theory_arith.h.
References CVCL::Type::getExpr(), CVCL::Expr::getKind(), and INT.
Referenced by CVCL::TheoryArith::computeType(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::print(), and CVCL::TheoryArith::projectInequalities().

bool CVCL::isIntegerConst ( const Expr & e ) [inline]

Definition at line 389 of file theory_arith.h.
References CVCL::Expr::getRational(), CVCL::Rational::isInteger(), and CVCL::Expr::isRational().
Referenced by CVCL::TheoryArith::checkType().

bool CVCL::isUMinus ( const Expr & e ) [inline]

Definition at line 391 of file theory_arith.h.
References CVCL::Expr::getKind(), and UMINUS.
Referenced by CVCL::TheoryArith::isSyntacticRational(), and CVCL::TheoryArith::isSyntacticUMinusVar().

bool CVCL::isMinus ( const Expr & e ) [inline]

Definition at line 393 of file theory_arith.h.
References CVCL::Expr::getKind(), and MINUS.
Referenced by CVCL::TheoryArith::printRational().

bool CVCL::isDivide ( const Expr & e ) [inline]

Definition at line 395 of file theory_arith.h.
References DIVIDE, and CVCL::Expr::getKind().
Referenced by CVCL::TheoryArith::isSyntacticRational().

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

Definition at line 397 of file theory_arith.h.
References CVCL::Expr::getKind(), and LE.
Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::finiteInterval(), isIneq(), CVCL::TheoryArith::isolateVariable(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::projectInequalities(), CVCL::ArithTheoremProducer::realShadow(), CVCL::ArithTheoremProducer::realShadowEq(), CVCL::TheoryArith::setup(), and CVCL::TheoryArith::updateSubsumptionDB().

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

Definition at line 398 of file theory_arith.h.
References CVCL::Expr::getKind(), and GT.
Referenced by CVCL::ArithTheoremProducer::flipInequality(), isIneq(), CVCL::ArithTheoremProducer::negatedInequality(), and CVCL::TheoryArith::rewrite().

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

Definition at line 399 of file theory_arith.h.
References GE, and CVCL::Expr::getKind().
Referenced by CVCL::ArithTheoremProducer::flipInequality(), isIneq(), and CVCL::TheoryArith::rewrite().

bool CVCL::isDarkShadow ( const Expr & e ) [inline]

Definition at line 400 of file theory_arith.h.
References DARK_SHADOW, and CVCL::Expr::getKind().
Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::expandDarkShadow(), and CVCL::TheoryArith::setup().

bool CVCL::isGrayShadow ( const Expr & e ) [inline]

Definition at line 401 of file theory_arith.h.
References CVCL::Expr::getKind(), and GRAY_SHADOW.
Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::ArithTheoremProducer::expandGrayShadow0(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::TheoryArith::setup(), and CVCL::ArithTheoremProducer::splitGrayShadow().

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

Definition at line 402 of file theory_arith.h.
References isGE(), isGT(), isLE(), and isLT().
Referenced by CVCL::TheoryArith::freeConstIneq(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::TheoryArith::normalize(), CVCL::TheoryArith::print(), CVCL::TheoryArith::printMinus(), CVCL::TheoryArith::printPlus(), CVCL::TheoryArith::printRational(), CVCL::TheoryArith::rewrite(), and CVCL::TheoryArith::update().

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

Definition at line 404 of file theory_arith.h.
References CVCL::Expr::getKind(), and IS_INTEGER.
Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), and CVCL::ArithTheoremProducer::lessThanToLE().

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

Definition at line 407 of file theory_arith.h.
References UMINUS.
Referenced by operator-(), and CVCL::TheoryArith::parseExprOp().

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

Definition at line 411 of file theory_arith.h.
References PLUS.

Expr CVCL::minusExpr ( const Expr & left,

const Expr & right

) [inline]

Definition at line 415 of file theory_arith.h.
References MINUS.
Referenced by CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), operator-(), and CVCL::TheoryArith::parseExprOp().

Expr CVCL::multExpr ( const Expr & left,

const Expr & right

) [inline]

Definition at line 417 of file theory_arith.h.
References MULT.
Referenced by CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::ArithTheoremProducer::monomialMulF(), operator *(), CVCL::TheoryArith::parseExprOp(), CVCL::TheoryArith::separateMonomial(), and CVCL::ArithTheoremProducer::simplifiedMultExpr().

Expr CVCL::multExpr ( const std::vector< Expr > & children ) [inline]

a Mult expr with two or more children

Definition at line 421 of file theory_arith.h.
References MULT.

Expr CVCL::powExpr ( const Expr & pow,

const Expr & base

) [inline]

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

Definition at line 426 of file theory_arith.h.
References POW.
Referenced by CVCL::ArithTheoremProducer::canonInvertLeaf(), CVCL::ArithTheoremProducer::canonInvertPow(), CVCL::ArithTheoremProducer::canonMultLeafLeaf(), CVCL::ArithTheoremProducer::canonMultLeafOrPowMult(), CVCL::ArithTheoremProducer::canonMultPowLeaf(), CVCL::ArithTheoremProducer::canonMultPowPow(), CVCL::TheoryArith::parseExprOp(), and CVCL::VCL::powExpr().

Expr CVCL::divideExpr ( const Expr & left,

const Expr & right

) [inline]

Definition at line 429 of file theory_arith.h.
References DIVIDE.
Referenced by CVCL::VCL::divideExpr(), operator/(), and CVCL::TheoryArith::parseExprOp().

Expr CVCL::ltExpr ( const Expr & left,

const Expr & right

) [inline]

Definition at line 431 of file theory_arith.h.
References LT.
Referenced by CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::VCL::ltExpr(), and CVCL::TheoryArith::parseExprOp().

Expr CVCL::leExpr ( const Expr & left,

const Expr & right

) [inline]

Definition at line 433 of file theory_arith.h.
References LE.
Referenced by CVCL::TheoryArith::computeTypePred(), CVCL::ArithTheoremProducer::expandDarkShadow(), CVCL::ArithTheoremProducer::expandGrayShadow(), CVCL::VCL::leExpr(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::TheoryArith::parseExprOp(), and CVCL::TheoryArith::updateSubsumptionDB().

Expr CVCL::gtExpr ( const Expr & left,

const Expr & right

) [inline]

Definition at line 435 of file theory_arith.h.
References GT.
Referenced by CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::VCL::gtExpr(), and CVCL::TheoryArith::parseExprOp().

Expr CVCL::geExpr ( const Expr & left,

const Expr & right

) [inline]

Definition at line 437 of file theory_arith.h.
References GE.
Referenced by CVCL::VCL::geExpr(), and CVCL::TheoryArith::parseExprOp().

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

Definition at line 440 of file theory_arith.h.
References uminusExpr().

Expr CVCL::operator+ ( const Expr & left,

const Expr & right

) [inline]

Definition at line 442 of file theory_arith.h.
References plusExpr().

Expr CVCL::operator- ( const Expr & left,

const Expr & right

) [inline]

Definition at line 444 of file theory_arith.h.
References minusExpr().

Expr CVCL::operator * ( const Expr & left,

const Expr & right

) [inline]

Definition at line 446 of file theory_arith.h.
References multExpr().

Expr CVCL::operator/ ( const Expr & left,

const Expr & right

) [inline]

Definition at line 448 of file theory_arith.h.
References divideExpr().

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

Definition at line 99 of file theory_array.h.
References ARRAY, CVCL::Type::getExpr(), and CVCL::Expr::getKind().
Referenced by CVCL::TheoryArray::computeModel(), and CVCL::TheoryArray::computeType().

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

Definition at line 100 of file theory_array.h.
References CVCL::Expr::getKind(), and READ.
Referenced by CVCL::TheoryArray::computeModel(), CVCL::TheoryArray::computeModelTerm(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::TheoryArray::setup(), and CVCL::TheoryArray::update().

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

Definition at line 101 of file theory_array.h.
References CVCL::Expr::getKind(), and WRITE.
Referenced by CVCL::ArrayTheoremProducer::interchangeIndices(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite2(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::TheoryArray::setup(), CVCL::TheoryArray::solve(), and CVCL::TheoryArray::update().

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

Definition at line 102 of file theory_array.h.
References ARRAY_LITERAL, CVCL::Expr::getKind(), and CVCL::Expr::isClosure().

Type CVCL::arrayType ( const Type & type1,

const Type & type2

) [inline]

Definition at line 106 of file theory_array.h.
References ARRAY, and CVCL::Type::getExpr().
Referenced by CVCL::VCL::arrayType(), and CVCL::TheoryArray::computeType().

Expr CVCL::arrayLiteral ( const Expr & ind,

const Expr & body

)

Definition at line 744 of file theory_array.cpp.
References ARRAY_LITERAL, CVCL::Expr::getEM(), and CVCL::ExprManager::newClosureExpr().
Referenced by CVCL::TheoryArray::computeModel().

Rational CVCL::computeBVConst ( const Expr & e )

computes the integer value of a bitvector constant

Definition at line 4240 of file theory_bitvector.cpp.
References BVCONST, CVCL::Expr::getExprValue(), CVCL::Expr::getKind(), CVCL::BVConstExpr::getValue(), CVCL::BVConstExpr::size(), and CVCL::Expr::toString().

std::ostream& CVCL::operator<< ( std::ostream & os,

const NotifyList & l

)

Printing NotifyList class.

bool CVCL::isDatatype ( const Type & t ) [inline]

Definition at line 132 of file theory_datatype.h.
References DATATYPE, CVCL::Type::getExpr(), and CVCL::Expr::getKind().
Referenced by CVCL::TheoryDatatype::getConsPos(), CVCL::TheoryDatatype::getConstant(), CVCL::TheoryDatatype::getReachablePredicate(), and CVCL::DatatypeTheoremProducer::noCycle().

bool CVCL::isSelector ( const Expr & e ) [inline]

Definition at line 139 of file theory_datatype.h.
References CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), and SELECTOR.
Referenced by CVCL::TheoryDatatype::canCollapse(), CVCL::TheoryDatatype::checkSat(), CVCL::TheoryDatatype::rewrite(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), CVCL::TheoryDatatypeLazy::setup(), CVCL::TheoryDatatype::setup(), CVCL::TheoryDatatypeLazy::update(), and CVCL::TheoryDatatype::update().

bool CVCL::isTester ( const Expr & e ) [inline]

Definition at line 142 of file theory_datatype.h.
References CVCL::Expr::getOpKind(), CVCL::Expr::isApply(), and TESTER.
Referenced by CVCL::TheoryDatatype::rewrite(), CVCL::DatatypeTheoremProducer::rewriteTestCons(), CVCL::TheoryDatatypeLazy::update(), and CVCL::TheoryDatatype::update().

Expr CVCL::getConstructor ( const Expr & e ) [inline]

Definition at line 145 of file theory_datatype.h.
References CVCL::Expr::getOpExpr(), CVCL::Expr::isApply(), and isConstructor().
Referenced by CVCL::TheoryDatatypeLazy::initializeLabels(), CVCL::TheoryDatatype::initializeLabels(), CVCL::DatatypeTheoremProducer::rewriteSelCons(), and CVCL::DatatypeTheoremProducer::rewriteTestCons().

bool CVCL::operator== ( const Type & t1,

const Type & t2

) [inline]

Definition at line 79 of file type.h.
References CVCL::Type::getExpr().

bool CVCL::operator!= ( const Type & t1,

const Type & t2

) [inline]

Definition at line 82 of file type.h.
References CVCL::Type::getExpr().

std::ostream& CVCL::operator<< ( std::ostream & os,

const Type & t

) [inline]

Definition at line 86 of file type.h.
References CVCL::Type::getExpr().

Literal CVCL::operator! ( const Variable & v ) [inline]

Definition at line 196 of file variable.h.

Literal CVCL::operator! ( const Literal & l ) [inline]

Definition at line 200 of file variable.h.
References CVCL::Literal::getVar(), and CVCL::Literal::isNegative().

std::ostream& CVCL::operator<< ( std::ostream & os,

const Literal & l

)

ostream& CVCL::operator<< ( ostream & os,

const Clause & c

)

Definition at line 143 of file clause.cpp.
References CVCL::Clause::deleted(), CVCL::Clause::dir(), CVCL::Clause::getTheorem(), CVCL::Clause::id(), IF_DEBUG(), CVCL::Clause::isNull(), CVCL::Clause::sat(), CVCL::Clause::size(), and CVCL::Clause::wp().

static void CVCL::printLit ( ostream & os,

const Literal & l

) [static]

Definition at line 165 of file clause.cpp.
References CVCL::Variable::getExpr(), CVCL::Literal::getScope(), CVCL::Literal::getValue(), CVCL::Literal::getVar(), and CVCL::Literal::isNegative().
Referenced by operator<<().

ostream& CVCL::operator<< ( std::ostream & os,

const CompactClause & c

)

Definition at line 172 of file clause.cpp.
References CVCL::CompactClause::d_clause, CVCL::Clause::deleted(), CVCL::Clause::getLiterals(), CVCL::Clause::owners(), printLit(), CVCL::Clause::size(), and CVCL::Clause::wp().

ostream& CVCL::operator<< ( ostream & os,

const Variable & l

)

Definition at line 210 of file variable.cpp.
References CVCL::Variable::d_val.

ostream& CVCL::operator<< ( ostream & os,

const Literal & l

)

Definition at line 225 of file variable.cpp.
References CVCL::Literal::count(), CVCL::Literal::getVar(), CVCL::Literal::isNegative(), and CVCL::Literal::score().

ostream& CVCL::operator<< ( ostream & os,

const VariableValue & v

)

Definition at line 345 of file variable.cpp.
References CVCL::VariableValue::getAntecedent(), CVCL::VariableValue::getAntecedentIdx(), CVCL::VariableValue::getExpr(), CVCL::VariableValue::getScope(), CVCL::VariableValue::getTheorem(), CVCL::VariableValue::getValue(), CVCL::Clause::isNull(), and CVCL::Theorem::isNull().

Assumptions CVCL::operator- ( const Assumptions & a,

const Expr & e

)

Definition at line 321 of file assumptions.cpp.
References CVCL::Assumptions::begin(), CVCL::Assumptions::copy(), CVCL::Assumptions::end(), CVCL::Assumptions::findExpr(), and CVCL::Assumptions::isNull().

Assumptions CVCL::operator- ( const Assumptions & a,

const vector< Expr > & es

)

Definition at line 332 of file assumptions.cpp.
References CVCL::Assumptions::begin(), CVCL::Assumptions::copy(), CVCL::Assumptions::end(), CVCL::Assumptions::findExprs(), and CVCL::Assumptions::isNull().

ostream& CVCL::operator<< ( ostream & os,

const Assumptions & assump

)

Definition at line 343 of file assumptions.cpp.
References CVCL::Assumptions::d_val, and CVCL::Assumptions::isNull().

bool CVCL::operator== ( const Assumptions & a1,

const Assumptions & a2

)

Definition at line 350 of file assumptions.cpp.
References CVCL::Assumptions::d_val.

bool CVCL::operator!= ( const Assumptions & a1,

const Assumptions & a2

)

Definition at line 357 of file assumptions.cpp.
References CVCL::Assumptions::d_val.

ostream& CVCL::operator<< ( ostream & os,

const AssumptionsValue & assump

)

Definition at line 233 of file assumptions_value.cpp.
References CVCL::AssumptionsValue::d_vector.

int CVCL::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 53 of file theorem.cpp.
References compare(), CVCL::Theorem::d_thm, CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Theorem::isNull(), and CVCL::Theorem::isRewrite().

int CVCL::compare ( const Theorem & t1,

const Expr & e2

)

Definition at line 73 of file theorem.cpp.
References compare(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getRHS(), CVCL::Expr::isEq(), CVCL::Expr::isIff(), and CVCL::Theorem::isRewrite().

int CVCL::compareByPtr ( const Theorem & t1,

const Theorem & t2

)

Definition at line 91 of file theorem.cpp.
References CVCL::Theorem::d_thm.
Referenced by CVCL::TheoremLess::operator()().

ostream& CVCL::operator<< ( ostream & os,

const TheoryArith::FreeConst & fc

)

Definition at line 51 of file theory_arith.cpp.
References CVCL::TheoryArith::FreeConst::getConst(), and CVCL::TheoryArith::FreeConst::strict().

ostream& CVCL::operator<< ( ostream & os,

const TheoryArith::Ineq & ineq

)

Definition at line 61 of file theory_arith.cpp.
References CVCL::TheoryArith::Ineq::getConst(), CVCL::Theorem::getExpr(), CVCL::TheoryArith::Ineq::ineq(), and CVCL::TheoryArith::Ineq::varOnRHS().

template<class _Key, class _Data>

std::ostream& CVCL::operator<< ( std::ostream & cout,

Dict_Entry< _Key, _Data > & element

)

Definition at line 249 of file dictionary.h.

template<class _Key, class _Data>

std::ostream& CVCL::operator<< ( std::ostream & cout,

Dict< _Key, _Data > & dict

)

Definition at line 260 of file dictionary.h.

template<class _Key>

static size_t CVCL::hash ( _Key e ) [static]

Definition at line 22 of file hash.h.
Referenced by CVCL::BVConstExpr::computeHash(), CVCL::ExprRational::computeHash(), CVCL::ExprString::computeHash(), CVCL::ExprNode::computeHash(), and CVCL::ExprClosure::computeHash().

template<class _Key>

static size_t CVCL::equal_to ( _Key x,

_Key y

) [static]

Definition at line 24 of file hash.h.

template<class InputIterator>

void CVCL::insert ( InputIterator l,

InputIterator r

)

Definition at line 451 of file hash.h.

template<class _Key, class _Data>

void CVCL::HashUpdateIntData ( Hash_Table< _Key, _Data > & t,

_Key key,

_Data i

)

Definition at line 596 of file hash.h.
References CVCL::Hash_Table< _Key, _Data >::Fetch(), and CVCL::Hash_Table< _Key, _Data >::Insert().

ostream& CVCL::operator<< ( ostream & os,

const NotifyList & l

)

Definition at line 97 of file theory_core.cpp.
References CVCL::NotifyList::getExpr(), CVCL::Theory::getName(), CVCL::NotifyList::getTheory(), and CVCL::NotifyList::size().

DebugTime CVCL::operator+ ( const DebugTime & t1,

const DebugTime & t2

)

Definition at line 116 of file debug.cpp.

DebugTime CVCL::operator- ( const DebugTime & t1,

const DebugTime & t2

)

Definition at line 121 of file debug.cpp.

bool CVCL::operator== ( const DebugTime & t1,

const DebugTime & t2

)

Definition at line 127 of file debug.cpp.
References CVCL::DebugTime::d_tv.

bool CVCL::operator!= ( const DebugTime & t1,

const DebugTime & t2

)

Definition at line 132 of file debug.cpp.

bool CVCL::operator== ( const DebugTimer & t1,

const DebugTimer & t2

)

Definition at line 226 of file debug.cpp.
References CVCL::DebugTimer::d_time.

bool CVCL::operator!= ( const DebugTimer & t1,

const DebugTimer & t2

)

Definition at line 229 of file debug.cpp.
References CVCL::DebugTimer::d_time.

bool CVCL::operator< ( const DebugTimer & t1,

const DebugTimer & t2

)

Definition at line 232 of file debug.cpp.
References CVCL::DebugTimer::d_time.

bool CVCL::operator> ( const DebugTimer & t1,

const DebugTimer & t2

)

Definition at line 237 of file debug.cpp.
References CVCL::DebugTimer::d_time.

bool CVCL::operator<= ( const DebugTimer & t1,

const DebugTimer & t2

)

Definition at line 242 of file debug.cpp.
References CVCL::DebugTimer::d_time.

bool CVCL::operator>= ( const DebugTimer & t1,

const DebugTimer & t2

)

Definition at line 247 of file debug.cpp.
References CVCL::DebugTimer::d_time.

ostream& CVCL::operator<< ( ostream & os,

const DebugTime & t

)

Definition at line 254 of file debug.cpp.
References CVCL::DebugTime::d_tv.

ostream& CVCL::operator<< ( ostream & os,

const DebugTimer & timer

)

Definition at line 258 of file debug.cpp.
References CVCL::DebugTimer::d_time.

ostream & CVCL::operator<< ( ostream & os,

const Rational & n

)

Definition at line 400 of file rational-gmp.cpp.
References CVCL::Rational::toString().

static void CVCL::checkInt ( const Rational & n,

const string & funName

) [static]

Definition at line 407 of file rational-gmp.cpp.
References CVCL::Rational::isInteger(), CVCL::Rational::toString(), and TRACE.
Referenced by gcd(), CVCL::Rational::getInt(), CVCL::Rational::getUnsigned(), lcm(), and mod().

Rational CVCL::gcd ( const Rational & x,

const Rational & y

)

Definition at line 418 of file rational-gmp.cpp.
References checkInt(), and CVCL::Rational::d_n.
Referenced by CVCL::TheoryArith::computeNormalFactor(), gcd(), and lcm().

Rational CVCL::gcd ( const vector< Rational > & v )

Definition at line 424 of file rational-gmp.cpp.
References checkInt(), and gcd().

Rational CVCL::lcm ( const Rational & x,

const Rational & y

)

Definition at line 440 of file rational-gmp.cpp.
References checkInt(), and CVCL::Rational::d_n.
Referenced by CVCL::TheoryArith::computeNormalFactor(), and lcm().

Rational CVCL::lcm ( const vector< Rational > & v )

Definition at line 446 of file rational-gmp.cpp.
References checkInt(), and lcm().

Rational CVCL::abs ( const Rational & x )

Definition at line 456 of file rational-gmp.cpp.

Rational CVCL::floor ( const Rational & x )

Definition at line 461 of file rational-gmp.cpp.
References CVCL::Rational::d_n.
Referenced by CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::ArithTheoremProducer::f(), CVCL::ArithTheoremProducer::grayShadowConst(), CVCL::ArithTheoremProducer::modEq(), and CVCL::ArithTheoremProducer::splitGrayShadow().

Rational CVCL::ceil ( const Rational & x )

Definition at line 465 of file rational-gmp.cpp.
References CVCL::Rational::d_n.
Referenced by CVCL::TheoryArith::assignVariables(), and CVCL::ArithTheoremProducer::grayShadowConst().

Rational CVCL::mod ( const Rational & x,

const Rational & y

)

Definition at line 469 of file rational-gmp.cpp.
References checkInt(), and CVCL::Rational::d_n.
Referenced by boundedModulo(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvplusConst(), and CVCL::ArithTheoremProducer::constRHSGrayShadow().

bool CVCL::operator== ( const Rational & n1,

const Rational & n2

)

Definition at line 536 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

bool CVCL::operator< ( const Rational & n1,

const Rational & n2

)

Definition at line 540 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

bool CVCL::operator<= ( const Rational & n1,

const Rational & n2

)

Definition at line 544 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

bool CVCL::operator> ( const Rational & n1,

const Rational & n2

)

Definition at line 548 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

bool CVCL::operator>= ( const Rational & n1,

const Rational & n2

)

Definition at line 552 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

bool CVCL::operator!= ( const Rational & n1,

const Rational & n2

)

Definition at line 556 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

Rational CVCL::operator+ ( const Rational & n1,

const Rational & n2

)

Definition at line 560 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

Rational CVCL::operator- ( const Rational & n1,

const Rational & n2

)

Definition at line 564 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

Rational CVCL::operator * ( const Rational & n1,

const Rational & n2

)

Definition at line 568 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

Rational CVCL::operator/ ( const Rational & n1,

const Rational & n2

)

Definition at line 572 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

Rational CVCL::operator% ( const Rational & n1,

const Rational & n2

)

Definition at line 576 of file rational-gmp.cpp.
References CVCL::Rational::d_n.

static long int CVCL::plus ( long int x,

long int y

) [static]

Add two integers and check for overflows.

Definition at line 48 of file rational-native.cpp.

static long int CVCL::uminus ( long int x ) [static]

Unary minus which checks for overflows.

Definition at line 56 of file rational-native.cpp.
Referenced by gcd(), and CVCL::BitvectorTheoremProducer::lhsMinusRhsRule().

static long int CVCL::mult ( long int x,

long int y

) [static]

Multiply two integers and check for overflows.

Definition at line 63 of file rational-native.cpp.
Referenced by CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConstBVMult(), and lcm().

static long int CVCL::gcd ( long int n1,

long int n2

) [static]

Compute GCD using Euclid's algorithm (from Aaron Stump's code).

Definition at line 71 of file rational-native.cpp.
References gcd(), int2string(), and uminus().

static long int CVCL::lcm ( long int n1,

long int n2

) [static]

Compute LCM.

Definition at line 93 of file rational-native.cpp.
References gcd(), and mult().

Variable Documentation

ParserTemp* CVCL::parserTemp

const int CVCL::HASH_TABLE_SIZE = 1024

Definition at line 27 of file hash.h.

const int CVCL::HASH_TABLE_GROW_THRESHOLD = 1

Definition at line 28 of file hash.h.

const int CVCL::HASH_TABLE_GROW_FACTOR = 2

Definition at line 29 of file hash.h.

Generated on Thu Apr 13 16:57:42 2006 for CVC Lite by

1.4.4