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 OperatorsAdditional OperatorsAlgorithmic Mismatchalgorithmic mismatchAngelic ExecutionAngelic ExecutionAngelic Execution LibraryArithmetic Operatorsassertassertion storeAssertionsAssertionsassertsbindingbitbitvectorbitvector->bitsbitvector->boolbitvector->integerbitvector->naturalbitvector?BitvectorsBitwise Operatorsbool->bitvectorBooleans, Integers, and RealsBoolectorboolectorboolector-available?boolector?BoxesBugs Due to Exceptions in ConditionalsBugs Due to Exceptions in Solver-Aided QueriesBuilt-In Datatypesbvbv?bvaddbvadd1bvandbvashrbveqbvlshrbvmulbvnegbvnotbvorbvrolbvrorbvsdivbvsgebvsgtbvshlbvslebvsltbvsmaxbvsminbvsmodbvsrembvsubbvsub1bvudivbvugebvugtbvulebvultbvumaxbvuminbvurembvxorbvzero?choosechoose*clear-asserts!clear-terms!Common Bugs in Solver-Aided CodeCommon Performance IssuesComparison Operatorscomplete-solutionconcatconstantconstant?Conversion OperatorscoreCPLEXcplexcplex-available?cplex?current-bitwidthcurrent-solverCVC4cvc4cvc4-available?cvc4?debugDebuggingDebuggingDebuggingDebugging Librarydefine-liftdefine-symbolicdefine-symbolic*define-synthaxdefine/debugdestructdestruct*destruct-lambdadistinct?effectively concreteEqualityError Tracererror tracerevaluateExamplesexistsExported Racket Librariesexpressionexpression?extractfor*/allfor/allforallfully concrete valuefunction?fv?gen:solvergenerate-formsGetting Startedguarded valuesholeInstalling RosetteInteger and Real Theoriesinteger->bitvectorInteracting with RosetteIrregular Representationirregular representationLayoutlayoutLibrariesliftedLifted Racket Formslsbminimal unsatisfiable coreMissed Concretizationmissed concretizationmodelmsbOptimizationoptimizeOptions and CaveatsOptions and Caveatsoutput-smtPairs and Listspath conditionpcPerformancePerformance Bottlenecksprint-formsProceduresprogram statequantified formulaQuantifiersReasoning Precisionreasoning precisionReflecting on Symbolic StateReflecting on Symbolic Valuesrenderrender-value/sniprender-value/windowrosetteRosette DialectsRosette Essentialsrosette/lib/angelicrosette/lib/destructrosette/lib/liftrosette/lib/renderrosette/lib/synthaxrosette/lib/value-browserrosette/query/debugrosette/saferosette/solver/mip/cplexrosette/solver/smt/boolectorrosette/solver/smt/cvc4rosette/solver/smt/yicesrosette/solver/smt/z3rotate-leftrotate-rightsatsat?sign-extendsketchsolutionsolution?Solutionssolvablesolvable?solvesolve+solverSolver-Aided FormsSolver-Aided LibrariesSolver-Aided Queriessolver-assertsolver-checksolver-check-with-initsolver-clearsolver-debugsolver-featuressolver-maximizesolver-minimizesolver-optionssolver-popsolver-pushsolver-shutdownsolver?Solvers and Solutionsstructure typeStructuresSupported SolversSymbolic ConstantsSymbolic constantsSymbolic Liftingsymbolic profilerSymbolic ProfilingSymbolic ReasoningSymbolic Reflectionsymbolic reflectionsymbolic termSymbolic TermsSymbolic Unionssymbolic unionsSymbolic ValuessymbolicsSyntactic FormsSynthesisSynthesisSynthesis Librarysynthesizetermterm-cacheterm?The Rosette GuideThe Solver Interfacetype-oftype?Uninterpreted Functionsuninterpreted functionsunion-contentsunion?unknownunknown?Unsafe Operationsunsatunsat?unsolvableUtility Librariesvalue browserValue Browser LibraryValue Destructuring LibraryVectorsVerificationVerificationverifyWalkthrough: Debugging Rosette PerformanceWalkthrough: Tracing Errors in Rosettewith-assertswith-asserts-onlyYicesyicesyices-available?yices?Z3z3z3?zero-extend~>