Merge pull request #8813 from Z3Prover/copilot/fix-issues-in-multiple-languages

Fix API discrepancies for Go, Python bindings

src/api/go/bitvec.go

@@ -158,3 +158,51 @@ func (c *Context) MkSignExt(i uint, expr *Expr) *Expr {
 func (c *Context) MkZeroExt(i uint, expr *Expr) *Expr {
 	return newExpr(c, C.Z3_mk_zero_ext(c.ptr, C.uint(i), expr.ptr))
 }
+
+// MkBVAddNoOverflow creates a predicate that checks that the bit-wise addition
+// of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.
+func (c *Context) MkBVAddNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
+	return newExpr(c, C.Z3_mk_bvadd_no_overflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
+}
+
+// MkBVAddNoUnderflow creates a predicate that checks that the bit-wise signed addition
+// of t1 and t2 does not underflow.
+func (c *Context) MkBVAddNoUnderflow(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvadd_no_underflow(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkBVSubNoOverflow creates a predicate that checks that the bit-wise signed subtraction
+// of t1 and t2 does not overflow.
+func (c *Context) MkBVSubNoOverflow(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsub_no_overflow(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkBVSubNoUnderflow creates a predicate that checks that the bit-wise subtraction
+// of t1 and t2 does not underflow. If isSigned is true, checks for signed underflow.
+func (c *Context) MkBVSubNoUnderflow(t1, t2 *Expr, isSigned bool) *Expr {
+	return newExpr(c, C.Z3_mk_bvsub_no_underflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
+}
+
+// MkBVSdivNoOverflow creates a predicate that checks that the bit-wise signed division
+// of t1 and t2 does not overflow.
+func (c *Context) MkBVSdivNoOverflow(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsdiv_no_overflow(c.ptr, t1.ptr, t2.ptr))
+}
+
+// MkBVNegNoOverflow creates a predicate that checks that bit-wise negation does not overflow
+// when t1 is interpreted as a signed bit-vector.
+func (c *Context) MkBVNegNoOverflow(t1 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvneg_no_overflow(c.ptr, t1.ptr))
+}
+
+// MkBVMulNoOverflow creates a predicate that checks that the bit-wise multiplication
+// of t1 and t2 does not overflow. If isSigned is true, checks for signed overflow.
+func (c *Context) MkBVMulNoOverflow(t1, t2 *Expr, isSigned bool) *Expr {
+	return newExpr(c, C.Z3_mk_bvmul_no_overflow(c.ptr, t1.ptr, t2.ptr, C.bool(isSigned)))
+}
+
+// MkBVMulNoUnderflow creates a predicate that checks that the bit-wise signed multiplication
+// of t1 and t2 does not underflow.
+func (c *Context) MkBVMulNoUnderflow(t1, t2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvmul_no_underflow(c.ptr, t1.ptr, t2.ptr))
+}

src/api/go/simplifier.go

@@ -52,3 +52,10 @@ func (s *Simplifier) GetHelp() string {
 func (s *Simplifier) GetParamDescrs() *ParamDescrs {
 	return newParamDescrs(s.ctx, C.Z3_simplifier_get_param_descrs(s.ctx.ptr, s.ptr))
 }
+
+// GetSimplifierDescr returns a description of the simplifier with the given name.
+func (c *Context) GetSimplifierDescr(name string) string {
+	cName := C.CString(name)
+	defer C.free(unsafe.Pointer(cName))
+	return C.GoString(C.Z3_simplifier_get_descr(c.ptr, cName))
+}

src/api/go/tactic.go

@@ -78,6 +78,72 @@ func (c *Context) TacticSkip() *Tactic {
 	return newTactic(c, C.Z3_tactic_skip(c.ptr))
 }
 
+// TryFor returns a tactic that applies t for at most ms milliseconds.
+// If t does not terminate in ms milliseconds, then it fails.
+func (t *Tactic) TryFor(ms uint) *Tactic {
+	return newTactic(t.ctx, C.Z3_tactic_try_for(t.ctx.ptr, t.ptr, C.uint(ms)))
+}
+
+// UsingParams returns a tactic that applies t using the given parameters.
+func (t *Tactic) UsingParams(params *Params) *Tactic {
+	return newTactic(t.ctx, C.Z3_tactic_using_params(t.ctx.ptr, t.ptr, params.ptr))
+}
+
+// GetParamDescrs returns parameter descriptions for the tactic.
+func (t *Tactic) GetParamDescrs() *ParamDescrs {
+	return newParamDescrs(t.ctx, C.Z3_tactic_get_param_descrs(t.ctx.ptr, t.ptr))
+}
+
+// ApplyEx applies the tactic to a goal with the given parameters.
+func (t *Tactic) ApplyEx(g *Goal, params *Params) *ApplyResult {
+	return newApplyResult(t.ctx, C.Z3_tactic_apply_ex(t.ctx.ptr, t.ptr, g.ptr, params.ptr))
+}
+
+// TacticFailIf creates a tactic that fails if the probe p evaluates to false.
+func (c *Context) TacticFailIf(p *Probe) *Tactic {
+	return newTactic(c, C.Z3_tactic_fail_if(c.ptr, p.ptr))
+}
+
+// TacticFailIfNotDecided creates a tactic that fails if the goal is not
+// trivially satisfiable (empty) or trivially unsatisfiable (contains false).
+func (c *Context) TacticFailIfNotDecided() *Tactic {
+	return newTactic(c, C.Z3_tactic_fail_if_not_decided(c.ptr))
+}
+
+// ParOr creates a tactic that applies the given tactics in parallel.
+func (c *Context) ParOr(tactics []*Tactic) *Tactic {
+	cTactics := make([]C.Z3_tactic, len(tactics))
+	for i, t := range tactics {
+		cTactics[i] = t.ptr
+	}
+	return newTactic(c, C.Z3_tactic_par_or(c.ptr, C.uint(len(tactics)), &cTactics[0]))
+}
+
+// ParAndThen creates a tactic that applies t to a goal and then t2 to every
+// subgoal produced by t, processing subgoals in parallel.
+func (t *Tactic) ParAndThen(t2 *Tactic) *Tactic {
+	return newTactic(t.ctx, C.Z3_tactic_par_and_then(t.ctx.ptr, t.ptr, t2.ptr))
+}
+
+// GetTacticDescr returns a description of the tactic with the given name.
+func (c *Context) GetTacticDescr(name string) string {
+	cName := C.CString(name)
+	defer C.free(unsafe.Pointer(cName))
+	return C.GoString(C.Z3_tactic_get_descr(c.ptr, cName))
+}
+
+// NewSolverFromTactic creates a solver from the given tactic.
+// The solver uses the tactic to solve goals.
+func (c *Context) NewSolverFromTactic(t *Tactic) *Solver {
+	ptr := C.Z3_mk_solver_from_tactic(c.ptr, t.ptr)
+	s := &Solver{ctx: c, ptr: ptr}
+	C.Z3_solver_inc_ref(c.ptr, ptr)
+	runtime.SetFinalizer(s, func(solver *Solver) {
+		C.Z3_solver_dec_ref(solver.ctx.ptr, solver.ptr)
+	})
+	return s
+}
+
 // Goal represents a set of formulas that can be solved or transformed.
 type Goal struct {
 	ctx *Context
@@ -243,6 +309,13 @@ func (p *Probe) Not() *Probe {
 	return newProbe(p.ctx, C.Z3_probe_not(p.ctx.ptr, p.ptr))
 }
 
+// GetProbeDescr returns a description of the probe with the given name.
+func (c *Context) GetProbeDescr(name string) string {
+	cName := C.CString(name)
+	defer C.free(unsafe.Pointer(cName))
+	return C.GoString(C.Z3_probe_get_descr(c.ptr, cName))
+}
+
 // Params represents a parameter set.
 type Params struct {
 	ctx *Context

src/api/python/z3/z3.py

@@ -8463,8 +8463,11 @@ class Optimize(Z3PPObject):
         self._on_models_id = None
         Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
 
+    def __copy__(self):
+        return self.translate(self.ctx)
+
     def __deepcopy__(self, memo={}):
-        return Optimize(self.optimize, self.ctx)
+        return self.translate(self.ctx)
 
     def __del__(self):
         if self.optimize is not None and self.ctx.ref() is not None and Z3_optimize_dec_ref is not None:
@@ -8672,6 +8675,19 @@ class Optimize(Z3PPObject):
         """
         return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
 
+    def translate(self, target):
+        """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
+
+        >>> c1 = Context()
+        >>> c2 = Context()
+        >>> o1 = Optimize(ctx=c1)
+        >>> o2 = o1.translate(c2)
+        """
+        if z3_debug():
+            _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
+        opt = Z3_optimize_translate(self.ctx.ref(), self.optimize, target.ref())
+        return Optimize(opt, target)
+
     def set_on_model(self, on_model):
         """Register a callback that is invoked with every incremental improvement to
         objective values. The callback takes a model as argument.