Merge branch 'master' of https://github.com/Z3Prover/z3

src/api/api_ast.cpp

@@ -1124,6 +1124,20 @@ extern "C" {
             case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
             case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
 
+            case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE;
+            case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT;
+            case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH;
+            case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS;
+            case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX;
+            case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX;
+            case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE;
+            case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE;
+            case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT;
+            case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT;
+            case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX;
+            case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET;
+            case _OP_REGEXP_FULL: return Z3_OP_RE_FULL_SET;
+
             case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
             case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
 

src/api/dotnet/Expr.cs

@@ -797,6 +797,22 @@ namespace Microsoft.Z3
         public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
         #endregion
 
+        #region Sequences and Strings
+
+        /// <summary>
+        /// Check whether expression is a string constant.
+        /// </summary>
+        /// <returns>a Boolean</returns>
+        public bool IsString  { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } }
+
+        /// <summary>
+        /// Retrieve string corresponding to string constant.
+        /// </summary>
+        /// <remarks>the expression should be a string constant, (IsString should be true).</remarks>
+        public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }        
+
+        #endregion
+
         #region Proof Terms
         /// <summary>
         /// Indicates whether the term is a binary equivalence modulo namings.

src/api/dotnet/Model.cs

@@ -19,6 +19,7 @@ Notes:
 
 using System;
 using System.Diagnostics.Contracts;
+using System.Collections.Generic;
 
 namespace Microsoft.Z3
 {
@@ -131,6 +132,24 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Enumerate constants in model.
+        /// </summary>
+        public IEnumerable<KeyValuePair<FuncDecl, Expr>> Consts
+        {
+            get
+            {
+                uint nc = NumConsts;
+                for (uint i = 0; i < nc; ++i)
+                {
+                    var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
+                    IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
+                    if (n == IntPtr.Zero) continue;
+                    yield return new KeyValuePair<FuncDecl, Expr>(f, Expr.Create(Context, n));
+                }
+            }
+        }
+
         /// <summary>
         /// The number of function interpretations in the model.
         /// </summary>

src/api/java/Expr.java

@@ -126,7 +126,7 @@ public class Expr extends AST
         if (isApp() && args.length != getNumArgs()) {
             throw new Z3Exception("Number of arguments does not match");
         }
-        return new Expr(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
+        return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
                 args.length, Expr.arrayToNative(args)));
     }
 
@@ -1277,6 +1277,26 @@ public class Expr extends AST
         return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
     }
 
+    /**
+     * Check whether expression is a string constant.
+     * @return a boolean
+     */
+    public boolean isString() 
+    {
+        return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
+    }
+
+    /**
+     * Retrieve string corresponding to string constant.
+     * Remark: the expression should be a string constant, (isString() should return true).
+     * @throws Z3Exception on error
+     * @return a string
+     */
+    public String getString()
+    {
+	return Native.getString(getContext().nCtx(), getNativeObject());
+    }
+
     /**
      * Indicates whether the term is a binary equivalence modulo namings.
      * Remarks: This binary predicate is used in proof terms. It captures

src/api/python/z3/z3.py

@@ -1304,8 +1304,10 @@ class BoolSortRef(SortRef):
         if isinstance(val, bool):
             return BoolVal(val, self.ctx)
         if __debug__:
-            _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
-            _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
+            if not is_expr(val):
+               _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
+            if not self.eq(val.sort()):
+               _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
         return val
 
     def subsort(self, other):

src/api/z3_api.h

@@ -5349,6 +5349,10 @@ extern "C" {
 
     /**
        \brief Add a new formula \c a to the given goal.
+        Conjunctions are split into separate formulas.
+        If the goal is \c false, adding new formulas is a no-op.
+        If the formula \c a is \c true, then nothing is added.
+        If the formula \c a is \c false, then the entire goal is replaced by the formula \c false.
 
        def_API('Z3_goal_assert', VOID, (_in(CONTEXT), _in(GOAL), _in(AST)))
     */