CVC3 Namespace Reference

Classes

• class Assumptions
• class CDFlags
• class CDList
• class CDOmap
• class CDMapData
• class CDMap
• class CDOmapOrdered
• class CDMapOrderedData
• class CDMapOrdered
• class CDO
• class Circuit
• class ClauseValue
• class Clause

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

• class ClauseOwner

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

• class CompactClause
• class CLException
• class CLFlag
• class CLFlags
• class CommonProofRules
• class Scope
• class ContextObjChain
• class ContextObj
• class Context
• class ContextManager

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

• class ContextNotifyObj
• class ScopeWatcher

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

• class DebugException

  Our exception to throw. More...
  

• class DebugFlag

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

• class DebugCounter

  Integer counter for debugging purposes. More...
  

• class DebugTimer

  Time counter. More...
  

• class Debug

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

• class EvalException
• class Exception
• class Expr

  Data structure of expressions in CVC3. More...
  

• class ExprManager
• class ExprManagerNotifyObj

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

• class ExprMap
• class ExprHashMap
• class Op
• class ExprStream

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

• class ExprTransform
• class ExprValue

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

• class ExprNode
• class ExprNodeTmp
• class ExprApplyTmp
• class ExprApply
• class ExprString
• class ExprSkolem
• class ExprRational
• class ExprVar
• class ExprSymbol
• class ExprBoundVar
• class ExprClosure

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

• class ExprTheorem
• class MemoryManager
• class MemoryManagerChunks
• class ContextMemoryManager

  ContextMemoryManager. More...
  

• class MemoryManagerMalloc
• class NotifyList
• class Parser
• class ParserException
• class PrettyPrinter

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

• class Proof
• class Rational
• class SearchEngine

  API to to a generic proof search engine. More...
  

• class SearchEngineFast

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

• class SearchImplBase

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

• class SearchSat

  Search engine that connects to a generic SAT reasoning module. More...
  

• class SearchSimple

  Implementation of the simple search engine. More...
  

• class SmartCDO

  SmartCDO. More...
  

• class SmtlibException
• class SoundException
• class StatFlag
• class StatCounter
• class Statistics
• class Theorem
• class Theorem3

  Theorem3. More...
  

• class TheoremLess

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

• class TheoremManager
• class TheoremProducer
• class Theory

  Base class for theories. More...
  

• class TheoryArith

  This theory handles basic linear arithmetic. More...
  

• class TheoryArithNew
• class TheoryArithOld
• class TheoryArray

  This theory handles arrays. More...
  

• class TheoryBitvector

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

• class TheoryCore

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

• class TheoryDatatype

  This theory handles datatypes. More...
  

• class TheoryDatatypeLazy

  This theory handles datatypes. More...
  

• class Trigger
• struct dynTrig
• class TheoryQuant

  This theory handles quantifiers. More...
  

• class TheoryRecords

  This theory handles records. More...
  

• class TheorySimulate

  "Theory" of symbolic simulation. More...
  

• class TheoryUF

  This theory handles uninterpreted functions. More...
  

• class Translator
• class Type
• class TypecheckException
• class Variable
• class Literal
• class VariableValue
• class VariableManager
• class VariableManagerNotifyObj

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

• class ValidityChecker

  Generic API for a validity checker. More...
  

• class VCCmd
• class VCL
• class ParserTemp
• class CNF_Rules

  API to the CNF proof rules. More...
  

• class CNF_TheoremProducer
• class DecisionEngine
• class DecisionEngineCaching
• class DecisionEngineDFS

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

• class DecisionEngineMBTF
• class CoreSatAPI_implBase
• class SearchEngineRules

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

• class SearchSatCoreSatAPI
• class SearchSatTheoryAPI
• class SearchSatDecider
• class SearchSatCNFCallback
• class SearchEngineTheoremProducer
• class CommonTheoremProducer
• class TheoremValue
• class RegTheoremValue
• class RWTheoremValue
• class ArithException
• class ArithProofRules
• class ArithTheoremProducer
• class ArithTheoremProducerOld
• class ArrayProofRules
• class ArrayTheoremProducer
• class BitvectorException
• class BVConstExpr
• class BitvectorProofRules
• class BitvectorTheoremProducer

  This class implements proof rules for bitvector normalizers (concatenation normal form, bvplus normal form), bitblaster rules, other relevant rewrite rules for bv arithmetic and word-level operators. More...
  

• class CoreProofRules
• class CoreTheoremProducer
• class PrettyPrinterCore

  Implementation of PrettyPrinter class. More...
  

• class TypeComputerCore
• class DatatypeProofRules
• class DatatypeTheoremProducer
• class QuantProofRules
• class QuantTheoremProducer
• class RecordsProofRules
• class RecordsTheoremProducer
• class SimulateProofRules
• class SimulateTheoremProducer
• class UFProofRules
• class UFTheoremProducer
• class DebugTime

Typedefs

• typedef long long unsigned ExprIndex

  Expression index type.
  

• typedef enum CVC3::QueryResult QueryResult
• typedef std::map< Theorem,
  bool, TheoremLess > TheoremMap
• typedef CVC3::dynTrig dynTrig

Enumerations

