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

CMakeLists.txt

@@ -2,7 +2,7 @@
 cmake_minimum_required(VERSION 3.4)
 
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.8.13.0 LANGUAGES CXX)
+project(Z3 VERSION 4.8.14.0 LANGUAGES CXX)
 
 ################################################################################
 # Project version

RELEASE_NOTES

@@ -3,14 +3,18 @@ RELEASE NOTES
 Version 4.8.next
 ================
 - Planned features
-  - specialized solver support for QF_ABV and ABV based on lazy SMT and dual reduction
+  - sat.euf 
-    - the smtfd solver and tactic implement this strategy, but is not prime for users.
+    - a new CDCL core for SMT queries. It extends the SAT engine with theory solver plugins.
+      the current state is unstable. It lacks efficient ematching.
+  - polysat
+    - native word level bit-vector solving.
   - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
-  - circuit optimization techniques for BV in-processing are available as the sat.cut
-    option, but at this point does not translate into benefits. It is currently 
-    turned off by default.
 
 
+Version 4.8.13
+==============
+The release integrates various bug fixes and tuning.
+
 Version 4.8.12
 ==============
 Release provided to fix git tag discrepancy issues with 4.8.11  

examples/c/test_capi.c

@@ -561,7 +561,6 @@ void display_ast(Z3_context c, FILE * out, Z3_ast v)
     }
     case Z3_QUANTIFIER_AST: {
         fprintf(out, "quantifier");
-        ;
     }
     default:
         fprintf(out, "#unknown");

scripts/mk_project.py

@@ -8,7 +8,7 @@
 from mk_util import *
 
 def init_version():
-    set_version(4, 8, 13, 0)
+    set_version(4, 8, 14, 0)
     
 # Z3 Project definition
 def init_project_def():

scripts/release.yml

@@ -309,7 +309,7 @@ stages:
   jobs:
 
   - job: GitHubPublish
-    condition: eq(1,0)
+    condition: eq(0,1)
     displayName: "Publish to GitHub"
     pool:
       vmImage: "windows-latest"
@@ -387,7 +387,7 @@ stages:
 
   # Enable on release:
   - job: PyPIPublish
-    condition: eq(0,1)
+    condition: eq(1,1)
     displayName: "Publish to PyPI"
     pool:
       vmImage: "ubuntu-latest"
@@ -397,9 +397,9 @@ stages:
         artifact: 'PythonPackage'
         path: dist
     - task: DownloadSecureFile@1
-      name: pypirc
+      name: pypircs
       inputs:
-        secureFile: 'pypirc'
+        secureFile: 'pypircs'
     - script: python3 -m pip install --upgrade pip
     - script: python3 -m pip install --user -U setuptools importlib_metadata wheel twine 
-    - script: python3 -m twine upload --config-file $(pypirc.secureFilePath) -r $(pypiReleaseServer) dist/*
+    - script: python3 -m twine upload --config-file $(pypircs.secureFilePath) -r $(pypiReleaseServer) dist/*

src/api/api_ast.cpp

@@ -1232,6 +1232,7 @@ extern "C" {
 
         if (mk_c(c)->get_char_fid() == _d->get_family_id()) {
             switch (_d->get_decl_kind()) {
+            case OP_CHAR_CONST: return Z3_OP_CHAR_CONST;
             case OP_CHAR_LE: return Z3_OP_CHAR_LE;
             case OP_CHAR_TO_INT: return Z3_OP_CHAR_TO_INT;
             case OP_CHAR_TO_BV: return Z3_OP_CHAR_TO_BV;

src/api/python/z3/z3printer.py

@@ -770,6 +770,8 @@ class Formatter:
             return self.pp_set("Empty", a)
         elif k == Z3_OP_RE_FULL_SET:
             return self.pp_set("Full", a)
+        elif k == Z3_OP_CHAR_CONST:
+            return self.pp_char(a)
         return self.pp_name(a)
 
     def pp_int(self, a):
@@ -1060,6 +1062,10 @@ class Formatter:
     def pp_set(self, id, a):
         return seq1(id, [self.pp_sort(a.sort())])
 
+    def pp_char(self, a):
+        n = a.params()[0]
+        return to_format(str(n))
+
     def pp_pattern(self, a, d, xs):
         if a.num_args() == 1:
             return self.pp_expr(a.arg(0), d, xs)

src/api/z3_api.h

@@ -1222,6 +1222,7 @@ typedef enum {
     Z3_OP_RE_COMPLEMENT,
 
     // char
+    Z3_OP_CHAR_CONST,
     Z3_OP_CHAR_LE,
     Z3_OP_CHAR_TO_INT,
     Z3_OP_CHAR_TO_BV,

src/ast/ast.h

@@ -1050,6 +1050,12 @@ public:
     */
     virtual bool is_value(app * a) const { return false; }
 
+
+    /**
+       \brief return true if the expression can be used as a model value.
+     */
+    virtual bool is_model_value(app* a) const { return is_value(a); }
+
     /**
        \brief Return true if \c a is a unique plugin value.
        The following property should hold for unique theory values:

src/ast/seq_decl_plugin.cpp

@@ -705,6 +705,17 @@ bool seq_decl_plugin::is_value(app* e) const {
     }
 }
 
+bool seq_decl_plugin::is_model_value(app* e) const {
+    if (is_app_of(e, m_family_id, OP_SEQ_EMPTY)) 
+        return true;
+    if (is_app_of(e, m_family_id, OP_STRING_CONST)) 
+        return true;
+    if (is_app_of(e, m_family_id, OP_SEQ_UNIT) &&
+        m_manager->is_value(e->get_arg(0))) 
+        return true;
+    return false;
+}
+
 bool seq_decl_plugin::are_equal(app* a, app* b) const {
     if (a == b) return true;
     // handle concatenations

src/ast/seq_decl_plugin.h

@@ -179,6 +179,8 @@ public:
 
     bool is_value(app * e) const override;
 
+    bool is_model_value(app* e) const override;
+
     bool is_unique_value(app * e) const override;
 
     bool are_equal(app* a, app* b) const override;

src/smt/smt_model_generator.cpp

@@ -105,7 +105,7 @@ namespace smt {
                     else
                         proc = alloc(expr_wrapper_proc, m.mk_false());
                 }
-                else if (m.is_value(r->get_expr()))
+                else if (m.is_model_value(r->get_expr()))
                     proc = alloc(expr_wrapper_proc, r->get_expr());                    
                 else {
                     family_id fid = s->get_family_id();

src/smt/theory_lra.cpp

@@ -3477,7 +3477,7 @@ public:
                 st = lp::lp_status::FEASIBLE;
                 lp().restore_x();
             }
-            if (m_nla && st == lp::lp_status::OPTIMAL) {
+            if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
                 st = lp::lp_status::FEASIBLE;
                 lp().restore_x();
             }