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

src/api/c++/z3++.h

@@ -366,8 +366,14 @@ namespace z3 {
         void      recdef(func_decl, expr_vector const& args, expr const& body);
         func_decl user_propagate_function(symbol const& name, sort_vector const& domain, sort const& range);
 
+        /**
+           \brief create an uninterpreted constant.
+         */
         expr constant(symbol const & name, sort const & s);
         expr constant(char const * name, sort const & s);
+        /**
+           \brief create uninterpreted constants of a given sort.
+         */
         expr bool_const(char const * name);
         expr int_const(char const * name);
         expr real_const(char const * name);
@@ -378,6 +384,12 @@ namespace z3 {
         template<size_t precision>
         expr fpa_const(char const * name);
 
+        /**
+           \brief create a de-Bruijn variable.
+         */
+        expr variable(unsigned index, sort const& s);
+
+
         expr fpa_rounding_mode();
 
         expr bool_val(bool b);
@@ -1907,21 +1919,21 @@ namespace z3 {
     inline expr operator>(expr const & a, int b) { return a > a.ctx().num_val(b, a.get_sort()); }
     inline expr operator>(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) > b; }
 
-    inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr operator&(expr const & a, expr const & b) { if (a.is_bool()) return a && b; check_context(a, b); Z3_ast r = Z3_mk_bvand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
     inline expr operator&(expr const & a, int b) { return a & a.ctx().num_val(b, a.get_sort()); }
     inline expr operator&(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) & b; }
 
-    inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr operator^(expr const & a, expr const & b) { check_context(a, b); Z3_ast r = a.is_bool() ? Z3_mk_xor(a.ctx(), a, b) : Z3_mk_bvxor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
     inline expr operator^(expr const & a, int b) { return a ^ a.ctx().num_val(b, a.get_sort()); }
     inline expr operator^(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) ^ b; }
 
-    inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr operator|(expr const & a, expr const & b) { if (a.is_bool()) return a || b; check_context(a, b); Z3_ast r = Z3_mk_bvor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
     inline expr operator|(expr const & a, int b) { return a | a.ctx().num_val(b, a.get_sort()); }
     inline expr operator|(int a, expr const & b) { return b.ctx().num_val(a, b.get_sort()) | b; }
 
-    inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); return expr(a.ctx(), r); }
-    inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); return expr(a.ctx(), r); }
-    inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); return expr(a.ctx(), r); }
+    inline expr nand(expr const& a, expr const& b) { if (a.is_bool()) return !(a && b); check_context(a, b); Z3_ast r = Z3_mk_bvnand(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
+    inline expr nor(expr const& a, expr const& b) { if (a.is_bool()) return !(a || b); check_context(a, b); Z3_ast r = Z3_mk_bvnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
+    inline expr xnor(expr const& a, expr const& b) { if (a.is_bool()) return !(a ^ b); check_context(a, b); Z3_ast r = Z3_mk_bvxnor(a.ctx(), a, b); a.check_error(); return expr(a.ctx(), r); }
     inline expr min(expr const& a, expr const& b) { 
         check_context(a, b); 
         Z3_ast r;
@@ -1935,6 +1947,7 @@ namespace z3 {
             assert(a.is_fpa());
             r = Z3_mk_fpa_min(a.ctx(), a, b); 
         }
+        a.check_error();
         return expr(a.ctx(), r); 
     }
     inline expr max(expr const& a, expr const& b) { 
@@ -1950,6 +1963,7 @@ namespace z3 {
             assert(a.is_fpa());
             r = Z3_mk_fpa_max(a.ctx(), a, b); 
         }
+        a.check_error();
         return expr(a.ctx(), r); 
     }
     inline expr bvredor(expr const & a) {
@@ -3580,6 +3594,11 @@ namespace z3 {
         return expr(*this, r);
     }
     inline expr context::constant(char const * name, sort const & s) { return constant(str_symbol(name), s); }
+    inline expr context::variable(unsigned idx, sort const& s) { 
+        Z3_ast r = Z3_mk_bound(m_ctx, idx, s);
+        check_error();
+        return expr(*this, r);
+    }
     inline expr context::bool_const(char const * name) { return constant(name, bool_sort()); }
     inline expr context::int_const(char const * name) { return constant(name, int_sort()); }
     inline expr context::real_const(char const * name) { return constant(name, real_sort()); }

src/api/python/z3/z3.py

@@ -1469,7 +1469,9 @@ def FreshConst(sort, prefix="c"):
 
 def Var(idx, s):
     """Create a Z3 free variable. Free variables are used to create quantified formulas.
-
+    A free variable with index n is bound when it occurs within the scope of n+1 quantified
+    declarations.
+    
     >>> Var(0, IntSort())
     Var(0)
     >>> eq(Var(0, IntSort()), Var(0, BoolSort()))

src/api/z3_api.h

@@ -4051,7 +4051,10 @@ extern "C" {
     Z3_pattern Z3_API Z3_mk_pattern(Z3_context c, unsigned num_patterns, Z3_ast const terms[]);
 
     /**
-       \brief Create a bound variable.
+       \brief Create a variable. 
+
+       Variables are intended to be bound by a scope created by a quantifier. So we call them bound variables
+       even if they appear as free variables in the expression produced by \c Z3_mk_bound.
 
        Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain
        the meaning of de-Bruijn indices by indicating the compilation process from
@@ -5318,8 +5321,9 @@ extern "C" {
                                 Z3_ast const to[]);
 
     /**
-       \brief Substitute the free variables in \c a with the expressions in \c to.
+       \brief Substitute the variables in \c a with the expressions in \c to.
        For every \c i smaller than \c num_exprs, the variable with de-Bruijn index \c i is replaced with term \ccode{to[i]}.
+       Note that a variable is created using the function \ref Z3_mk_bound. 
 
        def_API('Z3_substitute_vars', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
     */

src/ast/simplifiers/elim_unconstrained.cpp

@@ -65,7 +65,6 @@ void elim_unconstrained::eliminate() {
         expr_ref r(m), side_cond(m);
         int v = m_heap.erase_min();
         node& n = get_node(v);
-        IF_VERBOSE(11, verbose_stream() << mk_bounded_pp(n.m_orig, m) << " @ " << n.m_refcount << "\n");
         if (n.m_refcount == 0)
             continue;
         if (n.m_refcount > 1)
@@ -203,10 +202,11 @@ void elim_unconstrained::freeze(expr* t) {
         return;
     node& n = get_node(t);
     if (!n.m_term)
-        return;
-    n.m_refcount = UINT_MAX / 2;
-    if (m_heap.contains(root(t)))
+        return;    
+    if (m_heap.contains(root(t))) {
+        n.m_refcount = UINT_MAX / 2;
         m_heap.increased(root(t));
+    }
 }
 
 void elim_unconstrained::gc(expr* t) {

src/muz/base/dl_rule.cpp

@@ -1013,39 +1013,42 @@ namespace datalog {
         }
     }
 
-    void rule::display(context & ctx, std::ostream & out) const {
+    void rule::display(context & ctx, std::ostream & out, bool compact) const {
         ast_manager & m = ctx.get_manager();
-        out << m_name.str () << ":\n";
+        if (!compact)
+            out << m_name.str () << ":\n";
         output_predicate(ctx, m_head, out);
         if (m_tail_size == 0) {
-            out << ".\n";
+            out << ".";
+            if (!compact)
+                out << "\n";
             return;
         }
         out << " :- ";
         for (unsigned i = 0; i < m_tail_size; i++) {
             if (i > 0)
                 out << ",";
-            out << "\n ";
+            if (!compact)
+                out << "\n";
+            out << " ";
             if (is_neg_tail(i))
                 out << "not ";
             app * t = get_tail(i);
-            if (ctx.is_predicate(t)) {
+            if (ctx.is_predicate(t)) 
                 output_predicate(ctx, t, out);
-            }
-            else {
+            else 
                 out << mk_pp(t, m);
-            }
         }
         out << '.';
         if (ctx.output_profile()) {
             out << " {";
             output_profile(out);
             out << '}';
         }
-        out << '\n';
-        if (m_proof) {
+        if (!compact)
+            out << '\n';
+        if (m_proof) 
             out << mk_pp(m_proof, m) << '\n';
-        }
     }
 
 

src/muz/base/dl_rule.h

@@ -365,7 +365,7 @@ namespace datalog {
 
         void get_vars(ast_manager& m, ptr_vector<sort>& sorts) const;
 
-        void display(context & ctx, std::ostream & out) const;
+        void display(context & ctx, std::ostream & out, bool compact = false) const;
 
         /**
            \brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules.

src/muz/base/dl_util.h

@@ -320,32 +320,31 @@ namespace datalog {
         unsigned_vector & res, bool & identity);
 
     template<class T>
-    void permutate_by_cycle(T & container, unsigned cycle_len, const unsigned * permutation_cycle) {
-        if (cycle_len<2) {
+    void permute_by_cycle(T& container, unsigned cycle_len, const unsigned * permutation_cycle) {
+        if (cycle_len < 2) 
             return;
-        }
         auto aux = container[permutation_cycle[0]];
-        for (unsigned i=1; i<cycle_len; i++) {
-            container[permutation_cycle[i-1]]=container[permutation_cycle[i]];
-        }
-        container[permutation_cycle[cycle_len-1]]=aux;
+        verbose_stream() << "xx " << cycle_len << "\n";
+        for (unsigned i = 1; i < cycle_len; i++) 
+            container[permutation_cycle[i-1]] = container[permutation_cycle[i]];
+        container[permutation_cycle[cycle_len-1]] = aux;
     }
-
     template<class T, class M>
-    void permutate_by_cycle(ref_vector<T,M> & container, unsigned cycle_len, const unsigned * permutation_cycle) {
+    void permute_by_cycle(ref_vector<T,M> & container, unsigned cycle_len, const unsigned * permutation_cycle) {
         if (cycle_len<2) {
             return;
         }
+        verbose_stream() << "ptr\n";
         T * aux = container.get(permutation_cycle[0]);
-        for (unsigned i=1; i<cycle_len; i++) {
+        for (unsigned i=1; i < cycle_len; i++) {
             container.set(permutation_cycle[i-1], container.get(permutation_cycle[i]));
         }
         container.set(permutation_cycle[cycle_len-1], aux);
     }
 
     template<class T>
-    void permutate_by_cycle(T & container, const unsigned_vector & permutation_cycle) {
-        permutate_by_cycle(container, permutation_cycle.size(), permutation_cycle.data());
+    void permute_by_cycle(T & container, const unsigned_vector & permutation_cycle) {
+        permute_by_cycle(container, permutation_cycle.size(), permutation_cycle.data());
     }
 
 

src/muz/rel/dl_base.h

@@ -160,7 +160,7 @@ namespace datalog {
                 SASSERT(cycle_len>=2);
                 result=src;
 
-                permutate_by_cycle(result, cycle_len, permutation_cycle);
+                permute_by_cycle(result, cycle_len, permutation_cycle);
             }
 
             /**

src/muz/rel/dl_finite_product_relation.cpp

@@ -674,7 +674,7 @@ namespace datalog {
             unsigned sig_sz = r.get_signature().size();
             unsigned_vector permutation;
             add_sequence(0, sig_sz, permutation);
-            permutate_by_cycle(permutation, cycle_len, permutation_cycle);
+            permute_by_cycle(permutation, cycle_len, permutation_cycle);
 
             unsigned_vector table_permutation;
 

src/muz/rel/dl_mk_explanations.cpp

@@ -70,20 +70,16 @@ namespace datalog {
             m_union_decl(mk_explanations::get_union_decl(get_context()), get_ast_manager()) {}
 
         ~explanation_relation_plugin() override {
-            for (unsigned i = 0; i < m_pool.size(); ++i) {
-                for (unsigned j = 0; j < m_pool[i].size(); ++j) {
+            for (unsigned i = 0; i < m_pool.size(); ++i) 
+                for (unsigned j = 0; j < m_pool[i].size(); ++j) 
                     dealloc(m_pool[i][j]);
-                }
-            }
         }
 
         bool can_handle_signature(const relation_signature & s) override {
             unsigned n=s.size();
-            for (unsigned i=0; i<n; i++) {
-                if (!get_context().get_decl_util().is_rule_sort(s[i])) {
+            for (unsigned i=0; i<n; i++) 
+                if (!get_context().get_decl_util().is_rule_sort(s[i])) 
                     return false;
-                }
-            }
             return true;
         }
 
@@ -105,9 +101,10 @@ namespace datalog {
         relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t,
             const relation_base & negated_obj, unsigned joined_col_cnt,
             const unsigned * t_cols, const unsigned * negated_cols) override;
-        relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & t,
-                const relation_base & src, unsigned joined_col_cnt,
-                const unsigned * t_cols, const unsigned * src_cols) override;
+        relation_intersection_filter_fn * mk_filter_by_intersection_fn(
+            const relation_base & t,
+            const relation_base & src, unsigned joined_col_cnt,
+            const unsigned * t_cols, const unsigned * src_cols) override;
 
     };
 
@@ -150,7 +147,7 @@ namespace datalog {
         void assign_data(const relation_fact & f) {
             m_empty = false;
 
-            unsigned n=get_signature().size();
+            unsigned n = get_signature().size();
             SASSERT(f.size()==n);
             m_data.reset();
             m_data.append(n, f.data());
@@ -161,11 +158,12 @@ namespace datalog {
             m_data.resize(get_signature().size());
         }
         void unite_with_data(const relation_fact & f) {
+
             if (empty()) {
                 assign_data(f);
                 return;
             }
-            unsigned n=get_signature().size();
+            unsigned n = get_signature().size();
             SASSERT(f.size()==n);
             for (unsigned i=0; i<n; i++) {
                 SASSERT(!is_undefined(i));
@@ -365,9 +363,9 @@ namespace datalog {
 
             explanation_relation * res = static_cast<explanation_relation *>(plugin.mk_empty(get_result_signature()));
             if (!r.empty()) {
-                relation_fact permutated_data = r.m_data;
-                permutate_by_cycle(permutated_data, m_cycle);
-                res->assign_data(permutated_data);
+                relation_fact permuted_data = r.m_data;
+                permute_by_cycle(dynamic_cast<app_ref_vector&>(permuted_data), m_cycle);
+                res->assign_data(permuted_data);
             }
             return res;
         }
@@ -704,7 +702,7 @@ namespace datalog {
     symbol mk_explanations::get_rule_symbol(rule * r) {
         if (r->name() == symbol::null) {
             std::stringstream sstm;
-            r->display(m_context, sstm);
+            r->display(m_context, sstm, true);
             std::string res = sstm.str();
             res = res.substr(0, res.find_last_not_of('\n')+1);
             return symbol(res.c_str());

src/muz/rel/dl_relation_manager.cpp

@@ -1149,7 +1149,7 @@ namespace datalog {
         }
 
         void modify_fact(table_fact & f) const override {
-            permutate_by_cycle(f, m_cycle);
+            permute_by_cycle(f, m_cycle);
         }
 
         table_base * operator()(const table_base & t) override {

src/muz/rel/dl_sieve_relation.cpp

@@ -413,14 +413,14 @@ namespace datalog {
         unsigned sig_sz = r.get_signature().size();
         unsigned_vector permutation;
         add_sequence(0, sig_sz, permutation);
-        permutate_by_cycle(permutation, cycle_len, permutation_cycle);
+        permute_by_cycle(permutation, cycle_len, permutation_cycle);
 
         bool inner_identity;
         unsigned_vector inner_permutation;
         collect_sub_permutation(permutation, r.m_sig2inner, inner_permutation, inner_identity);
 
         bool_vector result_inner_cols = r.m_inner_cols;
-        permutate_by_cycle(result_inner_cols, cycle_len, permutation_cycle);
+        permute_by_cycle(result_inner_cols, cycle_len, permutation_cycle);
 
         relation_signature result_sig;
         relation_signature::from_rename(r.get_signature(), cycle_len, permutation_cycle, result_sig);

src/params/context_params.cpp

@@ -109,6 +109,7 @@ void context_params::set(char const * param, char const * value) {
     else if (p == "encoding") {
         if (strcmp(value, "unicode") == 0 || strcmp(value, "bmp") == 0 || strcmp(value, "ascii") == 0) {
             m_encoding = value;
+            gparams::set("encoding", value);
         }
         else {
             std::stringstream strm;