• enum CLFlagType {
    CLFLAG_NULL, CLFLAG_BOOL, CLFLAG_INT, CLFLAG_STRING,
    CLFLAG_STRVEC
  }

  Different types of command line flags. More...
  

• enum ExprValueType {
    EXPR_VALUE, EXPR_NODE, EXPR_APPLY, EXPR_STRING,
    EXPR_RATIONAL, EXPR_SKOLEM, EXPR_UCONST, EXPR_SYMBOL,
    EXPR_BOUND_VAR, EXPR_CLOSURE, EXPR_THEOREM, EXPR_VALUE_TYPE_LAST
  }

  Type ID of each ExprValue subclass. More...
  

• enum Kind {
    NULL_KIND = 0, RAW_LIST, ID, STRING_EXPR,
    RATIONAL_EXPR, TRUE_EXPR, FALSE_EXPR, BOOLEAN,
    ANY_TYPE, ARROW, TYPE, TYPEDECL,
    TYPEDEF, EQ, NEQ, DISTINCT,
    NOT, AND, OR, XOR,
    IFF, IMPLIES, AND_R, IFF_R,
    ITE_R, ITE, FORALL, EXISTS,
    UFUNC, APPLY, ASSERT, QUERY,
    CHECKSAT, CONTINUE, RESTART, DBG,
    TRACE, UNTRACE, OPTION, HELP,
    TRANSFORM, PRINT, CALL, ECHO,
    INCLUDE, DUMP_PROOF, DUMP_ASSUMPTIONS, DUMP_SIG,
    DUMP_TCC, DUMP_TCC_ASSUMPTIONS, DUMP_TCC_PROOF, DUMP_CLOSURE,
    DUMP_CLOSURE_PROOF, WHERE, ASSERTIONS, ASSUMPTIONS,
    COUNTEREXAMPLE, COUNTERMODEL, PUSH, POP,
    POPTO, PUSH_SCOPE, POP_SCOPE, POPTO_SCOPE,
    CONTEXT, FORGET, GET_TYPE, CHECK_TYPE,
    GET_CHILD, SUBSTITUTE, SEQ, TCC,
    VARDECL, VARDECLS, BOUND_VAR, BOUND_ID,
    SUBTYPE, IF, IFTHEN, ELSE,
    COND, LET, LETDECLS, LETDECL,
    LAMBDA, SIMULATE, CONST, VARLIST,
    UCONST, DEFUN, PF_APPLY, PF_HOLE,
    SKOLEM_VAR, THEOREM_KIND, LAST_KIND
  }
• enum InputLanguage {
    PRESENTATION_LANG, SMTLIB_LANG, LISP_LANG, AST_LANG,
    SIMPLIFY_LANG
  }

  Different input languages. More...
  

• enum QueryResult {
    SATISFIABLE = 0, INVALID = 0, VALID = 1, UNSATISFIABLE = 1,
    ABORT, UNKNOWN
  }
• 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,
    REAL_CONST
  }
• enum ArrayKinds { ARRAY = 2000, READ, WRITE, ARRAY_LITERAL }
• enum BVKinds {
    BITVECTOR = 8000, BVCONST, CONCAT, EXTRACT,
    BOOLEXTRACT, LEFTSHIFT, CONST_WIDTH_LEFTSHIFT, RIGHTSHIFT,
    BVSHL, BVLSHR, BVASHR, SX,
    BVREPEAT, BVZEROEXTEND, BVROTL, BVROTR,
    BVAND, BVOR, BVXOR, BVXNOR,
    BVNEG, BVNAND, BVNOR, BVCOMP,
    BVUMINUS, BVPLUS, BVSUB, BVMULT,
    BVUDIV, BVSDIV, BVUREM, BVSREM,
    BVSMOD, BVLT, BVLE, BVGT,
    BVGE, BVSLT, BVSLE, BVSGT,
    BVSGE, INTTOBV, BVTOINT, BVTYPEPRED
  }
• enum DatatypeKinds { DATATYPE = 600, CONSTRUCTOR, SELECTOR, TESTER }

  Local kinds for datatypes. More...
  

• enum Polarity { Ukn, Pos, Neg, PosNeg }
• enum RecordKinds {
    RECORD = 2500, RECORD_SELECT, RECORD_UPDATE, RECORD_TYPE,
    TUPLE, TUPLE_SELECT, TUPLE_UPDATE, TUPLE_TYPE
  }
• enum UFKinds { TRANS_CLOSURE = 500, OLD_ARROW }

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

• enum ArithLang {
    NOT_USED = 0, TERMS_ONLY, DIFF_ONLY, LINEAR,
    NONLINEAR
  }

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

Functions

• static bool subExprRec (const Expr &e1, const Expr &e2)
• int compare (const Expr &e1, const Expr &e2)
• ostream & operator<< (ostream &os, const Expr &e)
• static bool isTrivialExpr (const Expr &e)
• ExprStream & operator<< (ExprStream &os, ExprStream &(*manip)(ExprStream &))

  Use manipulators which are functions over ExprStream&.
  

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

  Print Expr.
  

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

  Print Type.
  

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

  Print string.
  

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

  Print char* string.
  

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

  Print Rational.
  

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

  Print int.
  

• ExprStream & push (ExprStream &os)

  Set the indentation to the current position.
  

