diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d4ff556fe..36283356d 100644 --- a/src/api/python/z3/z3.py +++ b/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: - if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): + try: + 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): - args = _get_args(args) +def _pb_args_coeffs(args, default_ctx = None): + 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') diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 3a6b7269e..8fd0c182e 100644 --- a/src/api/python/z3/z3printer.py +++ b/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): diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 878f4ef4c..dfb6542d6 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -194,12 +194,14 @@ bool rewriter_tpl::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(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(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); } diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index fd2dc7656..227e14ca6 100644 --- a/src/model/model_evaluator.cpp +++ b/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 (; it != end; ++it) { - switch (compare((*it)[arity], else2)) { + for (auto const& t : table1) { + switch (compare((t)[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); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index f072a1d13..f4f56df5d 100644 --- a/src/smt/smt_context_pp.cpp +++ b/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(*m_conflict_resolution).justification2literals(j.get_justification(), lits); - display_literals(out, lits); + display_literals_verbose(out, lits); break; } default: diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 0ca244185..1f6811a0f 100644 --- a/src/smt/smt_quantifier.cpp +++ b/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) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index b90735a07..94841603d 100644 --- a/src/smt/theory_seq.cpp +++ b/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) { - --i; + for (unsigned i = sz, c = 1; i-- > 0; c *= 10) { 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) { - ctx.mark_as_relevant(lits[i]); + for (literal lit : lits) { + 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(m_stoi_axioms, val)); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index e1340c301..69cf80de6 100644 --- a/src/smt/theory_str.cpp +++ b/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(); + internal_variable_scope_levels[sLevel] = obj_hashtable(); } 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; - } else { + unroll_var_map.insert(unrFunc, toAssert); + } + else { toAssert = unroll_var_map[unrFunc]; } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 09d6498a4..508a1c905 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -286,7 +286,7 @@ protected: obj_hashtable variable_set; obj_hashtable internal_variable_set; obj_hashtable regex_variable_set; - std::map > internal_variable_scope_levels; + std::map > internal_variable_scope_levels; obj_hashtable internal_lenTest_vars; obj_hashtable internal_valTest_vars; @@ -295,21 +295,20 @@ protected: obj_hashtable input_var_in_len; obj_map fvar_len_count_map; - // TBD: need to replace by obj_map for determinism std::map > fvar_lenTester_map; obj_map lenTester_fvar_map; // TBD: need to replace by obj_map for determinism std::map > > > fvar_valueTester_map; - std::map valueTester_fvar_map; + obj_map valueTester_fvar_map; - std::map val_range_map; + obj_map 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, ptr_vector > > unroll_tries_map; - std::map unroll_var_map; + obj_map unroll_var_map; // TBD: need to replace by obj_pair_map for determinism std::map, expr*> concat_eq_unroll_ast_map; @@ -323,7 +322,7 @@ protected: std::map, expr*> regex_in_bool_map; // TBD: need to replace by obj_map for determinism std::map > regex_in_var_reg_str_map; - std::map regex_nfa_cache; // Regex term --> NFA + obj_map regex_nfa_cache; // Regex term --> NFA svector char_set; std::map charSetLookupTable;