Go-stp provides bindings for the Simple Theorem Prover on Linux. Most operations are supported.
The bindings make use of the Simple Theorem Prover which should be setup first. After STP has been setup, just clone the repo in your $GOPATH/src folder.
git clone https://github.com/arckt/go-stp.gitNote that for the bindings to work, the stp dynamic library is assumed to be in /usr/local/lib/. If the library is unaccessible run the following.
sudo ldconfig /path/to/lib/libraryThe bindings could be used purely as a c wrapper which is done through cgo or with the convenient Python-like API which is used in the Python STP bindings.
An example of a golang program that uses the Python-like API.
package main
import "fmt"
import g"arckt/go-stp"
func main() {
h := g.Init() //Initialize solver
defer h.Destroy() //Destroy solver at end of main()
x := h.Bitvec("x", 32) //Add symbollic variable of bitwidth 32 of name "x"
h.add("x + 3 == 5") //Add constraint for the solver to evaluate
res := h.Solve(x) //Tell solver to evaluate value of symbollic variable x to fulfill constraints
fmt.Println(res[0]) //Print symbollic variable of x if it is solvable
}Anyone is free to contribute or suggest any changes to this repository if they are interested.