CVCL Namespace Reference

Classes

• class CVCL::DebugTime
• class CVCL::Rational::Impl

  Implementation of the forward-declared internal class. More...
  

• class CVCL::Assumptions
• class CVCL::Assumptions::iterator

  Iterator for the Assumptions: points to class Theorem. More...
  

• class CVCL::Assumptions::iterator::Proxy

  Proxy class for postfix increment. More...
  

• class CVCL::AVHash
• class CVCL::AssumptionsValue
• class CVCL::CDList< T >
• class CVCL::CDOmap< Key, Data, HashFcn >
• class CVCL::CDMapData
• class CVCL::CDMap< Key, Data, HashFcn >
• class CVCL::CDMap< Key, Data, HashFcn >::iterator
• class CVCL::CDMap< Key, Data, HashFcn >::iterator::Proxy
• class CVCL::CDMap< Key, Data, HashFcn >::orderedIterator
• class CVCL::CDMap< Key, Data, HashFcn >::orderedIterator::Proxy
• class CVCL::CDOmapOrdered< Key, Data >
• class CVCL::CDMapOrderedData
• class CVCL::CDMapOrdered< Key, Data >
• class CVCL::CDMapOrdered< Key, Data >::iterator
• class CVCL::CDMapOrdered< Key, Data >::iterator::Proxy
• class CVCL::CDMapOrdered< Key, Data >::orderedIterator
• class CVCL::CDMapOrdered< Key, Data >::orderedIterator::Proxy
• class CVCL::CDO< T >
• class CVCL::Circuit
• class CVCL::ClauseValue
• class CVCL::Clause

  A class representing a CNF clause (a smart pointer). More...
  

• class CVCL::ClauseOwner

  Same as class Clause, but when destroyed, marks the clause as deleted. More...
  

• class CVCL::CompactClause
• class CVCL::CLException
• class CVCL::CLFlag
• class CVCL::CLFlags
• class CVCL::CommonProofRules

  Commonly used proof rules (reflexivity, symmetry, transitivity, substitutivity, etc.). More...
  

• class CVCL::Scope
• class CVCL::ContextObjChain
• class CVCL::ContextObj
• class CVCL::Context
• class CVCL::ContextManager

  Manager for multiple contexts. Also holds current context. More...
  

• class CVCL::ContextNotifyObj
• class CVCL::ScopeWatcher

  A class which sets a boolean value to true when created, and resets to false when deleted. More...
  

• class CVCL::DebugException

  Our exception to throw. More...
  

• class CVCL::DebugFlag

  Boolean flag (can only be true or false). More...
  

• class CVCL::DebugCounter

  Integer counter for debugging purposes. More...
  

• class CVCL::DebugTimer

  Time counter. More...
  

• class CVCL::Debug

  The heart of the Bug Extermination Kingdom. More...
  

• class CVCL::Debug::stringHash

  Private hasher class for strings. More...
  

• class CVCL::EvalException
• class CVCL::Exception
• class CVCL::Expr

  Data structure of expressions in CVC Lite. More...
  

• class CVCL::Expr::iterator
• class CVCL::Expr::iterator::Proxy

  Postfix increment requires a Proxy object to hold the intermediate value for dereferencing. More...
  

• class CVCL::ExprManager
• class CVCL::ExprManager::HashString

  Private class for hashing strings. More...
  

• class CVCL::ExprManager::HashEV

  Private classe for d_exprSet. More...
  

• class CVCL::ExprManager::EqEV

  Private class for d_exprSet. More...
  

• class CVCL::ExprManagerNotifyObj

  Notifies ExprManager before and after each pop(). More...
  

• class CVCL::ExprGeneric

  ExprGeneric. More...
  

• class CVCL::ExprMap< Data >
• class CVCL::ExprMap< Data >::iterator
• class CVCL::ExprMap< Data >::iterator::Proxy
• class CVCL::ExprHashMap< Data >
• class CVCL::ExprHashMap< Data >::iterator
• class CVCL::ExprHashMap< Data >::iterator::Proxy
• class CVCL::Op
• class CVCL::ExprStream

  Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING! More...
  

• class CVCL::ExprValue

  The base class for holding the actual data in expressions. More...
  

• class CVCL::ExprNode
• class CVCL::ExprString
• class CVCL::ExprSkolem
• class CVCL::ExprRational
• class CVCL::ExprVar
• class CVCL::ExprBoundVar
• class CVCL::ExprCC
• class CVCL::ExprApply
• class CVCL::ExprClosure

  A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers. More...
  

• class CVCL::NamedExprValue

  NamedExprValue. More...
  

• class CVCL::BoolVarExprValue

  Boolean variables are treated as 0-ary predicates. More...
  

• class CVCL::MemoryManager
• class CVCL::MemoryManagerChunks
• class CVCL::MemoryManagerMalloc
• class CVCL::NotifyList
• class CVCL::Parser
• class CVCL::ParserException
• class CVCL::PrettyPrinter

  Abstract API to a pretty-printer for Expr. More...
  

• class CVCL::Proof
• class CVCL::Rational
• class CVCL::SearchEngine

  API to to a generic proof search engine (a.k.a. SAT solver). More...
  

• class CVCL::SearchEngine::Splitter

  Representation of a DP-suggested splitter. More...
  

• class CVCL::SearchEngine::SearchNotifyObj
• class CVCL::SearchEngineFast

  Implementation of a faster search engine, using newer techniques. More...
  

• class CVCL::SearchEngineFast::ConflictClauseManager
• class CVCL::SearchSimple

  Implementation of the simple search engine. More...
  

• class CVCL::SmartCDO< T >

  SmartCDO. More...
  

• class CVCL::SmartCDO< T >::RefCDO< U >
• class CVCL::SmartCDO< T >::RefCDO< U >::RefNotifyObj
• class CVCL::SmtlibException
• class CVCL::SoundException
• class CVCL::StatFlag
• class CVCL::StatCounter
• class CVCL::Statistics
• class CVCL::Theorem
• class CVCL::Theorem3

  Theorem3. More...
  

• class CVCL::TheoremManager
• class CVCL::TheoremProducer
• class CVCL::Theory

  Base class for theories. More...
  

• class CVCL::TheoryArith

  This theory handles basic linear arithmetic. More...
  

• class CVCL::TheoryArith::FreeConst

  Data class for the strongest free constant in separation inqualities. More...
  

• class CVCL::TheoryArith::Ineq

  Private class for an inequality in the Fourier-Motzkin database. More...
  

• class CVCL::TheoryArith::VarOrderGraph
• class CVCL::TheoryArray

  This theory handles arrays. More...
  

• class CVCL::TheoryBitvector

  Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG). More...
  

• class CVCL::TheoryCore

  This theory handles the built-in logical connectives plus equality. It also handles the registration and cooperation among all other theories. More...
  

• class CVCL::TheoryCore::CoreNotifyObj
• class CVCL::TheoryDatatype

  This theory handles datatypes. More...
  

• class CVCL::TheoryQuant

  This theory handles quantifiers. More...
  

• class CVCL::TheoryQuant::TypeComp
• class CVCL::TheoryRecords

  This theory handles records. More...
  

• class CVCL::TheorySimulate

  "Theory" of symbolic simulation. More...
  

• class CVCL::TheoryUF

  This theory handles uninterpreted functions. More...
  

• struct CVCL::TheoryUF::TCMapPair
• class CVCL::Type
• class CVCL::TypecheckException
• class CVCL::Variable
• class CVCL::Literal
• class CVCL::VariableValue
• class CVCL::VariableManager
• class CVCL::VariableManager::HashLV
• class CVCL::VariableManager::EqLV
• class CVCL::VariableManagerNotifyObj

  Notifies VariableManager before and after each pop(). More...
  

• class CVCL::ValidityChecker

  Generic API for a validity checker. More...
  

• class CVCL::VCCmd
• struct CVCL::ltstr
• class CVCL::VCL
• class CVCL::VCL::UserAssertion

  Structure to hold user assertions indexed by declaration order. More...
  

• class CVCL::CNF
• class CVCL::ParserTemp
• class CVCL::DecisionEngine
• class CVCL::DecisionEngineCaching
• class CVCL::DecisionEngineCaching::CacheEntry
• class CVCL::DecisionEngineDFS

  Decision Engine for use with the Search Engine. More...
  

• class CVCL::DecisionEngineMBTF
• class CVCL::DecisionEngineMBTF::CacheEntry
• class CVCL::SearchEngineRules

  API to the proof rules for the Search Engines. More...
  

