{"size": 1859, "ext": "scrbl", "max_stars_repo_path": "rosette/guide/scribble/datatypes/builtin-datatypes.scrbl", "max_stars_repo_name": "remysucre/rosette", "max_stars_repo_stars_event_min_datetime": "2015-01-06T08:42:46.000Z", "max_stars_repo_stars_event_max_datetime": "2022-03-31T01:49:34.000Z", "max_issues_repo_path": "rosette/guide/scribble/datatypes/builtin-datatypes.scrbl", "max_issues_repo_name": "remysucre/rosette", "max_issues_repo_issues_event_min_datetime": "2015-10-13T17:42:20.000Z", "max_issues_repo_issues_event_max_datetime": "2022-03-30T17:19:53.000Z", "max_forks_repo_path": "rosette/guide/scribble/datatypes/builtin-datatypes.scrbl", "max_forks_repo_name": "remysucre/rosette", "max_forks_repo_forks_event_min_datetime": "2015-02-12T06:58:13.000Z", "max_forks_repo_forks_event_max_datetime": "2022-03-12T21:36:46.000Z"}
{"max_stars_count": 576, "max_issues_count": 188, "max_forks_count": 78, "avg_line_length": 39.5531914894, "max_line_length": 92, "alphanum_fraction": 0.7670790748}
#lang scribble/manual


@(require (for-label racket)
          (for-label rosette/base/form/define rosette/base/core/type))

@title[#:tag "ch:built-in-datatypes" #:style 'toc]{Built-In Datatypes}

The @seclink["ch:syntactic-forms"]{previous chapter} describes the  
Racket syntax forms that are @tech[#:key "lifted constructs"]{lifted} by Rosette to
work on symbolic values. 
This chapter describes the lifted datatypes and their corresponding operations. Most 
lifted operations retain their Racket semantics, with the exception of  
equality predicates (Section @seclink["sec:equality"]{4.1}) and
numeric operations (Section @seclink["sec:bools+ints+reals"]{4.2}).

Rosette distinguishes between two kinds of built-in datatypes:
@deftech[#:key "solvable type"]{solvable} and @deftech[#:key "unsolvable type"]{unsolvable}.
Solvable types are (efficiently) supported by SMT solvers, and they include booleans,
integers, reals, bitvectors, and uninterpreted functions.  All other built-in types are
unsolvable---that is, not as well supported by SMT solvers.   

Every lifted type is equipped with a predicate (e.g., @racket[boolean?]) that
recognizes values of that type.  Solvable types are themselves recognized by
the @racket[solvable?] predicate.  Lifted types include both concrete Racket
values and symbolic Rosette values, but only solvable types include
@tech[#:key "symbolic constant"]{symbolic constants},
as introduced by @seclink["sec:symbolic-constants"]{@code{define-symbolic[*]}}.

@(table-of-contents)
@include-section["equality.scrbl"]
@include-section["bools+ints+reals.scrbl"]
@include-section["bitvectors.scrbl"]
@include-section["uninterpreted.scrbl"]
@include-section["procedures.scrbl"]
@include-section["pairs.scrbl"]
@include-section["vectors.scrbl"]
@include-section["boxes.scrbl"]
@include-section["solvers+solutions.scrbl"]







