Public Repository

Last pushed: 2 years ago
Short Description
Various constraint solvers
Full Description

A tiny image (based on busybox) containing binaries of the following constraint solvers:

  • minisat
  • z3

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))
Docker Pull Command
Owner
wunderseltsam

Comments (0)