Add bindings for optimize

README.md

@@ -48,9 +48,10 @@ You can customize the Z3 compilation by setting a couple environmental
 variables prior to calling `make`:
 
   * `Z3_REF` is the git ref that will be checked out for Z3. This
-    defaults to to a recently tagged version. It is recommended that you
+    defaults to to `master`. It is recommended that you
     explicitly set this to a ref that works for you to avoid any changes
-    in this library later.
+    in this library later. The tag `z3-4.5.0` is proven to work with 
+    the current version. 
 
 ## Usage
 

ast_arith.go

@@ -74,7 +74,7 @@ func (a *AST) Lt(a2 *AST) *AST {
 	}
 }
 
-// Le creates a "less than" comparison.
+// Le creates a "less or equal than" comparison.
 //
 // Maps to: Z3_mk_le
 func (a *AST) Le(a2 *AST) *AST {
@@ -94,7 +94,7 @@ func (a *AST) Gt(a2 *AST) *AST {
 	}
 }
 
-// Ge creates a "less than" comparison.
+// Ge creates a "greater or equal than" comparison.
 //
 // Maps to: Z3_mk_ge
 func (a *AST) Ge(a2 *AST) *AST {

enum.go

@@ -11,3 +11,15 @@ const (
 	Undef       = C.Z3_L_UNDEF
 	True        = C.Z3_L_TRUE
 )
+
+func (b LBool) String() string {
+	if b == False {
+		return "False"
+	} else if b == Undef {
+		return "Undef"
+	} else if b == True {
+		return "True"
+	} else {
+		panic("Unknown LBool")
+	}
+}

optimize.go

@@ -0,0 +1,86 @@
+package z3
+
+// #include "go-z3.h"
+import "C"
+
+type Optimize struct {
+	rawCtx      C.Z3_context
+	rawOptimize C.Z3_optimize
+}
+
+// NewOptimize creates a new optimize.
+func (c *Context) NewOptimize() *Optimize {
+	rawOptimize := C.Z3_mk_optimize(c.raw)
+	C.Z3_optimize_inc_ref(c.raw, rawOptimize)
+
+	return &Optimize{
+		rawOptimize: rawOptimize,
+		rawCtx:      c.raw,
+	}
+}
+
+// Close frees the memory associated with this.
+func (s *Optimize) Close() error {
+	C.Z3_optimize_dec_ref(s.rawCtx, s.rawOptimize)
+	return nil
+}
+
+// Add adds a constraint onto the Optimize.
+//
+// Maps to: Z3_optimize_assert
+func (s *Optimize) Add(a *AST) {
+	C.Z3_optimize_assert(s.rawCtx, s.rawOptimize, a.rawAST)
+}
+
+// Maximize adds a function to maximize and returns a handle to be later used in Lower or Upper.
+//
+// Maps to: Z3_optimize_maximize
+func (s *Optimize) Maximize(a *AST) (handle uint) {
+	return uint(C.Z3_optimize_maximize(s.rawCtx, s.rawOptimize, a.rawAST))
+}
+
+// Minimize adds a function to minimize and returns a handle to be later used in Lower or Upper.
+//
+// Maps to: Z3_optimize_minimize
+func (s *Optimize) Minimize(a *AST) (handle uint) {
+	return uint(C.Z3_optimize_minimize(s.rawCtx, s.rawOptimize, a.rawAST))
+}
+
+// Lower returns a lower value or the current approximation.
+//
+// Maps to: Z3_optimize_get_lower
+func (s *Optimize) Lower(handle uint) *AST {
+	return &AST{
+		rawCtx: s.rawCtx,
+		rawAST: C.Z3_optimize_get_lower(s.rawCtx, s.rawOptimize, C.uint(handle)),
+	}
+}
+
+// Upper returns an upper value or the current approximation.
+//
+// Maps to: Z3_optimize_get_upper
+func (s *Optimize) Upper(handle uint) *AST {
+	return &AST{
+		rawCtx: s.rawCtx,
+		rawAST: C.Z3_optimize_get_upper(s.rawCtx, s.rawOptimize, C.uint(handle)),
+	}
+}
+
+// Check checks if the currently set formula is consistent.
+//
+// Maps to: Z3_optimize_check
+func (s *Optimize) Check() LBool {
+	return LBool(C.Z3_optimize_check(s.rawCtx, s.rawOptimize))
+}
+
+// Model returns the last model from a Check.
+//
+// Maps to: Z3_optimize_get_model
+func (s *Optimize) Model() *Model {
+	m := &Model{
+		rawCtx:   s.rawCtx,
+		rawModel: C.Z3_optimize_get_model(s.rawCtx, s.rawOptimize),
+	}
+	m.IncRef()
+	return m
+}

optimize_test.go

@@ -0,0 +1,57 @@
+package z3
+
+import (
+	"testing"
+)
+
+func TestOptimize(t *testing.T) {
+	config := NewConfig()
+	defer config.Close()
+
+	ctx := NewContext(config)
+	defer ctx.Close()
+
+	// Create the "x xor y" constraint
+	intTyp := ctx.IntSort()
+	x := ctx.Const(ctx.Symbol("x"), intTyp)
+	y := ctx.Const(ctx.Symbol("y"), intTyp)
+	zero := ctx.Int(0, intTyp)
+	ten := ctx.Int(10, intTyp)
+	eleven := ctx.Int(11, intTyp)
+
+	// Create the optimize
+	o := ctx.NewOptimize()
+	defer o.Close()
+
+	// Assert constraints
+	o.Add(ten.Ge(x).And(x.Ge(zero)))
+	o.Add(ten.Ge(y).And(y.Ge(zero)))
+	o.Add(x.Add(y).Le(eleven))
+
+	handleX := o.Maximize(x)
+	handleY := o.Maximize(y)
+
+	// Optimize
+	result := o.Check()
+	if result != True {
+		t.Fatalf("bad: %s", result)
+	}
+
+	if upperX := o.Upper(handleX).Int(); upperX != 10 {
+		t.Fatalf("bad: %d", upperX)
+	}
+	if lowerX := o.Lower(handleX).Int(); lowerX != 10 {
+		t.Fatalf("bad: %d", lowerX)
+	}
+	if upperY := o.Upper(handleY).Int(); upperY != 1 {
+		t.Fatalf("bad: %d", upperY)
+	}
+	if lowerY := o.Lower(handleY).Int(); lowerY != 1 {
+		t.Fatalf("bad: %d", lowerY)
+	}
+
+	// Get the model
+	m := o.Model()
+	defer m.Close()
+	t.Logf("\nModel:\n%s", m.String())
+}