• class CVCL::TheoremLess

  "Less" comparator for theorems by TheoremValue pointers More...
  

• class CVCL::SearchEngineTheoremProducer
• class CVCL::TheoremValue
• class CVCL::RWTheoremValue
• class CVCL::ReflexivityTheoremValue

  A special subclass for reflexivity theorems: e = e and e <=> e. More...
  

• class CVCL::ArithException
• class CVCL::ExprGrayShadow

  Subclass of ExprValue for gray shadow expressions. More...
  

• class CVCL::ArithProofRules
• class CVCL::ArithTheoremProducer
• class CVCL::RefinedArithTheoremProducer
• class CVCL::ArrayProofRules
• class CVCL::ArrayTheoremProducer
• class CVCL::BitvectorException
• class CVCL::BVConstExpr
• class CVCL::BVPlusExpr
• class CVCL::BVParameterExpr
• class CVCL::BVTypePredExpr

  BVTypePredExpr. More...
  

• class CVCL::BitvectorProofRules
• class CVCL::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 CVCL::CommonTheoremProducer
• class CVCL::Dict_Entry< _Key, _Data >
• class CVCL::Dict< _Key, _Data >
• class CVCL::Dict_Ptr< _Key, _Data >
• struct CVCL::_Hashtable_iterator< _Key, _Data >
• struct CVCL::_Hashtable_const_iterator< _Key, _Data >
• class CVCL::Hash_Entry< _Key, _Data >
• class CVCL::Hash_Table< _Key, _Data >
• class CVCL::Hash_Ptr< _Key, _Data >
• class CVCL::PrettyPrinterCore

  Implementation of PrettyPrinter class. More...
  

• class CVCL::DatatypeProofRules
• class CVCL::DatatypeTheoremProducer
• class CVCL::QuantProofRules
• class CVCL::QuantTheoremProducer
• class CVCL::ExprRecord

  Record literal: contains list of field names as an attribute. More...
  

• class CVCL::RecField

  Record field access (select, update). More...
  

• class CVCL::TupleIndex

  Tuple element access (select, update). More...
  

• class CVCL::RecordsProofRules
• class CVCL::RecordsTheoremProducer
• class CVCL::SimulateProofRules
• class CVCL::SimulateTheoremProducer
• class CVCL::UFProofRules
• class CVCL::UFTheoremProducer

Typedefs

• typedef long long unsigned ExprIndex

  Expression index type.
  

• typedef std::map< const std::string,
  Expr, ltstr > Str_To_Expr
• typedef std::map< Theorem,
  bool, TheoremLess > TheoremMap
• 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_STRING, EXPR_RATIONAL,
    EXPR_SKOLEM, EXPR_UCONST, EXPR_BOUND_VAR, EXPR_CC,
    EXPR_APPLY, EXPR_CLOSURE, EXPR_NAMED, EXPR_BOOL_VAR,
    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, OLD_ARROW, TYPE, TYPEDECL,
    TYPEDEF, EQ, NEQ, NOT,
    AND, OR, XOR, IFF,
    IMPLIES, BOOL_VAR, AND_R, IFF_R,
    ITE_R, ITE, FORALL, EXISTS,
    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, COUNTEREXAMPLE, PUSH,
    POP, POPTO, PUSH_SCOPE, POP_SCOPE,
    POPTO_SCOPE, CONTEXT, FORGET, GET_TYPE,
    CHECK_TYPE, GET_CHILD, SUBSTITUTE, 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,
    INTTOBV, BVTOINT, BVTYPEPRED, BVPARAMOP
  }
• enum DatatypeKinds {
    DATATYPE = 600, THISTYPE, 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 }

  Local kinds for transitive closure of binary relations. More...
  

Functions

• 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.
  

• 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)
• Expr recursiveSubst (const Expr &e, const ExprHashMap< Expr > &subst, ExprHashMap< Expr > &visited)
• bool subExprRec (const Expr &e1, const Expr &e2)
• Expr substExpr (const Expr &e, const vector< Expr > &oldTerms, const vector< Expr > &newTerms)
• Expr substExpr (const Expr &e, const ExprHashMap< Expr > &oldToNew)
• int compare (const Expr &e1, const Expr &e2)
• ostream & operator<< (ostream &os, const Expr &e)
• ostream & operator<< (ostream &os, const NotifyList &l)

  Printing NotifyList class.
  

• Type funType (const std::vector< Type > &typeDom, const Type &typeRan)

  n-ary function type
  

• 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)
• ostream & operator<< (ostream &os, const Rational &n)
• 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)
• long int plus (long int x, long int y)

  Add two integers and check for overflows.
  

• long int uminus (long int x)

  Unary minus which checks for overflows.
  

• long int mult (long int x, long int y)

  Multiply two integers and check for overflows.
  

• long int gcd (long int n1, long int n2)

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

• long int lcm (long int n1, long int n2)

  Compute LCM.
  

• bool operator== (const AssumptionsValue &a1, const AssumptionsValue &a2)
• bool operator!= (const AssumptionsValue &a1, const AssumptionsValue &a2)
• bool operator== (const Assumptions &a1, const Assumptions &a2)
• bool operator!= (const Assumptions &a1, const Assumptions &a2)
• 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)
• Expr newExpr (ExprValue *ev)
• Expr newExpr (ExprManager *em, const Expr &e)
• Expr newExpr (ExprManager *em, const Op &op)
• Expr newExpr (ExprManager *em, const Op &op, const Expr &child)
• Expr newExpr (ExprManager *em, const Op &op, const Expr &child0, const Expr &child1)
• Expr newExpr (ExprManager *em, const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)
• Expr newExpr (ExprManager *em, const Op &op, const std::vector< Expr > &children)
• Expr newExpr (ExprManager *em, int kind)
• Expr newExpr (ExprManager *em, int kind, const Expr &child)
• Expr newExpr (ExprManager *em, int kind, const Expr &child0, const Expr &child1)
• Expr newExpr (ExprManager *em, int kind, const Expr &child0, const Expr &child1, const Expr &child2)
• Expr newExpr (ExprManager *em, int kind, const std::vector< Expr > &children)
• Expr newClosureExpr (ExprManager *em, int kind, const std::vector< Expr > &vars, const Expr &body)
• Expr newClosureExpr (int kind, const std::vector< Expr > &vars, const Expr &body)
• Expr newApplyExpr (ExprManager *em, const Expr &func, const std::vector< Expr > &args)
• Expr newNamedExpr (ExprManager *em, int kind, const std::string &name)
• Expr newNamedExpr (ExprManager *em, int kind, const std::string &name, const std::vector< Expr > &kids)
• Expr newNamedExpr (int kind, const std::string &name, const std::vector< Expr > &kids)
• Expr newExpr (const Op &op)
• Expr newExpr (const Op &op, const Expr &child)
• Expr newExpr (const Op &op, const Expr &child0, const Expr &child1)
• Expr newExpr (const Op &op, const Expr &child0, const Expr &child1, const Expr &child2)
• Expr newExpr (const Op &op, const std::vector< Expr > &children)
• Expr newStringExpr (ExprManager *em, const std::string &s)
• Expr newVarExpr (ExprManager *em, const std::string &s)
• Expr newBoundVarExpr (ExprManager *em, const std::string &name, const std::string &uid)
• Expr newRatExpr (ExprManager *em, const Rational &r)
• Expr newSkolemExpr (const Expr &e, int index)
• Expr newBoolVarExpr (const Expr &e)
• const Expr & falseExpr (ExprManager *em)
• const Expr & trueExpr (ExprManager *em)
• 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)
• Op getOp (const Expr &e)
• bool isLeafKind (int kind)
• 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 Assumptions &a1, const Assumptions &a2)
• Assumptions merge (const std::vector< Assumptions > &a)
• 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 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 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 read (const Expr &arr, const Expr &index)
• Expr write (const Expr &arr, const Expr &index, const Expr &value)
• Expr arrayLiteral (const Expr &ind, const Expr &body)
• Rational computeBVConst (const Expr &e)

  computes the integer value of a bitvector constant
  

• Rational computeNegBVConst (const Expr &e)

  computes the integer value of ~c+1 or BVUMINUS(c)
  

