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

examples/tptp/tptp5.cpp

@@ -1630,10 +1630,8 @@ public:
                 unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0));
                 std::set<unsigned> const& hyps = m_proof_hypotheses.find(parent_id)->second;
                 print_hypotheses(out, hyps);
-                out << ").\n";
+                out << "))).\n";
                 break;                
-                display_inference(out, "lemma", "thm", p);
-                break;           
             }     
             case Z3_OP_PR_UNIT_RESOLUTION:                                 
                 display_inference(out, "unit_resolution", "thm", p);

src/api/python/z3.py

@@ -899,6 +899,7 @@ def _coerce_expr_merge(s, a):
             return s
         else:
             if __debug__:
+                _z3_assert(s1.ctx == s.ctx, "context mismatch")
                 _z3_assert(False, "sort mismatch")
     else:
         return s
@@ -1459,9 +1460,18 @@ def And(*args):
     >>> And(P)
     And(p__0, p__1, p__2, p__3, p__4)
     """
-    args  = _get_args(args)
+    last_arg = None
-    ctx   = _ctx_from_ast_arg_list(args)
+    if len(args) > 0:
+        last_arg = args[len(args)-1]
+    if isinstance(last_arg, Context):
+        ctx = args[len(args)-1]
+        args = args[:len(args)-1]
+    else:
+        ctx = main_ctx()
+    args = _get_args(args)
+    ctx_args  = _ctx_from_ast_arg_list(args, ctx)
     if __debug__:
+        _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
     if _has_probe(args):
         return _probe_and(args, ctx)
@@ -1480,9 +1490,18 @@ def Or(*args):
     >>> Or(P)
     Or(p__0, p__1, p__2, p__3, p__4)
     """
-    args  = _get_args(args)
+    last_arg = None
-    ctx   = _ctx_from_ast_arg_list(args)
+    if len(args) > 0:
+        last_arg = args[len(args)-1]
+    if isinstance(last_arg, Context):
+        ctx = args[len(args)-1]
+        args = args[:len(args)-1]
+    else:
+        ctx = main_ctx()
+    args = _get_args(args)
+    ctx_args  = _ctx_from_ast_arg_list(args, ctx)
     if __debug__:
+        _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
         _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
     if _has_probe(args):
         return _probe_or(args, ctx)
