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
Algorithmic Mismatch
algorithmic mismatch
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
Boolector
boolector
boolector-available?
boolector?
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!
Common Performance Issues
Comparison Operators
complete-solution
concat
constant
constant?
Conversion Operators
core
CPLEX
cplex
cplex-available?
cplex?
current-bitwidth
current-solver
CVC4
cvc4
cvc4-available?
cvc4?
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 and Real Theories
integer->bitvector
Interacting with Rosette
Irregular Representation
irregular representation
Libraries
lifted
Lifted Racket Forms
minimal unsatisfiable core
Missed Concretization
missed concretization
model
Optimization
optimize
Options and Caveats
output-smt
Pairs and Lists
path condition
pc
Performance
Performance Bottlenecks
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/mip/cplex
rosette/solver/smt/boolector
rosette/solver/smt/cvc4
rosette/solver/smt/yices
rosette/solver/smt/z3
sat
sat?
sign-extend
sketch
solution
solution?
Solutions
solvable
solvable?
solve
solve+
solver
Solver-Aided Forms
Solver-Aided Libraries
Solver-Aided Queries
solver-assert
solver-check
solver-check-with-init
solver-clear
solver-debug
solver-features
solver-maximize
solver-minimize
solver-options
solver-pop
solver-push
solver-shutdown
solver?
Solvers and Solutions
structure type
Structures
Supported Solvers
Symbolic Constants
Symbolic constants
Symbolic Lifting
symbolic profiler
Symbolic Profiling
Symbolic Reasoning
Symbolic Reflection
symbolic reflection
symbolic term
Symbolic Terms
Symbolic Unions
symbolic unions
Symbolic Values
symbolics
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
Walkthrough: Debugging Rosette Performance
with-asserts
with-asserts-only
Yices
yices
yices-available?
yices?
Z3
z3
z3?
zero-extend
~>