• 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)
• 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 &a1, const Assumptions &a2)
• Assumptions operator- (const Assumptions &a1, const Assumptions &a2)
• Assumptions operator- (const Assumptions &a, const Expr &e)
• bool findExpr (const Assumptions &a, const Expr &e, vector< Theorem > &gamma)
• Assumptions operator- (const Assumptions &a, const vector< Expr > &es)
• bool findExprs (const Assumptions &a, const vector< Expr > &es, vector< Theorem > &gamma)
• bool TheoremEq (const Theorem &t1, const Theorem &t2)
• void mergeVectors (const vector< Theorem > &v1, const vector< Theorem > &v2, vector< Theorem > &v)
• AssumptionsValue * operator+ (const AssumptionsValue &av1, const AssumptionsValue &av2)
• AssumptionsValue * operator- (const AssumptionsValue &av1, const AssumptionsValue &av2)
• ostream & operator<< (ostream &os, const Assumptions &assump)
• 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)
• Assumptions merge (const vector< Assumptions > &a)
• 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> size_t hash (_Key e)
• template<class _Key> 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)

Variables

• Debug debugger
• ParserTemp * parserTemp
• const int HASH_TABLE_SIZE = 1024
• const int HASH_TABLE_GROW_THRESHOLD = 1
• const int HASH_TABLE_GROW_FACTOR = 2

---

Typedef Documentation

typedef long long unsigned CVCL::ExprIndex

Expression index type. Definition at line 87 of file expr.h. Referenced by CVCL::Expr::getIndex(), CVCL::ExprManager::lastIndex(), CVCL::ExprManager::nextIndex(), and recursiveSubst().

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

Definition at line 69 of file vcl.h.

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

Definition at line 48 of file search_theorem_producer.h. Referenced by CVCL::SearchEngineTheoremProducer::conflictClause().

typedef void* CVCL::void_ptr

Definition at line 22 of file dictionary.h. Referenced by CVCL::Dict_Ptr< _Key, _Data >::operator void_ptr().

typedef void* CVCL::void_pointer

Definition at line 30 of file hash.h. Referenced by CVCL::Hash_Ptr< _Key, _Data >::operator void_pointer().

---

Enumeration Type Documentation

enum CLFlagType

Different types of command line flags. Enumeration values: CLFLAG_NULL  CLFLAG_BOOL  CLFLAG_INT  CLFLAG_STRING  CLFLAG_STRVEC  Vector of pair<string, bool>. Definition at line 42 of file command_line_flags.h. Referenced by CVCL::CLFlag::getType(), parse_args(), and printUsage().

enum ExprValueType

Type ID of each ExprValue subclass. It is defined in expr.h, so that ExprManager can use it before loading expr_value.h Enumeration values: EXPR_VALUE  EXPR_NODE  EXPR_STRING  EXPR_RATIONAL  EXPR_SKOLEM  EXPR_UCONST  EXPR_BOUND_VAR  EXPR_CC  Expression with sig and rep attributes for congruence closure. EXPR_APPLY  Application of functions and predicates. EXPR_CLOSURE  EXPR_NAMED  EXPR_BOOL_VAR  EXPR_VALUE_TYPE_LAST  Definition at line 66 of file expr.h.

enum Kind

Enumeration values: 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  OLD_ARROW  TYPE  TYPEDECL  TYPEDEF  EQ  NEQ  NOT  AND  OR  XOR  IFF  IMPLIES  BOOL_VAR  Boolean variables are treated as 0-ary predicates. AND_R  IFF_R  ITE_R  ITE  FORALL  EXISTS  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  COUNTEREXAMPLE  PUSH  POP  POPTO  PUSH_SCOPE  POP_SCOPE  POPTO_SCOPE  CONTEXT  FORGET  GET_TYPE  CHECK_TYPE  GET_CHILD  SUBSTITUTE  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 InputLanguage

Different input languages. Enumeration values: 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. Referenced by getLanguage(), and CVCL::ExprStream::lang().

enum ArithKinds

Enumeration values: 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 43 of file theory_arith.h.

enum ArithLang

Used to keep track of which subset of arith is being used. Enumeration values: NOT_USED  TERMS_ONLY  DIFF_ONLY  LINEAR  NONLINEAR  Definition at line 68 of file theory_arith.h. Referenced by CVCL::TheoryArith::getLangUsed().

enum ArrayKinds

Enumeration values: ARRAY  READ  WRITE  ARRAY_LITERAL  Definition at line 40 of file theory_array.h.

enum BVKinds

Enumeration values: BITVECTOR  BVCONST  HEXBVCONST  CONCAT  BVOR  BVAND  BVNEG  BVXOR  BVNAND  BVNOR  BVXNOR  EXTRACT  LEFTSHIFT  RIGHTSHIFT  VARSHIFT  BVPLUS  BVSUB  BVUMINUS  BVMULT  BOOLEXTRACT  BVLT  BVLE  BVGT  BVGE  INTTOBV  BVTOINT  BVTYPEPRED  BVPARAMOP  Definition at line 44 of file theory_bitvector.h.

enum DatatypeKinds

Local kinds for datatypes. Enumeration values: DATATYPE  THISTYPE  CONSTRUCTOR  SELECTOR  TESTER  Definition at line 42 of file theory_datatype.h.

enum RecordKinds

Enumeration values: RECORD  RECORD_SELECT  RECORD_UPDATE  RECORD_TYPE  TUPLE  TUPLE_SELECT  TUPLE_UPDATE  TUPLE_TYPE  Definition at line 40 of file theory_records.h.

enum UFKinds

Local kinds for transitive closure of binary relations. Enumeration values: TRANS_CLOSURE  Definition at line 42 of file theory_uf.h.

---

Function Documentation

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 44 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 64 of file debug.cpp.

DebugTime operator+ (  const DebugTime &  t1, const DebugTime &  t2 )

Definition at line 122 of file debug.cpp.

DebugTime operator- (  const DebugTime &  t1, const DebugTime &  t2 )

Definition at line 127 of file debug.cpp.

bool operator== (  const DebugTime &  t1, const DebugTime &  t2 )

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

bool operator!= (  const DebugTime &  t1, const DebugTime &  t2 )

Definition at line 138 of file debug.cpp.

bool operator== (  const DebugTimer &  t1, const DebugTimer &  t2 )

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

bool operator!= (  const DebugTimer &  t1, const DebugTimer &  t2 )

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

bool operator< (  const DebugTimer &  t1, const DebugTimer &  t2 )

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

bool operator> (  const DebugTimer &  t1, const DebugTimer &  t2 )

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

bool operator<= (  const DebugTimer &  t1, const DebugTimer &  t2 )

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

bool operator>= (  const DebugTimer &  t1, const DebugTimer &  t2 )

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

ostream& operator<< (  ostream &  os, const DebugTime &  t )

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

ostream& operator<< (  ostream &  os, const DebugTimer &  timer )

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

Expr recursiveSubst (  const Expr &  e, const ExprHashMap< Expr > &  subst, ExprHashMap< Expr > &  visited )  [static]

Definition at line 54 of file expr.cpp. References CVCL::Expr::begin(), CVCL::ExprHashMap< Data >::begin(), CVCL::ExprHashMap< Data >::clear(), CVCL::Expr::clearFlags(), CVCL::ExprHashMap< Data >::count(), CVCL::Debug::counter(), debugger, CVCL::Expr::end(), CVCL::ExprHashMap< Data >::end(), CVCL::ExprHashMap< Data >::erase(), ExprIndex, CVCL::Expr::getBody(), CVCL::Expr::getEM(), CVCL::Expr::getFlag(), CVCL::Expr::getIndex(), CVCL::Expr::getKind(), getOp(), CVCL::Expr::getVars(), IF_DEBUG(), CVCL::ExprHashMap< Data >::insert(), CVCL::Expr::isClosure(), newClosureExpr(), newExpr(), and CVCL::Expr::setFlag(). Referenced by substExpr().

bool 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().

Expr substExpr (  const Expr &  e, const vector< Expr > &  oldTerms, const vector< Expr > &  newTerms )

Definition at line 157 of file expr.cpp. References CVCL::Expr::clearFlags(), CVCL::ExprHashMap< Data >::insert(), and recursiveSubst(). Referenced by CVCL::UFTheoremProducer::applyLambda(), CVCL::SearchEngineTheoremProducer::conflictClause(), CVCL::ArrayTheoremProducer::readArrayLiteral(), CVCL::SearchEngineTheoremProducer::skolemize(), CVCL::VCCmd::skolemizeAx(), and CVCL::QuantTheoremProducer::universalInst().

Expr substExpr (  const Expr &  e, const ExprHashMap< Expr > &  oldToNew )

