Various constraint solvers
1.0K
A tiny image (based on busybox) containing binaries of the following constraint solvers:
They're all in /usr/local/bin. Here's an example using z3:
$ docker run -it --rm wunderseltsam/constraint-solvers /usr/local/bin/z3 -in -smt2
(set-logic QF_NIA)
(set-option :produce-models true)
(declare-fun P () Int) (declare-fun Q () Int)
(declare-fun R () Int) (declare-fun S () Int)
(assert (and (< 0 P) (<= 0 Q) (< 0 R) (<= 0 S)))
(assert (> (+ (* P S) Q) (+ (* R Q) S)))
(check-sat)
(get-value (P Q R S))
Content type
Image
Digest
sha256:f1507e986…
Size
9 MB
Last updated
almost 11 years ago
docker pull wunderseltsam/constraint-solvers