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

Author: NikolajBjorner

CMakeLists.txt

@@ -34,7 +34,7 @@ endif()
 ################################################################################
 set(Z3_VERSION_MAJOR 4)
 set(Z3_VERSION_MINOR 8)
-set(Z3_VERSION_PATCH 0)
+set(Z3_VERSION_PATCH 2)
 set(Z3_VERSION_TWEAK 0)
 set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
 set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
@@ -99,7 +99,7 @@ set(GIT_DIR "${CMAKE_SOURCE_DIR}/.git")
 if (EXISTS "${GIT_DIR}")
   # Try to make CMake configure depend on the current git HEAD so that
   # a re-configure is triggered when the HEAD changes.
-  add_git_dir_dependency("${GIT_DIR}" ADD_GIT_DEP_SUCCESS)
+  add_git_dir_dependency("${CMAKE_SOURCE_DIR}" ADD_GIT_DEP_SUCCESS)
   if (ADD_GIT_DEP_SUCCESS)
     if (INCLUDE_GIT_HASH)
       get_git_head_hash("${GIT_DIR}" Z3GITHASH)

README.md

@@ -5,8 +5,11 @@ under the [MIT license](LICENSE.txt).
 
 If you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background).
 
+Pre-built binaries for releases are available from [here](https://github.com/Z3Prover/z3/releases), 
+and nightly builds from [here](https://github.com/Z3Prover/bin/tree/master/nightly).
+
 Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides
-[bindings for several programming languages][4].
+[bindings for several programming languages][4]. 
 
 See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3.
 

cmake/msvc_legacy_quirks.cmake

@@ -8,13 +8,13 @@
 # FIXME: All the commented out defines should be removed once
 # we are confident it is correct to not set them.
 set(Z3_MSVC_LEGACY_DEFINES
-  # Don't set `_DEBUG`. The old build sytem sets this but this
+  # Don't set `_DEBUG`. The old build system sets this but this
   # is wrong. MSVC will set this depending on which runtime is being used.
   # See https://msdn.microsoft.com/en-us/library/b0084kay.aspx
   # _DEBUG
 
   # The old build system only set `UNICODE` and `_UNICODE` for x86_64 release.
-  # That seems completly wrong so set it for all configurations.
+  # That seems completely wrong so set it for all configurations.
   # According to https://blogs.msdn.microsoft.com/oldnewthing/20040212-00/?p=40643/
   # `UNICODE` affects Windows headers and `_UNICODE` affects C runtime header files.
   # There is some discussion of this define at https://msdn.microsoft.com/en-us/library/dybsewaf.aspx
@@ -116,7 +116,7 @@ z3_add_cxx_flag("/analyze-" REQUIRED)
 ################################################################################
 
 # By default CMake enables incremental linking for Debug and RelWithDebInfo
-# builds. The old build sytem disables it for all builds so try to do the same
+# builds. The old build system disables it for all builds so try to do the same
 # by changing all configurations if necessary
 string(TOUPPER "${available_build_types}" _build_types_as_upper)
 foreach (_build_type ${_build_types_as_upper})

cmake/z3_add_component.cmake

@@ -7,7 +7,7 @@ function(z3_expand_dependencies output_var)
   if (ARGC LESS 2)
     message(FATAL_ERROR "Invalid number of arguments")
   endif()
-  # Remaing args should be component names
+  # Remaining args should be component names
   set(_expanded_deps ${ARGN})
   set(_old_number_of_deps 0)
   list(LENGTH _expanded_deps _number_of_deps)
@@ -33,7 +33,7 @@ function(z3_add_component_dependencies_to_target target_name)
   if (NOT (TARGET ${target_name}))
     message(FATAL_ERROR "Target \"${target_name}\" does not exist")
   endif()
-  # Remaing args should be component names
+  # Remaining args should be component names
   set(_expanded_deps ${ARGN})
   foreach (dependency ${_expanded_deps})
     # Ensure this component's dependencies are built before this component.
@@ -219,7 +219,7 @@ macro(z3_add_component component_name)
   # Record this component's dependencies
   foreach (dependency ${Z3_MOD_COMPONENT_DEPENDENCIES})
     if (NOT (TARGET ${dependency}))
-      message(FATAL_ERROR "Component \"${component_name}\" depends on a non existant component \"${dependency}\"")
+      message(FATAL_ERROR "Component \"${component_name}\" depends on a non existent component \"${dependency}\"")
     endif()
     set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_DEPS "${dependency}")
   endforeach()

contrib/ci/README.md

@@ -1,4 +1,4 @@
-# Continous integration scripts
+# Continuous integration scripts
 
 ## TravisCI
 
@@ -45,7 +45,7 @@ the future.
 * `Z3_VERBOSE_BUILD_OUTPUT` - Show compile commands in CMake builds (`0` or `1`)
 * `Z3_STATIC_BUILD` - Build Z3 binaries and libraries statically (`0` or `1`)
 * `Z3_SYSTEM_TEST_GIT_REVISION` - Git revision of [z3test](https://github.com/Z3Prover/z3test). If empty lastest revision will be used.
-* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option pased to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`)
+* `Z3_WARNINGS_AS_ERRORS` - Set the `WARNINGS_AS_ERRORS` CMake option passed to Z3 (`OFF`, `ON`, or `SERIOUS_ONLY`)
 
 ### Linux
 

doc/z3api.cfg.in

@@ -944,7 +944,7 @@ HTML_STYLESHEET        =
 # user-defined cascading style sheet that is included after the standard
 # style sheets created by doxygen. Using this option one can overrule
 # certain style aspects. This is preferred over using HTML_STYLESHEET
-# since it does not replace the standard style sheet and is therefor more
+# since it does not replace the standard style sheet and is therefore more
 # robust against future updates. Doxygen will copy the style sheet file to
 # the output directory.
 
@@ -1711,7 +1711,7 @@ UML_LOOK               = NO
 # the class node. If there are many fields or methods and many nodes the
 # graph may become too big to be useful. The UML_LIMIT_NUM_FIELDS
 # threshold limits the number of items for each type to make the size more
-# managable. Set this to 0 for no limit. Note that the threshold may be
+# manageable. Set this to 0 for no limit. Note that the threshold may be
 # exceeded by 50% before the limit is enforced.
 
 UML_LIMIT_NUM_FIELDS   = 10

examples/c++/CMakeLists.txt

@@ -7,8 +7,8 @@ find_package(Z3
   REQUIRED
   CONFIG
   # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
-  # This should prevent us from accidently picking up an installed
-  # copy of Z3. This is here to benefit Z3's build sytem when building
+  # This should prevent us from accidentally picking up an installed
+  # copy of Z3. This is here to benefit Z3's build system when building
   # this project. When making your own project you probably shouldn't
   # use this option.
   NO_DEFAULT_PATH

examples/c++/example.cpp

@@ -835,6 +835,17 @@ void tst_visit() {
     visit(f);
 }
 
+void tst_numeral() {
+    context c;
+    expr x = c.real_val("1/3");
+    double d = 0;
+    if (!x.is_numeral(d)) {
+        std::cout << x << " is not recognized as a numeral\n";
+        return;
+    }
+    std::cout << x << " is " << d << "\n";
+}
+
 void incremental_example1() {
     std::cout << "incremental example1\n";
     context c;
@@ -1212,6 +1223,7 @@ int main() {
         tactic_example9(); std::cout << "\n";
         tactic_qe(); std::cout << "\n";
         tst_visit(); std::cout << "\n";
+        tst_numeral(); std::cout << "\n";
         incremental_example1(); std::cout << "\n";
         incremental_example2(); std::cout << "\n";
         incremental_example3(); std::cout << "\n";

examples/c/CMakeLists.txt

@@ -24,8 +24,8 @@ find_package(Z3
   REQUIRED
   CONFIG
   # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
-  # This should prevent us from accidently picking up an installed
-  # copy of Z3. This is here to benefit Z3's build sytem when building
+  # This should prevent us from accidentally picking up an installed
+  # copy of Z3. This is here to benefit Z3's build system when building
   # this project. When making your own project you probably shouldn't
   # use this option.
   NO_DEFAULT_PATH

examples/dotnet/Program.cs

@@ -363,10 +363,10 @@ static void ArrayExample1(Context ctx)
 
             Console.WriteLine("Model = " + s.Model);
 
-            Console.WriteLine("Interpretation of MyArray:\n" + s.Model.FuncInterp(aex.FuncDecl));
+            //Console.WriteLine("Interpretation of MyArray:\n" + s.Model.ConstInterp(aex.FuncDecl));
             Console.WriteLine("Interpretation of x:\n" + s.Model.ConstInterp(xc));
             Console.WriteLine("Interpretation of f:\n" + s.Model.FuncInterp(fd));
-            Console.WriteLine("Interpretation of MyArray as Term:\n" + s.Model.FuncInterp(aex.FuncDecl));
+            //Console.WriteLine("Interpretation of MyArray as Term:\n" + s.Model.ConstInterp(aex.FuncDecl));
         }
 
         /// <summary>

examples/maxsat/CMakeLists.txt

@@ -11,8 +11,8 @@ find_package(Z3
   REQUIRED
   CONFIG
   # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
-  # This should prevent us from accidently picking up an installed
-  # copy of Z3. This is here to benefit Z3's build sytem when building
+  # This should prevent us from accidentally picking up an installed
+  # copy of Z3. This is here to benefit Z3's build system when building
   # this project. When making your own project you probably shouldn't
   # use this option.
   NO_DEFAULT_PATH

examples/maxsat/maxsat.c

@@ -138,7 +138,7 @@ void assert_hard_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z
 
 /**
    \brief Assert soft constraints stored in the given array.
-   This funtion will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
+   This function will assert each soft-constraint C_i as (C_i or k_i) where k_i is a fresh boolean variable.
    It will also return an array containing these fresh variables.
 */
 Z3_ast * assert_soft_constraints(Z3_context ctx, Z3_solver s, unsigned num_cnstrs, Z3_ast * cnstrs) 
@@ -565,7 +565,7 @@ int fu_malik_maxsat(Z3_context ctx, Z3_solver s, unsigned num_hard_cnstrs, Z3_as
 
 /**
   \brief Finds the maximal number of assumptions that can be satisfied.
-  An assumption is any formula preceeded with the :assumption keyword.
+  An assumption is any formula preceded with the :assumption keyword.
   "Hard" constraints can be supported by using the :formula keyword.
   
   Input: file in SMT-LIB format, and MaxSAT algorithm to be used: 0 - Naive, 1 - Fu&Malik's algo.

examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs

@@ -226,7 +226,7 @@ internal void AssertArith(int vid, ArithExpr variable)
         }
 
         /// <summary>
-        /// Adds a MSF variable with the coresponding assertion to the Z3 variables.
+        /// Adds a MSF variable with the corresponding assertion to the Z3 variables.
         /// </summary>
         /// <param name="vid">The MSF id of the variable</param>
         internal void AddVariable(int vid)

examples/tptp/CMakeLists.txt

@@ -7,8 +7,8 @@ find_package(Z3
   REQUIRED
   CONFIG
   # `NO_DEFAULT_PATH` is set so that -DZ3_DIR has to be passed to find Z3.
-  # This should prevent us from accidently picking up an installed
-  # copy of Z3. This is here to benefit Z3's build sytem when building
+  # This should prevent us from accidentally picking up an installed
+  # copy of Z3. This is here to benefit Z3's build system when building
   # this project. When making your own project you probably shouldn't
   # use this option.
   NO_DEFAULT_PATH

examples/tptp/tptp5.cpp

@@ -233,7 +233,7 @@ class env {
 
     void check_arity(unsigned num_args, unsigned arity) {
         if (num_args != arity) {
-            throw failure_ex("arity missmatch");
+            throw failure_ex("arity mismatch");
         }
     }
 

noarch/repodata.json

@@ -9,7 +9,7 @@
 
 # Z3 Project definition
 def init_project_def():
-    set_version(4, 8, 0, 0)
+    set_version(4, 8, 2, 0)
     add_lib('util', [], includes2install = ['z3_version.h'])
     add_lib('polynomial', ['util'], 'math/polynomial')
     add_lib('sat', ['util'])

noarch/repodata.json.bz2

@@ -3276,7 +3276,7 @@ class MakeRuleCmd(object):
         needed commands used in Makefile rules
         Note that several of the method are meant for use during ``make
         install`` and ``make uninstall``.  These methods correctly use
-        ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferrable
+        ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferable
         to writing commands manually which can be error prone.
     """
     @classmethod

scripts/mk_project.py

@@ -220,7 +220,7 @@ lbool lackr::lazy() {
     lackr_model_constructor mc(m_m, m_info);
     push_abstraction();
     unsigned ackr_head = 0;
-    while (1) {
+    while (true) {
         m_st.m_it++;
         checkpoint();
         TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";);

scripts/mk_util.py

@@ -276,7 +276,7 @@ struct lackr_model_constructor::imp {
             SASSERT(a->get_num_args() == 0);
             func_decl * const fd = a->get_decl();
             expr * val = m_abstr_model->get_const_interp(fd);
-            if (val == nullptr) { // TODO: avoid model completetion?
+            if (val == nullptr) { // TODO: avoid model completion?
                 sort * s = fd->get_range();
                 val = m_abstr_model->get_some_value(s);
             }

src/ackermannization/lackr.cpp

@@ -219,7 +219,7 @@ namespace api {
         if (m_user_ref_count) {
             // Corner case bug: n may be in m_last_result, and this is the only reference to n.
             // When, we execute reset() it is deleted
-            // To avoid this bug, I bump the reference counter before reseting m_last_result
+            // To avoid this bug, I bump the reference counter before resetting m_last_result
             ast_ref node(n, m());
             m_last_result.reset();
             m_last_result.push_back(std::move(node));

src/ackermannization/lackr_model_constructor.cpp

@@ -210,7 +210,7 @@ extern "C" {
         if (!out) {
             return Z3_FALSE;
         }
-        // must start loggging here, since function uses Z3_get_sort_kind above
+        // must start logging here, since function uses Z3_get_sort_kind above
         LOG_Z3_get_finite_domain_sort_size(c, s, out);
         RESET_ERROR_CODE();  
         VERIFY(mk_c(c)->datalog_util().try_get_size(to_sort(s), *out));