Definition at line 178 of file expr.cpp. References CVCL::ExprHashMap< Data >::begin(), CVCL::Expr::clearFlags(), CVCL::ExprHashMap< Data >::end(), recursiveSubst(), and CVCL::ExprHashMap< Data >::size().

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

Definition at line 462 of file expr.cpp. References CVCL::Expr::d_expr, and CVCL::Expr::getIndex(). Referenced by CVCL::AssumptionsValue::add(), CVCL::AssumptionsValue::AssumptionsValue(), CVCL::AssumptionsValue::find(), mergeVectors(), operator-(), operator<(), operator<=(), operator>(), operator>=(), and TheoremEq().

ostream& operator<< (  ostream &  os, const Expr &  e )

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

ostream& operator<< (  ostream &  os, const NotifyList &  l )

Printing NotifyList class. Definition at line 512 of file expr.cpp. References CVCL::NotifyList::getExpr(), CVCL::Theory::getName(), CVCL::NotifyList::getTheory(), and CVCL::NotifyList::size().

Type CVCL::funType (  const std::vector< Type > &  typeDom, const Type &  typeRan )

n-ary function type Definition at line 522 of file expr.cpp. References ARROW, CVCL::Type::getExpr(), and newExpr(). Referenced by CVCL::TheoryUF::computeTCC(), CVCL::TheoryUF::computeType(), CVCL::TheorySimulate::computeType(), and CVCL::VCL::funType().

bool isTrivialExpr (  const Expr &  e  )  [static]

Definition at line 61 of file expr_stream.cpp. References CVCL::Expr::arity(), and CVCL::Expr::isClosure(). Referenced by CVCL::ExprStream::collectShared().

ostream & CVCL::operator<< (  ostream &  os, const Rational &  n )

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

void CVCL::checkInt (  const Rational &  n, const string &  funName )  [static]

Definition at line 410 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 421 of file rational-gmp.cpp. References checkInt(), and CVCL::Rational::d_n. Referenced by CVCL::TheoryArith::computeNormalFactor(), and gcd().

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

Definition at line 427 of file rational-gmp.cpp. References checkInt(), CVCL::Rational::d_n, and gcd().

Rational CVCL::lcm (  const Rational &  x, const Rational &  y )

Definition at line 443 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 449 of file rational-gmp.cpp. References checkInt(), and lcm().

Rational CVCL::abs (  const Rational &  x  )

Definition at line 459 of file rational-gmp.cpp. Referenced by CVCL::TheoryArith::computeNormalFactor(), CVCL::BitvectorTheoremProducer::constMultToPlus(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), and CVCL::TheoryArith::pickIntEqMonomial().

Rational CVCL::floor (  const Rational &  x  )

Definition at line 464 of file rational-gmp.cpp. References CVCL::Rational::d_n, and CVCL::Rational::floor. 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 468 of file rational-gmp.cpp. References CVCL::Rational::ceil, and 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 472 of file rational-gmp.cpp. References checkInt(), and CVCL::Rational::d_n. Referenced by CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), and CVCL::ArithTheoremProducer::constRHSGrayShadow().

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

long int plus (  long int  x, long int  y )  [static]

Add two integers and check for overflows. Definition at line 51 of file rational-native.cpp.

long int uminus (  long int  x  )  [static]

Unary minus which checks for overflows. Definition at line 59 of file rational-native.cpp. Referenced by gcd().

long int mult (  long int  x, long int  y )  [static]

Multiply two integers and check for overflows. Definition at line 66 of file rational-native.cpp. Referenced by lcm().

long int gcd (  long int  n1, long int  n2 )  [static]

Compute GCD using Euclid's algorithm (from Aaron Stump's code). Definition at line 74 of file rational-native.cpp. References int2string(), and uminus(). Referenced by lcm().

long int lcm (  long int  n1, long int  n2 )  [static]

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

bool CVCL::operator== (  const AssumptionsValue &  a1, const AssumptionsValue &  a2 )  [inline]

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

bool CVCL::operator!= (  const AssumptionsValue &  a1, const AssumptionsValue &  a2 )  [inline]

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

bool operator== (  const Assumptions &  a1, const Assumptions &  a2 )  [inline]

Definition at line 213 of file assumptions.h. References CVCL::Assumptions::d_val.

bool operator!= (  const Assumptions &  a1, const Assumptions &  a2 )  [inline]

Definition at line 219 of file assumptions.h. References CVCL::Assumptions::d_val.

bool operator== (  const DebugFlag &  f1, const DebugFlag &  f2 )  [inline]

Checks if the *values* of the flags are equal. Definition at line 184 of file debug.h. References CVCL::DebugFlag::d_flag.

bool operator!= (  const DebugFlag &  f1, const DebugFlag &  f2 )  [inline]

Checks if the *values* of the flags are disequal. Definition at line 188 of file debug.h. References CVCL::DebugFlag::d_flag.

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

Printing flags. Definition at line 192 of file debug.h. References CVCL::DebugFlag::d_flag.

bool operator== (  const DebugCounter &  c1, const DebugCounter &  c2 )  [inline]

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

bool operator!= (  const DebugCounter &  c1, const DebugCounter &  c2 )  [inline]

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

bool operator== (  int  c1, const DebugCounter &  c2 )  [inline]

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

bool operator!= (  int  c1, const DebugCounter &  c2 )  [inline]

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

bool operator== (  const DebugCounter &  c1, int  c2 )  [inline]

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

bool operator!= (  const DebugCounter &  c1, int  c2 )  [inline]

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

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

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

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

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

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

Definition at line 871 of file expr.h. References AND. Referenced by CVCL::CommonTheoremProducer::andIntro(), CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::CNF::cnf(), CVCL::TheoryUF::computeModel(), CVCL::TheoryUF::computeTCC(), CVCL::TheorySimulate::computeTCC(), CVCL::TheoryCore::computeTCC(), CVCL::TheoryArray::computeTCC(), CVCL::Theory::computeTCC(), CVCL::TheoryRecords::computeTypePred(), CVCL::TheoryArith::computeTypePred(), CVCL::CommonTheoremProducer::convertToCNF(), CVCL::BitvectorTheoremProducer::eqToBits(), CVCL::RecordsTheoremProducer::expandEq(), CVCL::BitvectorTheoremProducer::expandTypePred(), CVCL::CommonTheoremProducer::implIntro(), CVCL::CommonTheoremProducer::implIntro3(), CVCL::CommonTheoremProducer::opCNFRule(), CVCL::Expr::operator &&(), CVCL::CommonTheoremProducer::rewriteAnd(), and CVCL::CommonTheoremProducer::rewriteNotOr().

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

Definition at line 881 of file expr.h. References OR. Referenced by CVCL::BitvectorTheoremProducer::bitExtractBitwise(), CVCL::BitvectorTheoremProducer::computeCarry(), CVCL::TheoryCore::computeTCC(), CVCL::CommonTheoremProducer::convertToCNF(), CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::RecordsTheoremProducer::expandNeq(), CVCL::Expr::operator||(), CVCL::CommonTheoremProducer::rewriteNotAnd(), and CVCL::CommonTheoremProducer::rewriteOr().

Expr newExpr (  ExprValue *  ev  )  [inline]

