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

.travis.yml

@@ -65,4 +65,7 @@ env:
 #    - os: osx
 #      osx_image: xcode 8.2
 script:
-  - contrib/ci/scripts/travis_ci_entry_point.sh
+  # Use `travis_wait` to handle commands that don't show output for a long period of time.
+  # Currently this is the LTO build which can be very slow.
+  # Allow at most 45 minutes for the build.
+  - travis_wait 45 contrib/ci/scripts/travis_ci_entry_point.sh

src/api/api_qe.cpp

@@ -25,15 +25,24 @@ Notes:
 #include "api/api_model.h"
 #include "api/api_ast_map.h"
 #include "api/api_ast_vector.h"
-
 #include "qe/qe_vartest.h"
 #include "qe/qe_lite.h"
 #include "muz/spacer/spacer_util.h"
-
 #include "ast/expr_map.h"
 
 extern "C"
 {
+
+    static bool to_apps(unsigned n, Z3_app const es[], app_ref_vector& result) {
+        for (unsigned i = 0; i < n; ++i) {
+            if (!is_app(to_app(es[i]))) {
+                return false;
+            }
+            result.push_back (to_app (es [i]));
+        }
+        return true;
+    }
+
     Z3_ast Z3_API Z3_qe_model_project (Z3_context c,
                                        Z3_model m,
                                        unsigned num_bounds,
@@ -45,16 +54,10 @@ extern "C"
         RESET_ERROR_CODE();
       
         app_ref_vector vars(mk_c(c)->m ());
-    for (unsigned i = 0; i < num_bounds; ++i)
+        if (!to_apps(num_bounds, bound, vars)) {
-    {
-      app *a = to_app (bound [i]);
-      if (a->get_kind () != AST_APP)
-      {
             SET_ERROR_CODE (Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-      vars.push_back (a);
-    }
 
         expr_ref result (mk_c(c)->m ());
         result = to_expr (body);
@@ -79,16 +82,9 @@ extern "C"
 
         ast_manager& man = mk_c(c)->m ();
         app_ref_vector vars(man);
-      for (unsigned i = 0; i < num_bounds; ++i)
+        if (!to_apps(num_bounds, bound, vars)) {
-      {
-        app *a = to_app (bound [i]);
-        if (a->get_kind () != AST_APP)
-        {
-          SET_ERROR_CODE (Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        vars.push_back (a);
-      }
 
         expr_ref result (mk_c(c)->m ());
         result = to_expr (body);
@@ -145,11 +141,9 @@ extern "C"
         ast_ref_vector &vVars = to_ast_vector_ref (vars);
 
         app_ref_vector vApps (mk_c(c)->m());
-    for (unsigned i = 0; i < vVars.size (); ++i)
+        for (unsigned i = 0; i < vVars.size (); ++i) {
-    {
             app *a = to_app (vVars.get (i));
-      if (a->get_kind () != AST_APP)
+            if (a->get_kind () != AST_APP) {
-      {
                 SET_ERROR_CODE (Z3_INVALID_ARG);
                 RETURN_Z3(0);
             }
@@ -164,11 +158,11 @@ extern "C"
         qe (vApps, result);
 
         // -- copy back variables that were not eliminated
-    if (vApps.size () < vVars.size ())
+        if (vApps.size () < vVars.size ()) {
-    {
             vVars.reset ();
-      for (unsigned i = 0; i < vApps.size (); ++i)
+            for (app* v : vApps) {
-        vVars.push_back (vApps.get (i));
+                vVars.push_back (v);
+            }
         }
 
         mk_c(c)->save_ast_trail (result.get ());

src/ast/CMakeLists.txt

@@ -23,6 +23,7 @@ z3_add_component(ast
     expr_map.cpp
     expr_stat.cpp
     expr_substitution.cpp
+    factor_equivs.cpp
     for_each_ast.cpp
     for_each_expr.cpp
     format.cpp

src/ast/factor_equivs.cpp

@@ -0,0 +1,109 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    factor_equivs.cpp
+
+Abstract:
+  Factor equivalence classes out of an expression.
+
+  "Equivalence class structure" for objs. Uses a union_find structure internally.
+  Operations are :
+  -Declare a new equivalence class with a single element
+  -Merge two equivalence classes
+  -Retrieve whether two elements are in the same equivalence class
+  -Iterate on all the elements of the equivalence class of a given element
+  -Iterate on all equivalence classes (and then within them)
+
+Author:
+
+    Julien Braine
+    Arie Gurfinkel
+
+Revision History:
+
+*/
+
+#include "ast/factor_equivs.h"
+#include "ast/arith_decl_plugin.h"
+
+/**
+   Factors input vector v into equivalence classes and the rest
+ */
+void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
+    ast_manager &m = v.get_manager();
+    arith_util arith(m);
+    expr *e1 = 0, *e2 = 0;
+
+    flatten_and(v);
+    unsigned j = 0;
+    for (unsigned i = 0; i < v.size(); ++i) {
+        if (m.is_eq(v.get(i), e1, e2)) {
+            if (arith.is_zero(e1)) {
+                std::swap(e1, e2);
+            }
+
+            // y + -1*x == 0
+            expr* a0 = 0, *a1 = 0, *x = 0;
+            if (arith.is_zero(e2) && arith.is_add(e1, a0, a1)) {
+                if (arith.is_times_minus_one(a1, x)) {
+                    e1 = a0;
+                    e2 = x;
+                }
+                else if (arith.is_times_minus_one(a0, x)) {
+                    e1 = a1;
+                    e2 = x;
+                }
+            }
+            equiv.merge(e1, e2);
+        }
+        else {
+            if (j < i) { 
+                v[j] = v.get(i); 
+            }
+            j++;
+        }
+    }
+    v.shrink(j);
+}
+
+/**
+ * converts equivalence classes to equalities
+ */
+void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out) {
+    ast_manager &m = out.get_manager();
+    for (auto eq_class : equiv) {
+        expr *rep = nullptr;
+        for (expr *elem : eq_class) {
+            if (!m.is_value(elem)) {
+                rep = elem;
+                break;
+            }
+        }
+        SASSERT(rep);
+        for (expr *elem : eq_class) {
+            if (rep != elem) {
+                out.push_back (m.mk_eq (rep, elem));
+            }
+        }
+    }
+}
+
+/**
+ * expands equivalence classes to all derivable equalities
+ */
+bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) {
+    ast_manager &m = out.get_manager();
+    bool dirty = false;
+    for (auto eq_class : equiv) {
+        for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) {
+            expr_equiv_class::iterator b(a);
+            for (++b; b != end; ++b) {
+                out.push_back(m.mk_eq(*a, *b));
+                dirty = true;
+            }
+        }
+    }
+    return dirty;
+}

src/ast/factor_equivs.h

@@ -3,9 +3,11 @@ Copyright (c) 2017 Arie Gurfinkel
 
 Module Name:
 
-    obj_equiv_class.h
+    factor_equivs.h
 
 Abstract:
+  Factor equivalence classes out of an expression.
+
   "Equivalence class structure" for objs. Uses a union_find structure internally.
   Operations are :
   -Declare a new equivalence class with a single element
@@ -17,19 +19,19 @@ Abstract:
 Author:
 
     Julien Braine
+    Arie Gurfinkel
 
 Revision History:
 
 */
 
-#ifndef OBJ_EQUIV_CLASS_H_
+#ifndef FACTOR_EQUIVS_H_
-#define OBJ_EQUIV_CLASS_H_
+#define FACTOR_EQUIVS_H_
 
 #include "util/union_find.h"
 #include "ast/ast_util.h"
 
-namespace spacer {
+///All functions naturally add their parameters to the union_find class
-//All functions naturally add their parameters to the union_find class
 template<typename OBJ, typename Manager>
 class obj_equiv_class {
     basic_union_find m_uf;
@@ -164,87 +166,18 @@ typedef obj_equiv_class<expr, ast_manager> expr_equiv_class;
 
 
 /**
-   Factors input vector v into equivalence classes and the rest
+ *  Factors input vector v into equivalence classes and the rest
  */
-inline void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
+void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv);
-    ast_manager &m = v.get_manager();
-    arith_util arith(m);
-    expr *e1, *e2;
-
-    flatten_and(v);
-    unsigned j = 0;
-    for (unsigned i = 0; i < v.size(); ++i) {
-        if (m.is_eq(v.get(i), e1, e2)) {
-            if (arith.is_zero(e1)) {
-                expr* t;
-                t = e1; e1 = e2; e2 = t;
-            }
-
-            // y + -1*x == 0
-            if (arith.is_zero(e2) && arith.is_add(e1) &&
-                to_app(e1)->get_num_args() == 2) {
-                expr *a0, *a1, *x;
-
-                a0 = to_app(e1)->get_arg(0);
-                a1 = to_app(e1)->get_arg(1);
-
-                if (arith.is_times_minus_one(a1, x)) {
-                    e1 = a0;
-                    e2 = x;
-                }
-                else if (arith.is_times_minus_one(a0, x)) {
-                    e1 = a1;
-                    e2 = x;
-                }
-            }
-            equiv.merge(e1, e2);
-        }
-        else {
-            if (j < i) {v[j] = v.get(i);}
-            j++;
-        }
-    }
-    v.shrink(j);
-}
-
 /**
  * converts equivalence classes to equalities
  */
-inline void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out) {
+void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out);
-    ast_manager &m = out.get_manager();
-    for (auto eq_class : equiv) {
-        expr *rep = nullptr;
-        for (expr *elem : eq_class) {
-            if (!m.is_value (elem)) {
-                rep = elem;
-                break;
-            }
-        }
-        SASSERT(rep);
-        for (expr *elem : eq_class) {
-            if (rep != elem) {out.push_back (m.mk_eq (rep, elem));}
-        }
-    }
-}
 
 /**
  * expands equivalence classes to all derivable equalities
  */
-inline bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) {
+bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out);
-    ast_manager &m = out.get_manager();
-    bool dirty = false;
-    for (auto eq_class : equiv) {
-        for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) {
-            expr_equiv_class::iterator b(a);
-            for (++b; b != end; ++b) {
-                out.push_back(m.mk_eq(*a, *b));
-                dirty = true;
-            }
-        }
-    }
-    return dirty;
-}
 
-}
 
 #endif

src/muz/spacer/spacer_context.cpp

@@ -50,7 +50,6 @@ Notes:
 #include "util/luby.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_abstract.h"
-#include "muz/spacer/obj_equiv_class.h"
 
 namespace spacer {
 

src/muz/spacer/spacer_generalizers.cpp

@@ -24,7 +24,7 @@ Revision History:
 #include "ast/expr_abstract.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/for_each_expr.h"
-#include "muz/spacer/obj_equiv_class.h"
+#include "ast/factor_equivs.h"
 
 
 namespace spacer {

src/muz/spacer/spacer_legacy_frames.cpp

@@ -34,7 +34,7 @@
 #include "util/luby.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_abstract.h"
-#include "muz/spacer/obj_equiv_class.h"
+#include "ast/factor_equivs.h"
 
 
 namespace spacer {

src/muz/spacer/spacer_util.cpp

@@ -63,7 +63,7 @@ Notes:
 #include "tactic/arith/propagate_ineqs_tactic.h"
 #include "tactic/arith/arith_bounds_tactic.h"
 
-#include "muz/spacer/obj_equiv_class.h"
+#include "ast/factor_equivs.h"
 
 namespace spacer {
 

src/muz/transforms/dl_mk_array_eq_rewrite.cpp

@@ -22,11 +22,7 @@ Revision History:
 #include "muz/base/dl_context.h"
 #include "muz/base/fixedpoint_params.hpp"
 #include "muz/transforms/dl_mk_array_eq_rewrite.h"
-#include "../spacer/obj_equiv_class.h"
+#include "ast/factor_equivs.h"
-
-// NSB code review: avoid dependency on spacer inside this directory.
-// The python build system will rightfully complain if you include 
-// "muz/spacer/obj_equiv_class.h".
 
 namespace datalog {
 
@@ -65,7 +61,7 @@ namespace datalog {
             new_tail.push_back(r.get_tail(i));
         }
 
-        spacer::expr_equiv_class array_eq_classes(m);
+        expr_equiv_class array_eq_classes(m);
         for(unsigned i = nb_predicates; i < tail_size; i++) {
             expr* cond = r.get_tail(i);
             expr* e1, *e2;

src/muz/transforms/dl_mk_array_eq_rewrite.h

@@ -18,9 +18,7 @@ Revision History:
 #ifndef DL_MK_ARRAY_EQ_REWRITE_H_
 #define DL_MK_ARRAY_EQ_REWRITE_H_
 
-
 #include "muz/base/dl_rule_transformer.h"
-#include "../spacer/obj_equiv_class.h"
 
 namespace datalog {
 
@@ -51,4 +49,3 @@ namespace datalog {
 };
 
 #endif /* DL_MK_ARRAY_EQ_REWRITE_H_ */
-

src/muz/transforms/dl_mk_array_instantiation.cpp

@@ -24,7 +24,6 @@ Revision History:
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/expr_abstract.h"
 #include "muz/base/fixedpoint_params.hpp"
-#include "../spacer/obj_equiv_class.h"
 
 namespace datalog {
 
@@ -244,7 +243,7 @@ namespace datalog {
   expr_ref_vector mk_array_instantiation::retrieve_all_selects(expr*array)
   {
     expr_ref_vector all_selects(m);
-    for(spacer::expr_equiv_class::iterator it = eq_classes.begin(array);
+    for(expr_equiv_class::iterator it = eq_classes.begin(array);
         it != eq_classes.end(array); ++it)
     {
       selects.insert_if_not_there(*it, ptr_vector<expr>());

src/muz/transforms/dl_mk_array_instantiation.h

@@ -70,8 +70,8 @@ Revision History:
 #define DL_MK_ARRAY_INSTANTIATION_H_
 
 
+#include "ast/factor_equivs.h"
 #include "muz/base/dl_rule_transformer.h"
-#include "../spacer/obj_equiv_class.h"
 
 namespace datalog {
 
@@ -89,7 +89,7 @@ namespace datalog {
 
        //Rule context
        obj_map<expr, ptr_vector<expr> > selects;
-        spacer::expr_equiv_class eq_classes;
+       expr_equiv_class eq_classes;
        unsigned cnt;//Index for new variables
        obj_map<expr, var*> done_selects;
        expr_ref_vector ownership;

src/util/trail.h

@@ -22,6 +22,7 @@ Revision History:
 #include "util/obj_hashtable.h"
 #include "util/region.h"
 #include "util/obj_ref.h"
+#include "util/vector.h"
 
 template<typename Ctx>
 class trail {
@@ -357,4 +358,3 @@ public:
 };
 
 #endif /* TRAIL_H_ */
-