To load: | (require (planet ianj/smt-solver:1:3/smt-solve)) |
Old style: | (require (planet "smt-solve.rkt" ("ianj" "smt-solver.plt" 1 3))) |
Min Racket version: | 4.0 |
Package description: | An implementation of the DPLL(T) framework. |
Downloads this week: | 0 |
Total downloads: | 28 |
Tickets: | 0 |
Open tickets: | 0 |
Primary files: | [no interface available] |
Current version |
PLaneT version | External version | Source | DLs | Docs | Req. PLT | Date added |
(1 3) | 0.1 | [browse] | 28 | [docs] | 4.0 | 2010-12-17 |
To load: (require (planet ianj/smt-solver:1:3/smt-solve)) | ||||||
Available in repositories: 4.x | ||||||
0.2 (1 1) - Second release. The core solver now supports clause forgetting and random restarts. The interface had been changed slightly to take a random seed. 0.1 (1 0) - First release |
Old versions |
PLaneT version | External version | Source | DLs | Docs | Req. PLT | Date added |
(1 2) | 0.1 | [browse] | 0 | [docs] | 4.0 | 2010-12-13 |
To load: (require (planet "smt-solve.rkt" ("ianj" "smt-solver.plt" 1 (= 2)))) | ||||||
Available in repositories: 4.x | ||||||
0.1 (1 0) - first release | ||||||
(1 1) | 0.1 | [browse] | 0 | [docs] | 4.0 | 2010-12-13 |
To load: (require (planet "smt-solve.rkt" ("ianj" "smt-solver.plt" 1 (= 1)))) | ||||||
Available in repositories: 4.x | ||||||
0.1 (1 0) - first release | ||||||
(1 0) | 0.1 | [browse] | 0 | [docs] | 4.0 | 2010-12-13 |
To load: (require (planet "smt-solve.rkt" ("ianj" "smt-solver.plt" 1 (= 0)))) | ||||||
Available in repositories: 4.x | ||||||
0.1 (1 0) - first release |