Definition at line 923 of file expr.h. Referenced by CVCL::RefinedArithTheoremProducer::addAssoc(), CVCL::Theory::addBoundVar(), CVCL::RefinedArithTheoremProducer::addInvR(), CVCL::ExprStream::addLetHeader(), CVCL::RefinedArithTheoremProducer::addLID(), CVCL::RefinedArithTheoremProducer::addSymm(), CVCL::BitvectorTheoremProducer::andOne(), CVCL::VCL::assertFormula(), CVCL::BitvectorTheoremProducer::bitwiseConst(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::VCL::checkContinue(), CVCL::CNF::cnf(), CVCL::TheoryCore::collectBasicVars(), CVCL::TheoryCore::collectModelValues(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryCore::computeTypePred(), CVCL::TheoryArith::computeTypePred(), CVCL::BitvectorTheoremProducer::concatFlatten(), CVCL::SearchEngineTheoremProducer::conflictClause(), CVCL::CommonTheoremProducer::convertToCNF(), CVCL::VCL::createOp(), CVCL::VCL::createType(), CVCL::TheoryDatatype::dataType(), CVCL::RefinedArithTheoremProducer::distribL(), CVCL::RefinedArithTheoremProducer::distribR(), CVCL::RefinedArithTheoremProducer::divideDef(), CVCL::VCCmd::evaluateCommand(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::ExprManager::ExprManager(), CVCL::BitvectorTheoremProducer::extractBitwise(), CVCL::ArithTheoremProducer::flipInequality(), CVCL::RefinedArithTheoremProducer::frac(), CVCL::VCL::funExpr(), funType(), CVCL::VCL::getConcreteModel(), CVCL::Theory::getOpKind(), CVCL::TheoryArith::grayShadow(), CVCL::VCL::idExpr(), CVCL::CommonTheoremProducer::ifLiftRule(), CVCL::RefinedArithTheoremProducer::inv(), CVCL::TheoryArith::isIntegerThm(), CVCL::BitvectorTheoremProducer::lhsMinusRhsRule(), CVCL::VCL::listExpr(), CVCL::RefinedArithTheoremProducer::ltAddR(), CVCL::RefinedArithTheoremProducer::ltScale(), CVCL::RefinedArithTheoremProducer::ltTrans(), CVCL::RefinedArithTheoremProducer::minusDef(), CVCL::RefinedArithTheoremProducer::multAssoc(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::RefinedArithTheoremProducer::multInvR(), CVCL::RefinedArithTheoremProducer::multLID(), CVCL::RefinedArithTheoremProducer::multSymm(), CVCL::RefinedArithTheoremProducer::multZeroL(), CVCL::RefinedArithTheoremProducer::neg(), CVCL::ArithTheoremProducer::negatedInequality(), newApplyExpr(), CVCL::TheoryBitvector::newBitvectorTypeExpr(), CVCL::TheoryBitvector::newBitvectorTypePred(), CVCL::TheoryBitvector::newBoolExtractExpr(), newBoundVarExpr(), CVCL::TheoryBitvector::newBVAndExpr(), CVCL::TheoryBitvector::newBVConstExpr(), CVCL::TheoryBitvector::newBVExtractExpr(), CVCL::TheoryBitvector::newBVLEExpr(), CVCL::TheoryBitvector::newBVLTExpr(), CVCL::TheoryBitvector::newBVMultExpr(), CVCL::TheoryBitvector::newBVNandExpr(), CVCL::TheoryBitvector::newBVNegExpr(), CVCL::TheoryBitvector::newBVNorExpr(), CVCL::TheoryBitvector::newBVOrExpr(), CVCL::TheoryBitvector::newBVPlusExpr(), CVCL::TheoryBitvector::newBVUminusExpr(), CVCL::TheoryBitvector::newBVXnorExpr(), CVCL::TheoryBitvector::newBVXorExpr(), newClosureExpr(), CVCL::TheoryBitvector::newConcatExpr(), CVCL::TheoryBitvector::newFixedLeftShiftExpr(), CVCL::TheoryBitvector::newFixedRightShiftExpr(), newNamedExpr(), newRatExpr(), newStringExpr(), CVCL::Theory::newTypeExpr(), CVCL::Theory::newVar(), newVarExpr(), CVCL::CommonTheoremProducer::opCNFRule(), CVCL::BitvectorTheoremProducer::orZero(), CVCL::TheoryUF::parseExprOp(), CVCL::TheoryCore::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::TheoryArith::parseExprOp(), CVCL::RefinedArithTheoremProducer::plus(), CVCL::ArithTheoremProducer::plusPredicate(), CVCL::VCL::pop(), CVCL::VCL::popScope(), CVCL::VCL::popto(), CVCL::VCL::poptoScope(), CVCL::VCL::push(), CVCL::VCL::pushScope(), CVCL::VCL::query(), read(), CVCL::ArithTheoremProducer::realShadow(), CVCL::TheoryRecords::recordExpr(), CVCL::TheoryRecords::recordSelect(), CVCL::TheoryRecords::recordType(), CVCL::TheoryRecords::recordUpdate(), CVCL::UFTheoremProducer::relTrans(), CVCL::VCL::restart(), CVCL::ArithTheoremProducer::rightMinusLeft(), CVCL::VCL::simplifyThm(), CVCL::VCL::simulateExpr(), CVCL::SearchEngineTheoremProducer::skolemizeRewriteVar(), CVCL::CommonTheoremProducer::substitutivityRule(), CVCL::VCL::subtypeType(), CVCL::TheoremProducer::TheoremProducer(), CVCL::TheoryArith::TheoryArith(), CVCL::TheoryDatatype::TheoryDatatype(), CVCL::TheoryRecords::tupleExpr(), CVCL::TheoryRecords::tupleSelect(), CVCL::TheoryRecords::tupleType(), CVCL::TheoryRecords::tupleUpdate(), CVCL::VCL::varExpr(), and write().

Expr newExpr (  ExprManager *  em, const Expr &  e )  [inline]

Definition at line 927 of file expr.h. References CVCL::Expr::rebuild().

Expr newExpr (  ExprManager *  em, const Op &  op )  [inline]

Definition at line 931 of file expr.h.

Expr newExpr (  ExprManager *  em, const Op &  op, const Expr &  child )  [inline]

Definition at line 934 of file expr.h.

Expr newExpr (  ExprManager *  em, const Op &  op, const Expr &  child0, const Expr &  child1 )  [inline]

Definition at line 937 of file expr.h.

Expr newExpr (  ExprManager *  em, const Op &  op, const Expr &  child0, const Expr &  child1, const Expr &  child2 )  [inline]

Definition at line 941 of file expr.h.

Expr newExpr (  ExprManager *  em, const Op &  op, const std::vector< Expr > &  children )  [inline]

Definition at line 945 of file expr.h.

Expr newExpr (  ExprManager *  em, int  kind )  [inline]

Definition at line 950 of file expr.h.

Expr newExpr (  ExprManager *  em, int  kind, const Expr &  child )  [inline]

Definition at line 953 of file expr.h.

Expr newExpr (  ExprManager *  em, int  kind, const Expr &  child0, const Expr &  child1 )  [inline]

Definition at line 956 of file expr.h.

Expr newExpr (  ExprManager *  em, int  kind, const Expr &  child0, const Expr &  child1, const Expr &  child2 )  [inline]

Definition at line 960 of file expr.h.

Expr newExpr (  ExprManager *  em, int  kind, const std::vector< Expr > &  children )  [inline]

Definition at line 964 of file expr.h.

Expr newClosureExpr (  ExprManager *  em, int  kind, const std::vector< Expr > &  vars, const Expr &  body )  [inline]

Definition at line 969 of file expr.h. References newExpr(). Referenced by arrayLiteral(), CVCL::TheoryQuant::computeTCC(), CVCL::ArithTheoremProducer::eqElimIntRule(), CVCL::VCL::existsExpr(), CVCL::VCL::forallExpr(), CVCL::VCL::lambdaExpr(), CVCL::TheoryUF::lambdaExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoryQuant::parseExprOp(), CVCL::TheoryArray::parseExprOp(), CVCL::QuantTheoremProducer::rewriteNotExists(), CVCL::CommonTheoremProducer::rewriteNotExists(), CVCL::QuantTheoremProducer::rewriteNotForall(), and CVCL::CommonTheoremProducer::rewriteNotForall().

Expr newClosureExpr (  int  kind, const std::vector< Expr > &  vars, const Expr &  body )  [inline]

Definition at line 975 of file expr.h. References CVCL::Expr::getEM(), and newExpr(). Referenced by recursiveSubst().

Expr newApplyExpr (  ExprManager *  em, const Expr &  func, const std::vector< Expr > &  args )  [inline]

Definition at line 981 of file expr.h. References args, and newExpr(). Referenced by CVCL::TheoryUF::applyExpr(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::Theory::newFunction(), CVCL::TheoryUF::parseExprOp(), and CVCL::UFTheoremProducer::rewriteOpDef().

Expr newNamedExpr (  ExprManager *  em, int  kind, const std::string &  name )  [inline]

Definition at line 986 of file expr.h. References newExpr(). Referenced by CVCL::TheoryDatatype::dataType(), and CVCL::TheoryUF::transClosureExpr().

Expr newNamedExpr (  ExprManager *  em, int  kind, const std::string &  name, const std::vector< Expr > &  kids )  [inline]

Definition at line 990 of file expr.h. References newExpr().

Expr newNamedExpr (  int  kind, const std::string &  name, const std::vector< Expr > &  kids )  [inline]

Definition at line 995 of file expr.h. References newExpr().

Expr newExpr (  const Op &  op  )  [inline]

Definition at line 1003 of file expr.h.

Expr newExpr (  const Op &  op, const Expr &  child )  [inline]

Definition at line 1006 of file expr.h.

Expr newExpr (  const Op &  op, const Expr &  child0, const Expr &  child1 )  [inline]

Definition at line 1010 of file expr.h.

Expr newExpr (  const Op &  op, const Expr &  child0, const Expr &  child1, const Expr &  child2 )  [inline]

Definition at line 1013 of file expr.h.

Expr newExpr (  const Op &  op, const std::vector< Expr > &  children )  [inline]

Definition at line 1017 of file expr.h. Referenced by arrayType(), CVCL::TheoryArith::darkShadow(), divideExpr(), CVCL::Type::funType(), geExpr(), gtExpr(), leExpr(), ltExpr(), minusExpr(), multExpr(), plusExpr(), powExpr(), CVCL::RefinedArithTheoremProducer::rat(), recursiveSubst(), CVCL::TheoryArith::subrangeType(), and uminusExpr().

Expr newStringExpr (  ExprManager *  em, const std::string &  s )  [inline]

Definition at line 1022 of file expr.h. References newExpr(). Referenced by CVCL::Theory::newTypeExpr(), and CVCL::VCL::stringExpr().

Expr newVarExpr (  ExprManager *  em, const std::string &  s )  [inline]

Definition at line 1026 of file expr.h. References newExpr(). Referenced by CVCL::ExprStream::addLetHeader(), CVCL::Theory::lookupVar(), CVCL::Theory::newFunction(), CVCL::TheoremProducer::newPf(), and CVCL::Theory::newVar().

Expr newBoundVarExpr (  ExprManager *  em, const std::string &  name, const std::string &  uid )  [inline]

Definition at line 1030 of file expr.h. References newExpr(). Referenced by CVCL::TheoryUF::computeModel(), CVCL::TheoryArray::computeModel(), CVCL::ArithTheoremProducer::eqElimIntRule(), CVCL::Theory::newBoundVar(), and CVCL::CommonTheoremProducer::newExprBoundVar().

Expr newRatExpr (  ExprManager *  em, const Rational &  r )  [inline]

Definition at line 1035 of file expr.h. References newExpr(). Referenced by CVCL::CommonTheoremProducer::andElim(), CVCL::TheorySimulate::computeTCC(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::CommonTheoremProducer::ifLiftRule(), CVCL::TheoryBitvector::rat(), CVCL::TheoryArith::rat(), CVCL::BitvectorTheoremProducer::rat(), CVCL::ArithTheoremProducer::rat(), and CVCL::VCL::ratExpr().

Expr newSkolemExpr (  const Expr &  e, int  index )  [inline]

Definition at line 1040 of file expr.h. References CVCL::Expr::skolemExpr().

Expr newBoolVarExpr (  const Expr &  e  )  [inline]

Definition at line 1044 of file expr.h. References CVCL::Expr::boolVarExpr(). Referenced by CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::Theory::newVar(), CVCL::SearchEngineTheoremProducer::skolemize(), CVCL::SearchEngine::skolemize(), and CVCL::SearchEngineTheoremProducer::skolemizeRewriteVar().

const Expr& falseExpr (  ExprManager *  em  )  [inline]

Definition at line 1047 of file expr.h. References CVCL::ExprManager::falseExpr(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractConstant(), CVCL::BitvectorTheoremProducer::bitExtractFixedLeftShift(), CVCL::BitvectorTheoremProducer::bitExtractFixedRightShift(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::SearchEngineTheoremProducer::eliminateSkolemAxioms(), CVCL::BitvectorTheoremProducer::eqConst(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::BitvectorTheoremProducer::lhsEqRhsIneqn(), CVCL::VariableValue::setValue(), and CVCL::BitvectorTheoremProducer::zeroPaddingRule().

const Expr& trueExpr (  ExprManager *  em  )  [inline]

Definition at line 1050 of file expr.h. References CVCL::ExprManager::trueExpr(). Referenced by CVCL::BitvectorTheoremProducer::bitExtractBVMult(), CVCL::BitvectorTheoremProducer::bitExtractConstant(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::eqConst(), CVCL::BitvectorTheoremProducer::generalIneqn(), CVCL::BitvectorTheoremProducer::lhsEqRhsIneqn(), and CVCL::Theory::trueTheorem().

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

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

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

Definition at line 1489 of file expr.h.

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

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

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

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

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

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

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

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

Op getOp (  const Expr &  e  )  [inline]

Definition at line 130 of file expr_op.h. Referenced by CVCL::BitvectorTheoremProducer::andOne(), CVCL::TheoryBitvector::bitBlastTerm(), CVCL::BitvectorTheoremProducer::bitwiseFlatten(), CVCL::ArithTheoremProducer::canonMultConstPlus(), CVCL::TheoryArith::canonPred(), CVCL::TheoryArith::canonPredEquiv(), CVCL::TheoryBitvector::checkSat(), CVCL::CNF::cnf(), CVCL::TheoryUF::computeBaseType(), CVCL::TheoryRecords::computeBaseType(), CVCL::TheoryArray::computeBaseType(), CVCL::TheoryCore::computeTypePred(), CVCL::BitvectorTheoremProducer::concatFlatten(), CVCL::BitvectorTheoremProducer::extractBitwise(), CVCL::Theory::getOpKind(), CVCL::CommonTheoremProducer::ifLiftRule(), CVCL::TheoryCore::ite_convert(), CVCL::ArithTheoremProducer::multIneqn(), CVCL::Theory::newFunction(), CVCL::CommonTheoremProducer::opCNFRule(), CVCL::BitvectorTheoremProducer::orZero(), CVCL::TheoryCore::pushNegationRec(), recursiveSubst(), CVCL::UFTheoremProducer::relTrans(), CVCL::TheoryRecords::rewriteAux(), CVCL::TheoryBitvector::rewriteBV(), CVCL::ArithTheoremProducer::rightMinusLeft(), CVCL::SearchEngineTheoremProducer::skolemizeRewriteVar(), CVCL::CommonTheoremProducer::substitutivityRule(), CVCL::TheoryCore::transformDiseq(), and CVCL::TheoryCore::traverseDiseq().

bool isLeafKind (  int  kind  )  [inline]

Definition at line 301 of file kinds.h. References BOUND_VAR, RATIONAL_EXPR, STRING_EXPR, and UCONST.

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

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

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

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

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

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

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

Raise 'base' into the power of 'pow' (pow must be an integer). Definition at line 161 of file rational.h. References CVCL::Rational::isInteger(), pow(), and CVCL::Rational::toString(). Referenced by CVCL::ArithTheoremProducer::canonPowConst(), pow(), and powExpr().

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

Definition at line 175 of file rational.h.

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

Definition at line 176 of file rational.h.

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

Definition at line 178 of file rational.h.

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

Definition at line 180 of file rational.h.

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

Definition at line 182 of file rational.h.

void printRational (  const Rational &  x  )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Assumptions merge (  const Assumptions &  a1, const Assumptions &  a2 )  [inline]

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

Assumptions merge (  const std::vector< Assumptions > &  a  )

Assumptions merge (  const Theorem &  t1, const Theorem &  t2 )  [inline]

Definition at line 391 of file theorem.h.

Assumptions merge (  const Assumptions &  a, const Theorem &  t )  [inline]

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

Assumptions merge (  const Theorem &  t, const Assumptions &  a )  [inline]

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

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

Definition at line 404 of file theorem.h.

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

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

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

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

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

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

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

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

bool isReal (  Type  t  )  [inline]

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

bool isInt (  Type  t  )  [inline]

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

bool isRational (  const Expr &  e  )  [inline]

Definition at line 380 of file theory_arith.h. References CVCL::Expr::isRational(). Referenced by CVCL::ArithTheoremProducer::canonDivideConst(), CVCL::ArithTheoremProducer::canonDivideMult(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonDivideVar(), CVCL::ArithTheoremProducer::canonInvertConst(), CVCL::ArithTheoremProducer::canonMultConstConst(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::canonMultConstTerm(), CVCL::ArithTheoremProducer::canonMultTermConst(), CVCL::TheoryArith::computeModel(), CVCL::ArithTheoremProducer::constPredicate(), CVCL::ArithTheoremProducer::eqElimIntRule(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::SimulateTheoremProducer::expandSimulate(), CVCL::TheoryArith::findRationalBound(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::ArithTheoremProducer::isIntConst(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::lessThanVar(), CVCL::TheoryArith::normalize(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::separateMonomial(), CVCL::TheoryArith::setup(), and CVCL::TheoryArith::updateSubsumptionDB().

bool isUMinus (  const Expr &  e  )  [inline]

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

bool isPlus (  const Expr &  e  )  [inline]

Definition at line 382 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::addToBuffer(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::TheoryArith::computeNormalFactor(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::create_t2(), CVCL::ArithTheoremProducer::create_t3(), CVCL::ArithTheoremProducer::eqElimIntRule(), CVCL::ArithTheoremProducer::finiteInterval(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::pickMonomial(), CVCL::TheoryArith::print(), CVCL::TheoryArith::processBuffer(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArith::separateMonomial(), CVCL::ArithTheoremProducer::substitute(), and CVCL::TheoryArith::updateSubsumptionDB().

bool isMinus (  const Expr &  e  )  [inline]

Definition at line 383 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::print().

bool isMult (  const Expr &  e  )  [inline]

Definition at line 384 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDivideMult(), CVCL::ArithTheoremProducer::canonMultMtermMterm(), CVCL::TheoryArith::computeNormalFactor(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::expandGrayShadowConst(), CVCL::ArithTheoremProducer::intVarEqnConst(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::isSyntacticUMinusVar(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::ArithTheoremProducer::monomialMulF(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::pickIntEqMonomial(), CVCL::TheoryArith::processFiniteInterval(), CVCL::TheoryArith::processRealEq(), CVCL::TheoryArith::processSimpleIntEq(), CVCL::TheoryArith::projectInequalities(), CVCL::TheoryArith::separateMonomial(), and CVCL::ArithTheoremProducer::substitute().

bool isDivide (  const Expr &  e  )  [inline]

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

bool isLT (  const Expr &  e  )  [inline]

Definition at line 386 of file theory_arith.h. References CVCL::Expr::getKind(). Referenced by CVCL::TheoryArith::assertFact(), CVCL::TheoryArith::findBounds(), isIneq(), CVCL::TheoryArith::isolateVariable(), CVCL::TheoryArith::isStale(), CVCL::ArithTheoremProducer::lessThanToLE(), CVCL::ArithTheoremProducer::negatedInequality(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::TheoryArith::projectInequalities(), CVCL::ArithTheoremProducer::realShadow(), CVCL::TheoryArith::setup(), and CVCL::TheoryArith::updateSubsumptionDB().

bool isLE (  const Expr &  e  )  [inline]

Definition at line 387 of file theory_arith.h. References CVCL::Expr::getKind(). 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 isGT (  const Expr &  e  )  [inline]

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

bool isGE (  const Expr &  e  )  [inline]

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

bool isDarkShadow (  const Expr &  e  )  [inline]

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

bool isIneq (  const Expr &  e  )  [inline]

Definition at line 391 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::rewrite(), and CVCL::TheoryArith::update().

bool isIntPred (  const Expr &  e  )  [inline]

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

Expr uminusExpr (  const Expr &  child  )  [inline]

Definition at line 396 of file theory_arith.h. References CVCL::Expr::getEM(), and newExpr(). Referenced by operator-(), and CVCL::TheoryArith::parseExprOp().

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

Definition at line 398 of file theory_arith.h. References CVCL::Expr::getEM(), and newExpr(). Referenced by CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::canonComboLikeTerms(), CVCL::ArithTheoremProducer::canonDividePlus(), CVCL::ArithTheoremProducer::canonFlattenSum(), CVCL::ArithTheoremProducer::canonMultConstSum(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::create_t2(), CVCL::ArithTheoremProducer::create_t3(), CVCL::TheoryArith::parseExprOp(), CVCL::ArithTheoremProducer::substitute(), and CVCL::TheoryArith::updateSubsumptionDB().

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

Definition at line 400 of file theory_arith.h. References newExpr(), and PLUS. Referenced by operator+().

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

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

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

Definition at line 406 of file theory_arith.h. References CVCL::Expr::getEM(), and newExpr(). Referenced by CVCL::ArithTheoremProducer::canonCombineLikeTerms(), CVCL::ArithTheoremProducer::create_t(), CVCL::ArithTheoremProducer::darkGrayShadow2ab(), CVCL::ArithTheoremProducer::darkGrayShadow2ba(), CVCL::ArithTheoremProducer::monomialModM(), CVCL::ArithTheoremProducer::monomialMulF(), CVCL::TheoryArith::parseExprOp(), CVCL::TheoryArith::separateMonomial(), and CVCL::ArithTheoremProducer::simplifiedMultExpr().

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

a Mult expr with two or more children Definition at line 410 of file theory_arith.h. References MULT, and newExpr(). Referenced by operator *().

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

Power (x^n, or base^{pow}) expressions. Definition at line 415 of file theory_arith.h. References newExpr(), and 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 divideExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 418 of file theory_arith.h. References CVCL::Expr::getEM(), and newExpr(). Referenced by CVCL::VCL::divideExpr(), operator/(), and CVCL::TheoryArith::parseExprOp().

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

Definition at line 420 of file theory_arith.h. References CVCL::Expr::getEM(), and newExpr(). Referenced by CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::VCL::ltExpr(), and CVCL::TheoryArith::parseExprOp().

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

Definition at line 422 of file theory_arith.h. References CVCL::Expr::getEM(), and newExpr(). 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 gtExpr (  const Expr &  left, const Expr &  right )  [inline]

Definition at line 424 of file theory_arith.h. References CVCL::Expr::getEM(), and newExpr(). Referenced by CVCL::ArithTheoremProducer::diseqToIneq(), CVCL::VCL::gtExpr(), and CVCL::TheoryArith::parseExprOp().

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

Definition at line 426 of file theory_arith.h. References CVCL::Expr::getEM(), and newExpr(). Referenced by CVCL::VCL::geExpr(), and CVCL::TheoryArith::parseExprOp().

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

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

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

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

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

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

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

Definition at line 435 of file theory_arith.h. References multExpr(). Referenced by CVCL::_Hashtable_const_iterator< _Key, _Data >::operator->(), CVCL::_Hashtable_iterator< _Key, _Data >::operator->(), and CVCL::Assumptions::iterator::operator->().

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

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

bool isArray (  const Type &  t  )  [inline]

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

bool isRead (  const Expr &  e  )  [inline]

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

bool isWrite (  const Expr &  e  )  [inline]

Definition at line 105 of file theory_array.h. References CVCL::Expr::getKind(). 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 isArrayLiteral (  const Expr &  e  )  [inline]

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

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

Definition at line 110 of file theory_array.h. References CVCL::Expr::getEM(), CVCL::Type::getExpr(), and newExpr(). Referenced by CVCL::VCL::arrayType(), and CVCL::TheoryArray::computeType().

Expr CVCL::read (  const Expr &  arr, const Expr &  index )

Definition at line 706 of file theory_array.cpp. References CVCL::Expr::getEM(), and newExpr(). Referenced by CVCL::TheoryArray::computeModel(), CVCL::TheoryArray::parseExprOp(), CVCL::VCL::readExpr(), CVCL::ArrayTheoremProducer::rewriteReadWrite(), CVCL::ArrayTheoremProducer::rewriteSameStore(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::TheoryArray::setup(), and std::fdinbuf::underflow().

Expr CVCL::write (  const Expr &  arr, const Expr &  index, const Expr &  value )

Definition at line 715 of file theory_array.cpp. References CVCL::Expr::getEM(), and newExpr(). Referenced by CVCL::ArrayTheoremProducer::interchangeIndices(), std::fdoutbuf::overflow(), CVCL::TheoryArray::parseExprOp(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite1(), CVCL::ArrayTheoremProducer::rewriteRedundantWrite2(), CVCL::ArrayTheoremProducer::rewriteWriteWrite(), CVCL::VCL::writeExpr(), and std::fdoutbuf::xsputn().

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

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

Rational CVCL::computeBVConst (  const Expr &  e  )

computes the integer value of a bitvector constant Definition at line 3588 of file theory_bitvector.cpp. References BVCONST, CVCL::Expr::getIntValue(), CVCL::Expr::getIntValueSize(), CVCL::Expr::getKind(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::andZero(), CVCL::BitvectorTheoremProducer::bvConstIneqn(), CVCL::BitvectorTheoremProducer::bvConstMultAssocRule(), CVCL::BitvectorTheoremProducer::bvmultConst(), CVCL::BitvectorTheoremProducer::bvplusConst(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), CVCL::BitvectorTheoremProducer::combineLikeTermsRule(), CVCL::TheoryBitvector::normalizeBVArith(), CVCL::BitvectorTheoremProducer::oneCoeffBVMult(), CVCL::BitvectorTheoremProducer::orZero(), and CVCL::BitvectorTheoremProducer::zeroCoeffBVMult().

Rational CVCL::computeNegBVConst (  const Expr &  e  )

computes the integer value of ~c+1 or BVUMINUS(c) Definition at line 3603 of file theory_bitvector.cpp. References BVCONST, CVCL::Expr::getIntValue(), CVCL::Expr::getIntValueSize(), CVCL::Expr::getKind(), and CVCL::Expr::toString(). Referenced by CVCL::BitvectorTheoremProducer::bvmultBVUminus(), CVCL::BitvectorTheoremProducer::bvuminusBVConst(), and CVCL::BitvectorTheoremProducer::bvuminusBVMult().

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

Definition at line 111 of file type.h. References CVCL::Type::getExpr(). Referenced by CVCL::TupleIndex::operator==(), CVCL::RecField::operator==(), CVCL::ExprRecord::operator==(), and CVCL::NamedExprValue::operator==().

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

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

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

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

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

Definition at line 209 of file variable.h.

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

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

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

ostream& operator<< (  ostream &  os, const Clause &  c )

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

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

Definition at line 167 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& operator<< (  std::ostream &  os, const CompactClause &  c )

Definition at line 174 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& operator<< (  ostream &  os, const Variable &  l )

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

ostream& 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& 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 operator+ (  const Assumptions &  a1, const Assumptions &  a2 )

Definition at line 262 of file assumptions_value.cpp. References CVCL::Assumptions::copy(), CVCL::Assumptions::d_val, and CVCL::Assumptions::isNull().

Assumptions operator- (  const Assumptions &  a1, const Assumptions &  a2 )

Definition at line 269 of file assumptions_value.cpp. References CVCL::Assumptions::copy(), CVCL::Assumptions::d_val, and CVCL::Assumptions::isNull().

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

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

bool findExpr (  const Assumptions &  a, const Expr &  e, vector< Theorem > &  gamma )

Definition at line 286 of file assumptions_value.cpp. References CVCL::Assumptions::begin(), and CVCL::Assumptions::end(). Referenced by operator-().

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

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

bool findExprs (  const Assumptions &  a, const vector< Expr > &  es, vector< Theorem > &  gamma )

Definition at line 328 of file assumptions_value.cpp. References CVCL::Assumptions::begin(), and CVCL::Assumptions::end(). Referenced by operator-().

bool TheoremEq (  const Theorem &  t1, const Theorem &  t2 )  [inline]

Definition at line 378 of file assumptions_value.cpp. References compare(), and CVCL::Theorem::isNull().

void mergeVectors (  const vector< Theorem > &  v1, const vector< Theorem > &  v2, vector< Theorem > &  v )

Definition at line 456 of file assumptions_value.cpp. References compare(). Referenced by CVCL::AssumptionsValue::add(), and operator+().

AssumptionsValue* operator+ (  const AssumptionsValue &  av1, const AssumptionsValue &  av2 )

Definition at line 520 of file assumptions_value.cpp. References CVCL::AssumptionsValue::d_vector, and mergeVectors().

AssumptionsValue* operator- (  const AssumptionsValue &  av1, const AssumptionsValue &  av2 )

Definition at line 528 of file assumptions_value.cpp. References compare(), CVCL::AssumptionsValue::d_vector, and CVCL::AssumptionsValue::size().

ostream& operator<< (  ostream &  os, const Assumptions &  assump )

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

ostream& operator<< (  ostream &  os, const AssumptionsValue &  assump )

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

int 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 55 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 compare (  const Theorem &  t1, const Expr &  e2 )

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

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

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

Assumptions merge (  const vector< Assumptions > &  a  )

Definition at line 468 of file theorem.cpp. References CVCL::Assumptions::add().

ostream& operator<< (  ostream &  os, const TheoryArith::FreeConst &  fc )

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

ostream& operator<< (  ostream &  os, const TheoryArith::Ineq &  ineq )

Definition at line 60 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& operator<< (  std::ostream &  cout, Dict_Entry< _Key, _Data > &  element )

Definition at line 249 of file dictionary.h.

template<class _Key, class _Data> std::ostream& operator<< (  std::ostream &  cout, Dict< _Key, _Data > &  dict )

Definition at line 260 of file dictionary.h.

template<class _Key> size_t hash (  _Key  e  )  [static]

Definition at line 22 of file hash.h. Referenced by CVCL::BVTypePredExpr::computeHash(), CVCL::BVParameterExpr::computeHash(), CVCL::BVPlusExpr::computeHash(), CVCL::BVConstExpr::computeHash(), CVCL::ExprRational::computeHash(), CVCL::ExprString::computeHash(), CVCL::ExprNode::computeHash(), CVCL::ExprValue::computeHash(), CVCL::ExprClosure::computeHash(), CVCL::ExprGrayShadow::computeHash(), CVCL::Hash_Ptr< _Key, _Data >::Hash_Ptr(), CVCL::Hash_Table< _Key, _Data >::Hash_Table(), and CVCL::Hash_Ptr< _Key, _Data >::Reset().

template<class _Key> size_t equal_to (  _Key  x, _Key  y )  [static]

Definition at line 24 of file hash.h.

template<class InputIterator> void insert (  InputIterator  l, InputIterator  r )

Definition at line 451 of file hash.h.

template<class _Key, class _Data> void 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().

---

Variable Documentation

Debug CVCL::debugger

Definition at line 412 of file debug.cpp. Referenced by CVCL::TheoryCore::addEquality(), CVCL::TheoryCore::addFact(), CVCL::SearchEngineFast::addNonLiteralFact(), CVCL::TheoryBitvector::addSharedTerm(), CVCL::SearchEngineFast::analyzeUIPs(), CVCL::TheoryBitvector::assertFact(), CVCL::TheoryArith::assertFact(), CVCL::TheoryCore::assertFactCore(), CVCL::TheoryCore::assertFormula(), CVCL::AVHash::AVHash(), CVCL::SearchEngineFast::bcp(), CVCL::TheoryBitvector::bitBlastDisEqn(), CVCL::TheoryBitvector::bitBlastEqn(), CVCL::TheoryUF::checkSat(), CVCL::TheoryCore::checkSat(), CVCL::TheoryBitvector::checkSat(), CVCL::TheoryCore::checkSATCore(), CVCL::TheoryBitvector::collectSharedSubterms(), CVCL::SearchEngineTheoremProducer::conflictClause(), CVCL::TheoryArith::doSolve(), CVCL::TheoryCore::enqueueEquality(), CVCL::TheoryCore::enqueueFact(), CVCL::VCCmd::evaluateCommand(), CVCL::VCCmd::evaluateNext(), CVCL::CommonTheoremProducer::findInLocalCache(), CVCL::SearchEngineFast::findSplitter(), CVCL::DecisionEngineMBTF::findSplitter(), CVCL::DecisionEngineDFS::findSplitter(), CVCL::DecisionEngineCaching::findSplitter(), CVCL::SearchEngineFast::fixConflict(), CVCL::TheoryArith::kidsCanonical(), main(), CVCL::TheoremProducer::newTheorem(), CVCL::TheoremProducer::newTheorem3(), CVCL::SearchEngine::newUserAssertion(), CVCL::TheoryArith::normalizeProjectIneqs(), CVCL::VCL::popScope(), CVCL::VCL::poptoScope(), CVCL::TheoryCore::processEquality(), CVCL::TheoryCore::processFactQueue(), CVCL::TheoryArith::projectInequalities(), CVCL::Context::push(), CVCL::VCL::pushScope(), CVCL::SearchEngineFast::recordFact(), recursiveSubst(), CVCL::TheoryUF::rewrite(), CVCL::TheoryBitvector::rewrite(), CVCL::TheoryBitvector::rewriteBV(), CVCL::Theory::setInconsistent(), CVCL::SearchEngineFast::setInconsistent(), CVCL::TheoryBitvector::setupExpr(), CVCL::TheoryCore::setupTerm(), sighandler(), CVCL::TheoryCore::simplify(), CVCL::TheoryCore::simplifyOp(), CVCL::TheoryArith::solvedForm(), CVCL::SearchEngineFast::split(), CVCL::CommonTheoremProducer::substitutivityRule(), CVCL::TheoryCore::transformDiseq(), CVCL::TheoryBitvector::update(), CVCL::TheoryArith::update(), and CVCL::Scope::~Scope().

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.

---