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

doc/mk_api_doc.py

@@ -188,7 +188,7 @@ try:
 
     if Z3PY_ENABLED:
         print("Z3Py documentation enabled")
-        doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3.py'
+        doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3*.py'
     else:
         print("Z3Py documentation disabled")
         doxygen_config_substitutions['PYTHON_API_FILES'] = ''
@@ -288,8 +288,21 @@ try:
         # Put z3py at the beginning of the search path to try to avoid picking up
         # an installed copy of Z3py.
         sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH))
-        pydoc.writedoc('z3')
-        shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html'))
+        for modulename in (
+                'z3',
+                'z3.z3consts',
+                'z3.z3core',
+                'z3.z3num',
+                'z3.z3poly',
+                'z3.z3printer',
+                'z3.z3rcf',
+                'z3.z3types',
+                'z3.z3util',
+                ):
+            pydoc.writedoc(modulename)
+            doc = modulename + '.html'
+            shutil.move(doc, os.path.join(OUTPUT_DIRECTORY, 'html', doc))
+
         print("Generated pydoc Z3Py documentation.")
 
     if ML_ENABLED:

scripts/mk_util.py

@@ -1913,7 +1913,11 @@ class MLComponent(Component):
             src_dir = self.to_src_dir
             mk_dir(os.path.join(BUILD_DIR, self.sub_dir))
             api_src = get_component(API_COMPONENT).to_src_dir
-            out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n') # remove /GL; the ocaml tools don't like it.
+            # remove /GL and -std=c++11; the ocaml tools don't like them.
+            if IS_WINDOWS:                
+                out.write('CXXFLAGS_OCAML=$(CXXFLAGS:/GL=)\n')
+            else:
+                out.write('CXXFLAGS_OCAML=$(subst -std=c++11,,$(CXXFLAGS))\n')
 
             if IS_WINDOWS:
                 prefix_lib = '-L' + os.path.abspath(BUILD_DIR).replace('\\', '\\\\')

src/interp/iz3mgr.cpp

@@ -33,9 +33,11 @@
 #include <fstream>
 #include <iostream>
 #include <ostream>
+#include <sstream>
 
 #include "ast/expr_abstract.h"
 #include "util/params.h"
+#include "ast/used_vars.h"
 
 
 using namespace stl_ext;
@@ -938,3 +940,30 @@ void iz3mgr::get_bound_substitutes(stl_ext::hash_map<ast,bool> &memo, const ast
  
     }
 #endif
+
+unsigned  iz3mgr::num_free_variables(const ast &e){
+    used_vars uv;
+    uv(to_expr(e.raw()));
+    return uv.get_num_vars();
+}
+
+iz3mgr::ast iz3mgr::close_universally (ast e){
+   used_vars uv;
+   uv(to_expr(e.raw()));
+   std::vector<ast> bvs;
+   stl_ext::hash_map<ast,ast> subst_memo;
+   for (unsigned i = 0; i < uv.get_max_found_var_idx_plus_1(); i++){
+       if (uv.get(i)) {
+           std::ostringstream os;
+           os << "%%" << i;
+           ast c = make_var(os.str(),uv.get(i));
+           ast v = cook(m().mk_var(i,uv.get(i)));
+           subst_memo[v] = c;
+           bvs.push_back(c);
+       }
+   }
+   e = subst(subst_memo,e);
+   for (unsigned i = 0; i < bvs.size(); i++)
+       e = apply_quant(Forall,bvs[i],e);
+   return e;
+}

src/interp/iz3mgr.h

@@ -661,6 +661,12 @@ class iz3mgr  {
 
     ast apply_quant(opr quantifier, ast var, ast e);
 
+    // Universally quantify all the free variables in a formula.
+    // Makes up names for the quntifiers.
+
+    ast close_universally (ast e);
+
+    unsigned num_free_variables(const ast &e);
 
     /** For debugging */
     void show(ast);

src/interp/iz3proof_itp.cpp

@@ -2968,9 +2968,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast interpolate(const node &pf){
         // proof of false must be a formula, with quantified symbols
 #ifndef BOGUS_QUANTS
-        return add_quants(z3_simplify(pf));
+        return close_universally(add_quants(z3_simplify(pf)));
 #else
-        return z3_simplify(pf);
+        return close_universally(z3_simplify(pf));
 #endif
     }
 

src/interp/iz3translate.cpp

@@ -234,6 +234,11 @@ public:
                 }
             }
 
+            // if(!range_is_empty(rng)){
+            //     if (num_free_variables(con) > 0)
+            //         rng = range_empty();
+            // }
+
             if(res == INT_MAX){
                 if(range_is_empty(rng))
                     res = -1;