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

src/api/python/z3/z3.py

@@ -114,15 +114,26 @@ def _symbol2py(ctx, s):
 
 # Hack for having nary functions that can receive one argument that is the
 # list of arguments.
+# Use this when function takes a single list of arguments
 def _get_args(args):
-    try:
+     try:
-        if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
+       if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
             return args[0]
-        elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
+       elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
             return [arg for arg in args[0]]
+       else:
+            return args
+     except:  # len is not necessarily defined when args is not a sequence (use reflection?)
+        return args
+
+# Use this when function takes multiple arguments
+def _get_args_ast_list(args):
+    try:
+        if isinstance(args, set) or isinstance(args, AstVector) or isinstance(args, tuple):
+            return [arg for arg in args]
         else:
             return args
-    except:  # len is not necessarily defined when args is not a sequence (use reflection?)
+    except:
         return args
 
 def _to_param_value(val):
@@ -7943,8 +7954,10 @@ def AtLeast(*args):
     return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
 
 
-def _pb_args_coeffs(args):
+def _pb_args_coeffs(args, default_ctx = None):
-    args  = _get_args(args)
+    args  = _get_args_ast_list(args)
+    if len(args) == 0:
+       return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
     args, coeffs = zip(*args)
     if __debug__:
         _z3_assert(len(args) > 0, "Non empty list of arguments expected")
@@ -7976,7 +7989,7 @@ def PbGe(args, k):
     ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
     return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
