Skip to content
OLIV3R: solving floating-point constraints via stochastic local search
Racket Dockerfile
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
data
parsing
test
.gitignore
.gitmodules
Dockerfile
LICENSE
QUESTIONS.md
README.md
TODOs.md
elim-eqs.rkt
fp2real.rkt
main.rkt
score.rkt
sls.rkt

README.md

Overview

This project is intended as a reimplementation of "Stochastic Local Search for Satisfiability Modulo Theories" in Racket. But now it serves as an incomplete QF_(BV)FP solver.

Dependency

Just Racket (what else should you need?)

Maybe Z3, too. Z3 needs to be installed if the options --try-real-models and --elim-eqs are enabled.

How To

See racket main.rkt -h

You can’t perform that action at this time.