Expr

From CVC4
Revision as of 16:34, 6 December 2012 by Taking (Talk | contribs) (Created page with "Expr is CVC4's public-facing symbolic expression interface. Exprs are linked to a an ExprManager. ExprManagers take care of memory management for Exprs (allocation, garbage coll…")

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Expr is CVC4's public-facing symbolic expression interface. Exprs are linked to a an ExprManager. ExprManagers take care of memory management for Exprs (allocation, garbage collection, etc.)

Const

CVC4 supports making constant expressions for a number of different types: true, 5, 0bin0100, etc. To make a constant expression for an ExprManager em, use mkConst(const T&); for T.

Commonly used types T that can be used with mkConst(const T&):

  • bool
  • CVC4::Rational
  • CVC4::BitVector
  • std::string
  • CVC4::Datatype

mkConst() allows for arbitrary other kinds to be included into the expr system. Must of the types T for use with mkConst() is to internally break out of the expr system:

  • bv
    • CVC4::BitVector
    • CVC4::BitVectorSize
    • CVC4::BitVectorBitOf
    • CVC4::BitVectorExtract
    • CVC4::BitVectorRepeat
    • CVC4::BitVectorZeroExtend
    • CVC4::BitVectorSignExtend
    • CVC4::BitVectorRotateLeft
    • CVC4::BitVectorRotateRight
  • datatypes
    • CVC4::Datatype
    • CVC4::AscriptionType
    • CVC4::TupleSelect
    • CVC4::TupleUpdate
    • CVC4::Record
    • CVC4::RecordSelect
    • CVC4::RecordUpdate
  • builtin
    •  ::CVC4::UninterpretedConstant


  • uf
    • (See builtin)
CVC4::Predicate
CVC4::Rational
CVC4::SubrangeBounds


CVC4::UninterpretedConstant
CVC4::AbstractValue
CVC4::Kind
CVC4::TypeConstant
  • CVC4::ArrayStoreAll (INTERNAL)
  • CVC4::TypeConstant (internal)
Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=Expr&oldid=4075"