Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/api/python/z3.py

@@ -635,7 +635,7 @@ class FuncDeclRef(AstRef):
 	args = _get_args(args)
         num = len(args)
         if __debug__:
-            _z3_assert(num == self.arity(), "Incorrect number of arguments")
+            _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self)
         _args = (Ast * num)()
         saved = []
         for i in range(num):
@@ -1735,7 +1735,7 @@ class ArithSortRef(SortRef):
     """Real and Integer sorts."""
 
     def is_real(self):
-        """Return `True` if `self` is the integer sort.
+        """Return `True` if `self` is of the sort Real.
         
         >>> x = Real('x')
         >>> x.is_real()
@@ -1749,7 +1749,7 @@ class ArithSortRef(SortRef):
         return self.kind() == Z3_REAL_SORT
 
     def is_int(self):
-        """Return `True` if `self` is the real sort.
+        """Return `True` if `self` is of the sort Integer.
         
         >>> x = Int('x')
         >>> x.is_int()

src/ast/ast_smt_pp.cpp

@@ -949,6 +949,10 @@ public:
         mark.mark(s, true);
     }
 
+    void operator()(sort* s) {
+        ast_mark mark;
+        pp_sort_decl(mark, s);
+    }
 
     void operator()(func_decl* d) {
         if (m_is_smt2) {
@@ -962,7 +966,6 @@ public:
             m_out << ") ";
             visit_sort(d->get_range());
             m_out << ")";
-            newline();
         }
         else {
             m_out << "(";
@@ -1021,6 +1024,22 @@ void ast_smt_pp::display_expr_smt2(std::ostream& strm, expr* n, unsigned indent,
     p(n);
 }
 
+void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, unsigned num_var_names, char const* const* var_names) {
+    ptr_vector<quantifier> ql;
+    smt_renaming rn;
+    smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names);
+    if (is_expr(a)) {
+        p(to_expr(a));
+    }
+    else if (is_func_decl(a)) {
+        p(to_func_decl(a));
+    }
+    else {
+        SASSERT(is_sort(a));
+        p(to_sort(a));
+    }
+}
+
 
 void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     ptr_vector<quantifier> ql;
@@ -1071,6 +1090,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
         if (!(*m_is_declared)(d)) {
             smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p(d);
+            strm << "\n";
         }
     }
 
@@ -1079,6 +1099,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
         if (!(*m_is_declared)(d)) {
             smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p(d);
+            strm << "\n";
         }
     }
 

src/ast/ast_smt_pp.h

@@ -79,22 +79,23 @@ public:
     void display_smt2(std::ostream& strm, expr* n);
     void display_expr(std::ostream& strm, expr* n);
     void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
+    void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
 
 };
 
 struct mk_smt_pp {
-    expr * m_expr;
+    ast*   m_ast;
     ast_manager& m_manager;
     unsigned m_indent;
     unsigned m_num_var_names;
     char const* const* m_var_names;
-    mk_smt_pp(expr* e, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0) :
-        m_expr(e), m_manager(m), m_indent(indent), m_num_var_names(num_var_names), m_var_names(var_names) {}
+    mk_smt_pp(ast* e, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0) :
+        m_ast(e), m_manager(m), m_indent(indent), m_num_var_names(num_var_names), m_var_names(var_names) {}
 };
 
 inline std::ostream& operator<<(std::ostream& out, const mk_smt_pp & p) {
     ast_smt_pp pp(p.m_manager);
-    pp.display_expr_smt2(out, p.m_expr, p.m_indent, p.m_num_var_names, p.m_var_names);
+    pp.display_ast_smt2(out, p.m_ast, p.m_indent, p.m_num_var_names, p.m_var_names);
     return out;
 }
 

src/muz_qe/dl_context.cpp