• ExprStream & pop (ExprStream &os)

  Restore the indentation to the previous position.
  

• ExprStream & popSave (ExprStream &os)

  Remember the current indentation and pop to the previous position.
  

• ExprStream & pushRestore (ExprStream &os)

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

• ExprStream & reset (ExprStream &os)

  Reset the indentation to the default at this level.
  

• ExprStream & space (ExprStream &os)

  Insert a single white space separator.
  

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

  Similar to fatalError to raise an exception when DebugAssert fires.
  

• bool operator== (const DebugFlag &f1, const DebugFlag &f2)

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

• bool operator!= (const DebugFlag &f1, const DebugFlag &f2)

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

• std::ostream & operator<< (std::ostream &os, const DebugFlag &f)

  Printing flags.
  

• bool operator== (const DebugCounter &c1, const DebugCounter &c2)
• bool operator!= (const DebugCounter &c1, const DebugCounter &c2)
• bool operator== (int c1, const DebugCounter &c2)
• bool operator!= (int c1, const DebugCounter &c2)
• bool operator== (const DebugCounter &c1, int c2)
• bool operator!= (const DebugCounter &c1, int c2)
• std::ostream & operator<< (std::ostream &os, const DebugCounter &c)
• std::ostream & operator<< (std::ostream &os, const Exception &e)
• Expr andExpr (const std::vector< Expr > &children)
• Expr orExpr (const std::vector< Expr > &children)
• bool operator== (const Expr &e1, const Expr &e2)
• bool operator!= (const Expr &e1, const Expr &e2)
• bool operator< (const Expr &e1, const Expr &e2)
• bool operator<= (const Expr &e1, const Expr &e2)
• bool operator> (const Expr &e1, const Expr &e2)
• bool operator>= (const Expr &e1, const Expr &e2)
• InputLanguage getLanguage (const std::string &lang)
• std::ostream & operator<< (std::ostream &os, const Proof &pf)
• bool operator== (const Proof &pf1, const Proof &pf2)
• Rational pow (Rational pow, const Rational &base)

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

• Rational newRational (int n, int d=1)
• Rational newRational (const char *n, int base=10)
• Rational newRational (const std::string &n, int base=10)
• Rational newRational (const char *n, const char *d, int base=10)
• Rational newRational (const std::string &n, const std::string &d, int base=10)
• void printRational (const Rational &x)
• bool operator< (const SearchSat::LitPriorityPair &p1, const SearchSat::LitPriorityPair &p2)
• bool operator== (const StatFlag &f1, const StatFlag &f2)
• bool operator!= (const StatFlag &f1, const StatFlag &f2)
• std::ostream & operator<< (std::ostream &os, const StatFlag &f)
• bool operator== (const StatCounter &c1, const StatCounter &c2)
• bool operator!= (const StatCounter &c1, const StatCounter &c2)
• bool operator== (int c1, const StatCounter &c2)
• bool operator!= (int c1, const StatCounter &c2)
• bool operator== (const StatCounter &c1, int c2)
• bool operator!= (const StatCounter &c1, int c2)
• std::ostream & operator<< (std::ostream &os, const StatCounter &c)
• bool operator< (const Theorem &t1, const Theorem &t2)
• bool operator<= (const Theorem &t1, const Theorem &t2)
• bool operator> (const Theorem &t1, const Theorem &t2)
• bool operator>= (const Theorem &t1, const Theorem &t2)
• bool isReal (Type t)
• bool isInt (Type t)
• bool isRational (const Expr &e)
• bool isIntegerConst (const Expr &e)
• bool isUMinus (const Expr &e)
• bool isPlus (const Expr &e)
• bool isMinus (const Expr &e)
• bool isMult (const Expr &e)
• bool isDivide (const Expr &e)
• bool isPow (const Expr &e)
• bool isLT (const Expr &e)
• bool isLE (const Expr &e)
• bool isGT (const Expr &e)
• bool isGE (const Expr &e)
• bool isDarkShadow (const Expr &e)
• bool isGrayShadow (const Expr &e)
• bool isIneq (const Expr &e)
• bool isIntPred (const Expr &e)
• Expr uminusExpr (const Expr &child)
• Expr plusExpr (const Expr &left, const Expr &right)
• Expr plusExpr (const std::vector< Expr > &children)
• Expr minusExpr (const Expr &left, const Expr &right)
• Expr multExpr (const Expr &left, const Expr &right)
• Expr multExpr (const std::vector< Expr > &children)

  a Mult expr with two or more children
  

• Expr powExpr (const Expr &pow, const Expr &base)

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

• Expr divideExpr (const Expr &left, const Expr &right)
• Expr ltExpr (const Expr &left, const Expr &right)
• Expr leExpr (const Expr &left, const Expr &right)
• Expr gtExpr (const Expr &left, const Expr &right)
• Expr geExpr (const Expr &left, const Expr &right)
• Expr operator- (const Expr &child)
• Expr operator+ (const Expr &left, const Expr &right)
• Expr operator- (const Expr &left, const Expr &right)
• Expr operator * (const Expr &left, const Expr &right)
• Expr operator/ (const Expr &left, const Expr &right)
• bool isArray (const Type &t)
• bool isRead (const Expr &e)
• bool isWrite (const Expr &e)
• bool isArrayLiteral (const Expr &e)
• Type arrayType (const Type &type1, const Type &type2)
• Expr arrayLiteral (const Expr &ind, const Expr &body)
• Rational computeBVConst (const Expr &e)

  computes the integer value of a bitvector constant
  

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

  Printing NotifyList class.
  