@@ -4128,6 +4147,7 @@ class Datatype:
         """
         if __debug__:
             _z3_assert(isinstance(name, str), "String expected")
+            _z3_assert(name != "", "Constructor name cannot be empty")
         return self.declare_core(name, "is_" + name, *args)
 
     def __repr__(self):

src/ast/dl_decl_plugin.cpp

@@ -599,7 +599,23 @@ namespace datalog {
                         return 0;
                 }
                 result = mk_compare(OP_DL_LT, m_lt_sym, domain);
-                break;                
+                break;   
+
+            case OP_DL_REP: {
+                if (!check_domain(0, 0, num_parameters) ||
+                    !check_domain(1, 1, arity)) return 0;
+                func_decl_info info(m_family_id, k, 0, 0);
+                result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info);
+                break;
+            }
+                
+            case OP_DL_ABS: {
+                if (!check_domain(0, 0, num_parameters) ||
+                    !check_domain(1, 1, arity)) return 0;
+                func_decl_info info(m_family_id, k, 0, 0);
+                result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info);
+                break;
+            }
 
             default:
                 m_manager->raise_exception("operator not recognized");

src/ast/dl_decl_plugin.h

@@ -48,6 +48,8 @@ namespace datalog {
         OP_RA_CLONE,
         OP_DL_CONSTANT,
         OP_DL_LT,
+        OP_DL_REP,
+        OP_DL_ABS,
         LAST_RA_OP
     };
     

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -323,6 +323,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
     
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
+        TRACE("bit_blaster", tout << f->get_name() << " ";
+              for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
+              tout << "\n";);
         if (num == 0 && f->get_family_id() == null_family_id && butil().is_bv_sort(f->get_range())) {
             mk_const(f, result);
             return BR_DONE;

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -828,6 +828,12 @@ void bit_blaster_tpl<Cfg>::mk_eq(unsigned sz, expr * const * a_bits, expr * cons
 
 template<typename Cfg>
 void bit_blaster_tpl<Cfg>::mk_rotate_left(unsigned sz, expr * const * a_bits, unsigned n, expr_ref_vector & out_bits) {
+    TRACE("bit_blaster", tout << n << ": " << sz << " ";
+          for (unsigned i = 0; i < sz; ++i) {
+              tout << mk_pp(a_bits[i], m()) << " ";
+          }
+          tout << "\n";
+          );
     n = n % sz;
     for (unsigned i = sz - n; i < sz; i++) 
         out_bits.push_back(a_bits[i]);
@@ -974,7 +980,7 @@ void bit_blaster_tpl<Cfg>::mk_ashr(unsigned sz, expr * const * a_bits, expr * co
                 mk_ite(eqs.get(i - j), a_bits[sz - j - 1], out, new_out);
                 out = new_out;
             }
-            TRACE("bit_blaster_tpl<Cfg>", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
+            TRACE("bit_blaster", tout << (sz - i - 1) << " :\n" << mk_pp(out, m()) << "\n";);
             out_bits.set(sz - i - 1, out);
         }
     }
@@ -1004,7 +1010,7 @@ void bit_blaster_tpl<Cfg>::mk_ext_rotate_left_right(unsigned sz, expr * const *
             out = a_bits[i];
             for (unsigned j = 1; j < sz; j++) {
                 expr_ref new_out(m());
-                unsigned src = (Left ? (i - j) : (i + j)) % sz;
+                unsigned src = (Left ? (sz + i - j) : (i + j)) % sz;
                 mk_ite(eqs.get(j), a_bits[src], out, new_out);
                 out = new_out;
             }

src/ast/rewriter/bv_rewriter.cpp

@@ -21,6 +21,7 @@ Notes:
 #include"poly_rewriter_def.h"
 #include"ast_smt2_pp.h"
 
+
 mk_extract_proc::mk_extract_proc(bv_util & u):
     m_util(u),
     m_high(0),

src/smt/params/preprocessor_params.cpp

@@ -23,6 +23,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) {
     smt_params_helper p(_p);
     m_macro_finder            = p.macro_finder();
     m_pull_nested_quantifiers = p.pull_nested_quantifiers();
+    m_refine_inj_axiom        = p.refine_inj_axioms();
 }
 
 void preprocessor_params::updt_params(params_ref const & p) {

src/smt/params/smt_params_helper.pyg

@@ -14,6 +14,7 @@ def_module_params(module_name='smt',
                           ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
                           ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'),
                           ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'),
+                          ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'),
                           ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'),
                           ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'),
                           ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'),

src/smt/proto_model/datatype_factory.cpp

@@ -191,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) {
     // Approach 2)
     // For recursive datatypes.
     // search for constructor...
+    unsigned num_iterations = 0;
     if (m_util.is_recursive(s)) {
         while(true) {
+            ++num_iterations;
             TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
             ptr_vector<func_decl> const * constructors = m_util.get_datatype_constructors(s);
             ptr_vector<func_decl>::const_iterator it   = constructors->begin();
@@ -212,7 +214,13 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                           << found_sibling << "\n";);
                     if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
                         found_sibling = true;
-                        expr * maybe_new_arg = get_almost_fresh_value(s_arg);
+                        expr * maybe_new_arg = 0;
+                        if (num_iterations <= 1) {
+                            maybe_new_arg = get_almost_fresh_value(s_arg);
+                        }
+                        else {
+                            maybe_new_arg = get_fresh_value(s_arg);
+                        }
                         if (!maybe_new_arg) {
                             TRACE("datatype_factory", 
                                   tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);
@@ -231,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                 if (found_sibling) {
                     expr_ref new_value(m_manager);
                     new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr());
+                    TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
                     m_last_fresh_value.insert(s, new_value);
                     if (!set->contains(new_value)) {
                         register_value(new_value);

src/smt/smt_model_generator.cpp

@@ -102,6 +102,7 @@ namespace smt {
                     if (th && th->build_models()) {
                         if (r->get_th_var(th->get_id()) != null_theory_var) {
                             proc = th->mk_value(r, *this);
+                            SASSERT(proc);
                         }
                         else {
                             TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
@@ -110,6 +111,7 @@ namespace smt {
                     }
                     else {
                         proc = mk_model_value(r);
+                        SASSERT(proc);
                     }
                 }
                 SASSERT(proc);

src/smt/theory_arith_eq.h

@@ -193,7 +193,7 @@ namespace smt {
             return true;
         }
 
-        if (!r.get_base_var() == x && x > y) {
+        if (r.get_base_var() != x && x > y) {
             std::swap(x, y);
             k.neg();
         }

src/smt/theory_dl.cpp

@@ -162,7 +162,7 @@ namespace smt {
             m.register_factory(alloc(dl_factory, m_util, m.get_model()));
         }
         
-        virtual smt::model_value_proc * mk_value(smt::enode * n) {
+        virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) {
             return alloc(dl_value_proc, *this, n);
         }
 
@@ -201,9 +201,8 @@ namespace smt {
             if(!m_reps.find(s, r) || !m_vals.find(s,v)) {
                 SASSERT(!m_reps.contains(s));
                 sort* bv = b().mk_sort(64);
-                // TBD: filter these from model.
+                r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv);
-                r = m().mk_fresh_func_decl("rep",1, &s,bv);
+                v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s);
-                v = m().mk_fresh_func_decl("val",1, &bv,s);
                 m_reps.insert(s, r);
                 m_vals.insert(s, v);
                 add_trail(r);