Difference between revisions of "Datatypes"

From CVC4
Jump to: navigation, search
(→‎Syntax/API)
 
(30 intermediate revisions by the same user not shown)
Line 1: Line 1:
 +
=Logic=
 +
To enable CVC4's decision procedure for datatypes, include "DT" in the logic:
 +
  (set-logic QF_UFDT)
 +
Alternatively, use the "ALL_SUPPORTED" logic:
 +
  (set-logic ALL_SUPPORTED)
 +
 
=Syntax=
 
=Syntax=
−
CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files:
+
CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files in the smt lib 2.6 format:
−
   (declare-datatypes (U1...Un)  
+
   (declare-datatypes ((D1 n1)...(Dk nk))  
−
     ((D1 (C1 (S1 T1)....(Si Ti))
+
     (((C1 (S1 T1)....(Si Ti))...(Cj .... ))
 
     ...
 
     ...
−
     (Cj .... ))...(Dk (....) ... (....)))
+
     ((....) ... (....)))
  
−
where D1...Dk are datatype types, C1...Cj are the constructors for datatype D1, S1....Si are the selectors (or "destructors") of constructor C1, and each T1...Ti is a previously declared type or one of D1...k. The symbols U1...Un are type parameters (fresh symbols).
+
where D1...Dk are datatype types, C1...Cj are the constructors for datatype D1, S1....Si are the selectors (or "destructors") of constructor C1, and each T1...Ti is a previously declared type or one of D1...k. The symbols U1...Un are type parameters (fresh symbols).  The numbers n1...nk denote the number of type parameters for the datatype, where 0 is used for non-parametric datatypes.
  
−
In addition to declaring symbols for constructors and selectors, the above command also adds tester symbols of the form "is-C1", ..., "is-Cn" for constructors C1, ... Cn.
+
In addition to declaring symbols for constructors and selectors, the above command also adds tester (or "discriminator") indexed symbols of the form (_ is C) for each constructor C, which are unary predicates which evaluate to true iff their argument has top-symbol C.
 +
 
 +
CVC4 also supports datatypes in its native format [http://cvc4.cs.nyu.edu/wiki/CVC4%27s_native_language#Inductive_Data_Types].
 +
 
 +
=Semantics=
 +
 
 +
The decision procedure for inductive datatypes can be found [http://homepage.cs.uiowa.edu/~tinelli/papers/BarST-JSAT-07.pdf here].
  
 
=Example Declarations=
 
=Example Declarations=
 
An enumeration:
 
An enumeration:
−
   (declare-datatypes ()  
+
   (declare-datatypes ((Color 0))  
−
     ((Color (Red) (Black))))
+
     (((Red) (Black))))
  
 
A List of Int with "cons" and "nil" as constructors:
 
A List of Int with "cons" and "nil" as constructors:
−
   (declare-datatypes ()  
+
   (declare-datatypes ((list 0))  
−
     ((list (cons (head Int) (tail list)) (nil))))
+
     (((cons (head Int) (tail list)) (nil))))
  
 
A parametric List of T's:
 
A parametric List of T's:
−
   (declare-datatypes (T)  
+
   (declare-datatypes ((list 1))  
−
     ((list (cons (head T) (tail (list T))) (nil))))
+
     ((par (T) ((cons (head T) (tail (list T))) (nil)))))
  
 
Mutual recursion:
 
Mutual recursion:
−
   (declare-codatatypes ()  
+
   (declare-datatypes ((list 0) (tree 0))  
−
     ((list (cons (head tree) (tail list)) (nil))
+
     (((cons (head tree) (tail list)) (nil))
−
     (tree (node (data Int) (children list)))))
+
     ((node (data Int) (children list)))))
−
+
 
 +
A (non-recursive) record type:
 +
  (declare-datatypes ((record 0))
 +
    (((rec (fname String) (lname String) (id Int)))))
 +
 
 
=Examples=
 
=Examples=
 +
 +
  (declare-datatypes ((list 0))
 +
    (((cons (head Int) (tail list)) (nil))))
 +
  (declare-fun a () list)
 +
  (declare-fun b () list)
 +
  (assert (and (= (tail a) b) (not ((_ is nil) b)) (> (head b) 0)))
 +
  (check-sat)
 +
 +
  (declare-datatypes ((record 0))
 +
    (((rec (fname String) (lname String) (id Int)))))
 +
  (declare-const x record)
 +
  (assert (and (= (fname x) "John") (= (lname x) "Smith")))
 +
  (check-sat)
  
 
=Parametric Datatypes=
 
=Parametric Datatypes=
  
 
Instances of parametric datatypes must have their arguments instantiated with concrete types. For instance, in the example:
 
Instances of parametric datatypes must have their arguments instantiated with concrete types. For instance, in the example:
−
   (declare-datatypes (T) ((list (cons (head T) (tail (list T))) (nil))))
+
   (declare-datatypes ((list 1)) ((par (T) (cons (head T) (tail (list T))) (nil))))
  
 
To declare a list of Int, use the command:
 
To declare a list of Int, use the command:
−
   (declare-fun f () (List Int))
+
   (declare-fun f () (list Int))
  
 
Use of constructors that are ambiguously typed must be cast to a concrete type, for instance all occurrences of "nil" for the above datatype must be cast with the syntax:
 
Use of constructors that are ambiguously typed must be cast to a concrete type, for instance all occurrences of "nil" for the above datatype must be cast with the syntax:
−
   (as nil (List Int))
+
   (as nil (list Int))
 +
 
 +
=Tuples=
 +
 
 +
Tuples are a particular instance of an inductive datatype. CVC4 supports special syntax for tuples as an extension of the SMT-LIB version 2 format. For example:
 +
  (declare-fun t () (Tuple Int Int))
 +
  (assert (= ((_ tupSel 0) t) 3))
 +
  (assert (not (= t (mkTuple 3 4))))
 +
 
 +
=Codatatypes=
 +
 
 +
CVC4 also supports co-inductive datatypes, as described [http://homepage.cs.uiowa.edu/~ajreynol/cade15.pdf here].  The syntax for declaring mutually recursive coinductive datatype blocks is identical to inductive datatypes, except that "declare-datatypes" is replaced by "declare-codatatypes".  For example, the following declares the type denote streams of Int:
 +
  (declare-codatatypes ((stream 0))
 +
    (((cons (head Int) (tail stream)))))
 +
 
 +
=Syntax/API=
 +
 
 +
{| class="wikitable" cellpadding="5" border="0" style="border-collapse:collapse"
 +
|-
 +
!
 +
! CVC language
 +
! SMTLIB language
 +
! C++ API
 +
|-
 +
| Logic string
 +
| Not needed
 +
| <code>(set-logic QF_'''DT''')</code>
 +
| <code>smt.setLogic("QF_'''DT'''");</code>
 +
|-
 +
| Tuple Sort
 +
| [<Sort_1>, ..., <Sort_n>]
 +
| (Tuple <Sort_1>, ..., <Sort_n>)
 +
| CVC4::ExprManager::mkTupleType(std::vector<CVC4::Type>& types)
 +
|-
 +
|
 +
| <code>t: '''[INT, INT]''';</code>
 +
| <code> (declare-fun t () '''(Tuple Int Int)''') </code>
 +
| <code>std::vector<Type> types;</code><br>
 +
<code>types.push_back(em.mkIntegerType());</code><br>
 +
<code>types.push_back(em.mkIntegerType());</code><br>
 +
<code>em.'''mkTupleType'''( types );</code>
 +
|-
 +
| Tuple constructor
 +
| <code>'''(t1, ..., tn)'''</code>
 +
| <code>('''mkTuple''' t1, ..., tn)</code>
 +
| <code>DatatypeType tt = em.mkTupleType(types);</code>
 +
<code>const Datatype& dt = tt.getDatatype();</code><br>
 +
<code>Expr c = dt[0].getConstructor();</code><br>
 +
<code>em.mkExpr('''kind::APPLY_CONSTRUCTOR''', c, t1, ..., tn);</code>
 +
|-
 +
| Tuple selector
 +
| <code>'''t.i'''</code>
 +
| <code>('''(_ tupSel i)''' t)</code>
 +
| <code>DatatypeType tt = em.mkTupleType(types);</code><br>
 +
<code>const Datatype& dt = tt.getDatatype();</code><br>
 +
<code>Expr s = dt[0][i].getSelector();</code><br>
 +
<code>em.mkExpr('''kind::APPLY_SELECTOR''', s, t);</code>
 +
|-
 +
| Record Sort
 +
| [# f1:<Sort_1>, ..., fn:<Sort_n> #]
 +
| n/a
 +
| CVC4::ExprManager::mkRecordType(const Record& r)
 +
|-
 +
|
 +
| <code>t: '''[#''' fst:'''INT''', snd:'''INT]''';</code>
 +
| n/a
 +
| <code>std::vector< std::pair<std::string, Type> > vec;</code><br>
 +
<code>vec.push_back(std::pair<std::string, Type>("fst",em.integerType());</code><br>
 +
<code>vec.push_back(std::pair<std::string, Type>("snd",em.integerType());</code><br>
 +
<code>Record r(vec);</code><br>
 +
<code>em.'''mkRecordType'''(r);</code>
 +
|-
 +
| Record constructor
 +
| <code>'''(# f1 := t1, ..., fn := tn #)'''</code>
 +
| n/a
 +
| <code>Record r(vec);</code><br>
 +
<code>DatatypeType tt = em.mkRecordType(r);</code><br>
 +
<code>const Datatype& dt = tt.getDatatype();</code><br>
 +
<code>Expr c = dt[0].getConstructor();</code><br>
 +
<code>em.mkExpr('''kind::APPLY_CONSTRUCTOR''', c, t1, ..., tn);</code>
 +
|-
 +
| Record selector
 +
| <code>'''f1(t)'''</code>
 +
| n/a
 +
| <code>Record r(vec);</code><br>
 +
<code>DatatypeType tt = em.mkRecordType(r);</code><br>
 +
<code>const Datatype& dt = tt.getDatatype();</code><br>
 +
<code>Expr s = dt[0][i].getSelector();</code><br>
 +
<code>em.mkExpr('''kind::APPLY_SELECTOR''', s, t);</code>
 +
|-}

Latest revision as of 10:51, 8 May 2018

Logic

To enable CVC4's decision procedure for datatypes, include "DT" in the logic: 

 (set-logic QF_UFDT)

Alternatively, use the "ALL_SUPPORTED" logic: 

 (set-logic ALL_SUPPORTED)

Syntax

CVC4 supports the following syntax for declaring mutually recursive blocks of datatypes in *.smt2 input files in the smt lib 2.6 format: 

 (declare-datatypes ((D1 n1)...(Dk nk)) 
   (((C1 (S1 T1)....(Si Ti))...(Cj .... ))
    ...
    ((....) ... (....)))

where D1...Dk are datatype types, C1...Cj are the constructors for datatype D1, S1....Si are the selectors (or "destructors") of constructor C1, and each T1...Ti is a previously declared type or one of D1...k. The symbols U1...Un are type parameters (fresh symbols). The numbers n1...nk denote the number of type parameters for the datatype, where 0 is used for non-parametric datatypes.

In addition to declaring symbols for constructors and selectors, the above command also adds tester (or "discriminator") indexed symbols of the form (_ is C) for each constructor C, which are unary predicates which evaluate to true iff their argument has top-symbol C.

CVC4 also supports datatypes in its native format [1].

Semantics

The decision procedure for inductive datatypes can be found here.

Example Declarations

An enumeration: 

 (declare-datatypes ((Color 0)) 
   (((Red) (Black))))

A List of Int with "cons" and "nil" as constructors: 

 (declare-datatypes ((list 0)) 
   (((cons (head Int) (tail list)) (nil))))

A parametric List of T's: 

 (declare-datatypes ((list 1)) 
   ((par (T) ((cons (head T) (tail (list T))) (nil)))))

Mutual recursion: 

 (declare-datatypes ((list 0) (tree 0)) 
   (((cons (head tree) (tail list)) (nil))
    ((node (data Int) (children list)))))

A (non-recursive) record type: 

 (declare-datatypes ((record 0))
   (((rec (fname String) (lname String) (id Int)))))

Examples

 (declare-datatypes ((list 0)) 
   (((cons (head Int) (tail list)) (nil))))
 (declare-fun a () list)
 (declare-fun b () list)
 (assert (and (= (tail a) b) (not ((_ is nil) b)) (> (head b) 0)))
 (check-sat)

 (declare-datatypes ((record 0))
   (((rec (fname String) (lname String) (id Int)))))
 (declare-const x record)
 (assert (and (= (fname x) "John") (= (lname x) "Smith")))
 (check-sat)

Parametric Datatypes

Instances of parametric datatypes must have their arguments instantiated with concrete types. For instance, in the example: 

 (declare-datatypes ((list 1)) ((par (T) (cons (head T) (tail (list T))) (nil))))

To declare a list of Int, use the command: 

 (declare-fun f () (list Int))

Use of constructors that are ambiguously typed must be cast to a concrete type, for instance all occurrences of "nil" for the above datatype must be cast with the syntax: 

 (as nil (list Int))

Tuples

Tuples are a particular instance of an inductive datatype. CVC4 supports special syntax for tuples as an extension of the SMT-LIB version 2 format. For example: 

 (declare-fun t () (Tuple Int Int))
 (assert (= ((_ tupSel 0) t) 3))
 (assert (not (= t (mkTuple 3 4))))

Codatatypes

CVC4 also supports co-inductive datatypes, as described here. The syntax for declaring mutually recursive coinductive datatype blocks is identical to inductive datatypes, except that "declare-datatypes" is replaced by "declare-codatatypes". For example, the following declares the type denote streams of Int: 

 (declare-codatatypes ((stream 0)) 
   (((cons (head Int) (tail stream)))))

Syntax/API

CVC language SMTLIB language C++ API
Logic string Not needed (set-logic QF_DT) smt.setLogic("QF_DT");
Tuple Sort [<Sort_1>, ..., <Sort_n>] (Tuple <Sort_1>, ..., <Sort_n>) CVC4::ExprManager::mkTupleType(std::vector<CVC4::Type>& types)
t: [INT, INT]; (declare-fun t () (Tuple Int Int)) std::vector<Type> types;

types.push_back(em.mkIntegerType());
types.push_back(em.mkIntegerType());
em.mkTupleType( types );

Tuple constructor (t1, ..., tn) (mkTuple t1, ..., tn) DatatypeType tt = em.mkTupleType(types);

const Datatype& dt = tt.getDatatype();
Expr c = dt[0].getConstructor();
em.mkExpr(kind::APPLY_CONSTRUCTOR, c, t1, ..., tn);

Tuple selector t.i ((_ tupSel i) t) DatatypeType tt = em.mkTupleType(types);

const Datatype& dt = tt.getDatatype();
Expr s = dt[0][i].getSelector();
em.mkExpr(kind::APPLY_SELECTOR, s, t);

Record Sort [# f1:<Sort_1>, ..., fn:<Sort_n> #] n/a CVC4::ExprManager::mkRecordType(const Record& r)
t: [# fst:INT, snd:INT]; n/a std::vector< std::pair<std::string, Type> > vec;

vec.push_back(std::pair<std::string, Type>("fst",em.integerType());
vec.push_back(std::pair<std::string, Type>("snd",em.integerType());
Record r(vec);
em.mkRecordType(r);

Record constructor (# f1 := t1, ..., fn := tn #) n/a Record r(vec);

DatatypeType tt = em.mkRecordType(r);
const Datatype& dt = tt.getDatatype();
Expr c = dt[0].getConstructor();
em.mkExpr(kind::APPLY_CONSTRUCTOR, c, t1, ..., tn);

Record selector f1(t) n/a Record r(vec);

DatatypeType tt = em.mkRecordType(r);
const Datatype& dt = tt.getDatatype();
Expr s = dt[0][i].getSelector();
em.mkExpr(kind::APPLY_SELECTOR, s, t);

Retrieved from "http://cvc4.cs.stanford.edu/w/index.php?title=Datatypes&oldid=5722"