• bool isDatatype (const Type &t)
• bool isConstructor (const Expr &e)
• bool isSelector (const Expr &e)
• bool isTester (const Expr &e)
• Expr getConstructor (const Expr &e)
• bool operator== (const Type &t1, const Type &t2)
• bool operator!= (const Type &t1, const Type &t2)
• std::ostream & operator<< (std::ostream &os, const Type &t)
• Literal operator! (const Variable &v)
• Literal operator! (const Literal &l)
• std::ostream & operator<< (std::ostream &os, const Literal &l)
• ostream & operator<< (ostream &os, const Clause &c)
• static void printLit (ostream &os, const Literal &l)
• ostream & operator<< (std::ostream &os, const CompactClause &c)
• ostream & operator<< (ostream &os, const Variable &l)
• ostream & operator<< (ostream &os, const VariableValue &v)
• Assumptions operator- (const Assumptions &a, const Expr &e)
• Assumptions operator- (const Assumptions &a, const vector< Expr > &es)
• ostream & operator<< (ostream &os, const Assumptions &assump)
• int compare (const Theorem &t1, const Theorem &t2)

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

• int compare (const Theorem &t1, const Expr &e2)
• int compareByPtr (const Theorem &t1, const Theorem &t2)
• ostream & operator<< (ostream &os, const TheoryArithNew::FreeConst &fc)
• ostream & operator<< (ostream &os, const TheoryArithNew::Ineq &ineq)
• ostream & operator<< (ostream &os, const TheoryArithOld::FreeConst &fc)
• ostream & operator<< (ostream &os, const TheoryArithOld::Ineq &ineq)
• 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 DebugTime &t1, const DebugTime &t2)
• bool 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)

Variables

• Debug debugger
• ParserTemp * parserTemp
• Debug debugger
• VCL * myvcl

---

Typedef Documentation

typedef long long unsigned CVC3::ExprIndex

Expression index type.

Definition at line 81 of file expr.h.

typedef enum CVC3::QueryResult CVC3::QueryResult

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

Definition at line 385 of file theorem.h.

typedef struct CVC3::dynTrig CVC3::dynTrig

---

Enumeration Type Documentation

enum CVC3::CLFlagType

Different types of command line flags.

Enumerator:

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

Definition at line 33 of file command_line_flags.h.

enum CVC3::ExprValueType

Type ID of each ExprValue subclass.

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

Enumerator:

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

Definition at line 65 of file expr.h.

enum CVC3::Kind

Enumerator:

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

Definition at line 29 of file kinds.h.

enum CVC3::InputLanguage

Different input languages.

Enumerator:

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

Definition at line 30 of file lang.h.

enum CVC3::QueryResult

Enumerator:

SATISFIABLE
INVALID
VALID
UNSATISFIABLE
ABORT
UNKNOWN

Definition at line 32 of file queryresult.h.

enum CVC3::ArithKinds

Enumerator:

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

Definition at line 31 of file theory_arith.h.

enum CVC3::ArrayKinds

Enumerator:

ARRAY
READ
WRITE
ARRAY_LITERAL

Definition at line 30 of file theory_array.h.

enum CVC3::BVKinds

Enumerator:

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

Definition at line 32 of file theory_bitvector.h.

enum CVC3::DatatypeKinds

Local kinds for datatypes.

Enumerator:

DATATYPE
CONSTRUCTOR
SELECTOR
TESTER

Definition at line 33 of file theory_datatype.h.

enum CVC3::Polarity

Enumerator:

Ukn
Pos
Neg
PosNeg

Definition at line 48 of file theory_quant.h.

enum CVC3::RecordKinds

Enumerator:

RECORD
RECORD_SELECT
RECORD_UPDATE
RECORD_TYPE
TUPLE
TUPLE_SELECT
TUPLE_UPDATE
TUPLE_TYPE

Definition at line 29 of file theory_records.h.

enum CVC3::UFKinds

Local kinds for transitive closure of binary relations.

Enumerator:

TRANS_CLOSURE
OLD_ARROW

Definition at line 31 of file theory_uf.h.

enum CVC3::ArithLang

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

Enumerator:

NOT_USED
TERMS_ONLY
DIFF_ONLY
LINEAR
NONLINEAR

Definition at line 48 of file translator.h.

---

Function Documentation

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

Definition at line 126 of file expr.cpp.

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

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

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

Definition at line 420 of file expr.cpp.

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

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

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

Definition at line 437 of file expr.cpp.

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

static bool CVC3::isTrivialExpr

(

const Expr &

e

)

[static]

Definition at line 48 of file expr_stream.cpp.

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

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

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

Function for fatal exit.

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

Definition at line 33 of file debug.cpp.

References std::endl().

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

Similar to fatalError to raise an exception when DebugAssert fires.

This does not necessarily cause the program to quit.

Definition at line 50 of file debug.cpp.

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

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

Definition at line 149 of file debug.h.

References CVC3::DebugFlag::d_flag.

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

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

