From b71580f11c5c4006e794e9c239c536de58e37068 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 24 Mar 2014 03:11:53 -0700
Subject: [PATCH] fix APIs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_opt.cpp        |  2 +-
 src/api/dotnet/Optimize.cs |  2 +-
 src/api/python/z3.py       | 19 ++++++++++++++++---
 3 files changed, 18 insertions(+), 5 deletions(-)

diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index ebad997da..b1e4b9203 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -79,7 +79,7 @@ extern "C" {
         LOG_Z3_optimize_assert_soft(c, o, a, weight, id);
         RESET_ERROR_CODE();
         CHECK_FORMULA(a,0);        
-        rational w("weight");
+        rational w(weight);
         return to_optimize_ref(o).add_soft_constraint(to_expr(a), w, to_symbol(id));
         Z3_CATCH_RETURN(0);
     }
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 03a78df9b..29fbfbf75 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -165,7 +165,7 @@ namespace Microsoft.Z3
             }
         }
 
-x
+
         #region Internal
         internal Optimize(Context ctx, IntPtr obj)
             : base(ctx, obj)
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 448389b27..f513fd4bd 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -6321,9 +6321,22 @@ class Optimize(Z3PPObject):
         """Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
         self.assert_exprs(*args)
 
-    def add_soft(self, arg, weight = None):
-	"""Add soft constraint with optional weight."""
-	pass
+    def add_soft(self, arg, weight = "1", id = None):
+	"""Add soft constraint with optional weight and optional identifier.
+	   If no weight is supplied, then the penalty for violating the soft constraint
+	   is 1.
+	   Soft constraints are grouped by identifiers. Soft constraints that are
+	   added without identifiers are grouped by default.
+	"""
+	if _is_int(weight):
+	    weight = "%d" % weight
+	if not isinstance(weight, str):
+	    raise Z3Exception("weight should be a string or an integer")
+	if id == None:
+	    id = 0
+	id = to_symbol(id, self.ctx)
+	v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
+	return OptimizeObjective(v)
 
     def maximize(self, arg):
 	"""Add objective function to maximize."""