README
¶
go-stp
Go-stp provides bindings for the Simple Theorem Prover on Linux. Most operations are supported.
Installation
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.git
Note 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/library
Usage
The 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
}
Contributing
Anyone is free to contribute or suggest any changes to this repository if they are interested.
License
Documentation
¶
Index ¶
- func ExprString(e Expr) string
- func GetBVLen(e Expr) int
- func RegisterErrorHandler()
- type Expr
- type Solver
- func (s *Solver) Add(in string)
- func (s *Solver) AndExpr(left, right Expr) Expr
- func (s *Solver) AssertFormula(e Expr)
- func (s *Solver) BitVec(in string, bitWidth int) Expr
- func (s *Solver) BvAndExpr(left, right Expr) Expr
- func (s *Solver) BvConstExprFromInt(bitWidth int, value uint) Expr
- func (s *Solver) BvDivExpr(bitWidth int, dividend Expr, divisor Expr) Expr
- func (s *Solver) BvGeExpr(left, right Expr) Expr
- func (s *Solver) BvGtExpr(left, right Expr) Expr
- func (s *Solver) BvLShiftExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvLeExpr(left, right Expr) Expr
- func (s *Solver) BvLtExpr(left, right Expr) Expr
- func (s *Solver) BvMinusExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvModExpr(bitWidth int, dividend Expr, divisor Expr) Expr
- func (s *Solver) BvMultExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvNotExpr(child Expr) Expr
- func (s *Solver) BvOrExpr(left, right Expr) Expr
- func (s *Solver) BvPlusExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvRShiftExpr(bitWidth int, left Expr, right Expr) Expr
- func (s *Solver) BvType(no_bits int) Type
- func (s *Solver) BvUMinusExpr(child Expr) Expr
- func (s *Solver) BvXorExpr(left, right Expr) Expr
- func (s *Solver) Destroy()
- func (s *Solver) EqExpr(child0 Expr, child1 Expr) Expr
- func (s *Solver) Eval(exp ast.Expr) Expr
- func (s *Solver) EvalBinaryExpr(exp *ast.BinaryExpr) Expr
- func (s *Solver) EvalUnaryExpr(exp *ast.UnaryExpr) Expr
- func (s *Solver) FalseExpr() Expr
- func (s *Solver) GetTermFromCounterExample(e Expr, c WholeCounterExample) Expr
- func (s *Solver) GetWholeCounterExample() WholeCounterExample
- func (s *Solver) H2i(in string) uint64
- func (s *Solver) ImpliesExpr(hyp Expr, conc Expr) Expr
- func (s *Solver) NotExpr(child Expr) Expr
- func (s *Solver) OrExpr(left, right Expr) Expr
- func (s *Solver) PrintAsserts(simplify_print int)
- func (s *Solver) PrintCounterExample()
- func (s *Solver) PrintQuery()
- func (s *Solver) Query(e Expr) int
- func (s *Solver) SH2i(in string) int64
- func (s *Solver) SSolve(vars ...Expr) []int64
- func (s *Solver) Solve(vars ...Expr) []uint64
- func (s *Solver) TrueExpr() Expr
- func (s *Solver) VarExpr(name string, typ Type) Expr
- func (s *Solver) XorExpr(left, right Expr) Expr
- type Type
- type VC
- type WholeCounterExample
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func ExprString ¶
HIGH LEVEL API FUNCTIONS ExprString converts an Expr e into its string counterpart
func RegisterErrorHandler ¶
func RegisterErrorHandler()
SOLVER RELATED FUNCTIONS RegisterErrorHandler registers an error handler which triggers when there is an error in the C api
Types ¶
type Solver ¶
type Solver struct {
// contains filtered or unexported fields
}
func (*Solver) AssertFormula ¶
AssertFormula adds constraint e to the solver
func (*Solver) BitVec ¶
BitVec returns an Expr which is symbollic of string in with bit length bithWidth
func (*Solver) BvAndExpr ¶
BvAndExpr returns an Expr of bit length bitWidth between two Exprs left and right which are bitwise and
func (*Solver) BvConstExprFromInt ¶
BvConstExprFromInt returns an Expr of bit length bitWidth which is a constant of value
func (*Solver) BvDivExpr ¶
BvDivExpr returns an Expr of bit length bitWidth between two Exprs dividend and divisor which are divided
func (*Solver) BvLShiftExpr ¶
BvLShiftExpr returns an Expr of bit length bitWidth where left << right
func (*Solver) BvMinusExpr ¶
BVPlusExpr returns an Expr of bit length bitWidth between two Exprs left and right which are subtracted
func (*Solver) BvModExpr ¶
BvDivExpr returns an Expr of bit length bitWidth between two Exprs dividend and divisor which are in modulo
func (*Solver) BvMultExpr ¶
BvMultExpr returns an Expr of bit length bitWidth between two Exprs left and right which are multiplied
func (*Solver) BvOrExpr ¶
BvAndExpr returns an Expr of bit length bitWidth between two Exprs left and right which are bitwise or
func (*Solver) BvPlusExpr ¶
BVPlusExpr returns an Expr of bit length bitWidth between two Exprs left and right which are added
func (*Solver) BvRShiftExpr ¶
BvRShiftExpr returns an Expr of bit length bitWidth where left >> right
func (*Solver) BvType ¶
BITVECTOR RELATED FUNCTIONS BvType returns a type of bitwidth no_bits that could be used in VarExpr
func (*Solver) BvUMinusExpr ¶
BvUMinusExpr returns the arithmetic negation of Expr child
func (*Solver) BvXorExpr ¶
BvAndExpr returns an Expr of bit length bitWidth between two Exprs left and right which are bitwise xor
func (*Solver) Eval ¶
Eval recursively traverses the ast and returns the associated Expr form of the ast
func (*Solver) EvalBinaryExpr ¶
func (s *Solver) EvalBinaryExpr(exp *ast.BinaryExpr) Expr
EvalBinaryExpr returns an associated Expr which is representive of the BinaryExpr within an ast
func (*Solver) EvalUnaryExpr ¶
EvalUnaryExpr returns an associated Expr which is representive of the UnaryExpr within an ast
func (*Solver) GetTermFromCounterExample ¶
func (s *Solver) GetTermFromCounterExample(e Expr, c WholeCounterExample) Expr
GetTermFromCounterExample returns an Expr that is associated with Expr e from the WholeCounterExample c
func (*Solver) GetWholeCounterExample ¶
func (s *Solver) GetWholeCounterExample() WholeCounterExample
GetWholeCounterExample returns the full CounterExample that invalidates the Queried Expr
func (*Solver) ImpliesExpr ¶
ImpliesExpr returns an Expr where hyp implies conc
func (*Solver) PrintAsserts ¶
PrintAsserts prints to stdout the assertions made to the checker
func (*Solver) PrintCounterExample ¶
func (s *Solver) PrintCounterExample()
PrintCounterExample prints to stdout the CounterExample which invalidates the Queried Expr
func (*Solver) PrintQuery ¶
func (s *Solver) PrintQuery()
PrintQuery prints to stdout the most recent Query
func (*Solver) SSolve ¶
Signed solve evaluates the assertions which returns values of symbollic inputs vars in int form
func (*Solver) Solve ¶
Solve evaluates the assertions which returns values of symbollic inputs vars in int form
type WholeCounterExample ¶
type WholeCounterExample C.WholeCounterExample
Source Files