@@ -994,6 +994,7 @@ namespace datalog {
         p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
                       
         p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
+        p.insert(":print-low-level-smt2", CPK_BOOL, "(default true) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
         
         PRIVATE_PARAMS(
             p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL, 
@@ -1650,6 +1651,9 @@ namespace datalog {
         expr_ref_vector rules(m);
         svector<symbol> names;
         bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
+        bool print_low_level = m_params.get_bool(":print-low-level-smt2", true);
+
+#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);
 
         get_rules_as_formulas(rules, names);
 
@@ -1684,18 +1688,18 @@ namespace datalog {
         obj_hashtable<sort>& sorts = visitor.sorts();
         obj_hashtable<sort>::iterator sit = sorts.begin(), send = sorts.end();
         for (; sit != send; ++sit) {
-            ast_smt2_pp(out, *sit, env, params);
+            PP(*sit);
         }
         for (; it != end; ++it) {
             func_decl* f = *it;
-            ast_smt2_pp(out, f, env, params);
+            PP(f);
             out << "\n";
         }
         it = rels.begin(); end = rels.end();
         for (; it != end; ++it) {
             func_decl* f = *it;
             out << "(declare-rel " << f->get_name() << " (";
-            for (unsigned i = 0; i < f->get_arity(); ++i) {
+            for (unsigned i = 0; i < f->get_arity(); ++i) {                
                 ast_smt2_pp(out, f->get_domain(i), env, params);
                 if (i + 1 < f->get_arity()) {
                     out << " ";
@@ -1714,7 +1718,7 @@ namespace datalog {
 
         for (unsigned i = 0; i < num_axioms; ++i) {
             out << "(assert ";
-            ast_smt2_pp(out, axioms[i], env, params);
+            PP(axioms[i]);
             out << ")\n";
         }
         for (unsigned i = 0; i < rules.size(); ++i) {            
@@ -1724,12 +1728,7 @@ namespace datalog {
             if (symbol::null != nm) {
                 out << "(! ";
             }
-            if (use_fixedpoint_extensions) {
-                ast_smt2_pp(out, r, env, params);
-            }
-            else {
-                out << mk_smt_pp(r, m);
-            }
+            PP(r);
             if (symbol::null != nm) {
                 while (fresh_names.contains(nm)) {
                     std::ostringstream s;
@@ -1744,7 +1743,7 @@ namespace datalog {
         if (use_fixedpoint_extensions) {
             for (unsigned i = 0; i < num_queries; ++i) {
                 out << "(query ";
-                ast_smt2_pp(out, queries[i], env, params);
+                PP(queries[i]);
                 out << ")\n";
             }
         }
@@ -1754,7 +1753,7 @@ namespace datalog {
                 out << "(assert ";
                 expr_ref q(m);
                 q = m.mk_not(queries[i]);
-                ast_smt2_pp(out, q, env, params);
+                PP(q);
                 out << ")\n";
                 out << "(check-sat)\n";
                 if (num_queries > 1) out << "(pop)\n";

src/muz_qe/pdr_context.cpp

@@ -43,6 +43,7 @@ Notes:
 #include "qe_lite.h"
 #include "ast_ll_pp.h"
 #include "proof_checker.h"
+#include "smt_value_sort.h"
 
 namespace pdr {
 
@@ -1827,14 +1828,14 @@ namespace pdr {
         if (!vars.empty()) {
             // also fresh names for auxiliary variables in body?
             expr_substitution sub(m);
-            expr_ref_vector refs(m);
             expr_ref tmp(m);
             proof_ref pr(m);
             pr = m.mk_asserted(m.mk_true());
-            for (unsigned i = 0; i < vars.size(); ++i) {                
-                VERIFY (M->eval(vars[i].get(), tmp, true));                
-                refs.push_back(tmp);
-                sub.insert(vars[i].get(), tmp, pr);
+            for (unsigned i = 0; i < vars.size(); ++i) {    
+                if (smt::is_value_sort(m, vars[i].get())) {
+                    VERIFY (M->eval(vars[i].get(), tmp, true)); 
+                    sub.insert(vars[i].get(), tmp, pr);
+                }
             }
             if (!rep) rep = mk_expr_simp_replacer(m);
             rep->set_substitution(&sub);

src/muz_qe/pdr_util.cpp

@@ -903,6 +903,7 @@ namespace pdr {
         return !has_x;
     }
 
+
     void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
         ast_manager& m = fml.get_manager();
         expr_ref_vector conjs(m);

src/smt/smt_implied_equalities.cpp

@@ -29,6 +29,7 @@ Revision History:
 #include "array_decl_plugin.h"
 #include "uint_set.h"
 #include "model_v2_pp.h"
+#include "smt_value_sort.h"
 
 
 namespace smt {
@@ -134,44 +135,7 @@ namespace smt {
                     }                    
                 }
             }
-        }        
-        
-        bool is_simple_type(sort* s) {
-            arith_util arith(m);
-            datatype_util data(m);
-            
-            ptr_vector<sort> sorts;
-            ast_mark mark;
-            sorts.push_back(s);
-            
-            while (!sorts.empty()) {
-                s = sorts.back();
-                sorts.pop_back();
-                if (mark.is_marked(s)) {
-                    continue;
-                }
-                mark.mark(s, true);
-                if (arith.is_int_real(s)) {
-                    // simple
-                }
-                else if (m.is_bool(s)) {
-                    // simple
-                }
-                else if (data.is_datatype(s)) {
-                    ptr_vector<func_decl> const& cs = *data.get_datatype_constructors(s);
-                    for (unsigned i = 0; i < cs.size(); ++i) {
-                        func_decl* f = cs[i];
-                        for (unsigned j = 0; j < f->get_arity(); ++j) {
-                            sorts.push_back(f->get_domain(j));
-                        }
-                    }
-                }
-                else {
-                    return false;
-                }
-            }
-            return true;        
-        }
+        }                
         
         /**
            \brief Extract implied equalities for a collection of terms in the current context.
@@ -216,7 +180,7 @@ namespace smt {
 
             uint_set non_values;
             
-            if (!is_simple_type(srt)) {
+            if (!is_value_sort(m, srt)) {
                 for (unsigned i = 0; i < terms.size(); ++i) {
                     non_values.insert(i);
                 }

src/smt/smt_value_sort.cpp

@@ -0,0 +1,74 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    smt_value_sort.cpp
+
+Abstract:
+
+    Determine if elements of a given sort can be values.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-25
+
+Revision History:
+
+
+--*/
+
+#include "smt_value_sort.h"
+#include "bv_decl_plugin.h"
+#include "arith_decl_plugin.h"
+#include "datatype_decl_plugin.h"
+
+namespace smt {
+
+        
+    bool is_value_sort(ast_manager& m, sort* s) {
+        arith_util arith(m);
+        datatype_util data(m);
+        bv_util bv(m);
+        
+        ptr_vector<sort> sorts;
+        ast_mark mark;
+        sorts.push_back(s);
+        
+        while (!sorts.empty()) {
+            s = sorts.back();
+            sorts.pop_back();
+            if (mark.is_marked(s)) {
+                continue;
+            }
+            mark.mark(s, true);
+            if (arith.is_int_real(s)) {
+                // simple
+            }
+            else if (m.is_bool(s)) {
+                // simple
+            }
+            else if (bv.is_bv_sort(s)) {
+                // simple
+            }
+            else if (data.is_datatype(s)) {
+                ptr_vector<func_decl> const& cs = *data.get_datatype_constructors(s);
+                for (unsigned i = 0; i < cs.size(); ++i) {
+                    func_decl* f = cs[i];
+                    for (unsigned j = 0; j < f->get_arity(); ++j) {
+                        sorts.push_back(f->get_domain(j));
+                    }
+                }
+            }
+            else {
+                return false;
+            }
+        }
+        return true;        
+    }
+
+    bool is_value_sort(ast_manager& m, expr* e) {
+        return is_value_sort(m, m.get_sort(e));
+    }
+
+}

src/smt/smt_value_sort.h

@@ -0,0 +1,37 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    smt_value_sort.h
+
+Abstract:
+
+    Determine if elements of a given sort can be values.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-11-25
+
+Revision History:
+
+
+--*/
+
+
+#ifndef __SMT_VALUE_SORT_H__
+#define __SMT_VALUE_SORT_H__
+
+#include "ast.h"
+
+
+namespace smt {
+        
+    bool is_value_sort(ast_manager& m, sort* s);
+
+    bool is_value_sort(ast_manager& m, expr* e);
+    
+};
+
+
+#endif