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
Additional Operations on Pairs and Lists
Additional Operations on Vectors
Additional Operators
Algorithmic Mismatch
algorithmic mismatch
Angelic Execution
Angelic Execution
Angelic Execution Library
Arithmetic Operators
assert
Assertions and Assumptions
Assertions and Assumptions
assume
binding
bit
bitvector
bitvector->bits
bitvector->bool
bitvector->integer
bitvector->natural
bitvector?
Bitvectors
Bitwise Operators
Bitwuzla
bitwuzla
bitwuzla-available?
bitwuzla?
bool->bitvector
Booleans, Integers, and Reals
Boolector
boolector
boolector-available?
boolector?
Boxes
Bugs Due to Exceptions in Conditionals
Bugs Due to Exceptions in Solver-Aided Queries
Built-In Datatypes
bv
bv?
bvadd
bvadd1
bvand
bvashr
bveq
bvlshr
bvmul
bvneg
bvnot
bvor
bvrol
bvror
bvsdiv
bvsge
bvsgt
bvshl
bvsle
bvslt
bvsmax
bvsmin
bvsmod
bvsrem
bvsub
bvsub1
bvudiv
bvuge
bvugt
bvule
bvult
bvumax
bvumin
bvurem
bvxor
bvzero?
choose
choose*
clear-terms!
clear-vc!
Common Bugs in Solver-Aided Code
Common Performance Issues
Comparison Operators
complete-solution
concat
concrete?
constant
constant?
Conversion Operators
core
current-bitwidth
current-grammar-depth
current-solver
CVC4
cvc4
cvc4-available?
cvc4?
CVC5
cvc5
cvc5-available?
cvc5?
Debugging
define-grammar
define-simple-grammar
define-symbolic
define-symbolic*
destruct
destruct*
destruct-lambda
distinct?
drop-bv
drop-right-bv
effectively concrete
Equality
Error Tracer
error tracer
evaluate
Examples
exists
Exported Racket Libraries
expression
expression?
extract
failed?
finitization
for*/all
for/all
forall
fully concrete value
function?
fv?
gc-terms!
gen:solver
generate-forms
Getting Started
guarded values
holes
Installing Rosette
Integer and Real Theories
integer->bitvector
Interacting with Rosette
Irregular Representation
irregular representation
Layout
layout
length-bv
Libraries
lifted
Lifted Operations on Pairs and Lists
Lifted Operations on Vectors
Lifted Racket Forms
list-ref-bv
list-set-bv
list-tail-bv
lsb
Missed Concretization
missed concretization
Mixing Theories
model
msb
normal?
Optimization
optimize
Options and Caveats
Options and Caveats
output-smt
Pairs and Lists
Performance
Performance Bottlenecks
print-forms
Procedures
program states
quantified formula
Quantifiers
Reasoning Precision
Reasoning Precision
reasoning precision
Reflecting on Symbolic State
Reflecting on Symbolic Values
render-value/snip
render-value/window
result-state
result-value
result?
rosette
Rosette Dialects
Rosette Essentials
rosette/lib/angelic
rosette/lib/destruct
rosette/lib/synthax
rosette/lib/value-browser
rosette/safe
rosette/solver/smt/bitwuzla
rosette/solver/smt/boolector
rosette/solver/smt/cvc4
rosette/solver/smt/cvc5
rosette/solver/smt/stp
rosette/solver/smt/yices
rosette/solver/smt/z3
rotate-left
rotate-right
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-clear
solver-debug
solver-features
solver-maximize
solver-minimize
solver-options
solver-pop
solver-push
solver-shutdown
solver?
Solvers and Solutions
split-at-bv
split-at-right-bv
STP
stp
stp-available?
stp?
structure type
Structures
Supported Solvers
Symbolic Constants
Symbolic constants
Symbolic Evaluation
symbolic evaluation
Symbolic Heap
symbolic heap
Symbolic Lifting
symbolic profiler
Symbolic Profiling
Symbolic Reasoning
Symbolic Reflection
symbolic reflection
symbolic term
Symbolic Terms
Symbolic Unions
symbolic unions
Symbolic Values
symbolic?
symbolics
Syntactic Forms
Synthesis
Synthesis
Synthesis Library
synthesize
take-bv
take-right-bv
term
term?
terms
The Rosette Guide
The Solver Interface
type-of
type?
Uninterpreted Functions
uninterpreted functions
union-contents
union?
unknown
unknown?
Unsafe Operations
unsat
unsat?
unsolvable
Utility Libraries
value browser
Value Browser Library
Value Destructuring Library
vc
vc-asserts
vc-assumes
vc-true
vc-true?
vc?
vector-length-bv
vector-ref-bv
vector-set!-bv
Vectors
Verification
Verification
verification condition
Verification Conditions
verify
Walkthrough: Debugging Rosette Performance
Walkthrough: Tracing Errors in Rosette
with-terms
with-vc
yices
yices-available?
Yices2
yices?
Z3
z3
z3?
zero-extend
~>