Expr

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

Kinds

Kind is an enum embedded in each Expr to describe how to interpret the expression. In the smtlib expression "(= (+ x 1) 0)", the quality has the kind EQUAL, "(+ x 1)" is a PLUS, "0" and "1" have kind CONST_RATIONAL, and "x" has kind VARIABLE. You can get the Kind of an Expr using getKind().

The name space kinds live in is "CVC4::kind". Kinds are defined in src/theory/*/kinds files. These are scripts for defining new kinds of expressions. Each theory has its own kinds file. See the theory/builtin/kinds file for more information on kinds files: [[1]]. The *definitive* header file used for compilation is $CVC4/src/expr/kind.h is a generated file. If you are using a distributed source tarball this will be in this location. Otherwise, look in $CVC4/builds/src/expr/kind.h. (For this reason it will not appear in the source repositories like git.)

Constants

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. em.mkConst(true) makes a constant expression.

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

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

To make the constant, 1, you can use:

• em.mkConst(1)
• em.mkConst(Rational(1,1))
• em.mkConst(Integer(1)) [This will use Rational(const Integer& i).]

mkConst() allows for arbitrary other classes to be included into the expr system. Most of the types T for use with mkConst() is to internally break out of the Expr system. For example, CVC4::BitVectorSize is a struct wrapping around unsigned size;. Here is a complete list of

• arrays
  • CVC4::ArrayStoreAll
• arith
  • CVC4::Rational
  • CVC4::SubrangeBounds
• booleans
  • bool
• builtin
  • CVC4::UninterpretedConstant
  • CVC4::AbstractValue
  • CVC4::Kind
  • CVC4::TypeConstant
  • std::string
  • CVC4::Predicate
• 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