Index

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z

 

||
!
&&
<=>
=>
??
Additional Logical Operators
Angelic Execution
Angelic Execution
Angelic Execution Library
Arithmetic Operators
assert
assertion store
Assertions
Assertions
asserts
binding
bitvector
bitvector->integer
bitvector->natural
bitvector?
Bitvectors
Bitwise Operators
Booleans, Integers, and Reals
Boxes
Built-In Datatypes
bv
bv?
bvadd
bvand
bvashr
bveq
bvlshr
bvmul
bvneg
bvnot
bvor
bvsdiv
bvsge
bvsgt
bvshl
bvsle
bvslt
bvsmod
bvsrem
bvsub
bvudiv
bvuge
bvugt
bvule
bvult
bvurem
bvxor
choose
choose*
clear-asserts!
clear-terms!
Comparison Operators
concat
constant
constant?
Conversion Operators
core
current-bitwidth
current-solver
debug
Debugging
Debugging
Debugging Library
define-lift
define-symbolic
define-symbolic*
define-synthax
define/debug
distinct?
effectively concrete
Equality
evaluate
exists
Exported Racket Libraries
expression
expression?
extract
for*/all
for/all
forall
fully concrete value
function?
fv?
gen:solver
generate-forms
Getting Started
guarded values
hole
Installing Rosette
integer->bitvector
Interacting with Rosette
Libraries
lifted
Lifted Racket Forms
minimal unsatisfiable core
model
Optimization
optimize
Pairs and Lists
path condition
pc
print-forms
Procedures
program state
quantified formula
Reasoning Precision
reasoning precision
Reflecting on Symbolic State
Reflecting on Symbolic Values
render
rosette
Rosette Dialects
Rosette Essentials
rosette/lib/angelic
rosette/lib/lift
rosette/lib/render
rosette/lib/synthax
rosette/query/debug
rosette/safe
rosette/solver/smt/z3
sat
sat?
sign-extend
sketch
solution
solution?
Solutions
solvable
solvable?
solve
solver
Solver-Aided Forms
Solver-Aided Libraries
Solver-Aided Queries
solver-assert
solver-check
solver-clear
solver-debug
solver-maximize
solver-minimize
solver-pop
solver-push
solver-shutdown
solver?
Solvers and Solutions
structure type
Structures
Symbolic Constants
Symbolic constants
Symbolic Lifting
Symbolic Reasoning
Symbolic Reflection
symbolic reflection
symbolic term
Symbolic Terms
Symbolic Unions
symbolic unions
Symbolic Values
Syntactic Forms
Synthesis
Synthesis
Synthesis Library
synthesize
term
term-cache
term?
The Rosette Guide
The Solver Interface
type-of
type?
Uninterpreted Functions
uninterpreted functions
union-contents
union?
unknown
unknown?
Unsafe Operations
unsat
unsat?
unsolvable
Vectors
Verification
Verification
verify
with-asserts
z3
zero-extend
~>