-def PbEq(args, k):
+def PbEq(args, k, ctx = None):
     """Create a Pseudo-Boolean inequality k constraint.
 
     >>> a, b, c = Bools('a b c')

src/api/python/z3/z3printer.py

@@ -36,7 +36,7 @@ _z3_op_to_str = {
     Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int',
     Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', 
     Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext', 
-    Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe'
+    Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe', Z3_OP_PB_EQ : 'PbEq'
     }
 
 # List of infix operators
@@ -930,6 +930,8 @@ class Formatter:
                 return self.pp_pbcmp(a, d, f, xs)
             elif k == Z3_OP_PB_GE:
                 return self.pp_pbcmp(a, d, f, xs)
+            elif k == Z3_OP_PB_EQ:
+                return self.pp_pbcmp(a, d, f, xs)
             elif z3.is_pattern(a):
                 return self.pp_pattern(a, d, xs)
             elif self.is_infix(k):

src/ast/rewriter/rewriter_def.h

@@ -194,12 +194,14 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
             result_stack().shrink(fr.m_spos);
             result_stack().push_back(arg);
             fr.m_state = REWRITE_BUILTIN;
+            TRACE("rewriter_step", tout << "step\n" << mk_ismt2_pp(t, m()) << "\n";);
             if (visit<false>(arg, fr.m_max_depth)) {
                 m_r = result_stack().back();
                 result_stack().pop_back();
                 result_stack().pop_back();
                 result_stack().push_back(m_r);
                 cache_result<false>(t, m_r, m_pr, fr.m_cache_result);
+                TRACE("rewriter_step", tout << "step 1\n" << mk_ismt2_pp(m_r, m()) << "\n";);
                 frame_stack().pop_back();
                 set_new_child_flag(t);
             }

src/model/model_evaluator.cpp

@@ -187,14 +187,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
             TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
                   for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
                   tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
         if (st == BR_FAILED && !m.is_builtin_family_id(fid))
             st = evaluate_partial_theory_func(f, num, args, result, result_pr);
         if (st == BR_DONE && is_app(result)) {
             app* a = to_app(result);
             if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
-                return BR_DONE;
+                return BR_REWRITE1;
             }
         }
         CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
@@ -399,12 +399,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 }
             }
         }
-        args_table::iterator it = table1.begin(), end = table1.end();
+        for (auto const& t : table1) {
-        for (; it != end; ++it) {
+            switch (compare((t)[arity], else2)) {
-            switch (compare((*it)[arity], else2)) {
             case l_true: break;
             case l_false: result = m.mk_false(); return BR_DONE;
-            default: conj.push_back(m.mk_eq((*it)[arity], else2)); break;
+            default: conj.push_back(m.mk_eq((t)[arity], else2)); break;
             }
         }
         result = mk_and(conj);

src/smt/smt_context_pp.cpp

@@ -580,20 +580,20 @@ namespace smt {
         case b_justification::BIN_CLAUSE: {
             literal l2 = j.get_literal();
             out << "bin-clause ";
-            display_literal(out, l2);
+            display_literal_verbose(out, l2);
             break;
         }
         case b_justification::CLAUSE: {
             clause * cls = j.get_clause();
             out << "clause ";
-            if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
+            if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
             break;
         }
         case b_justification::JUSTIFICATION: {
             out << "justification " << j.get_justification()->get_from_theory() << ": ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals(out, lits);
+            display_literals_verbose(out, lits);
             break;
         }
         default:

src/smt/smt_quantifier.cpp

@@ -222,7 +222,7 @@ namespace smt {
 
         final_check_status final_check_eh(bool full) {
             if (full) {
-                IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
+                IF_VERBOSE(100, if (!m_quantifiers.empty()) verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
                 final_check_status result  = m_qi_queue.final_check_eh() ? FC_DONE : FC_CONTINUE;
                 final_check_status presult = m_plugin->final_check_eh(full);
                 if (presult != FC_DONE)

src/smt/theory_seq.cpp

@@ -2404,8 +2404,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
             lits.push_back(~is_digit(ith_char));
             nums.push_back(digit2int(ith_char));
         }        
-        for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
+        for (unsigned i = sz, c = 1; i-- > 0; c *= 10) {
-            --i;
             coeff = m_autil.mk_int(c);
             nums[i] = m_autil.mk_mul(coeff, nums[i].get());
         }
@@ -2414,9 +2413,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
         lits.push_back(mk_eq(e, num, false));
         ++m_stats.m_add_axiom;
         m_new_propagation = true;
-        for (unsigned i = 0; i < lits.size(); ++i) {
+        for (literal lit : lits) {
-            ctx.mark_as_relevant(lits[i]);
+            ctx.mark_as_relevant(lit);
         }
+        TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
         ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
         m_stoi_axioms.insert(val);
         m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));

src/smt/theory_str.cpp

@@ -441,7 +441,7 @@ namespace smt {
 
     void theory_str::track_variable_scope(expr * var) {
         if (internal_variable_scope_levels.find(sLevel) == internal_variable_scope_levels.end()) {
-            internal_variable_scope_levels[sLevel] = std::set<expr*>();
+            internal_variable_scope_levels[sLevel] = obj_hashtable<expr>();
         }
         internal_variable_scope_levels[sLevel].insert(var);
     }
@@ -6468,9 +6468,9 @@ namespace smt {
                             expr * regexTerm = a_regexIn->get_arg(1);
 
                             // TODO figure out regex NFA stuff
-                            if (regex_nfa_cache.find(regexTerm) == regex_nfa_cache.end()) {
+                            if (!regex_nfa_cache.contains(regexTerm)) {
                                 TRACE("str", tout << "regex_nfa_cache: cache miss" << std::endl;);
-                                regex_nfa_cache[regexTerm] = nfa(u, regexTerm);
+                                regex_nfa_cache.insert(regexTerm, nfa(u, regexTerm));
                             } else {
                                 TRACE("str", tout << "regex_nfa_cache: cache hit" << std::endl;);
                             }
@@ -9286,7 +9286,7 @@ namespace smt {
             h++;
             coverAll = get_next_val_encode(options[options.size() - 1], base);
         }
-        val_range_map[val_indicator] = options[options.size() - 1];
+        val_range_map.insert(val_indicator, options[options.size() - 1]);
 
         TRACE("str",
               tout << "value tester encoding " << "{" << std::endl;
@@ -9380,7 +9380,7 @@ namespace smt {
             TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;);
             int tries = 0;
             expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries);
-            valueTester_fvar_map[val_indicator] = freeVar;
+            valueTester_fvar_map.insert(val_indicator, freeVar);
             fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator));
             print_value_tester_list(fvar_valueTester_map[freeVar][len]);
             return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries);
@@ -9430,7 +9430,7 @@ namespace smt {
                     refresh_theory_var(valTester);
                 } else {
                     valTester = mk_internal_valTest_var(freeVar, len, i + 1);
-                    valueTester_fvar_map[valTester] = freeVar;
+                    valueTester_fvar_map.insert(valTester, freeVar);
                     fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester));
                     print_value_tester_list(fvar_valueTester_map[freeVar][len]);
                 }
@@ -9595,7 +9595,7 @@ namespace smt {
             if (low.is_neg()) {
                 toAssert = m_autil.mk_ge(cntInUnr, mk_int(0));
             } else {
-                if (unroll_var_map.find(unrFunc) == unroll_var_map.end()) {
+                if (!unroll_var_map.contains(unrFunc)) {
 
                     expr_ref newVar1(mk_regex_rep_var(), mgr);
                     expr_ref newVar2(mk_regex_rep_var(), mgr);
@@ -9627,8 +9627,9 @@ namespace smt {
                     // put together
                     toAssert = mgr.mk_and(ctx.mk_eq_atom(op0, and1), toAssert);
 
-                    unroll_var_map[unrFunc] = toAssert;
+                    unroll_var_map.insert(unrFunc, toAssert);
-                } else {
+                } 
+                else {
                     toAssert = unroll_var_map[unrFunc];
                 }
             }

src/smt/theory_str.h

@@ -286,7 +286,7 @@ protected:
     obj_hashtable<expr> variable_set;
     obj_hashtable<expr> internal_variable_set;
     obj_hashtable<expr> regex_variable_set;
-    std::map<int, std::set<expr*> > internal_variable_scope_levels;
+    std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
 
     obj_hashtable<expr> internal_lenTest_vars;
     obj_hashtable<expr> internal_valTest_vars;
@@ -295,21 +295,20 @@ protected:
     obj_hashtable<expr> input_var_in_len;
 
     obj_map<expr, unsigned int> fvar_len_count_map;
-    // TBD: need to replace by obj_map for determinism
     std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
     obj_map<expr, expr*> lenTester_fvar_map;
 
     // TBD: need to replace by obj_map for determinism
     std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
-    std::map<expr*, expr*> valueTester_fvar_map;
+    obj_map<expr, expr*> valueTester_fvar_map;
 
-    std::map<expr*, int_vector> val_range_map;
+    obj_map<expr, int_vector> val_range_map;
 
     // This can't be an expr_ref_vector because the constructor is wrong,
     // we would need to modify the allocator so we pass in ast_manager
     // TBD: need to replace by obj_map for determinism
     std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
-    std::map<expr*, expr*> unroll_var_map;
+    obj_map<expr, expr*> unroll_var_map;
     // TBD: need to replace by obj_pair_map for determinism
     std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
 
@@ -323,7 +322,7 @@ protected:
     std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
     // TBD: need to replace by obj_map for determinism
     std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
-    std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
+    obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
 
     svector<char> char_set;
     std::map<char, int>  charSetLookupTable;