Comments (1)
Rosette doesn’t lift Racket classes. This means that Rosette doesn’t perform symbolic evaluation of code that uses classes. Lifted and unlisted code can’t be mixed freely. It’s ok to mix them only when the programmer is sure that it won’t lead to unsafe behaviors, like this issue. See here for more details.
from rosette.
Related Issues (20)
- Support cvc5 HOT 2
- Recent change breaks Rosette on the package server HOT 1
- Synthesising with Grammar containing multiple instances of structs with different parameters returns unsat HOT 4
- defining a prop before verify results in different behavior than just verify HOT 2
- symtrace webserver terminates before instrumenting code and providing output HOT 5
- Unintentional value retain
- Minimization causes read-solution: unrecognized solver output: (error line 262 column 10: maximization suspended) HOT 1
- Does not work on M1 Mac because the bundled z3 is not compatible HOT 2
- Symbolic error tracing issue in recursive function for rosette synthesis HOT 8
- Adding Custom Floating Point Support HOT 3
- `raco symtrace` could use idiomatic `--` flag to indicate the end of symtrace flags/beginning of script-under-test flags HOT 2
- Call/cc support? HOT 2
- Bitwuzla converts 1-bit bitvectors to bools (similar to what boolector does) HOT 1
- Unknown sort 'Int' when using `QF_NRA theory
- choose* ing from list of unknown length HOT 2
- EOF error when running multiple programs with `synthesize` queries HOT 5
- Incompatible with z3 (4.8.12-3.1) version shipped in Debian Bookworm HOT 3
- EOF error when using bitwuzla HOT 5
- Confusing synthesizer behavior (choosing integers vs. forms) HOT 6
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from rosette.