Definition at line 153 of file debug.h.

References CVC3::DebugFlag::d_flag.

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

Printing flags.

Definition at line 157 of file debug.h.

References CVC3::DebugFlag::d_flag.

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

Definition at line 216 of file debug.h.

References CVC3::DebugCounter::d_counter.

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

Definition at line 219 of file debug.h.

References CVC3::DebugCounter::d_counter.

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

Definition at line 222 of file debug.h.

References CVC3::DebugCounter::d_counter.

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

Definition at line 225 of file debug.h.

References CVC3::DebugCounter::d_counter.

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

Definition at line 228 of file debug.h.

References CVC3::DebugCounter::d_counter.

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

Definition at line 231 of file debug.h.

References CVC3::DebugCounter::d_counter.

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

Definition at line 234 of file debug.h.

References CVC3::DebugCounter::d_counter.

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

Definition at line 52 of file exception.h.

References CVC3::Exception::toString().

Expr CVC3::andExpr

(

const std::vector< Expr > &

children

)

[inline]

Definition at line 867 of file expr.h.

References AND, and DebugAssert.

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

Expr CVC3::orExpr

(

const std::vector< Expr > &

children

)

[inline]

Definition at line 877 of file expr.h.

References DebugAssert, and OR.

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

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

Definition at line 1387 of file expr.h.

References CVC3::Expr::d_expr.

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

Definition at line 1392 of file expr.h.

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

Definition at line 1397 of file expr.h.

References compare().

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

Definition at line 1399 of file expr.h.

References compare().

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

Definition at line 1401 of file expr.h.

References compare().

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

Definition at line 1403 of file expr.h.

References compare().

InputLanguage CVC3::getLanguage

(

const std::string &

lang

)

[inline]

Definition at line 45 of file lang.h.

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

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

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

Definition at line 56 of file proof.h.

References CVC3::Proof::getExpr().

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

Definition at line 60 of file proof.h.

References CVC3::Proof::getExpr().

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

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

Definition at line 151 of file rational.h.

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

Referenced by CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), powExpr(), and CVC3::VCL::ratExpr().

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

Definition at line 166 of file rational.h.

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

Definition at line 167 of file rational.h.

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

Definition at line 169 of file rational.h.

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

Definition at line 171 of file rational.h.

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

Definition at line 173 of file rational.h.

void CVC3::printRational

(

const Rational &

x

)

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

Definition at line 276 of file search_sat.h.

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

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

Definition at line 66 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 69 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 72 of file statistics.h.

References CVC3::StatFlag::d_flag.

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

Definition at line 122 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 125 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 128 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 131 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 134 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 137 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 140 of file statistics.h.

References CVC3::StatCounter::d_counter.

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

Definition at line 410 of file theorem.h.

References compare().

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

Definition at line 412 of file theorem.h.

References compare().

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

Definition at line 414 of file theorem.h.

References compare().

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

Definition at line 416 of file theorem.h.

References compare().

bool CVC3::isReal

(

Type

t

)

[inline]

Definition at line 158 of file theory_arith.h.

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

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

bool CVC3::isInt

(

Type

t

)

[inline]

Definition at line 159 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::print(), CVC3::TheoryArithNew::print(), CVC3::Translator::printArrayExpr(), and CVC3::TheoryArithOld::projectInequalities().

bool CVC3::isRational

(

const Expr &

e

)

[inline]

Definition at line 162 of file theory_arith.h.

References CVC3::Expr::isRational().

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

bool CVC3::isIntegerConst

(

const Expr &

e

)

[inline]

Definition at line 163 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::checkType(), and CVC3::TheoryArithNew::checkType().

bool CVC3::isUMinus

(

const Expr &

e

)

[inline]

Definition at line 165 of file theory_arith.h.

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

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

bool CVC3::isPlus

(

const Expr &

e

)

[inline]

