diff --git a/go.sum b/go.sum index 36b3765776..e472ee3b3b 100644 --- a/go.sum +++ b/go.sum @@ -336,6 +336,8 @@ github.com/ghodss/yaml v1.0.0/go.mod h1:4dBDuWmgqj2HViK6kFavaiC9ZROes6MMH2rRYeME github.com/gliderlabs/ssh v0.2.2/go.mod h1:U7qILu1NlMHj9FlMhZLlkCdDnU1DBEAqr0aevW3Awn0= github.com/globalsign/mgo v0.0.0-20180905125535-1ca0a4f7cbcb/go.mod h1:xkRDCp4j0OGD1HRkm4kmhM+pmpv3AKq5SU7GMg4oO/Q= github.com/globalsign/mgo v0.0.0-20181015135952-eeefdecb41b8/go.mod h1:xkRDCp4j0OGD1HRkm4kmhM+pmpv3AKq5SU7GMg4oO/Q= +github.com/go-air/gini v1.0.4 h1:lteMAxHKNOAjIqazL/klOJJmxq6YxxSuJ17MnMXny+s= +github.com/go-air/gini v1.0.4/go.mod h1:dd8RvT1xcv6N1da33okvBd8DhMh1/A4siGy6ErjTljs= github.com/go-bindata/go-bindata/v3 v3.1.3 h1:F0nVttLC3ws0ojc7p60veTurcOm//D4QBODNM7EGrCI= github.com/go-bindata/go-bindata/v3 v3.1.3/go.mod h1:1/zrpXsLD8YDIbhZRqXzm1Ghc7NhEvIN9+Z6R5/xH4I= github.com/go-errors/errors v1.0.1 h1:LUHzmkK3GUKUrL/1gfBUxAHzcev3apQlezX/+O7ma6w= @@ -855,8 +857,6 @@ github.com/openzipkin-contrib/zipkin-go-opentracing v0.4.5/go.mod h1:/wsWhb9smxS github.com/openzipkin/zipkin-go v0.1.6/go.mod h1:QgAqvLzwWbR/WpD4A3cGpPtJrZXNIiJc5AZX7/PBEpw= github.com/openzipkin/zipkin-go v0.2.1/go.mod h1:NaW6tEwdmWMaCDZzg8sh+IBNOxHMPnhQw8ySjnjRyN4= github.com/openzipkin/zipkin-go v0.2.2/go.mod h1:NaW6tEwdmWMaCDZzg8sh+IBNOxHMPnhQw8ySjnjRyN4= -github.com/operator-framework/gini v1.1.0 h1:w84bE/pi0nlnIRAxzYguoYAnL9s5T6RSVZKYWcxO3yI= -github.com/operator-framework/gini v1.1.0/go.mod h1:L4GlF3xPPfQUoWglKhaBcR8/LZn3fWtMB1mwUyOGv98= github.com/otiai10/copy v1.2.0 h1:HvG945u96iNadPoG2/Ja2+AUJeW5YuFQMixq9yirC+k= github.com/otiai10/copy v1.2.0/go.mod h1:rrF5dJ5F0t/EWSYODDu4j9/vEeYHMkc8jt0zJChqQWw= github.com/otiai10/curr v0.0.0-20150429015615-9b4961190c95/go.mod h1:9qAhocn7zKJG+0mI8eUu6xqkFDYS2kb2saOteoSB3cE= diff --git a/staging/operator-lifecycle-manager/go.mod b/staging/operator-lifecycle-manager/go.mod index 326b311852..c96c72b6f9 100644 --- a/staging/operator-lifecycle-manager/go.mod +++ b/staging/operator-lifecycle-manager/go.mod @@ -10,6 +10,7 @@ require ( github.com/distribution/distribution v2.7.1+incompatible github.com/fsnotify/fsnotify v1.4.9 github.com/ghodss/yaml v1.0.0 + github.com/go-air/gini v1.0.4 github.com/go-bindata/go-bindata/v3 v3.1.3 github.com/go-logr/logr v0.4.0 github.com/golang/mock v1.4.1 @@ -25,7 +26,6 @@ require ( github.com/openshift/api v0.0.0-20200331152225-585af27e34fd github.com/openshift/client-go v0.0.0-20200326155132-2a6cd50aedd0 github.com/operator-framework/api v0.10.3 - github.com/operator-framework/gini v1.1.0 github.com/operator-framework/operator-registry v1.17.5 github.com/otiai10/copy v1.2.0 github.com/pkg/errors v0.9.1 diff --git a/staging/operator-lifecycle-manager/go.sum b/staging/operator-lifecycle-manager/go.sum index d862aed784..ef1e00aa99 100644 --- a/staging/operator-lifecycle-manager/go.sum +++ b/staging/operator-lifecycle-manager/go.sum @@ -350,6 +350,8 @@ github.com/ghodss/yaml v1.0.0/go.mod h1:4dBDuWmgqj2HViK6kFavaiC9ZROes6MMH2rRYeME github.com/gliderlabs/ssh v0.2.2/go.mod h1:U7qILu1NlMHj9FlMhZLlkCdDnU1DBEAqr0aevW3Awn0= github.com/globalsign/mgo v0.0.0-20180905125535-1ca0a4f7cbcb/go.mod h1:xkRDCp4j0OGD1HRkm4kmhM+pmpv3AKq5SU7GMg4oO/Q= github.com/globalsign/mgo v0.0.0-20181015135952-eeefdecb41b8/go.mod h1:xkRDCp4j0OGD1HRkm4kmhM+pmpv3AKq5SU7GMg4oO/Q= +github.com/go-air/gini v1.0.4 h1:lteMAxHKNOAjIqazL/klOJJmxq6YxxSuJ17MnMXny+s= +github.com/go-air/gini v1.0.4/go.mod h1:dd8RvT1xcv6N1da33okvBd8DhMh1/A4siGy6ErjTljs= github.com/go-bindata/go-bindata/v3 v3.1.3 h1:F0nVttLC3ws0ojc7p60veTurcOm//D4QBODNM7EGrCI= github.com/go-bindata/go-bindata/v3 v3.1.3/go.mod h1:1/zrpXsLD8YDIbhZRqXzm1Ghc7NhEvIN9+Z6R5/xH4I= github.com/go-errors/errors v1.0.1 h1:LUHzmkK3GUKUrL/1gfBUxAHzcev3apQlezX/+O7ma6w= @@ -878,8 +880,6 @@ github.com/openzipkin/zipkin-go v0.2.2/go.mod h1:NaW6tEwdmWMaCDZzg8sh+IBNOxHMPnh github.com/operator-framework/api v0.7.1/go.mod h1:L7IvLd/ckxJEJg/t4oTTlnHKAJIP/p51AvEslW3wYdY= github.com/operator-framework/api v0.10.3 h1:C4DE7Rr3+ztUw3mKiFyfAiUJSVOty/cJmpwE90/kYro= github.com/operator-framework/api v0.10.3/go.mod h1:tV0BUNvly7szq28ZPBXhjp1Sqg5yHCOeX19ui9K4vjI= -github.com/operator-framework/gini v1.1.0 h1:w84bE/pi0nlnIRAxzYguoYAnL9s5T6RSVZKYWcxO3yI= -github.com/operator-framework/gini v1.1.0/go.mod h1:L4GlF3xPPfQUoWglKhaBcR8/LZn3fWtMB1mwUyOGv98= github.com/operator-framework/operator-registry v1.17.5 h1:LR8m1rFz5Gcyje8WK6iYt+gIhtzqo52zMRALdmTYHT0= github.com/operator-framework/operator-registry v1.17.5/go.mod h1:sRQIgDMZZdUcmHltzyCnM6RUoDF+WS8Arj1BQIARDS8= github.com/otiai10/copy v1.2.0 h1:HvG945u96iNadPoG2/Ja2+AUJeW5YuFQMixq9yirC+k= diff --git a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/bench_test.go b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/bench_test.go index af07d55ce1..72f586e1e0 100644 --- a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/bench_test.go +++ b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/bench_test.go @@ -72,3 +72,12 @@ func BenchmarkSolve(b *testing.B) { s.Solve(context.Background()) } } + +func BenchmarkNewInput(b *testing.B) { + for i := 0; i < b.N; i++ { + _, err := New(WithInput(BenchmarkInput)) + if err != nil { + b.Fatalf("failed to initialize solver: %s", err) + } + } +} diff --git a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/constraints.go b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/constraints.go index ca3c4f5331..785ee409fd 100644 --- a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/constraints.go +++ b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/constraints.go @@ -4,8 +4,8 @@ import ( "fmt" "strings" - "github.com/operator-framework/gini/logic" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/logic" + "github.com/go-air/gini/z" ) // Constraint implementations limit the circumstances under which a diff --git a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/lit_mapping.go b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/lit_mapping.go index f837ffc3e8..dedb5fb8da 100644 --- a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/lit_mapping.go +++ b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/lit_mapping.go @@ -4,9 +4,9 @@ import ( "fmt" "strings" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/logic" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/logic" + "github.com/go-air/gini/z" ) type DuplicateIdentifier Identifier diff --git a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search.go b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search.go index f36678f1ee..ed84ea9309 100644 --- a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search.go +++ b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search.go @@ -3,8 +3,8 @@ package solver import ( "context" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" ) type choice struct { diff --git a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search_test.go b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search_test.go index 53dff9c748..5b00bcfd2c 100644 --- a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search_test.go +++ b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search_test.go @@ -1,4 +1,4 @@ -//go:generate go run github.com/maxbrunsfeld/counterfeiter/v6 -o zz_search_test.go ../../../../../vendor/github.com/operator-framework/gini/inter S +//go:generate go run github.com/maxbrunsfeld/counterfeiter/v6 -o zz_search_test.go ../../../../../vendor/github.com/go-air/gini/inter S package solver @@ -6,8 +6,8 @@ import ( "context" "testing" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" "github.com/stretchr/testify/assert" ) diff --git a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/solve.go b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/solve.go index 712ae3bcc7..5d81f459a2 100644 --- a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/solve.go +++ b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/solve.go @@ -6,9 +6,9 @@ import ( "fmt" "strings" - "github.com/operator-framework/gini" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" ) var Incomplete = errors.New("cancelled before a solution could be found") diff --git a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/zz_search_test.go b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/zz_search_test.go index 5ef7eed2c6..6fbdbccc46 100644 --- a/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/zz_search_test.go +++ b/staging/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/zz_search_test.go @@ -5,8 +5,8 @@ import ( "sync" "time" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" ) type FakeS struct { diff --git a/vendor/github.com/operator-framework/gini/.travis.yml b/vendor/github.com/go-air/gini/.travis.yml similarity index 100% rename from vendor/github.com/operator-framework/gini/.travis.yml rename to vendor/github.com/go-air/gini/.travis.yml diff --git a/vendor/github.com/operator-framework/gini/LICENSE b/vendor/github.com/go-air/gini/LICENSE similarity index 100% rename from vendor/github.com/operator-framework/gini/LICENSE rename to vendor/github.com/go-air/gini/LICENSE diff --git a/vendor/github.com/go-air/gini/README.md b/vendor/github.com/go-air/gini/README.md new file mode 100644 index 0000000000..558b5c84bc --- /dev/null +++ b/vendor/github.com/go-air/gini/README.md @@ -0,0 +1,51 @@ +# ⊧ Gini: A fast SAT solver. + +The Gini sat solver is a fast, clean SAT solver written in Go. It is to our knowledge +the first ever performant pure-Go SAT solver made available. + + +[![GoDoc](https://godoc.org/github.com/go-air/gini?status.svg)](https://godoc.org/github.com/go-air/gini) + +[Google Group](https://groups.google.com/d/forum/ginisat) + +This solver is fully open source, originally developped at IRI France. + +## Build/Install + +For the impatient: + + go install github.com/go-air/gini/...@latest + +I recommend however building the package github.com/go-air/gini/internal/xo with bounds checking +turned off. This package is all about anything-goes performance and is the workhorse behind most of +the gini sat solver. It is also extensively tested and well benchmarked, so it should not pose any +safety threat to client code. This makes a signficant speed difference (maybe 10%) on long running +problems. + +## The SAT problem in 5 minutes + +[The SAT Problem](docs/satprob.md) + +## Usage + +Our [user guide](docs/manual.md) shows how to solve SAT problems, circuits, do Boolean optimisation, +use concurrency, using our distributed CRISP protocol, and more. + + +## Citing Gini + +Zenodo DOI based citations and download: +[![DOI](https://zenodo.org/badge/64034957.svg)](https://zenodo.org/badge/latestdoi/64034957) + +BibText: +``` +@misc{scott_cotton_2019_2553490, + author = {Scott Cotton}, + title = {go-air/gini: Sapeur}, + month = jan, + year = 2019, + doi = {10.5281/zenodo.2553490}, + url = {https://doi.org/10.5281/zenodo.2553490} +} +``` + diff --git a/vendor/github.com/operator-framework/gini/dimacs/cfilt.go b/vendor/github.com/go-air/gini/dimacs/cfilt.go similarity index 100% rename from vendor/github.com/operator-framework/gini/dimacs/cfilt.go rename to vendor/github.com/go-air/gini/dimacs/cfilt.go diff --git a/vendor/github.com/operator-framework/gini/dimacs/cnf.go b/vendor/github.com/go-air/gini/dimacs/cnf.go similarity index 98% rename from vendor/github.com/operator-framework/gini/dimacs/cnf.go rename to vendor/github.com/go-air/gini/dimacs/cnf.go index c00451f51d..c426f7d3bf 100644 --- a/vendor/github.com/operator-framework/gini/dimacs/cnf.go +++ b/vendor/github.com/go-air/gini/dimacs/cnf.go @@ -8,7 +8,7 @@ import ( "fmt" "io" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) // Type Reader holds info for reading dimacs formatted intput. diff --git a/vendor/github.com/operator-framework/gini/dimacs/doc.go b/vendor/github.com/go-air/gini/dimacs/doc.go similarity index 100% rename from vendor/github.com/operator-framework/gini/dimacs/doc.go rename to vendor/github.com/go-air/gini/dimacs/doc.go diff --git a/vendor/github.com/operator-framework/gini/dimacs/icnf.go b/vendor/github.com/go-air/gini/dimacs/icnf.go similarity index 97% rename from vendor/github.com/operator-framework/gini/dimacs/icnf.go rename to vendor/github.com/go-air/gini/dimacs/icnf.go index 567762a1e9..5f058d2252 100644 --- a/vendor/github.com/operator-framework/gini/dimacs/icnf.go +++ b/vendor/github.com/go-air/gini/dimacs/icnf.go @@ -8,7 +8,7 @@ import ( "fmt" "io" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) type iCnfReader struct { diff --git a/vendor/github.com/operator-framework/gini/dimacs/int.go b/vendor/github.com/go-air/gini/dimacs/int.go similarity index 100% rename from vendor/github.com/operator-framework/gini/dimacs/int.go rename to vendor/github.com/go-air/gini/dimacs/int.go diff --git a/vendor/github.com/operator-framework/gini/dimacs/lit.go b/vendor/github.com/go-air/gini/dimacs/lit.go similarity index 89% rename from vendor/github.com/operator-framework/gini/dimacs/lit.go rename to vendor/github.com/go-air/gini/dimacs/lit.go index 9ed081687f..fdfd52441a 100644 --- a/vendor/github.com/operator-framework/gini/dimacs/lit.go +++ b/vendor/github.com/go-air/gini/dimacs/lit.go @@ -6,7 +6,7 @@ package dimacs import ( "bufio" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) func readLit(r *bufio.Reader) (m z.Lit, e error) { diff --git a/vendor/github.com/operator-framework/gini/dimacs/solve.go b/vendor/github.com/go-air/gini/dimacs/solve.go similarity index 100% rename from vendor/github.com/operator-framework/gini/dimacs/solve.go rename to vendor/github.com/go-air/gini/dimacs/solve.go diff --git a/vendor/github.com/operator-framework/gini/dimacs/vis.go b/vendor/github.com/go-air/gini/dimacs/vis.go similarity index 96% rename from vendor/github.com/operator-framework/gini/dimacs/vis.go rename to vendor/github.com/go-air/gini/dimacs/vis.go index 9934b37032..7fc57be38b 100644 --- a/vendor/github.com/operator-framework/gini/dimacs/vis.go +++ b/vendor/github.com/go-air/gini/dimacs/vis.go @@ -3,7 +3,7 @@ package dimacs -import "github.com/operator-framework/gini/z" +import "github.com/go-air/gini/z" // Type Vis provides a visitor interface to reading dimacs files. // diff --git a/vendor/github.com/operator-framework/gini/doc.go b/vendor/github.com/go-air/gini/doc.go similarity index 100% rename from vendor/github.com/operator-framework/gini/doc.go rename to vendor/github.com/go-air/gini/doc.go diff --git a/vendor/github.com/operator-framework/gini/gini.go b/vendor/github.com/go-air/gini/gini.go similarity index 97% rename from vendor/github.com/operator-framework/gini/gini.go rename to vendor/github.com/go-air/gini/gini.go index 52a6d4d054..5f32dc8e8b 100644 --- a/vendor/github.com/operator-framework/gini/gini.go +++ b/vendor/github.com/go-air/gini/gini.go @@ -7,10 +7,10 @@ import ( "io" "time" - "github.com/operator-framework/gini/dimacs" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/internal/xo" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/dimacs" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/internal/xo" + "github.com/go-air/gini/z" ) // Gini is a concrete implementation of solver diff --git a/vendor/github.com/go-air/gini/go.mod b/vendor/github.com/go-air/gini/go.mod new file mode 100644 index 0000000000..e5a95f859f --- /dev/null +++ b/vendor/github.com/go-air/gini/go.mod @@ -0,0 +1,3 @@ +module github.com/go-air/gini + +go 1.16 diff --git a/vendor/github.com/operator-framework/gini/go.sum b/vendor/github.com/go-air/gini/go.sum similarity index 100% rename from vendor/github.com/operator-framework/gini/go.sum rename to vendor/github.com/go-air/gini/go.sum diff --git a/vendor/github.com/operator-framework/gini/inter/doc.go b/vendor/github.com/go-air/gini/inter/doc.go similarity index 100% rename from vendor/github.com/operator-framework/gini/inter/doc.go rename to vendor/github.com/go-air/gini/inter/doc.go diff --git a/vendor/github.com/operator-framework/gini/inter/s.go b/vendor/github.com/go-air/gini/inter/s.go similarity index 99% rename from vendor/github.com/operator-framework/gini/inter/s.go rename to vendor/github.com/go-air/gini/inter/s.go index 835a93375c..248068d11f 100644 --- a/vendor/github.com/operator-framework/gini/inter/s.go +++ b/vendor/github.com/go-air/gini/inter/s.go @@ -6,7 +6,7 @@ package inter import ( "time" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) // Interface Solveable encapsulates a decision diff --git a/vendor/github.com/operator-framework/gini/inter/solve.go b/vendor/github.com/go-air/gini/inter/solve.go similarity index 100% rename from vendor/github.com/operator-framework/gini/inter/solve.go rename to vendor/github.com/go-air/gini/inter/solve.go diff --git a/vendor/github.com/operator-framework/gini/internal/xo/active.go b/vendor/github.com/go-air/gini/internal/xo/active.go similarity index 98% rename from vendor/github.com/operator-framework/gini/internal/xo/active.go rename to vendor/github.com/go-air/gini/internal/xo/active.go index 786f76204f..b0c906db6b 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/active.go +++ b/vendor/github.com/go-air/gini/internal/xo/active.go @@ -1,7 +1,7 @@ package xo import ( - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) type Active struct { diff --git a/vendor/github.com/operator-framework/gini/internal/xo/cdat.go b/vendor/github.com/go-air/gini/internal/xo/cdat.go similarity index 99% rename from vendor/github.com/operator-framework/gini/internal/xo/cdat.go rename to vendor/github.com/go-air/gini/internal/xo/cdat.go index 41b8367f0c..b97be0075b 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/cdat.go +++ b/vendor/github.com/go-air/gini/internal/xo/cdat.go @@ -9,7 +9,7 @@ import ( "io" "math" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) // Type CDat: basic operations for storing all the literals (and Chds) in a CNF diff --git a/vendor/github.com/operator-framework/gini/internal/xo/cdb.go b/vendor/github.com/go-air/gini/internal/xo/cdb.go similarity index 99% rename from vendor/github.com/operator-framework/gini/internal/xo/cdb.go rename to vendor/github.com/go-air/gini/internal/xo/cdb.go index d4615220b9..98c062c75f 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/cdb.go +++ b/vendor/github.com/go-air/gini/internal/xo/cdb.go @@ -8,7 +8,7 @@ import ( "fmt" "io" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) // Type Cdb is the main interface to clauses. diff --git a/vendor/github.com/operator-framework/gini/internal/xo/cgc.go b/vendor/github.com/go-air/gini/internal/xo/cgc.go similarity index 99% rename from vendor/github.com/operator-framework/gini/internal/xo/cgc.go rename to vendor/github.com/go-air/gini/internal/xo/cgc.go index 94cc04e747..01c7d6451b 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/cgc.go +++ b/vendor/github.com/go-air/gini/internal/xo/cgc.go @@ -6,7 +6,7 @@ package xo import ( "sort" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) // Type Cgc encapsulates clause compaction/garbage collection. diff --git a/vendor/github.com/operator-framework/gini/internal/xo/chd.go b/vendor/github.com/go-air/gini/internal/xo/chd.go similarity index 100% rename from vendor/github.com/operator-framework/gini/internal/xo/chd.go rename to vendor/github.com/go-air/gini/internal/xo/chd.go diff --git a/vendor/github.com/operator-framework/gini/internal/xo/cloc.go b/vendor/github.com/go-air/gini/internal/xo/cloc.go similarity index 82% rename from vendor/github.com/operator-framework/gini/internal/xo/cloc.go rename to vendor/github.com/go-air/gini/internal/xo/cloc.go index 158d40c3e1..46fabfdd8b 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/cloc.go +++ b/vendor/github.com/go-air/gini/internal/xo/cloc.go @@ -3,7 +3,7 @@ package xo -import "github.com/operator-framework/gini/z" +import "github.com/go-air/gini/z" const ( CNull z.C = 0 diff --git a/vendor/github.com/operator-framework/gini/internal/xo/ctl.go b/vendor/github.com/go-air/gini/internal/xo/ctl.go similarity index 99% rename from vendor/github.com/operator-framework/gini/internal/xo/ctl.go rename to vendor/github.com/go-air/gini/internal/xo/ctl.go index 5a2d25ee21..dc267a2dd5 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/ctl.go +++ b/vendor/github.com/go-air/gini/internal/xo/ctl.go @@ -7,7 +7,7 @@ import ( "sync" "time" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) // Type Ctl encapsulates low level asynchronous control diff --git a/vendor/github.com/operator-framework/gini/internal/xo/derive.go b/vendor/github.com/go-air/gini/internal/xo/derive.go similarity index 99% rename from vendor/github.com/operator-framework/gini/internal/xo/derive.go rename to vendor/github.com/go-air/gini/internal/xo/derive.go index 988acf99fc..a2e2b6267c 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/derive.go +++ b/vendor/github.com/go-air/gini/internal/xo/derive.go @@ -6,7 +6,7 @@ package xo import ( "fmt" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) type Deriver struct { diff --git a/vendor/github.com/operator-framework/gini/internal/xo/dimacs.go b/vendor/github.com/go-air/gini/internal/xo/dimacs.go similarity index 91% rename from vendor/github.com/operator-framework/gini/internal/xo/dimacs.go rename to vendor/github.com/go-air/gini/internal/xo/dimacs.go index 9478b14a8b..0ac4113dce 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/dimacs.go +++ b/vendor/github.com/go-air/gini/internal/xo/dimacs.go @@ -3,7 +3,7 @@ package xo -import "github.com/operator-framework/gini/z" +import "github.com/go-air/gini/z" // Type DimacsVis implements dimacs.Vis for constructing // solvers from dimacs cnf files. diff --git a/vendor/github.com/operator-framework/gini/internal/xo/doc.go b/vendor/github.com/go-air/gini/internal/xo/doc.go similarity index 100% rename from vendor/github.com/operator-framework/gini/internal/xo/doc.go rename to vendor/github.com/go-air/gini/internal/xo/doc.go diff --git a/vendor/github.com/operator-framework/gini/internal/xo/guess.go b/vendor/github.com/go-air/gini/internal/xo/guess.go similarity index 99% rename from vendor/github.com/operator-framework/gini/internal/xo/guess.go rename to vendor/github.com/go-air/gini/internal/xo/guess.go index f5d8414df8..7816467955 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/guess.go +++ b/vendor/github.com/go-air/gini/internal/xo/guess.go @@ -6,7 +6,7 @@ package xo import ( "math" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) const ( diff --git a/vendor/github.com/operator-framework/gini/internal/xo/luby.go b/vendor/github.com/go-air/gini/internal/xo/luby.go similarity index 100% rename from vendor/github.com/operator-framework/gini/internal/xo/luby.go rename to vendor/github.com/go-air/gini/internal/xo/luby.go diff --git a/vendor/github.com/operator-framework/gini/internal/xo/phases.go b/vendor/github.com/go-air/gini/internal/xo/phases.go similarity index 93% rename from vendor/github.com/operator-framework/gini/internal/xo/phases.go rename to vendor/github.com/go-air/gini/internal/xo/phases.go index 1f3bda755a..a04be18aab 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/phases.go +++ b/vendor/github.com/go-air/gini/internal/xo/phases.go @@ -1,6 +1,6 @@ package xo -import "github.com/operator-framework/gini/z" +import "github.com/go-air/gini/z" type phases z.Var diff --git a/vendor/github.com/operator-framework/gini/internal/xo/s.go b/vendor/github.com/go-air/gini/internal/xo/s.go similarity index 99% rename from vendor/github.com/operator-framework/gini/internal/xo/s.go rename to vendor/github.com/go-air/gini/internal/xo/s.go index 7d10639622..9f7d865693 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/s.go +++ b/vendor/github.com/go-air/gini/internal/xo/s.go @@ -11,9 +11,9 @@ import ( "sync" "time" - "github.com/operator-framework/gini/dimacs" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/dimacs" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" ) const ( diff --git a/vendor/github.com/operator-framework/gini/internal/xo/stats.go b/vendor/github.com/go-air/gini/internal/xo/stats.go similarity index 100% rename from vendor/github.com/operator-framework/gini/internal/xo/stats.go rename to vendor/github.com/go-air/gini/internal/xo/stats.go diff --git a/vendor/github.com/operator-framework/gini/internal/xo/tracer.go b/vendor/github.com/go-air/gini/internal/xo/tracer.go similarity index 100% rename from vendor/github.com/operator-framework/gini/internal/xo/tracer.go rename to vendor/github.com/go-air/gini/internal/xo/tracer.go diff --git a/vendor/github.com/operator-framework/gini/internal/xo/trail.go b/vendor/github.com/go-air/gini/internal/xo/trail.go similarity index 99% rename from vendor/github.com/operator-framework/gini/internal/xo/trail.go rename to vendor/github.com/go-air/gini/internal/xo/trail.go index 9f67388c8a..b7aa04d646 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/trail.go +++ b/vendor/github.com/go-air/gini/internal/xo/trail.go @@ -7,7 +7,7 @@ import ( "bytes" "fmt" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) type late struct { diff --git a/vendor/github.com/operator-framework/gini/internal/xo/vars.go b/vendor/github.com/go-air/gini/internal/xo/vars.go similarity index 98% rename from vendor/github.com/operator-framework/gini/internal/xo/vars.go rename to vendor/github.com/go-air/gini/internal/xo/vars.go index 02a25fd985..431dccf2ec 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/vars.go +++ b/vendor/github.com/go-air/gini/internal/xo/vars.go @@ -7,7 +7,7 @@ import ( "fmt" "strings" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) type Vars struct { diff --git a/vendor/github.com/operator-framework/gini/internal/xo/watch.go b/vendor/github.com/go-air/gini/internal/xo/watch.go similarity index 97% rename from vendor/github.com/operator-framework/gini/internal/xo/watch.go rename to vendor/github.com/go-air/gini/internal/xo/watch.go index 4e30635742..fdd753f79f 100644 --- a/vendor/github.com/operator-framework/gini/internal/xo/watch.go +++ b/vendor/github.com/go-air/gini/internal/xo/watch.go @@ -6,7 +6,7 @@ package xo import ( "fmt" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) // Watch holds other blocking literal, clause location ( diff --git a/vendor/github.com/operator-framework/gini/logic/c.go b/vendor/github.com/go-air/gini/logic/c.go similarity index 98% rename from vendor/github.com/operator-framework/gini/logic/c.go rename to vendor/github.com/go-air/gini/logic/c.go index 081d32cc62..c42c9e582c 100644 --- a/vendor/github.com/operator-framework/gini/logic/c.go +++ b/vendor/github.com/go-air/gini/logic/c.go @@ -4,8 +4,8 @@ package logic import ( - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" ) // C represents a formula or combinational circuit. @@ -376,5 +376,5 @@ func (p *C) grow() { } func strashCode(a, b z.Lit) uint32 { - return uint32((a << 13) * b) + return uint32(^(a << 13) * b) } diff --git a/vendor/github.com/operator-framework/gini/logic/card.go b/vendor/github.com/go-air/gini/logic/card.go similarity index 98% rename from vendor/github.com/operator-framework/gini/logic/card.go rename to vendor/github.com/go-air/gini/logic/card.go index af63f2ff22..2f8a074ce4 100644 --- a/vendor/github.com/operator-framework/gini/logic/card.go +++ b/vendor/github.com/go-air/gini/logic/card.go @@ -4,7 +4,7 @@ package logic import ( - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/z" ) // Card provides an interface for different implementations diff --git a/vendor/github.com/operator-framework/gini/logic/doc.go b/vendor/github.com/go-air/gini/logic/doc.go similarity index 100% rename from vendor/github.com/operator-framework/gini/logic/doc.go rename to vendor/github.com/go-air/gini/logic/doc.go diff --git a/vendor/github.com/operator-framework/gini/logic/roll.go b/vendor/github.com/go-air/gini/logic/roll.go similarity index 97% rename from vendor/github.com/operator-framework/gini/logic/roll.go rename to vendor/github.com/go-air/gini/logic/roll.go index abd501997f..3ec3c8af64 100644 --- a/vendor/github.com/operator-framework/gini/logic/roll.go +++ b/vendor/github.com/go-air/gini/logic/roll.go @@ -3,7 +3,7 @@ package logic -import "github.com/operator-framework/gini/z" +import "github.com/go-air/gini/z" // Roll creates an unroller of sequential logic into // combinational logic. diff --git a/vendor/github.com/operator-framework/gini/logic/s.go b/vendor/github.com/go-air/gini/logic/s.go similarity index 98% rename from vendor/github.com/operator-framework/gini/logic/s.go rename to vendor/github.com/go-air/gini/logic/s.go index badcae2843..2669aba57f 100644 --- a/vendor/github.com/operator-framework/gini/logic/s.go +++ b/vendor/github.com/go-air/gini/logic/s.go @@ -3,7 +3,7 @@ package logic -import "github.com/operator-framework/gini/z" +import "github.com/go-air/gini/z" // S adds sequential elements to C, gini's combinational // logic representation. diff --git a/vendor/github.com/operator-framework/gini/s.go b/vendor/github.com/go-air/gini/s.go similarity index 84% rename from vendor/github.com/operator-framework/gini/s.go rename to vendor/github.com/go-air/gini/s.go index caa6281b6a..bdea6ae82e 100644 --- a/vendor/github.com/operator-framework/gini/s.go +++ b/vendor/github.com/go-air/gini/s.go @@ -3,7 +3,7 @@ package gini -import "github.com/operator-framework/gini/inter" +import "github.com/go-air/gini/inter" // NewS creates a new solver, which is the Gini // implementation of inter.S. diff --git a/vendor/github.com/operator-framework/gini/sv.go b/vendor/github.com/go-air/gini/sv.go similarity index 95% rename from vendor/github.com/operator-framework/gini/sv.go rename to vendor/github.com/go-air/gini/sv.go index 546b93c0c2..f6a525fa39 100644 --- a/vendor/github.com/operator-framework/gini/sv.go +++ b/vendor/github.com/go-air/gini/sv.go @@ -6,8 +6,8 @@ package gini import ( "time" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" ) type svWrap struct { diff --git a/vendor/github.com/operator-framework/gini/z/c.go b/vendor/github.com/go-air/gini/z/c.go similarity index 100% rename from vendor/github.com/operator-framework/gini/z/c.go rename to vendor/github.com/go-air/gini/z/c.go diff --git a/vendor/github.com/operator-framework/gini/z/doc.go b/vendor/github.com/go-air/gini/z/doc.go similarity index 100% rename from vendor/github.com/operator-framework/gini/z/doc.go rename to vendor/github.com/go-air/gini/z/doc.go diff --git a/vendor/github.com/operator-framework/gini/z/dv.go b/vendor/github.com/go-air/gini/z/dv.go similarity index 100% rename from vendor/github.com/operator-framework/gini/z/dv.go rename to vendor/github.com/go-air/gini/z/dv.go diff --git a/vendor/github.com/operator-framework/gini/z/lit.go b/vendor/github.com/go-air/gini/z/lit.go similarity index 100% rename from vendor/github.com/operator-framework/gini/z/lit.go rename to vendor/github.com/go-air/gini/z/lit.go diff --git a/vendor/github.com/operator-framework/gini/z/var.go b/vendor/github.com/go-air/gini/z/var.go similarity index 100% rename from vendor/github.com/operator-framework/gini/z/var.go rename to vendor/github.com/go-air/gini/z/var.go diff --git a/vendor/github.com/operator-framework/gini/README.md b/vendor/github.com/operator-framework/gini/README.md deleted file mode 100644 index 42d6ff2fb1..0000000000 --- a/vendor/github.com/operator-framework/gini/README.md +++ /dev/null @@ -1,339 +0,0 @@ -# Gini SAT Solver - -The Gini sat solver is a fast, clean SAT solver written in Go. It is to our knowledge -the first ever performant pure-Go SAT solver made available. - -| [![Build Status](https://travis-ci.org/irifrance/gini.svg?branch=master)](https://travis-ci.org/irifrance/gini) | [![GoDoc](https://godoc.org/github.com/irifrance/gini?status.svg)](https://godoc.org/github.com/irifrance/gini) | [Google Group](https://groups.google.com/d/forum/ginisat) | -------------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------------------------------------------------------------|-----------------------------------------------------------| - -This solver is fully open source, originally developped at IRI France. - - -## Build/Install - -For the impatient: - - go get github.com/irifrance/gini... - -I recommend however building the package github.com/irifrance/gini/internal/xo with bounds checking -turned off. This package is all about anything-goes performance and is the workhorse behind most of -the gini sat solver. It is also extensively tested and well benchmarked, so it should not pose any -safety threat to client code. This makes a signficant speed difference (maybe 10%) on long running -problems. - - -## The SAT Problem - -The SAT problem is perhaps the most famous NP-complete problem. As such, SAT -solvers can be used to try to solve hard problems, such as travelling salesman -or RSA cracking. In practice, many SAT problems are quite easy (but not -decryption problems...yet). The solvers are used in software verification, -hardware verification and testing, AI planning, routing, etc. - -The SAT problem is a Boolean problem. All variables can either be true or -false, but nothing else. The SAT problem solves systems of Boolean -constraints, called clauses. Namely, SAT solvers work on conjunctive normal -form problems (CNFs). There are many ways to efficiently code arbitrary logic -into CNF, so this is not so much a restricting factor. Nonetheless, we present -CNF and the problem below in a brief self-contained fashion which we find -useful. Readers interested in more depth should consult Wikipedia, or The -Handbook of Satisfiability, or Donald Knuth's latest volume of The Art of -Computer Programming. - -### CNF - -A CNF is a conjunction of clauses - - c1 and c2 and ... and cM - -Each c[i], i in [1..M], is a clause, which is of the form - - m1 or m2 or ... or mN - -where each m[i], i in [1..N] is either a Boolean variable (such as x), or the -negation of a Boolean variable (such as not(y)). An expression which is either -a Boolean variable or its negation is called a "literal". - -In the following, we refer to variables simply by integers 1,2,3,... - -Clauses are often written in succint form - - -3 11 12 14 -257 - -Numerical negation indicates logical negation, and spaces are disjunctions -"or". Sometimes "+" is used for "or". - -Conjunctions are just concatenation of clauses. We can parenthesize clauses -such as - - (1 -2) (2 -3) (3 -4) (4 -1) - -which expresses a set of clauses whose satisfying assignments are - - {1,2,3,4} - or - {-1,-2,-3,-4} - -### Models - -A model of a CNF is a value for each of the variables which makes every clause -in the CNF true. The SAT problem is determining whether or not a model exists -for a given set of clauses. - - -### Proofs - -#### Resolution - -Resolution is a form of logical reasoning with conjunctions of clauses. Given -2 clauses of the form - - C + v -and - - D + -v - -We can conclude that - - C + D - -must be true. - -Here, C and D are arbitrary clauses. - -Resolution proof of unsatisfiability is a derivation of the empty disjuction -(false) by means of resolution. Resolution proofs, even minimally sized ones, -can be very large, exponentially larger than the input problem. - -Modern SAT solvers mostly rely on performing operations which correspond to -bounded size (in terms of number of variables) number of resolutions. Given -this fact together with the fact that the minimal proofs can be exponentially -large in the number of variables, some problems can take an exponential amount -of time. - -Nonetheless, many SAT solvers have heuristics and are optimised so much that -even hard problems become tractable. With up to several tens of millions of -resolutions happening per second on one modern single core CPU, even problems -with known exponential bounds on resolution steps can be solved. - -## Solving Formulas and Circuits - -Gini provides a simple and efficient logic modelling library which supports -easy construction of arbitrary Boolean formulas. The library uses and-inverter -graphs, structural hashing, constant propagation and can be used for -constructing compact formulas with a rich set of Boolean operators. The -circuit type implements an interface which makes it plug into a solver -automatically. In fact, the circuit type uses the same representation for -literals as the solver, so there is no need to map between solver and circuit -variables. - -Additionally, sequential circuits are supported. The sequential part of the -logic library provides memory elements (latches) which are evaluated initially -as inputs and take a "next" value which provides input to the next cycle of the -circuit. The library supports unrolling sequential circuits for a fixed number -of cycles to arrive at a non-sequential formula which can then be checked for -satisfiability using solving tools. - -Gini also supports cardinality constraints which can constrain how many of a -set of Boolean variables are true. Cardinality constraints in turn provide -an easy means of doing optimisation. Gini uses sorting networks to code -cardinality constraints into clauses. Sorting networks are a good general -purpose means of handling cardinality constraints in a problem context which -also contains lots of purely Boolean logic (implicitly or not). - -Most SAT use cases use a front end for modelling arbitrary formulas. When formats -are needed for interchange, Gini supports the following. - -### Aiger - -Gini supports [aiger version 1.9](http://fmv.jku.at/aiger/) in conjunction -with its logic library. The logic.C and logic.S circuit types can be -stored, exchanged, read and written in aiger ascii and binary formats. - -### Dimacs - -CNF Dimacs files, which are an ancient widely used format for representing CNF -formulas. Dimacs files are usually used for benchmarking solvers, to eliminate -the formula representation layer. The fact that the format is more or less -universally supported amongst SAT solvers leads some SAT users to use this -format, even though there is I/O, CNF translation, and parsing overhead by -comparison to using a logic library. - - -## Optimisation - -With Cardinality constraints, optimisation is easy - - import "github.com/irifrance/gini" - import "github.com/irifrance/gini/logic" - - c := logic.NewC() - - - // suppose we encode package constraints for a module in the circuit c - // and we have a slice S of dependent packages P each of which has an attribute - // P.needsRepl which indicates whether or not it needs to be replaced (of type - // github.com/irifrance/gini/z.Lit) - - repls := make([]z.Lit, 0, 1<<23) - for _, p := range pkgs { - repls = append(repls, p.needsRepl) - } - - // make a cardinality constraints object - cards := c.CardSort(repls) - - // loop through the constraints (note a linear search - // can be faster than a binary search in this case because the underlying solver - // often has locality of logic cache w.r.t. cardinality constraints) - s := gini.New() - c.ToCnf(s) - minRepls := -1 - for i := range repls { - s.Assume(cards.Leq(i)) - if s.Solve() == 1 { - minRepls = i - break - } - } - - // use the model, if one was found, from s to propose a build - -## Activation Literals - -Gini supports recycling activation literals with the -[Activatable interface](http://godoc.org/github.com/irifrance/gini/inter#Activatable) - -Even without recycling, activation literals provide an easy way to solve MAXSAT problems: -just activate each clause, use a cardinality constraint on the activation literals, -and then optimize the output. - -With recycling, one can do much more, such as activating and deactivating sets of clauses, -and constructing the clauses on the fly. Activations work underneath test scopes and -assumptions, making the interface for Gini perhaps the most flexible available. - - -## Performance - -In applications, SAT problems normally have an exponential tail runtime -distribution with a strong bias towards bigger problems populating the longer -runtime part of the distribution. So in practice, a good rule of thumb is 1 in -N problems will on average take longer than time alotted to solve it for a -problem of a given size, and then one measures N experimentally. Very often, -despite the NP nature of SAT, an application can be designed to use a SAT solver -in a way that problems almost never take too long. Additionally, the hardest known -hand-crafted problems for CDCL solvers which take significant time involve at least -a few hundred variables. So if you're application has only a few hundred variables, -you're probably not going to have any performance problems at all with any solver. - -As in almost every solver, the core CDCL solver in Gini is the workhorse and is a -good general purpose solver. Some specific applications do benefit from -pre- or in-processing, and some some applications may not be useable with such -techniques. Other solvers provide more and better pre- or in-processing than Gini -and help is welcome in adding such solving techniques to Gini. - -The core CDCL solver in Gini has been compared with that in MiniSAT and PicoSAT, -two standard such solvers on randomly chosen SAT competition problems. In this -evaluation, Gini out performed PicoSAT and was neck-in-neck with MiniSAT. The -core CDCL solver in Gini also measures up to PicoSAT and MiniSAT in terms of -"propagations per second", indicating the core routines are themselves competitive -with these solvers, not only the heuristics. This level of performance has not to -our knowledge been achieved by other sat solvers in Go, such as go-sat or gophersat. - -While the above evaluation casts a fairly wide net over application domains and -problem difficulty, the performance of sat solvers and underlying algorithms are -fundamentally hard to predict in any rigorous way. So your experience may differ, -but we are confident Gini's core solver is a well positioned alternative to standard -high-performance CDCL solvers in C/C++. We encourage you to give it a try and welcome -any comparisons. - -### Benchmarking - -To that end, gini comes with a nifty SAT solver benchmarking tool which allows -to easily select benchmarks into a "bench" format, which is just a particular -structure of directories and files. The tool can then also run solvers -on such generated "bench"'s, enforcing various timeouts and logging all details, -again in a standard format. To tool then can compare the results in various -fashions, printing out scatter and cactus plots (in UTF8/ascii art) of various -user selectable subsets of the benchmark run. - -You may find this tool useful to fork and adopt to benchmark a new kind of -program. The benchmarking mechanism is appropriate for any "solver" like -software (SMT, CPLEX, etc) where runtimes vary and are unpredictable and -potentially high. If you do so, please follow the license or ask for -alternatives. - -## Concurrency - -Gini is written in Go and uses several goroutines by default for garbage -collection and system call scheduling. There is a "core" single-goroutine -solver, xo, which is in an internal package for gutsy low level SAT hackers. - -### Connections to solving processes - -Gini provides safe connections to solving processes which are guaranteed to not -lose any solution found, can pause and resume, run with a timeout, test without -solving, etc. - -### Solve-time copyable solvers. - -Gini provides copyable solvers, which can be safely copied *at solvetime during -a pause*. - -### Ax -Gini provides an "Assumption eXchange" package for deploying solves -under different sets of assumptions to the same set of underlying constraints -in parallel. This can give linear speed up in tasks, such as PDR/IC3, which -generate lots of assumptions. - -We hope to extend this with clause sharing soon, which would give -superlinear speedup according to the literature. - -## Distributed and CRISP - -Gini provides a definition and reference implementation for -[CRISP-1.0](https://github.com/irifrance/gini/blob/master/doc/crisp/crisp.pdf), -the compressed incremental SAT protocol. The protocol is a client-server wire -protocol which can dispatch an incremental sat solver with very little overhead -as compared to direct API calls. The advantage of using a protocol is that it -allows arbitrary tools to implement the solving on arbitrary hardware without -affecting the client. - -Many SAT applications are incremental and easily solve huge numbers of problems -while only a few problems are hard. CRISP facilitates pulling out the big guns -for the hard problems while not affecting performance for easy problems. Big -guns tend to be harder to integrate into applications because of compilation -issues, hardware requirements, size and complexity of the code base, etc. -Applications that use CRISP can truly isolate themselves from the woes of -integrating big guns while benefiting on hard problems. - -CRISP also allows language independent incremental SAT solving. The -applications and solvers can be readily implemented without the headache of -synchronizing programming language, compilers, or coding style. - -We are planning on implementing some CRISP extensions, namely the multiplexing -interface which will enable (possibly remote) clients to control -programmatically partitioning or queuing of related SAT problems. - -The CRISP protocol provides a basis for distributed solving. Gini implements -a CRISP-1.0 client and server. - -A command, crispd, is supplied for the CRISP server. - -## Citing Gini - -Zenodo DOI based citations and download: -[![DOI](https://zenodo.org/badge/64034957.svg)](https://zenodo.org/badge/latestdoi/64034957) - -BibText: -``` -@misc{scott_cotton_2019_2553490, - author = {Scott Cotton}, - title = {irifrance/gini: Sapeur}, - month = jan, - year = 2019, - doi = {10.5281/zenodo.2553490}, - url = {https://doi.org/10.5281/zenodo.2553490} -} -``` - diff --git a/vendor/github.com/operator-framework/gini/go.mod b/vendor/github.com/operator-framework/gini/go.mod deleted file mode 100644 index 15f34b3a9f..0000000000 --- a/vendor/github.com/operator-framework/gini/go.mod +++ /dev/null @@ -1 +0,0 @@ -module github.com/operator-framework/gini diff --git a/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/constraints.go b/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/constraints.go index ca3c4f5331..785ee409fd 100644 --- a/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/constraints.go +++ b/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/constraints.go @@ -4,8 +4,8 @@ import ( "fmt" "strings" - "github.com/operator-framework/gini/logic" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/logic" + "github.com/go-air/gini/z" ) // Constraint implementations limit the circumstances under which a diff --git a/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/lit_mapping.go b/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/lit_mapping.go index f837ffc3e8..dedb5fb8da 100644 --- a/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/lit_mapping.go +++ b/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/lit_mapping.go @@ -4,9 +4,9 @@ import ( "fmt" "strings" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/logic" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/logic" + "github.com/go-air/gini/z" ) type DuplicateIdentifier Identifier diff --git a/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search.go b/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search.go index f36678f1ee..ed84ea9309 100644 --- a/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search.go +++ b/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/search.go @@ -3,8 +3,8 @@ package solver import ( "context" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" ) type choice struct { diff --git a/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/solve.go b/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/solve.go index 712ae3bcc7..5d81f459a2 100644 --- a/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/solve.go +++ b/vendor/github.com/operator-framework/operator-lifecycle-manager/pkg/controller/registry/resolver/solver/solve.go @@ -6,9 +6,9 @@ import ( "fmt" "strings" - "github.com/operator-framework/gini" - "github.com/operator-framework/gini/inter" - "github.com/operator-framework/gini/z" + "github.com/go-air/gini" + "github.com/go-air/gini/inter" + "github.com/go-air/gini/z" ) var Incomplete = errors.New("cancelled before a solution could be found") diff --git a/vendor/modules.txt b/vendor/modules.txt index 645d346fb5..3db020515b 100644 --- a/vendor/modules.txt +++ b/vendor/modules.txt @@ -199,6 +199,13 @@ github.com/form3tech-oss/jwt-go github.com/fsnotify/fsnotify # github.com/ghodss/yaml v1.0.0 github.com/ghodss/yaml +# github.com/go-air/gini v1.0.4 +github.com/go-air/gini +github.com/go-air/gini/dimacs +github.com/go-air/gini/inter +github.com/go-air/gini/internal/xo +github.com/go-air/gini/logic +github.com/go-air/gini/z # github.com/go-bindata/go-bindata/v3 v3.1.3 ## explicit github.com/go-bindata/go-bindata/v3 @@ -486,13 +493,6 @@ github.com/operator-framework/api/pkg/validation github.com/operator-framework/api/pkg/validation/errors github.com/operator-framework/api/pkg/validation/interfaces github.com/operator-framework/api/pkg/validation/internal -# github.com/operator-framework/gini v1.1.0 -github.com/operator-framework/gini -github.com/operator-framework/gini/dimacs -github.com/operator-framework/gini/inter -github.com/operator-framework/gini/internal/xo -github.com/operator-framework/gini/logic -github.com/operator-framework/gini/z # github.com/operator-framework/operator-lifecycle-manager v0.0.0-00010101000000-000000000000 => ./staging/operator-lifecycle-manager ## explicit github.com/operator-framework/operator-lifecycle-manager/cmd/catalog