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

CMakeLists.txt

@@ -112,6 +112,13 @@ else()
     set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types})
   endif()
   message(STATUS "Build type: ${CMAKE_BUILD_TYPE}")
+
+  # Check the selected build type is valid
+  list(FIND available_build_types "${CMAKE_BUILD_TYPE}" _build_type_index)
+  if ("${_build_type_index}" EQUAL "-1")
+    message(FATAL_ERROR "\"${CMAKE_BUILD_TYPE}\" is an invalid build type.\n"
+      "Use one of the following build types ${available_build_types}")
+  endif()
 endif()
 
 # CMAKE_BUILD_TYPE has no meaning for multi-configuration generators

README.md

@@ -168,7 +168,10 @@ python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/p
 
 If you do need to install to a non standard prefix a better approach is to use
 a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/)
-and install Z3 there.
+and install Z3 there. Python packages also work for Python3.
+Under Windows, recall to build inside the Visual C++ native command build environment.
+Note that the buit/python/z3 directory should be accessible from where python is used with Z3 
+and it depends on libz3.dll to be in the path.
 
 ```bash
 virtualenv venv
@@ -185,3 +188,10 @@ python -c 'import z3; print(z3.get_version_string())'
 ```
 
 See [``examples/python``](examples/python) for examples.
+
+
+Even though the build instruction says use python scripts/mk_make.py -x --python, this can build a package that works in python3.
+The building should take place inside the Visual C++ 2015 x64 Native Build Tools Prompt`.
+The z3.exe appears to be independent and can work anywhere, you can copy the built version wherever. The libz3.dll needs to be discoverable on the PATH. So you can copy both build/z3.exe and build/libz3.dll into somewhere on the PATH.
+Then the build/python/z3 directory should be copied into the site-packages directory of Python. On Windows, this isn't done automatically, instead you have to find your Windows site-packages: like python3 -c 'import site; print(site.getsitepackages())', then copy the entire directory there.
+Then to test if it finally all works run:

doc/mk_api_doc.py

@@ -12,10 +12,6 @@ import shutil
 ML_ENABLED=False
 BUILD_DIR='../build'
 
-def norm_path(p):
-    # We use '/' on mk_project for convenience
-    return os.path.join(*(p.split('/')))
-
 def display_help(exit_code):
     print("mk_api_doc.py: Z3 documentation generator\n")
     print("\nOptions:")
@@ -36,12 +32,12 @@ def parse_options():
 
     for opt, arg in options:
         if opt in ('-b', '--build'):
-            BUILD_DIR = norm_path(arg)
+            BUILD_DIR = mk_util.norm_path(arg)
         elif opt in ('h', '--help'):
             display_help()
             exit(1)
         elif opt in ('--ml'):
-            ML_ENABLED=True            
+            ML_ENABLED=True
         else:
             print("ERROR: Invalid command line option: %s" % opt)
             display_help(1)
@@ -59,7 +55,7 @@ def cleanup_API(inf, outf):
     pat1  = re.compile(".*def_API.*")
     pat2  = re.compile(".*extra_API.*")
     _inf  = open(inf, 'r')
-    _outf = open(outf, 'w') 
+    _outf = open(outf, 'w')
     for line in _inf:
         if not pat1.match(line) and not pat2.match(line):
             _outf.write(line)
@@ -90,9 +86,9 @@ try:
     cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h')
     cleanup_API('../src/api/z3_fixedpoint.h', 'tmp/z3_fixedpoint.h')
     cleanup_API('../src/api/z3_optimization.h', 'tmp/z3_optimization.h')
-    cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')    
+    cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')
     cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h')
-    
+
     print("Removed annotations from z3_api.h.")
     try:
         if subprocess.call(['doxygen', 'z3api.dox']) != 0:
@@ -112,7 +108,7 @@ try:
     os.remove('tmp/z3_interp.h')
     os.remove('tmp/z3_fpa.h')
     print("Removed temporary file header files.")
-    
+
     os.remove('tmp/website.dox')
     print("Removed temporary file website.dox")
     os.remove('tmp/z3py.py')
@@ -130,7 +126,7 @@ try:
             print("ERROR: ocamldoc failed.")
             exit(1)
         print("Generated ML/OCaml documentation.")
-        
+
     print("Documentation was successfully generated at subdirectory './api/html'.")
 except:
     exctype, value = sys.exc_info()[:2]

scripts/mk_unix_dist.py

@@ -1,7 +1,7 @@
 ############################################
 # Copyright (c) 2013 Microsoft Corporation
-# 
+#
-# Scripts for automatically generating 
+# Scripts for automatically generating
 # Linux/OSX/BSD distribution zip files.
 #
 # Author: Leonardo de Moura (leonardo)
@@ -42,7 +42,7 @@ def mk_dir(d):
 
 def set_build_dir(path):
     global BUILD_DIR
-    BUILD_DIR = path
+    BUILD_DIR = mk_util.norm_path(path)
     mk_dir(BUILD_DIR)
 
 def display_help():
@@ -65,7 +65,7 @@ def display_help():
 def parse_options():
     global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE
     path = BUILD_DIR
-    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 
+    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
                                                                    'help',
                                                                    'silent',
                                                                    'force',
@@ -89,7 +89,7 @@ def parse_options():
         elif opt == '--nodotnet':
             DOTNET_ENABLED = False
         elif opt == '--nopython':
-            PYTHON_ENABLED = False            
+            PYTHON_ENABLED = False
         elif opt == '--dotnet-key':
             DOTNET_KEY_FILE = arg
         elif opt == '--nojava':
@@ -121,7 +121,7 @@ def mk_build_dir(path):
             opts.append('--python')
         if subprocess.call(opts) != 0:
             raise MKException("Failed to generate build directory at '%s'" % path)
-    
+
 # Create build directories
 def mk_build_dirs():
     mk_build_dir(BUILD_DIR)

scripts/mk_util.py

@@ -153,8 +153,7 @@ def is_cygwin_mingw():
     return IS_CYGWIN_MINGW
 
 def norm_path(p):
-    # We use '/' on mk_project for convenience
+    return os.path.expanduser(os.path.normpath(p))
-    return os.path.join(*(p.split('/')))
 
 def which(program):
     import os
@@ -1393,7 +1392,7 @@ class DLLComponent(Component):
             shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
                         '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
-class PythonComponent(Component): 
+class PythonComponent(Component):
     def __init__(self, name, libz3Component):
         assert isinstance(libz3Component, DLLComponent)
         global PYTHON_ENABLED
@@ -1418,7 +1417,7 @@ class PythonComponent(Component):
 
     def mk_makefile(self, out):
         return
-   
+
 class PythonInstallComponent(Component):
     def __init__(self, name, libz3Component):
         assert isinstance(libz3Component, DLLComponent)
@@ -1521,7 +1520,7 @@ class PythonInstallComponent(Component):
                                       os.path.join('python', 'z3', '*.pyc'),
                                       os.path.join(self.pythonPkgDir,'z3'),
                                       in_prefix=self.in_prefix_install)
-            
+
         if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
             out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
 
@@ -1586,7 +1585,7 @@ class DotNetDLLComponent(Component):
 
     def mk_makefile(self, out):
         global DOTNET_KEY_FILE
-        
+
         if not is_dotnet_enabled():
             return
         cs_fp_files = []
@@ -1631,7 +1630,7 @@ class DotNetDLLComponent(Component):
             else:
                 print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name))
                 self.key_file = None
-                
+
         if not self.key_file is None:
             print("%s.dll will be signed using key '%s'." % (self.dll_name, self.key_file))
             cscCmdLine.append('/keyfile:{}'.format(self.key_file))
@@ -1658,7 +1657,7 @@ class DotNetDLLComponent(Component):
                              )
         else:
             cscCmdLine.extend(['/optimize+'])
-            
+
         if IS_WINDOWS:
             if VS_X64:
                 cscCmdLine.extend(['/platform:x64'])
@@ -1962,7 +1961,7 @@ class MLComponent(Component):
 
             OCAMLMKLIB = 'ocamlmklib'
 
-            LIBZ3 = '-L. -lz3'           
+            LIBZ3 = '-L. -lz3'
             if is_cygwin() and not(is_cygwin_mingw()):
                 LIBZ3 = 'libz3.dll'
 
@@ -2214,7 +2213,7 @@ class PythonExampleComponent(ExampleComponent):
     def mk_win_dist(self, build_path, dist_path):
         full = os.path.join(EXAMPLE_DIR, self.path)
         py = 'example.py'
-        shutil.copyfile(os.path.join(full, py), 
+        shutil.copyfile(os.path.join(full, py),
                         os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py))
 
     def mk_unix_dist(self, build_path, dist_path):
@@ -2263,7 +2262,7 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man
 def add_python(libz3Component):
     name = 'python'
     reg_component(name, PythonComponent(name, libz3Component))
-    
+
 def add_python_install(libz3Component):
     name = 'python_install'
     reg_component(name, PythonInstallComponent(name, libz3Component))
@@ -2689,7 +2688,7 @@ def get_full_version_string(major, minor, build, revision):
         branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD', '--long'])
         res += " master " + check_output(['git', 'describe'])
     return '"' + res + '"'
-        
+
 # Update files with the version number
 def mk_version_dot_h(major, minor, build, revision):
     c = get_component(UTIL_COMPONENT)

scripts/mk_win_dist.py

@@ -1,7 +1,7 @@
 ############################################
 # Copyright (c) 2012 Microsoft Corporation
-# 
+#
-# Scripts for automatically generating 
+# Scripts for automatically generating
 # Window distribution zip files.
 #
 # Author: Leonardo de Moura (leonardo)
@@ -46,7 +46,7 @@ def mk_dir(d):
 
 def set_build_dir(path):
     global BUILD_DIR, BUILD_X86_DIR, BUILD_X64_DIR
-    BUILD_DIR = path
+    BUILD_DIR = mk_util.norm_path(path)
     BUILD_X86_DIR = os.path.join(path, 'x86')
     BUILD_X64_DIR = os.path.join(path, 'x64')
     mk_dir(BUILD_X86_DIR)
@@ -74,7 +74,7 @@ def display_help():
 def parse_options():
     global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED, X86ONLY, X64ONLY
     path = BUILD_DIR
-    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 
+    options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=',
                                                                    'help',
                                                                    'silent',
                                                                    'force',
@@ -102,7 +102,7 @@ def parse_options():
         elif opt == '--nopython':
             PYTHON_ENABLED = False
         elif opt == '--dotnet-key':
-            DOTNET_KEY_FILE = arg            
+            DOTNET_KEY_FILE = arg
         elif opt == '--nojava':
             JAVA_ENABLED = False
         elif opt == '--githash':
@@ -139,7 +139,7 @@ def mk_build_dir(path, x64):
             opts.append('--python')
         if subprocess.call(opts) != 0:
             raise MKException("Failed to generate build directory at '%s'" % path)
-    
+
 # Create build directories
 def mk_build_dirs():
     mk_build_dir(BUILD_X86_DIR, False)
@@ -176,7 +176,7 @@ def mk_z3(x64):
     cmds = []
     if x64:
         cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" amd64')
-        cmds.append('cd %s' % BUILD_X64_DIR)    
+        cmds.append('cd %s' % BUILD_X64_DIR)
     else:
         cmds.append('call "%VCINSTALLDIR%vcvarsall.bat" x86')
         cmds.append('cd %s' % BUILD_X86_DIR)
@@ -248,12 +248,12 @@ def mk_zips():
 VS_RUNTIME_PATS = [re.compile('vcomp.*\.dll'),
                    re.compile('msvcp.*\.dll'),
                    re.compile('msvcr.*\.dll')]
-                              
+
 # Copy Visual Studio Runtime libraries
-def cp_vs_runtime(x64):    
+def cp_vs_runtime(x64):
     if x64:
         platform = "x64"
-        
+
     else:
         platform = "x86"
     vcdir = os.environ['VCINSTALLDIR']
@@ -261,7 +261,7 @@ def cp_vs_runtime(x64):
     VS_RUNTIME_FILES = []
     for root, dirs, files in os.walk(path):
         for filename in files:
-            if fnmatch(filename, '*.dll'):            
+            if fnmatch(filename, '*.dll'):
                 for pat in VS_RUNTIME_PATS:
                     if pat.match(filename):
                         fname = os.path.join(root, filename)

scripts/update_api.py

@@ -710,6 +710,9 @@ def mk_java(java_dir, package_name):
                     java_wrapper.write('  }\n')
             elif k == OUT_MANAGED_ARRAY:
                 java_wrapper.write('  *(jlong**)a%s = (jlong*)_a%s;\n' % (i, i))
+
+            elif k == IN and param_type(param) == STRING:
+                java_wrapper.write('  jenv->ReleaseStringUTFChars(a%s, _a%s);\n' % (i, i));
             i = i + 1
         # return
         if result == STRING:

src/api/api_opt.cpp

@@ -218,6 +218,34 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    // get lower value or current approximation
+    Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_lower_as_vector(c, o, idx);
+        RESET_ERROR_CODE();
+        expr_ref_vector es(mk_c(c)->m());
+        to_optimize_ptr(o)->get_lower(idx, es);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        v->m_ast_vector.append(es.size(), (ast*const*)es.c_ptr());
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+
+    // get upper or current approximation
+    Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx) {
+        Z3_TRY;
+        LOG_Z3_optimize_get_upper_as_vector(c, o, idx);
+        RESET_ERROR_CODE();
+        expr_ref_vector es(mk_c(c)->m());
+        to_optimize_ptr(o)->get_upper(idx, es);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        v->m_ast_vector.append(es.size(), (ast*const*)es.c_ptr());
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+
     Z3_string Z3_API Z3_optimize_to_string(Z3_context c, Z3_optimize o) {
         Z3_TRY;
         LOG_Z3_optimize_to_string(c, o);

src/api/dotnet/Optimize.cs

@@ -144,6 +144,23 @@ namespace Microsoft.Z3
             {
                 get { return Lower; }
             }
+
+            /// <summary>
+            /// Retrieve a lower bound for the objective handle.
+            /// </summary>        	   	
+            public ArithExpr[] LowerAsVector
+            {
+                get { return opt.GetLowerAsVector(handle); }
+            }
+
+            /// <summary>
+            /// Retrieve an upper bound for the objective handle.
+            /// </summary>        	   	
+            public ArithExpr[] UpperAsVector
+            {
+                get { return opt.GetUpperAsVector(handle); }
+            }
+
         }
 
         /// <summary>
@@ -255,6 +272,25 @@ namespace Microsoft.Z3
             return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
         }
 
+        /// <summary>
+        /// Retrieve a lower bound for the objective handle.
+        /// </summary>        	
+        private ArithExpr[] GetLowerAsVector(uint index)
+        {
+            ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index));
+            return v.ToArithExprArray();
+        }
+
+
+        /// <summary>
+        /// Retrieve an upper bound for the objective handle.
+        /// </summary>        	
+        private ArithExpr[] GetUpperAsVector(uint index)
+        {
+            ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index));
+            return v.ToArithExprArray();
+        }
+
 	/// <summary>
 	/// Return a string the describes why the last to check returned unknown
 	/// </summary>	

src/api/java/Optimize.java

@@ -14,7 +14,6 @@ Author:
     Nikolaj Bjorner (nbjorner) 2015-07-16
 
 Notes:
-    
 **/
 
 package com.microsoft.z3;
@@ -23,10 +22,10 @@ import com.microsoft.z3.enumerations.Z3_lbool;
 
 
 /**
- * Object for managing optimizization context
+ * Object for managing optimization context
  **/
-public class Optimize extends Z3Object
+public class Optimize extends Z3Object {
-{
+
     /**
      * A string that describes all available optimize solver parameters.
      **/
@@ -55,7 +54,7 @@ public class Optimize extends Z3Object
 
     /**
      * Assert a constraint (or multiple) into the optimize solver.
-     **/        
+     **/
     public void Assert(BoolExpr ... constraints)
     {
         getContext().checkContextMatch(constraints);
@@ -67,80 +66,101 @@ public class Optimize extends Z3Object
 
     /**
      * Alias for Assert.
-     **/        
+     **/
     public void Add(BoolExpr ... constraints)
     {
-	Assert(constraints);
+        Assert(constraints);
     }
-    
+
     /**
      * Handle to objectives returned by objective functions.
      **/
-    public class Handle
+    public static class Handle {
-    {
-	Optimize opt;
-	int handle;
-	Handle(Optimize opt, int h)
-	{
-	    this.opt = opt;
-	    this.handle = h;
-	}
-	
-	/**
-	 * Retrieve a lower bound for the objective handle.
-	 **/        	   	
-	public ArithExpr getLower()
-	{
-	    return opt.GetLower(handle); 
-	}
-	
-	/**            
-	 * Retrieve an upper bound for the objective handle.
-	 **/        	   	
-	public ArithExpr getUpper()
-	{
-	    return opt.GetUpper(handle); 
-	}
-	
-	/**
-	 * Retrieve the value of an objective.
-	 **/        	   	
-	public ArithExpr getValue()
-	{
-	    return getLower(); 
-	}
 
-	/**
+        private final Optimize opt;
-	 * Print a string representation of the handle.
+        private final int handle;
-	 **/
+
-    @Override
+        Handle(Optimize opt, int h)
-    public String toString()
+        {
+            this.opt = opt;
+            this.handle = h;
+        }
+
+        /**
+         * Retrieve a lower bound for the objective handle.
+         **/
+        public ArithExpr getLower()
+        {
+            return opt.GetLower(handle);
+        }
+
+        /**
+         * Retrieve an upper bound for the objective handle.
+         **/
+        public ArithExpr getUpper()
+        {
+            return opt.GetUpper(handle);
+        }
+
+        /**
+         * @return a triple representing the upper bound of the objective handle.
+         *
+         * The triple contains values {@code inf, value, eps},
+         * where the objective value is unbounded iff {@code inf} is non-zero,
+         * and otherwise is represented by the expression {@code value + eps * EPSILON},
+         * where {@code EPSILON} is an arbitrarily small real number.
+         */
+        public ArithExpr[] getUpperAsVector()
+        {
+            return opt.GetUpperAsVector(handle);
+        }
+
+        /**
+         * @return a triple representing the upper bound of the objective handle.
+         *
+         * <p>See {@link #getUpperAsVector()} for triple semantics.
+         */
+        public ArithExpr[] getLowerAsVector()
+        {
+            return opt.GetLowerAsVector(handle);
+        }
+
+        /**
+         * Retrieve the value of an objective.
+         **/
+        public ArithExpr getValue()
+        {
+            return getLower();
+        }
+
+        /**
+         * Print a string representation of the handle.
+         **/
+        @Override
+        public String toString()
         {
             return getValue().toString();
         }
     }
 
-    /**        
+    /**
      * Assert soft constraint
      *
      * Return an objective which associates with the group of constraints.
      *
-     **/        
+     **/
-
     public Handle AssertSoft(BoolExpr constraint, int weight, String group)
     {
         getContext().checkContextMatch(constraint);
         Symbol s = getContext().mkSymbol(group);
         return new Handle(this, Native.optimizeAssertSoft(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), Integer.toString(weight), s.getNativeObject()));
     }
-    
 
-    /**        
+    /**
      * Check satisfiability of asserted constraints.
      * Produce a model that (when the objectives are bounded and 
      * don't use strict inequalities) meets the objectives.
      **/
-
     public Status Check()
     {
         Z3_lbool r = Z3_lbool.fromInt(Native.optimizeCheck(getContext().nCtx(), getNativeObject()));
@@ -153,7 +173,7 @@ public class Optimize extends Z3Object
                 return Status.UNKNOWN;
         }
     }
-    
+
     /**
      * Creates a backtracking point.
      **/
@@ -162,13 +182,11 @@ public class Optimize extends Z3Object
         Native.optimizePush(getContext().nCtx(), getNativeObject());
     }
 
-
+    /**
-    /** 
      * Backtrack one backtracking point.
      *
      * Note that an exception is thrown if Pop is called without a corresponding Push.
      **/
-     
     public void Pop()
     {
         Native.optimizePop(getContext().nCtx(), getNativeObject());
@@ -191,7 +209,7 @@ public class Optimize extends Z3Object
         }
     }
 
-    /** 
+    /**
      *  Declare an arithmetical maximization objective.
      *  Return a handle to the objective. The handle is used as
      *  to retrieve the values of objectives after calling Check.
@@ -200,11 +218,11 @@ public class Optimize extends Z3Object
     {
         return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
-    
+
     /**
      *  Declare an arithmetical minimization objective. 
      *  Similar to MkMaximize.
-     **/        	
+     **/
     public Handle MkMinimize(ArithExpr e)
     {
         return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
@@ -212,21 +230,56 @@ public class Optimize extends Z3Object
     
     /**
      *  Retrieve a lower bound for the objective handle.
-     **/        	
+     **/
     private ArithExpr GetLower(int index)
     {
         return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
     }
-    
+
-    
     /**
      *  Retrieve an upper bound for the objective handle.
-     **/        	
+     **/
     private ArithExpr GetUpper(int index)
     {
         return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
     }
 
+    /**
+     * @return Triple representing the upper bound for the objective handle.
+     *
+     * <p>See {@link Handle#getUpperAsVector}.
+     */
+    private ArithExpr[] GetUpperAsVector(int index) {
+        return unpackObjectiveValueVector(
+                Native.optimizeGetUpperAsVector(
+                        getContext().nCtx(), getNativeObject(), index
+                )
+        );
+    }
+
+    /**
+     * @return Triple representing the upper bound for the objective handle.
+     *
+     * <p>See {@link Handle#getLowerAsVector}.
+     */
+    private ArithExpr[] GetLowerAsVector(int index) {
+        return unpackObjectiveValueVector(
+                Native.optimizeGetLowerAsVector(
+                        getContext().nCtx(), getNativeObject(), index
+                )
+        );
+    }
+
+    private ArithExpr[] unpackObjectiveValueVector(long nativeVec) {
+        ASTVector vec = new ASTVector(
+                getContext(), nativeVec
+        );
+        return new ArithExpr[] {
+                (ArithExpr) vec.get(0), (ArithExpr) vec.get(1), (ArithExpr) vec.get(2)
+        };
+
+    }
+
     /**
      * Return a string the describes why the last to check returned unknown
      **/
@@ -235,8 +288,7 @@ public class Optimize extends Z3Object
         return Native.optimizeGetReasonUnknown(getContext().nCtx(),
                 getNativeObject());	
     }
-    
+
-    
     /**
      *  Print the context to a String (SMT-LIB parseable benchmark).
      **/
@@ -245,7 +297,7 @@ public class Optimize extends Z3Object
     {
         return Native.optimizeToString(getContext().nCtx(), getNativeObject());
     }
-    
+
     /**
      *  Optimize statistics.
      **/

src/api/python/z3/z3.py

@@ -6719,12 +6719,24 @@ class OptimizeObjective:
         opt = self._opt
         return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
 
+    def lower_values(self):
+        opt = self._opt
+        return AstVector(Z3_optimize_get_lower_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
+
+    def upper_values(self):
+        opt = self._opt
+        return AstVector(Z3_optimize_get_upper_as_vector(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
+
     def value(self):
         if self._is_max:
             return self.upper()
         else:
             return self.lower()
 
+    def __str__(self):
+        return "%s:%s" % (self._value, self._is_max)
+
+
 class Optimize(Z3PPObject):
     """Optimize API provides methods for solving using objective functions and weighted soft constraints"""
 
@@ -6829,6 +6841,16 @@ class Optimize(Z3PPObject):
             raise Z3Exception("Expecting objective handle returned by maximize/minimize")
         return obj.upper()
 
+    def lower_values(self, obj):
+        if not isinstance(obj, OptimizeObjective):
+            raise Z3Exception("Expecting objective handle returned by maximize/minimize")
+        return obj.lower_values()
+
+    def upper_values(self, obj):
+        if not isinstance(obj, OptimizeObjective):
+            raise Z3Exception("Expecting objective handle returned by maximize/minimize")
+        return obj.upper_values()
+
     def from_file(self, filename):
         """Parse assertions and objectives from a file"""
         Z3_optimize_from_file(self.ctx.ref(), self.optimize, filename)

src/api/z3_optimization.h

@@ -186,6 +186,33 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_optimize_get_upper(Z3_context c, Z3_optimize o, unsigned idx);
 
+
+    /**
+       \brief Retrieve lower bound value or approximation for the i'th optimization objective.
+              The returned vector is of length 3. It always contains numerals.
+              The three numerals are coefficients a, b, c and encode the result of \c Z3_optimize_get_lower
+              a * infinity + b + c * epsilon.
+              
+       \param c - context
+       \param o - optimization context
+       \param idx - index of optimization objective
+
+       def_API('Z3_optimize_get_lower_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
+    */
+    Z3_ast_vector Z3_API Z3_optimize_get_lower_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
+
+    /**
+       \brief Retrieve upper bound value or approximation for the i'th optimization objective.
+
+       \param c - context
+       \param o - optimization context
+       \param idx - index of optimization objective
+
+       def_API('Z3_optimize_get_upper_as_vector', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE), _in(UINT)))
+    */
+    Z3_ast_vector Z3_API Z3_optimize_get_upper_as_vector(Z3_context c, Z3_optimize o, unsigned idx);
+
+
     /**
        \brief Print the current context as a string.
        \param c - context.

src/ast/fpa_decl_plugin.cpp

@@ -836,7 +836,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range);
 
     case OP_FPA_INTERNAL_BVWRAP:
-        return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);    
+        return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range);
     case OP_FPA_INTERNAL_BV2RM:
         return mk_internal_bv2rm(k, num_parameters, parameters, arity, domain, range);
 
@@ -915,7 +915,7 @@ void fpa_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED));
 
     /* Extensions */
-	op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV));
+    op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV));
     op_names.push_back(builtin_name("fp.to_ieee_bv", OP_FPA_TO_IEEE_BV));
 }
 

src/ast/rewriter/enum2bv_rewriter.cpp

@@ -85,7 +85,7 @@ struct enum2bv_rewriter::imp {
 
         void throw_non_fd(expr* e) {
             std::stringstream strm;
-            strm << "unabled nested data-type expression " << mk_pp(e, m);
+            strm << "unable to handle nested data-type expression " << mk_pp(e, m);
             throw rewriter_exception(strm.str().c_str());
         }
 

src/ast/seq_decl_plugin.cpp

@@ -284,8 +284,54 @@ zstring zstring::operator+(zstring const& other) const {
     return result;
 }
 
-std::ostream& zstring::operator<<(std::ostream& out) const {
+bool zstring::operator==(const zstring& other) const {
-    return out << encode();
+    // two strings are equal iff they have the same length and characters
+    if (length() != other.length()) {
+        return false;
+    }
+    for (unsigned i = 0; i < length(); ++i) {
+        unsigned Xi = m_buffer[i];
+        unsigned Yi = other[i];
+        if (Xi != Yi) {
+            return false;
+        }
+    }
+
+    return true;
+}
+
+bool zstring::operator!=(const zstring& other) const {
+    return !(*this == other);
+}
+
+std::ostream& operator<<(std::ostream &os, const zstring &str) {
+    return os << str.encode();
+}
+
+bool operator<(const zstring& lhs, const zstring& rhs) {
+    // This has the same semantics as strcmp()
+    unsigned len = lhs.length();
+    if (rhs.length() < len) {
+        len = rhs.length();
+    }
+    for (unsigned i = 0; i < len; ++i) {
+        unsigned Li = lhs[i];
+        unsigned Ri = rhs[i];
+        if (Li < Ri) {
+            return true;
+        } else if (Li > Ri) {
+            return false;
+        } else {
+            continue;
+        }
+    }
+    // at this point, all compared characters are equal,
+    // so decide based on the relative lengths
+    if (lhs.length() < rhs.length()) {
+        return true;
+    } else {
+        return false;
+    }
 }
 
 
@@ -473,6 +519,7 @@ void seq_decl_plugin::init() {
     sort* str2TintT[3] = { strT, strT, intT };
     sort* seqAintT[2] = { seqA, intT };
     sort* seq3A[3] = { seqA, seqA, seqA };
+    sort* reTintT[2] = { reT, intT };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
     m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq.unit",     1, 1, &A, seqA);
@@ -516,6 +563,7 @@ void seq_decl_plugin::init() {
     m_sigs[_OP_REGEXP_EMPTY]      = alloc(psig, m, "re.nostr", 0, 0, 0, reT);
     m_sigs[_OP_REGEXP_FULL]       = alloc(psig, m, "re.allchar", 0, 0, 0, reT);
     m_sigs[_OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, strT);
+    m_sigs[_OP_RE_UNROLL]         = alloc(psig, m, "_re.unroll", 0, 2, reTintT, strT);
 }
 
 void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
@@ -672,6 +720,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
             m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters");
         }
         
+    case _OP_RE_UNROLL:
+        match(*m_sigs[k], arity, domain, range, rng);
+        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
 
     case OP_STRING_CONST:
         if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {

src/ast/seq_decl_plugin.h

@@ -79,6 +79,7 @@ enum seq_op_kind {
     _OP_REGEXP_EMPTY,
     _OP_REGEXP_FULL,
     _OP_SEQ_SKOLEM,
+    _OP_RE_UNROLL,
     LAST_SEQ_OP
 };
 
@@ -113,7 +114,11 @@ public:
     int  indexof(zstring const& other, int offset) const;
     zstring extract(int lo, int hi) const;
     zstring operator+(zstring const& other) const;
-    std::ostream& operator<<(std::ostream& out) const;
+    bool operator==(const zstring& other) const;
+    bool operator!=(const zstring& other) const;
+
+    friend std::ostream& operator<<(std::ostream &os, const zstring &str);
+    friend bool operator<(const zstring& lhs, const zstring& rhs);
 };
 
 class seq_decl_plugin : public decl_plugin {
@@ -334,6 +339,7 @@ public:
         MATCH_UNARY(is_opt);
         bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi);
         bool is_loop(expr const* n, expr*& body, unsigned& lo);
+        bool is_unroll(expr const* n) const { return is_app_of(n, m_fid, _OP_RE_UNROLL); }
     };
     str str;
     re  re;

src/cmd_context/tactic_cmds.cpp

@@ -223,7 +223,7 @@ public:
                 cmd_context::scoped_watch sw(ctx);
                 lbool r = l_undef;
                 try {
-                    r = check_sat(t, g, md, result->labels, pr, core, reason_unknown);
+                    r = check_sat(t, g, md, result->labels, pr, core, reason_unknown);                    
                     ctx.display_sat_result(r);
                     result->set_status(r);
                     if (r == l_undef) {

src/model/model_evaluator.cpp

@@ -50,6 +50,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
     unsigned                        m_max_steps;
     bool                            m_model_completion;
     bool                            m_cache;
+    bool                            m_array_equalities;
 
     evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p):
         m_model(md),
@@ -81,6 +82,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         m_max_steps        = p.max_steps();
         m_model_completion = p.completion();
         m_cache            = p.cache();
+        m_array_equalities = p.array_equalities();
     }
 
     ast_manager & m() const { return m_model.get_manager(); }
@@ -264,11 +266,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
 
 
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
-        return BR_FAILED;
         if (a == b) {
             result = m().mk_true();
             return BR_DONE;
         }
+        if (!m_array_equalities) {
+            return BR_FAILED;
+        }
+
         // disabled until made more efficient
         vector<expr_ref_vector> stores1, stores2;
         bool args_are_unique1, args_are_unique2;
@@ -508,6 +513,10 @@ void model_evaluator::set_model_completion(bool f) {
     m_imp->cfg().m_model_completion = f;
 }
 
+void model_evaluator::set_expand_array_equalities(bool f) {
+    m_imp->cfg().m_array_equalities = f;
+}
+
 unsigned model_evaluator::get_num_steps() const {
     return m_imp->get_num_steps();
 }

src/model/model_evaluator.h

@@ -35,6 +35,7 @@ public:
 
     ast_manager & m () const;
     void set_model_completion(bool f);
+    void set_expand_array_equalities(bool f);
 
     void updt_params(params_ref const & p);
     static void get_param_descrs(param_descrs & r);

src/model/model_evaluator_params.pyg

@@ -3,6 +3,7 @@ def_module_params('model_evaluator',
                   params=(max_memory_param(),
                           max_steps_param(),
                           ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'),
-                          ('cache', BOOL, True, 'cache intermediate results in the model evaluator')
+                          ('cache', BOOL, True, 'cache intermediate results in the model evaluator'),
+                          ('array_equalities', BOOL, True, 'evaluate array equalities')
                           ))
 

src/opt/opt_context.cpp

@@ -1002,7 +1002,8 @@ namespace opt {
             TRACE("opt", tout << "Term does not evaluate " << term << "\n";);
             return false;
         }
-        if (!m_arith.is_numeral(val, r)) {
+        unsigned bvsz;
+        if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) {
             TRACE("opt", tout << "model does not evaluate objective to a value\n";);
             return false;
         }
@@ -1290,6 +1291,15 @@ namespace opt {
         return to_expr(get_upper_as_num(idx));
     }
 
+    void context::to_exprs(inf_eps const& n, expr_ref_vector& es) {
+        rational inf = n.get_infinity();
+        rational r   = n.get_rational();
+        rational eps = n.get_infinitesimal();
+        es.push_back(m_arith.mk_numeral(inf, inf.is_int()));
+        es.push_back(m_arith.mk_numeral(r, r.is_int()));
+        es.push_back(m_arith.mk_numeral(eps, eps.is_int()));
+    }
+
     expr_ref context::to_expr(inf_eps const& n) {
         rational inf = n.get_infinity();
         rational r   = n.get_rational();
@@ -1455,9 +1465,10 @@ namespace opt {
 
     void context::validate_maxsat(symbol const& id) {
         maxsmt& ms = *m_maxsmts.find(id);
+        TRACE("opt", tout << "Validate: " << id << "\n";);
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];
-            if (obj.m_id == id) {
+            if (obj.m_id == id && obj.m_type == O_MAXSMT) {        
                 SASSERT(obj.m_type == O_MAXSMT);
                 rational value(0);
                 expr_ref val(m);

src/opt/opt_context.h

@@ -207,6 +207,9 @@ namespace opt {
         expr_ref get_lower(unsigned idx);
         expr_ref get_upper(unsigned idx);
 
+        void get_lower(unsigned idx, expr_ref_vector& es) { to_exprs(get_lower_as_num(idx), es); }
+        void get_upper(unsigned idx, expr_ref_vector& es) { to_exprs(get_upper_as_num(idx), es); }
+
         std::string to_string() const;
 
 
@@ -238,6 +241,7 @@ namespace opt {
         lbool adjust_unknown(lbool r);
         bool scoped_lex();
         expr_ref to_expr(inf_eps const& n);
+        void to_exprs(inf_eps const& n, expr_ref_vector& es);
 
         void reset_maxsmts();
         void import_scoped_state();

src/smt/proto_model/proto_model.cpp

@@ -93,6 +93,7 @@ bool proto_model::is_select_of_model_value(expr* e) const {
 
 bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
     m_eval.set_model_completion(model_completion);
+    m_eval.set_expand_array_equalities(false);
     try {
         m_eval(e, result);
 #if 0

src/smt/smt_model_checker.cpp

@@ -290,7 +290,7 @@ namespace smt {
 
         while (true) {
             lbool r = m_aux_context->check();
-            TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
+            TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);                
             if (r != l_true)
                 break; 
             model_ref cex;
@@ -300,7 +300,7 @@ namespace smt {
             }
             num_new_instances++;
             if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
-                TRACE("model_checker", tout << "Add blocking clause failed\n";);
+                TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";);
                 // add_blocking_clause failed... stop the search for new counter-examples...
                 break; 
             }
@@ -407,6 +407,7 @@ namespace smt {
                 found_relevant = true;
                 if (m.is_rec_fun_def(q)) {
                     if (!check_rec_fun(q)) {
+                        TRACE("model_checker", tout << "checking recursive function failed\n";);
                         num_failures++;
                     }
                 }
@@ -414,6 +415,7 @@ namespace smt {
                     if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) {
                         verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n";
                     }
+                    TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";);
                     num_failures++;
                 }
             }
@@ -452,6 +454,7 @@ namespace smt {
     }
 
     bool model_checker::has_new_instances() {
+        TRACE("model_checker", tout << "instances: " << m_new_instances.size() << "\n";);
         return !m_new_instances.empty();
     }
 

src/smt/tactic/smt_tactic.cpp

@@ -25,6 +25,9 @@ Notes:
 #include"filter_model_converter.h"
 #include"ast_util.h"
 #include"solver2tactic.h"
+#include"smt_solver.h"
+#include"solver.h"
+#include"mus.h"
 
 typedef obj_map<expr, expr *> expr2expr_map;
 
@@ -159,6 +162,8 @@ public:
             ref<filter_model_converter> fmc;
             if (in->unsat_core_enabled()) {
                 extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc);
+                TRACE("mus", in->display_with_dependencies(tout);
+                      tout << clauses << "\n";);
                 if (in->proofs_enabled() && !assumptions.empty())
                     throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores");
                 for (unsigned i = 0; i < clauses.size(); ++i) {

src/solver/mus.cpp

@@ -89,6 +89,7 @@ struct mus::imp {
     lbool get_mus1(expr_ref_vector& mus) {
         ptr_vector<expr> unknown(m_lit2expr.size(), m_lit2expr.c_ptr());
         ptr_vector<expr> core_exprs;
+        TRACE("mus", m_solver.display(tout););
         while (!unknown.empty()) { 
             IF_VERBOSE(12, verbose_stream() << "(mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";);
             TRACE("mus", display_vec(tout << "core:  ", unknown); display_vec(tout << "mus:   ", mus););

src/solver/tactic2solver.cpp

@@ -290,3 +290,5 @@ solver_factory * mk_tactic2solver_factory(tactic * t) {
 solver_factory * mk_tactic_factory2solver_factory(tactic_factory * f) {
     return alloc(tactic_factory2solver_factory, f);
 }
+
+

src/tactic/bv/dt2bv_tactic.cpp

@@ -64,7 +64,10 @@ class dt2bv_tactic : public tactic {
                 return;
             }
 
-            if (m_t.is_fd(a)) {
+            if (m_t.is_fd(a) && a->get_num_args() > 0) {
+                m_t.m_non_fd_sorts.insert(get_sort(a));
+            }
+            else if (m_t.is_fd(a)) {
                 m_t.m_fd_sorts.insert(get_sort(a));
             }
             else {

src/tactic/extension_model_converter.cpp

@@ -49,6 +49,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
     TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
     model_evaluator ev(*(md.get()));
     ev.set_model_completion(true);
+    ev.set_expand_array_equalities(false);
     expr_ref val(m());
     unsigned i = m_vars.size();
     while (i > 0) {

src/tactic/smtlogics/quant_tactics.cpp

@@ -28,6 +28,7 @@ Revision History:
 #include"ctx_simplify_tactic.h"
 #include"smt_tactic.h"
 #include"elim_term_ite_tactic.h"
+#include"probe_arith.h"
 
 static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = false) {
     params_ref pull_ite_p;
@@ -107,8 +108,10 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = and_then(mk_quant_preprocessor(m),
                            mk_qe_lite_tactic(m, p),
                            cond(mk_has_quantifier_probe(), 
-                                or_else(mk_qsat_tactic(m, p),
+                                cond(mk_is_lira_probe(),
-                                        and_then(mk_qe_tactic(m), mk_smt_tactic())),
+                                     or_else(mk_qsat_tactic(m, p),
+                                             and_then(mk_qe_tactic(m), mk_smt_tactic())),
+                                     mk_smt_tactic()),
                                 mk_smt_tactic()));
     st->updt_params(p);
     return st;

src/tactic/tactic.cpp

@@ -23,7 +23,6 @@ Notes:
 #include"model_v2_pp.h"
 
 
-
 struct tactic_report::imp {
     char const *    m_id;
     goal const &    m_goal;
@@ -175,6 +174,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve
     }
 }
 
+
 lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
     bool models_enabled = g->models_enabled();
     bool proofs_enabled = g->proofs_enabled();