Expr - Revision history

Taking: /* Const */

2012-12-07T00:11:04Z

‎Const

Taking: /* Const */

2012-12-07T00:10:39Z

‎Const

Taking: /* Const */

2012-12-07T00:10:19Z

‎Const

Taking: 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…"

2012-12-06T23:34:33Z

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…"

New page

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 <code>mkConst(const T&);</code> 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)

@@ Line 6: / Line 6: @@
 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: [[https://github.com/CVC4/CVC4/blob/master/src/theory/builtin/kinds]].  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 <code>$CVC4/builds/src/expr/kind.h</code>. (For this reason it will not appear in the source repositories like git.)
-=Const=
+=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 <code>mkConst(const T&);</code> for T.  <code>em.mkConst(true)</code> makes a constant expression.

@@ Line 33: / Line 33: @@
 ** CVC4::UninterpretedConstant
 ** CVC4::AbstractValue
-** ::CVC4::Kind
+** CVC4::Kind
-** ::CVC4::TypeConstant
+** CVC4::TypeConstant
 ** std::string
 ** CVC4::Predicate

@@ Line 1: / Line 1: @@
 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 <code>mkConst(const T&);</code> for T.
+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 <code>mkConst(const T&);</code> for T.  <code>em.mkConst(true)</code> makes a constant expression.
 Commonly used types T that can be used with mkConst(const T&):
@@ Line 11: / Line 16: @@
 * 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:
+To make the constant, 1, you can use:
 * bv
 ** CVC4::BitVector
@@ Line 30: / Line 55: @@
 ** CVC4::RecordSelect
 ** CVC4::RecordUpdate