Definition at line 166 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::addToBuffer(), CVC3::TheoryArithNew::addToBuffer(), CVC3::TheoryArithNew::assertFact(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::TheoryArithNew::findCoefficient(), CVC3::ArithTheoremProducerOld::finiteInterval(), CVC3::ArithTheoremProducer::finiteInterval(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryArithOld::isolateVariable(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArithOld::pickMonomial(), CVC3::TheoryArithOld::processBuffer(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithNew::rewrite(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::separateMonomial(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer::substitute(), and CVC3::TheoryArithOld::updateSubsumptionDB().

bool CVC3::isMinus

(

const Expr &

e

)

[inline]

Definition at line 167 of file theory_arith.h.

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

bool CVC3::isMult

(

const Expr &

e

)

[inline]

Definition at line 168 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::assertFact(), CVC3::TheoryArithNew::assertFact(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDivideMult(), CVC3::ArithTheoremProducer::canonDivideMult(), CVC3::ArithTheoremProducerOld::canonMultMtermMterm(), CVC3::ArithTheoremProducer::canonMultMtermMterm(), CVC3::TheoryArithOld::computeNormalFactor(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ab(), CVC3::ArithTheoremProducer::darkGrayShadow2ab(), CVC3::ArithTheoremProducerOld::darkGrayShadow2ba(), CVC3::ArithTheoremProducer::darkGrayShadow2ba(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::TheoryArithNew::findCoefficient(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::TheoryArithOld::isolateVariable(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducer::monomialMulF(), CVC3::TheoryArithNew::normalize(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::ArithTheoremProducerOld::oneElimination(), CVC3::ArithTheoremProducer::oneElimination(), CVC3::TheoryArithOld::pickIntEqMonomial(), CVC3::TheoryArithNew::pickIntEqMonomial(), CVC3::TheoryArithOld::processFiniteInterval(), CVC3::TheoryArithNew::processFiniteInterval(), CVC3::TheoryArithOld::processRealEq(), CVC3::TheoryArithNew::processRealEq(), CVC3::TheoryArithOld::processSimpleIntEq(), CVC3::TheoryArithNew::processSimpleIntEq(), CVC3::TheoryArithOld::projectInequalities(), CVC3::TheoryArithOld::separateMonomial(), CVC3::TheoryArithNew::separateMonomial(), CVC3::ArithTheoremProducerOld::substitute(), and CVC3::ArithTheoremProducer::substitute().

bool CVC3::isDivide

(

const Expr &

e

)

[inline]

Definition at line 169 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), and CVC3::TheoryArith::isSyntacticRational().

bool CVC3::isPow

(

const Expr &

e

)

[inline]

Definition at line 170 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::projectInequalities().

bool CVC3::isLT

(

const Expr &

e

)

[inline]

Definition at line 171 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::TheoryArithOld::assertFact(), CVC3::ArithTheoremProducerOld::clashingBounds(), CVC3::ArithTheoremProducer::clashingBounds(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), isIneq(), CVC3::TheoryArithOld::isolateVariable(), CVC3::TheoryArithOld::isStale(), isSysPred(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducerOld::negatedInequality(), CVC3::ArithTheoremProducer::negatedInequality(), CVC3::TheoryQuant::newTopMatch(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryArithOld::projectInequalities(), CVC3::ArithTheoremProducerOld::realShadow(), CVC3::ArithTheoremProducer::realShadow(), CVC3::TheoryArithOld::setup(), and CVC3::TheoryArithOld::updateSubsumptionDB().

bool CVC3::isLE

(

const Expr &

e

)

[inline]

Definition at line 172 of file theory_arith.h.

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

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

bool CVC3::isGT

(

const Expr &

e

)

[inline]

Definition at line 173 of file theory_arith.h.

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

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

bool CVC3::isGE

(

const Expr &

e

)

[inline]

Definition at line 174 of file theory_arith.h.

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

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

bool CVC3::isDarkShadow

(

const Expr &

e

)

[inline]

Definition at line 175 of file theory_arith.h.

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

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

bool CVC3::isGrayShadow

(

const Expr &

e

)

[inline]

Definition at line 176 of file theory_arith.h.

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

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

bool CVC3::isIneq

(

const Expr &

e

)

[inline]

Definition at line 177 of file theory_arith.h.

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

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

bool CVC3::isIntPred

(

const Expr &

e

)

[inline]

Definition at line 179 of file theory_arith.h.

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

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

Expr CVC3::uminusExpr

(

const Expr &

child

)

[inline]

Definition at line 182 of file theory_arith.h.

References UMINUS.

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

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

Definition at line 184 of file theory_arith.h.

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

Referenced by CVC3::ArithTheoremProducerOld::addInequalities(), CVC3::ArithTheoremProducer::addInequalities(), CVC3::ArithTheoremProducerOld::canonCombineLikeTerms(), CVC3::ArithTheoremProducerOld::canonComboLikeTerms(), CVC3::ArithTheoremProducer::canonComboLikeTerms(), CVC3::ArithTheoremProducerOld::canonDividePlus(), CVC3::ArithTheoremProducer::canonDividePlus(), CVC3::ArithTheoremProducerOld::canonFlattenSum(), CVC3::ArithTheoremProducer::canonFlattenSum(), CVC3::ArithTheoremProducerOld::canonMultConstSum(), CVC3::ArithTheoremProducer::canonMultConstSum(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducerOld::moveSumConstantRight(), CVC3::ArithTheoremProducer::moveSumConstantRight(), operator+(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArithNew::pivotRule(), CVC3::ArithTheoremProducerOld::substitute(), CVC3::ArithTheoremProducer::substitute(), and CVC3::TheoryArithOld::updateSubsumptionDB().

Expr CVC3::plusExpr

(

const std::vector< Expr > &

children

)

[inline]

Definition at line 186 of file theory_arith.h.

References DebugAssert, and PLUS.

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

Definition at line 190 of file theory_arith.h.

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

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

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

Definition at line 192 of file theory_arith.h.

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

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

Expr CVC3::multExpr

(

const std::vector< Expr > &

children

)

[inline]

a Mult expr with two or more children

Definition at line 196 of file theory_arith.h.

References DebugAssert, and MULT.

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

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

Definition at line 201 of file theory_arith.h.

References pow(), and POW.

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

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

Definition at line 204 of file theory_arith.h.

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

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

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

Definition at line 206 of file theory_arith.h.

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

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

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

Definition at line 208 of file theory_arith.h.

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

Referenced by CVC3::TheoryArithOld::computeTypePred(), CVC3::TheoryArithNew::computeTypePred(), CVC3::ArithTheoremProducerOld::eqToIneq(), CVC3::ArithTheoremProducer::eqToIneq(), CVC3::ArithTheoremProducerOld::expandDarkShadow(), CVC3::ArithTheoremProducer::expandDarkShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::VCL::leExpr(), CVC3::ArithTheoremProducerOld::lessThanToLE(), CVC3::ArithTheoremProducer::lessThanToLE(), CVC3::ArithTheoremProducer::multIneqn(), CVC3::TheoryArithOld::parseExprOp(), CVC3::TheoryArithNew::parseExprOp(), CVC3::TheoryArithNew::rewrite(), and CVC3::TheoryArithOld::updateSubsumptionDB().

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

Definition at line 210 of file theory_arith.h.

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

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

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

Definition at line 212 of file theory_arith.h.

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

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

Expr CVC3::operator-

(

const Expr &

child

)

[inline]

Definition at line 215 of file theory_arith.h.

References uminusExpr().

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

Definition at line 217 of file theory_arith.h.

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

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

Definition at line 219 of file theory_arith.h.

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

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

Definition at line 221 of file theory_arith.h.

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

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

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

Definition at line 223 of file theory_arith.h.

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

bool CVC3::isArray

(

const Type &

t

)

[inline]

Definition at line 92 of file theory_array.h.

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

Referenced by CVC3::TheoryArray::computeModel(), CVC3::TheoryArray::computeType(), and CVC3::Translator::printArrayExpr().

bool CVC3::isRead

(

const Expr &

e

)

[inline]

Definition at line 93 of file theory_array.h.

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

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

bool CVC3::isWrite

(

const Expr &

e

)

[inline]

Definition at line 94 of file theory_array.h.

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

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

bool CVC3::isArrayLiteral

(

const Expr &

e

)

[inline]

Definition at line 95 of file theory_array.h.

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

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

Definition at line 99 of file theory_array.h.

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

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

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

Definition at line 751 of file theory_array.cpp.

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

Referenced by CVC3::TheoryArray::computeModel().

Rational CVC3::computeBVConst

(

const Expr &

e

)

computes the integer value of a bitvector constant

Definition at line 4462 of file theory_bitvector.cpp.

References BVCONST, DebugAssert, CVC3::Expr::getExprValue(), CVC3::Expr::getKind(), CVC3::BVConstExpr::getValue(), CVC3::BVConstExpr::size(), and CVC3::Expr::toString().

Referenced by CVC3::BitvectorTheoremProducer::zeroLeq().

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

Printing NotifyList class.

Definition at line 90 of file theory_core.cpp.

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

bool CVC3::isDatatype

(

const Type &

t

)

[inline]

Definition at line 124 of file theory_datatype.h.

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

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

bool CVC3::isConstructor

(

const Expr &

e

)

[inline]

Definition at line 127 of file theory_datatype.h.

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

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

bool CVC3::isSelector

(

const Expr &

e

)

[inline]

Definition at line 131 of file theory_datatype.h.

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

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

bool CVC3::isTester

(

const Expr &

e

)

[inline]

Definition at line 134 of file theory_datatype.h.

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

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

Expr CVC3::getConstructor

(

const Expr &

e

)

[inline]

Definition at line 137 of file theory_datatype.h.

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

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

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

Definition at line 150 of file type.h.

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

Definition at line 153 of file type.h.

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

Definition at line 157 of file type.h.

Literal CVC3::operator!

(

const Variable &

v

)

[inline]

Definition at line 188 of file variable.h.

Literal CVC3::operator!

(

const Literal &

l

)

[inline]

Definition at line 192 of file variable.h.

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

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

Definition at line 217 of file variable.cpp.

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

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

Definition at line 135 of file clause.cpp.

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

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

Definition at line 157 of file clause.cpp.

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

Referenced by operator<<().

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

Definition at line 164 of file clause.cpp.

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

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

Definition at line 202 of file variable.cpp.

References CVC3::Variable::d_val.

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

Definition at line 337 of file variable.cpp.

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

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

Definition at line 284 of file assumptions.cpp.

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

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

Definition at line 294 of file assumptions.cpp.

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

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

Definition at line 304 of file assumptions.cpp.

References CVC3::Assumptions::d_vector.

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

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

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

Definition at line 45 of file theorem.cpp.

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

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

Definition at line 65 of file theorem.cpp.

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

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

Definition at line 83 of file theorem.cpp.

References CVC3::Theorem::d_thm.

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

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

Definition at line 44 of file theory_arith_new.cpp.

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

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

Definition at line 54 of file theory_arith_new.cpp.

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

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

Definition at line 44 of file theory_arith_old.cpp.

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

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

Definition at line 54 of file theory_arith_old.cpp.

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

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

Definition at line 94 of file debug.cpp.

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

Definition at line 99 of file debug.cpp.

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

Definition at line 105 of file debug.cpp.

References CVC3::DebugTime::d_clock.

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

Definition at line 109 of file debug.cpp.

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

Definition at line 113 of file debug.cpp.

References CVC3::DebugTime::d_clock.

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

Definition at line 117 of file debug.cpp.

References CVC3::DebugTime::d_clock.

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

Definition at line 121 of file debug.cpp.

References CVC3::DebugTime::d_clock.

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

Definition at line 125 of file debug.cpp.

References CVC3::DebugTime::d_clock.

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

Definition at line 219 of file debug.cpp.

References CVC3::DebugTimer::d_time.

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

Definition at line 222 of file debug.cpp.

References CVC3::DebugTimer::d_time.

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

Definition at line 225 of file debug.cpp.

References CVC3::DebugTimer::d_time.

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

Definition at line 228 of file debug.cpp.

References CVC3::DebugTimer::d_time.

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

Definition at line 231 of file debug.cpp.

References CVC3::DebugTimer::d_time.

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

Definition at line 234 of file debug.cpp.

References CVC3::DebugTimer::d_time.

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

Definition at line 239 of file debug.cpp.

References CVC3::DebugTime::d_clock.

ostream& CVC3::operator<<	(	std::ostream &	os,
		const DebugTimer &	timer
	)

Definition at line 245 of file debug.cpp.

References CVC3::DebugTimer::d_time.

---

Variable Documentation

Debug CVC3::debugger

Definition at line 365 of file debug.cpp.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryBitvector::addSharedTerm(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::SearchSat::check(), CVC3::Scope::check(), CVC3::TheoryUF::checkSat(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryCore::checkSATCore(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::TheoryArithOld::doSolve(), CVC3::TheoryArithNew::doSolve(), CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::evaluateNext(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::SearchEngineFast::findSplitter(), CVC3::DecisionEngineMBTF::findSplitter(), CVC3::DecisionEngineDFS::findSplitter(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::fullCheck(), IF_DEBUG(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::TheoryArithNew::kidsCanonical(), CVC3::CNF_TheoremProducer::learnedClause(), main(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), CVC3::SearchImplBase::newUserAssumption(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::projectInequalities(), CVC3::Context::push(), CVC3::SearchEngineFast::recordFact(), CVC3::Expr::recursiveSubst(), CVC3::TheoryUF::rewrite(), CVC3::TheoryBitvector::rewrite(), CVC3::TheoryArray::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::Theory::setInconsistent(), CVC3::SearchEngineFast::setInconsistent(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::setupTriggers(), sighandler(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryArithOld::solvedForm(), CVC3::TheoryArithNew::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::SearchEngineFast::traceConflict(), CVC3::TheoryArithOld::update(), and CVC3::TheoryArithNew::update().

ParserTemp* CVC3::parserTemp

Debug CVC3::debugger

Definition at line 365 of file debug.cpp.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::TheoryBitvector::addSharedTerm(), CVC3::SearchEngineFast::analyzeUIPs(), CVC3::TheoryArithOld::assertFact(), CVC3::TheoryCore::assertFactCore(), CVC3::TheoryCore::assertFormula(), CVC3::SearchEngineFast::bcp(), CVC3::TheoryBitvector::bitBlastDisEqn(), CVC3::TheoryBitvector::bitBlastEqn(), CVC3::Scope::check(), CVC3::SearchSat::check(), CVC3::TheoryQuant::checkSat(), CVC3::TheoryUF::checkSat(), CVC3::TheoryCore::checkSATCore(), CVC3::SearchEngineTheoremProducer::conflictClause(), CVC3::TheoryArithNew::doSolve(), CVC3::TheoryArithOld::doSolve(), CVC3::VCCmd::evaluateCommand(), CVC3::VCCmd::evaluateNext(), CVC3::SearchEngineTheoremProducer::findInLocalCache(), CVC3::DecisionEngineCaching::findSplitter(), CVC3::DecisionEngineDFS::findSplitter(), CVC3::DecisionEngineMBTF::findSplitter(), CVC3::SearchEngineFast::findSplitter(), CVC3::SearchEngineFast::fixConflict(), CVC3::SearchEngineFast::fullCheck(), IF_DEBUG(), CVC3::TheoryArithNew::kidsCanonical(), CVC3::TheoryArithOld::kidsCanonical(), CVC3::CNF_TheoremProducer::learnedClause(), main(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::newTheorem3(), CVC3::SearchImplBase::newUserAssumption(), CVC3::TheoryArithOld::normalizeProjectIneqs(), CVC3::TheoryQuant::notifyInconsistent(), CVC3::TheoryCore::processEquality(), CVC3::TheoryArithOld::projectInequalities(), CVC3::Context::push(), CVC3::SearchEngineFast::recordFact(), CVC3::Expr::recursiveSubst(), CVC3::TheoryArray::rewrite(), CVC3::TheoryBitvector::rewrite(), CVC3::TheoryUF::rewrite(), CVC3::TheoryBitvector::rewriteBV(), CVC3::SearchEngineFast::setInconsistent(), CVC3::Theory::setInconsistent(), CVC3::TheoryCore::setupTerm(), CVC3::TheoryQuant::setupTriggers(), sighandler(), CVC3::TheoryCore::simplifyOp(), CVC3::TheoryArithNew::solvedForm(), CVC3::TheoryArithOld::solvedForm(), CVC3::SearchEngineFast::split(), CVC3::CommonTheoremProducer::substitutivityRule(), CVC3::SearchEngineFast::traceConflict(), CVC3::TheoryArithNew::update(), and CVC3::TheoryArithOld::update().

VCL* CVC3::myvcl

Definition at line 48 of file vcl.cpp.

---