diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt index b01a0e016..74fddd2bb 100644 --- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt +++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt @@ -9,14 +9,15 @@ z3_add_component(rewriter datatype_rewriter.cpp der.cpp dl_rewriter.cpp + enum2bv_rewriter.cpp expr_replacer.cpp expr_safe_replace.cpp factor_rewriter.cpp - fd_rewriter.cpp fpa_rewriter.cpp label_rewriter.cpp mk_simplified_app.cpp pb_rewriter.cpp + pb2bv_rewriter.cpp quant_hoist.cpp rewriter.cpp seq_rewriter.cpp diff --git a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt index 201cdcf0f..c6f621f25 100644 --- a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt +++ b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt @@ -1,6 +1,9 @@ z3_add_component(portfolio SOURCES default_tactic.cpp + enum2bv_solver.cpp + pb2bv_solver.cpp + bounded_int2bv_solver.cpp fd_solver.cpp smt_strategic_solver.cpp COMPONENT_DEPENDENCIES diff --git a/contrib/cmake/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt index acaf186ba..6f6615e0c 100644 --- a/contrib/cmake/src/test/CMakeLists.txt +++ b/contrib/cmake/src/test/CMakeLists.txt @@ -78,6 +78,7 @@ add_executable(test-z3 old_interval.cpp optional.cpp parray.cpp + pb2bv.cpp pdr.cpp permutation.cpp polynomial.cpp diff --git a/examples/python/all_interval_series.py b/examples/python/all_interval_series.py new file mode 100644 index 000000000..d55017a56 --- /dev/null +++ b/examples/python/all_interval_series.py @@ -0,0 +1,76 @@ +# Copyright Microsoft Research 2016 +# The following script finds sequences of length n-1 of +# integers 0,..,n-1 such that the difference of the n-1 +# adjacent entries fall in the range 0,..,n-1 +# This is known as the "The All-Interval Series Problem" +# See http://www.csplib.org/Problems/prob007/ + +from z3 import * +import time + +def diff_at_j_is_i(xs, j, i): + assert(0 <= j and j + 1 < len(xs)) + assert(1 <= i and i < len(xs)) + return Or([ And(xs[j][k], xs[j+1][k-i]) for k in range(i,len(xs))] + + [ And(xs[j][k], xs[j+1][k+i]) for k in range(0,len(xs)-i)]) + + +def ais(n): + xij = [ [ Bool("x_%d_%d" % (i,j)) for j in range(n)] for i in range(n) ] + s = SolverFor("QF_FD") +# Optionally replace by (slower) default solver if using +# more then just finite domains (Booleans, Bit-vectors, enumeration types +# and bounded integers) +# s = Solver() + for i in range(n): + s.add(AtMost(xij[i] + [1])) + s.add(Or(xij[i])) + for j in range(n): + xi = [ xij[i][j] for i in range(n) ] + s.add(AtMost(xi + [1])) + s.add(Or(xi)) + dji = [ [ diff_at_j_is_i(xij, j, i + 1) for i in range(n-1)] for j in range(n-1) ] + for j in range(n-1): + s.add(AtMost(dji[j] + [1])) + s.add(Or(dji[j])) + for i in range(n-1): + dj = [dji[j][i] for j in range(n-1)] + s.add(AtMost(dj + [1])) + s.add(Or(dj)) + return s, xij + +def process_model(s, xij, n): + # x_ij integer i is at position j + # d_ij difference between integer at position j, j+1 is i + # sum_j d_ij = 1 i = 1,...,n-1 + # sum_j x_ij = 1 + # sum_i x_ij = 1 + m = s.model() + block = [] + values = [] + for i in range(n): + k = -1 + for j in range(n): + if is_true(m.eval(xij[i][j])): + assert(k == -1) + block += [xij[i][j]] + k = j + values += [k] + print values + sys.stdout.flush() + return block + +def all_models(n): + count = 0 + s, xij = ais(n) + start = time.clock() + while sat == s.check(): + block = process_model(s, xij, n) + s.add(Not(And(block))) + count += 1 + print s.statistics() + print time.clock() - start + print count + +set_option(verbose=1) +all_models(12) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 37197e730..5d423c725 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -914,7 +914,7 @@ extern "C" { fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); family_id fid = mk_c(c)->get_fpa_fid(); expr * e = to_expr(t); - if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); return 0; } @@ -933,6 +933,8 @@ extern "C" { Z3_TRY; LOG_Z3_fpa_get_numeral_significand_string(c, t); RESET_ERROR_CODE(); + CHECK_NON_NULL(t, 0); + CHECK_VALID_AST(t, 0); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); @@ -940,10 +942,7 @@ extern "C" { fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); SASSERT(plugin != 0); expr * e = to_expr(t); - if (!is_app(e) || - is_app_of(e, fid, OP_FPA_NAN) || - is_app_of(e, fid, OP_FPA_PLUS_INF) || - is_app_of(e, fid, OP_FPA_MINUS_INF)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } @@ -958,6 +957,7 @@ extern "C" { mpqm.set(q, mpfm.sig(val)); if (!mpfm.is_denormal(val)) mpqm.add(q, mpfm.m_powers2(sbits - 1), q); mpqm.div(q, mpfm.m_powers2(sbits - 1), q); + if (mpfm.is_inf(val)) mpqm.set(q, 0); std::stringstream ss; mpqm.display_decimal(ss, q, sbits); return mk_c(c)->mk_external_string(ss.str()); @@ -975,10 +975,7 @@ extern "C" { fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); SASSERT(plugin != 0); expr * e = to_expr(t); - if (!is_app(e) || - is_app_of(e, fid, OP_FPA_NAN) || - is_app_of(e, fid, OP_FPA_PLUS_INF) || - is_app_of(e, fid, OP_FPA_MINUS_INF)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); *n = 0; return 0; @@ -1008,10 +1005,7 @@ extern "C" { fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0); expr * e = to_expr(t); - if (!is_app(e) || - is_app_of(e, fid, OP_FPA_NAN) || - is_app_of(e, fid, OP_FPA_PLUS_INF) || - is_app_of(e, fid, OP_FPA_MINUS_INF)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); return ""; } @@ -1040,10 +1034,7 @@ extern "C" { fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0); expr * e = to_expr(t); - if (!is_app(e) || - is_app_of(e, fid, OP_FPA_NAN) || - is_app_of(e, fid, OP_FPA_PLUS_INF) || - is_app_of(e, fid, OP_FPA_MINUS_INF)) { + if (!is_app(e) || is_app_of(e, fid, OP_FPA_NAN) || !is_fp(c, t)) { SET_ERROR_CODE(Z3_INVALID_ARG); *n = 0; return 0; diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp index 58d8902c3..308db4081 100644 --- a/src/api/api_opt.cpp +++ b/src/api/api_opt.cpp @@ -27,6 +27,7 @@ Revision History: #include"cancel_eh.h" #include"scoped_timer.h" #include"smt2parser.h" +#include"api_ast_vector.h" extern "C" { @@ -296,6 +297,35 @@ extern "C" { } + Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o) { + Z3_TRY; + LOG_Z3_optimize_get_assertions(c, o); + RESET_ERROR_CODE(); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + expr_ref_vector hard(mk_c(c)->m()); + to_optimize_ptr(o)->get_hard_constraints(hard); + for (unsigned i = 0; i < hard.size(); i++) { + v->m_ast_vector.push_back(hard[i].get()); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + + Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o) { + Z3_TRY; + LOG_Z3_optimize_get_objectives(c, o); + RESET_ERROR_CODE(); + unsigned n = to_optimize_ptr(o)->num_objectives(); + Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); + mk_c(c)->save_object(v); + for (unsigned i = 0; i < n; i++) { + v->m_ast_vector.push_back(to_optimize_ptr(o)->get_objective(i)); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(0); + } + }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b03e38b7e..2a9c771a1 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2053,6 +2053,8 @@ namespace z3 { check_error(); return expr(ctx(), r); } + expr_vector assertions() const { Z3_ast_vector r = Z3_optimize_get_assertions(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); } + expr_vector objectives() const { Z3_ast_vector r = Z3_optimize_get_objectives(ctx(), m_opt); check_error(); return expr_vector(ctx(), r); } stats statistics() const { Z3_stats r = Z3_optimize_get_statistics(ctx(), m_opt); check_error(); return stats(ctx(), r); } friend std::ostream & operator<<(std::ostream & out, optimize const & s); void from_file(char const* filename) { Z3_optimize_from_file(ctx(), m_opt, filename); check_error(); } diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index e5982e4fc..036aaf2f2 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -290,6 +290,33 @@ namespace Microsoft.Z3 Native.Z3_optimize_from_string(Context.nCtx, NativeObject, s); } + /// + /// The set of asserted formulas. + /// + public BoolExpr[] Assertions + { + get + { + Contract.Ensures(Contract.Result() != null); + + ASTVector assertions = new ASTVector(Context, Native.Z3_optimize_get_assertions(Context.nCtx, NativeObject)); + return assertions.ToBoolExprArray(); + } + } + + /// + /// The set of asserted formulas. + /// + public Expr[] Objectives + { + get + { + Contract.Ensures(Contract.Result() != null); + + ASTVector objectives = new ASTVector(Context, Native.Z3_optimize_get_objectives(Context.nCtx, NativeObject)); + return objectives.ToExprArray(); + } + } /// diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index c360a9bdc..a037bbc5d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6796,6 +6796,14 @@ class Optimize(Z3PPObject): """Parse assertions and objectives from a string""" Z3_optimize_from_string(self.ctx.ref(), self.optimize, s) + def assertions(self): + """Return an AST vector containing all added constraints.""" + return AstVector(Z3_optimize_get_assertions(self.ctx.ref(), self.optimize), self.ctx) + + def objectives(self): + """returns set of objective functions""" + return AstVector(Z3_optimize_get_objectives(self.ctx.ref(), self.optimize), self.ctx) + def __repr__(self): """Return a formatted string with all added rules and constraints.""" return self.sexpr() @@ -8496,7 +8504,7 @@ class FPNumRef(FPRef): """ def as_string(self): s = Z3_fpa_get_numeral_string(self.ctx.ref(), self.as_ast()) - return ("FPVal(%s, %s)" % (s, FPSortRef(self.sort()).as_string())) + return ("FPVal(%s, %s)" % (s, self.sort())) def is_fp(a): """Return `True` if `a` is a Z3 floating-point expression. @@ -8536,7 +8544,7 @@ def FPSort(ebits, sbits, ctx=None): >>> eq(x, FP('x', FPSort(8, 24))) True """ - ctx = z3._get_ctx(ctx) + ctx = _get_ctx(ctx) return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx) def _to_float_str(val, exp=0): @@ -8722,7 +8730,7 @@ def FPs(names, fpsort, ctx=None): >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) fpMul(RNE(), fpAdd(RNE(), x, y), z) """ - ctx = z3._get_ctx(ctx) + ctx = _get_ctx(ctx) if isinstance(names, str): names = names.split(" ") return [FP(name, fpsort, ctx) for name in names] diff --git a/src/api/z3_api.h b/src/api/z3_api.h index cd889b3be..9e9771884 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5832,7 +5832,7 @@ extern "C" { void Z3_API Z3_solver_assert_and_track(Z3_context c, Z3_solver s, Z3_ast a, Z3_ast p); /** - \brief Return the set of asserted formulas as a goal object. + \brief Return the set of asserted formulas on the solver. def_API('Z3_solver_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(SOLVER))) */ diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index 15a6dff16..219f3ede8 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -239,6 +239,28 @@ extern "C" { def_API('Z3_optimize_get_statistics', STATS, (_in(CONTEXT), _in(OPTIMIZE))) */ Z3_stats Z3_API Z3_optimize_get_statistics(Z3_context c, Z3_optimize d); + + + /** + \brief Return the set of asserted formulas on the optimization context. + + def_API('Z3_optimize_get_assertions', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE))) + */ + Z3_ast_vector Z3_API Z3_optimize_get_assertions(Z3_context c, Z3_optimize o); + + /** + \brief Return objectives on the optimization context. + If the objective function is a max-sat objective it is returned + as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...) + If the objective function is entered as a maximization objective, then return the corresponding minimizaiton + objective. In this way the resulting objective function is always returned as a minimization objective. + + def_API('Z3_optimize_get_objectives', AST_VECTOR, (_in(CONTEXT), _in(OPTIMIZE))) + */ + Z3_ast_vector Z3_API Z3_optimize_get_objectives(Z3_context c, Z3_optimize o); + + + /*@}*/ /*@}*/ diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 368476b8e..81385c2af 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -162,8 +162,8 @@ bool arith_rewriter::div_polynomial(expr * t, numeral const & g, const_treatment } bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) { - numeral c; - if (!is_add(arg1) && is_numeral(arg2, c)) { + numeral b, c; + if (!is_add(arg1) && !m_util.is_mod(arg1) && is_numeral(arg2, c)) { numeral a; bool r = false; expr * pp = get_power_product(arg1, a); @@ -193,6 +193,45 @@ bool arith_rewriter::is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & case EQ: result = m_util.mk_eq(pp, k); return true; } } + expr* t1, *t2; + bool is_int; + if (m_util.is_mod(arg2)) { + std::swap(arg1, arg2); + switch (kind) { + case LE: kind = GE; break; + case GE: kind = LE; break; + case EQ: break; + } + } + + if (m_util.is_numeral(arg2, c, is_int) && is_int && + m_util.is_mod(arg1, t1, t2) && m_util.is_numeral(t2, b, is_int) && !b.is_zero()) { + // mod x b <= c = false if c < 0, b != 0, true if c >= b, b != 0 + if (c.is_neg()) { + switch (kind) { + case EQ: + case LE: result = m().mk_false(); return true; + case GE: result = m().mk_true(); return true; + } + } + if (c.is_zero() && kind == GE) { + result = m().mk_true(); + return true; + } + if (c.is_pos() && c >= abs(b)) { + switch (kind) { + case LE: result = m().mk_true(); return true; + case EQ: + case GE: result = m().mk_false(); return true; + } + } + // mod x b <= b - 1 + if (c + rational::one() == abs(b) && kind == LE) { + result = m().mk_true(); + return true; + } + } + return false; } diff --git a/src/ast/rewriter/fd_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp similarity index 86% rename from src/ast/rewriter/fd_rewriter.cpp rename to src/ast/rewriter/enum2bv_rewriter.cpp index 026387e22..bbe07f625 100644 --- a/src/ast/rewriter/fd_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation Module Name: - fd_rewriter.cpp + enum2bv_rewriter.cpp Abstract: @@ -19,11 +19,11 @@ Notes: #include"rewriter.h" #include"rewriter_def.h" -#include"fd_rewriter.h" +#include"enum2bv_rewriter.h" #include"ast_util.h" #include"ast_pp.h" -struct fd_rewriter::imp { +struct enum2bv_rewriter::imp { ast_manager& m; params_ref m_params; obj_map m_enum2bv; @@ -258,6 +258,7 @@ struct fd_rewriter::imp { m_enum_defs.resize(lim); m_enum_bvs.resize(lim); } + m_rw.reset(); } void flush_side_constraints(expr_ref_vector& side_constraints) { @@ -275,18 +276,18 @@ struct fd_rewriter::imp { }; -fd_rewriter::fd_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); } -fd_rewriter::~fd_rewriter() { dealloc(m_imp); } -void fd_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); } -ast_manager & fd_rewriter::m() const { return m_imp->m; } -unsigned fd_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } -void fd_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } -obj_map const& fd_rewriter::enum2bv() const { return m_imp->m_enum2bv; } -obj_map const& fd_rewriter::bv2enum() const { return m_imp->m_bv2enum; } -obj_map const& fd_rewriter::enum2def() const { return m_imp->m_enum2def; } -void fd_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); } -void fd_rewriter::push() { m_imp->push(); } -void fd_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } -void fd_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } -unsigned fd_rewriter::num_translated() const { return m_imp->m_num_translated; } -void fd_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); } +enum2bv_rewriter::enum2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); } +enum2bv_rewriter::~enum2bv_rewriter() { dealloc(m_imp); } +void enum2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); } +ast_manager & enum2bv_rewriter::m() const { return m_imp->m; } +unsigned enum2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } +void enum2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } +obj_map const& enum2bv_rewriter::enum2bv() const { return m_imp->m_enum2bv; } +obj_map const& enum2bv_rewriter::bv2enum() const { return m_imp->m_bv2enum; } +obj_map const& enum2bv_rewriter::enum2def() const { return m_imp->m_enum2def; } +void enum2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); } +void enum2bv_rewriter::push() { m_imp->push(); } +void enum2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } +void enum2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } +unsigned enum2bv_rewriter::num_translated() const { return m_imp->m_num_translated; } +void enum2bv_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); } diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp new file mode 100644 index 000000000..0aeeea81a --- /dev/null +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -0,0 +1,453 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + pb2bv_rewriter.cpp + +Abstract: + + Conversion from pseudo-booleans to bit-vectors. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ + +#include"rewriter.h" +#include"rewriter_def.h" +#include"statistics.h" +#include"pb2bv_rewriter.h" +#include"sorting_network.h" +#include"ast_util.h" +#include"ast_pp.h" + + +struct pb2bv_rewriter::imp { + + struct argc_t { + expr* m_arg; + rational m_coeff; + argc_t():m_arg(0), m_coeff(0) {} + argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {} + }; + + struct argc_gt { + bool operator()(argc_t const& a, argc_t const& b) const { + return a.m_coeff > b.m_coeff; + } + }; + + struct argc_entry { + unsigned m_index; + rational m_k; + expr* m_value; + argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {} + argc_entry():m_index(0), m_k(0), m_value(0) {} + + struct eq { + bool operator()(argc_entry const& a, argc_entry const& b) const { + return a.m_index == b.m_index && a.m_k == b.m_k; + } + }; + struct hash { + unsigned operator()(argc_entry const& a) const { + return a.m_index ^ a.m_k.hash(); + } + }; + }; + typedef hashtable argc_cache; + + ast_manager& m; + params_ref m_params; + expr_ref_vector m_lemmas; + func_decl_ref_vector m_fresh; // all fresh variables + unsigned_vector m_fresh_lim; + unsigned m_num_translated; + + struct card2bv_rewriter { + typedef expr* literal; + typedef ptr_vector literal_vector; + psort_nw m_sort; + ast_manager& m; + imp& m_imp; + arith_util au; + pb_util pb; + bv_util bv; + expr_ref_vector m_trail; + + unsigned get_num_bits(func_decl* f) { + rational r(0); + unsigned sz = f->get_arity(); + for (unsigned i = 0; i < sz; ++i) { + r += pb.get_coeff(f, i); + } + r = r > pb.get_k(f)? r : pb.get_k(f); + return r.get_num_bits(); + } + + void mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + + expr_ref zero(m), a(m), b(m); + expr_ref_vector es(m); + unsigned bw = get_num_bits(f); + zero = bv.mk_numeral(rational(0), bw); + for (unsigned i = 0; i < sz; ++i) { + es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero)); + } + switch (es.size()) { + case 0: a = zero; break; + case 1: a = es[0].get(); break; + default: + a = es[0].get(); + for (unsigned i = 1; i < es.size(); ++i) { + a = bv.mk_bv_add(a, es[i].get()); + } + break; + } + b = bv.mk_numeral(pb.get_k(f), bw); + + switch (f->get_decl_kind()) { + case OP_AT_MOST_K: + case OP_PB_LE: + result = bv.mk_ule(a, b); + break; + case OP_AT_LEAST_K: + case OP_PB_GE: + result = bv.mk_ule(b, a); + break; + case OP_PB_EQ: + result = m.mk_eq(a, b); + break; + default: + UNREACHABLE(); + } + TRACE("pb", tout << result << "\n";); + } + + bool mk_shannon(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + decl_kind kind = f->get_decl_kind(); + if (kind != OP_PB_GE && kind != OP_AT_LEAST_K) { + return false; + } + unsigned max_clauses = sz*10; + vector argcs; + for (unsigned i = 0; i < sz; ++i) { + argcs.push_back(argc_t(args[i], pb.get_coeff(f, i))); + } + std::sort(argcs.begin(), argcs.end(), argc_gt()); + DEBUG_CODE( + for (unsigned i = 0; i + 1 < sz; ++i) { + SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff); + }); + result = m.mk_app(f, sz, args); + TRACE("pb", tout << result << "\n";); + argc_cache cache; + expr_ref_vector trail(m); + vector todo_k; + unsigned_vector todo_i; + todo_k.push_back(pb.get_k(f)); + todo_i.push_back(0); + argc_entry entry1; + while (!todo_i.empty()) { + SASSERT(todo_i.size() == todo_k.size()); + if (cache.size() > max_clauses) { + return false; + } + unsigned i = todo_i.back(); + rational k = todo_k.back(); + argc_entry entry(i, k); + if (cache.contains(entry)) { + todo_i.pop_back(); + todo_k.pop_back(); + continue; + } + SASSERT(i < sz); + SASSERT(!k.is_neg()); + rational const& coeff = argcs[i].m_coeff; + expr* arg = argcs[i].m_arg; + if (i + 1 == sz) { + if (k.is_zero()) { + entry.m_value = m.mk_true(); + } + else if (coeff < k) { + entry.m_value = m.mk_false(); + } + else if (coeff.is_zero()) { + entry.m_value = m.mk_true(); + } + else { + SASSERT(coeff >= k && k.is_pos()); + entry.m_value = arg; + } + todo_i.pop_back(); + todo_k.pop_back(); + cache.insert(entry); + continue; + } + entry.m_index++; + expr* lo = 0, *hi = 0; + if (cache.find(entry, entry1)) { + lo = entry1.m_value; + } + else { + todo_i.push_back(i+1); + todo_k.push_back(k); + } + entry.m_k -= coeff; + if (!entry.m_k.is_pos()) { + hi = m.mk_true(); + } + else if (cache.find(entry, entry1)) { + hi = entry1.m_value; + } + else { + todo_i.push_back(i+1); + todo_k.push_back(entry.m_k); + } + if (hi && lo) { + todo_i.pop_back(); + todo_k.pop_back(); + entry.m_index = i; + entry.m_k = k; + entry.m_value = mk_ite(arg, hi, lo); + trail.push_back(entry.m_value); + cache.insert(entry); + } + } + argc_entry entry(0, pb.get_k(f)); + VERIFY(cache.find(entry, entry)); + result = entry.m_value; + TRACE("pb", tout << result << "\n";); + return true; + } + + expr* negate(expr* e) { + if (m.is_not(e, e)) return e; + return m.mk_not(e); + } + expr* mk_ite(expr* c, expr* hi, expr* lo) { + while (m.is_not(c, c)) { + std::swap(hi, lo); + } + if (hi == lo) return hi; + if (m.is_true(hi) && m.is_false(lo)) return c; + if (m.is_false(hi) && m.is_true(lo)) return negate(c); + if (m.is_true(hi)) return m.mk_or(c, lo); + if (m.is_false(lo)) return m.mk_and(c, hi); + if (m.is_false(hi)) return m.mk_and(negate(c), lo); + if (m.is_true(lo)) return m.mk_implies(c, hi); + return m.mk_ite(c, hi, lo); + } + + bool is_or(func_decl* f) { + switch (f->get_decl_kind()) { + case OP_AT_MOST_K: + case OP_PB_LE: + return false; + case OP_AT_LEAST_K: + case OP_PB_GE: + return pb.get_k(f).is_one(); + case OP_PB_EQ: + return false; + default: + UNREACHABLE(); + return false; + } + } + + + public: + + card2bv_rewriter(imp& i, ast_manager& m): + m(m), + m_imp(i), + au(m), + pb(m), + bv(m), + m_sort(*this), + m_trail(m) + {} + + br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + if (f->get_family_id() == pb.get_family_id()) { + mk_pb(f, sz, args, result); + ++m_imp.m_num_translated; + return BR_DONE; + } + else if (f->get_family_id() == au.get_family_id() && mk_arith(f, sz, args, result)) { + ++m_imp.m_num_translated; + return BR_DONE; + } + else { + return BR_FAILED; + } + } + + // + // NSB: review + // we should remove this code and rely on a layer above to deal with + // whatever it accomplishes. It seems to break types. + // + bool mk_arith(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + if (f->get_decl_kind() == OP_ADD) { + unsigned bits = 0; + for (unsigned i = 0; i < sz; i++) { + rational val1, val2; + if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) { + bits += val1.get_num_bits(); + } + else if (m.is_ite(args[i]) && + au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() && + au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) { + bits++; + } + else + return false; + } + + result = 0; + for (unsigned i = 0; i < sz; i++) { + rational val1, val2; + expr * q; + if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) + q = bv.mk_numeral(val1, bits); + else + q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits)); + result = (i == 0) ? q : bv.mk_bv_add(result.get(), q); + } + return true; + } + else { + return false; + } + } + + void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { + SASSERT(f->get_family_id() == pb.get_family_id()); + if (is_or(f)) { + result = m.mk_or(sz, args); + } + else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) { + result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args); + } + else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) { + result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args); + } + else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { + result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args); + } + else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { + result = m_sort.le(true, pb.get_k(f).get_unsigned(), sz, args); + } + else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { + result = m_sort.ge(true, pb.get_k(f).get_unsigned(), sz, args); + } + else if (!mk_shannon(f, sz, args, result)) { + mk_bv(f, sz, args, result); + } + } + + // definitions used for sorting network + literal mk_false() { return m.mk_false(); } + literal mk_true() { return m.mk_true(); } + literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); } + literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); } + literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); } + + std::ostream& pp(std::ostream& out, literal lit) { return out << mk_ismt2_pp(lit, m); } + + literal trail(literal l) { + m_trail.push_back(l); + return l; + } + literal fresh() { + expr_ref fr(m.mk_fresh_const("sn", m.mk_bool_sort()), m); + m_imp.m_fresh.push_back(to_app(fr)->get_decl()); + return trail(fr); + } + + void mk_clause(unsigned n, literal const* lits) { + m_imp.m_lemmas.push_back(mk_or(m, n, lits)); + } + }; + + struct card2bv_rewriter_cfg : public default_rewriter_cfg { + card2bv_rewriter m_r; + bool rewrite_patterns() const { return false; } + bool flat_assoc(func_decl * f) const { return false; } + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + result_pr = 0; + return m_r.mk_app_core(f, num, args, result); + } + card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {} + }; + + class card_pb_rewriter : public rewriter_tpl { + public: + card2bv_rewriter_cfg m_cfg; + card_pb_rewriter(imp& i, ast_manager & m): + rewriter_tpl(m, false, m_cfg), + m_cfg(i, m) {} + }; + + card_pb_rewriter m_rw; + + imp(ast_manager& m, params_ref const& p): + m(m), m_params(p), m_lemmas(m), + m_fresh(m), + m_num_translated(0), + m_rw(*this, m) { + } + + void updt_params(params_ref const & p) {} + unsigned get_num_steps() const { return m_rw.get_num_steps(); } + void cleanup() { m_rw.cleanup(); } + void operator()(expr * e, expr_ref & result, proof_ref & result_proof) { + m_rw(e, result, result_proof); + } + void push() { + m_fresh_lim.push_back(m_fresh.size()); + } + void pop(unsigned num_scopes) { + SASSERT(m_lemmas.empty()); // lemmas must be flushed before pop. + if (num_scopes > 0) { + SASSERT(num_scopes <= m_fresh_lim.size()); + unsigned new_sz = m_fresh_lim.size() - num_scopes; + unsigned lim = m_fresh_lim[new_sz]; + m_fresh.resize(lim); + m_fresh_lim.resize(new_sz); + } + m_rw.reset(); + } + + void flush_side_constraints(expr_ref_vector& side_constraints) { + side_constraints.append(m_lemmas); + m_lemmas.reset(); + } + + void collect_statistics(statistics & st) const { + st.update("pb-aux-variables", m_fresh.size()); + st.update("pb-aux-clauses", m_rw.m_cfg.m_r.m_sort.m_stats.m_num_compiled_clauses); + } + +}; + + +pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); } +pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); } +void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); } +ast_manager & pb2bv_rewriter::m() const { return m_imp->m; } +unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } +void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } +func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; } +void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); } +void pb2bv_rewriter::push() { m_imp->push(); } +void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } +void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } +unsigned pb2bv_rewriter::num_translated() const { return m_imp->m_num_translated; } + +void pb2bv_rewriter::collect_statistics(statistics & st) const { m_imp->collect_statistics(st); } diff --git a/src/ast/rewriter/fd_rewriter.h b/src/ast/rewriter/pb2bv_rewriter.h similarity index 52% rename from src/ast/rewriter/fd_rewriter.h rename to src/ast/rewriter/pb2bv_rewriter.h index 3d4ecae9c..47d8361cb 100644 --- a/src/ast/rewriter/fd_rewriter.h +++ b/src/ast/rewriter/pb2bv_rewriter.h @@ -3,46 +3,44 @@ Copyright (c) 2016 Microsoft Corporation Module Name: - fd_rewriter.h + pb2bv_rewriter.h Abstract: - Conversion from enumeration types to bit-vectors. + Conversion from pseudo-booleans to bit-vectors. Author: - Nikolaj Bjorner (nbjorner) 2016-10-18 + Nikolaj Bjorner (nbjorner) 2016-10-23 Notes: --*/ -#ifndef ENUM_REWRITER_H_ -#define ENUM_REWRITER_H_ +#ifndef PB2BV_REWRITER_H_ +#define PB2BV_REWRITER_H_ -#include"datatype_decl_plugin.h" +#include"pb_decl_plugin.h" #include"rewriter_types.h" #include"expr_functors.h" -class fd_rewriter { +class pb2bv_rewriter { struct imp; imp* m_imp; public: - fd_rewriter(ast_manager & m, params_ref const& p); - ~fd_rewriter(); + pb2bv_rewriter(ast_manager & m, params_ref const& p); + ~pb2bv_rewriter(); void updt_params(params_ref const & p); ast_manager & m() const; unsigned get_num_steps() const; void cleanup(); - obj_map const& enum2bv() const; - obj_map const& bv2enum() const; - obj_map const& enum2def() const; + func_decl_ref_vector const& fresh_constants() const; void operator()(expr * e, expr_ref & result, proof_ref & result_proof); void push(); void pop(unsigned num_scopes); void flush_side_constraints(expr_ref_vector& side_constraints); unsigned num_translated() const; - void set_is_fd(i_sort_pred* sp) const; + void collect_statistics(statistics & st) const; }; #endif diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index d233604f9..0fdbc858d 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -257,7 +257,12 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons all_unit &= m_coeffs.back().is_one(); } if (is_eq) { - result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k); + if (sz == 0) { + result = k.is_zero()?m.mk_true():m.mk_false(); + } + else { + result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k); + } } else if (all_unit && k.is_one()) { result = mk_or(m, sz, m_args.c_ptr()); diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 7a49f8fd0..d9fe9ab72 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -182,8 +182,8 @@ struct check_logic::imp { m_quantifiers = false; } else if (logic == "QF_FD") { - m_bvs = true; - m_uf = true; + m_bvs = true; + m_uf = true; m_ints = true; } else { diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 1df28b8e5..b7c80f65a 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -547,6 +547,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const { s == "QF_BVFP" || s == "QF_S" || s == "ALL" || + s == "QF_FD" || s == "HORN"; } diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index d9f060784..d8b166924 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -297,12 +297,16 @@ public: sort_assumptions(mutex); ptr_vector core(mutex.size(), mutex.c_ptr()); remove_soft(core, m_asms); - rational weight(0); + rational weight(0), sum1(0), sum2(0); + for (unsigned i = 0; i < mutex.size(); ++i) { + sum1 += get_weight(mutex[i].get()); + } while (!mutex.empty()) { expr_ref soft = mk_or(mutex); rational w = get_weight(mutex.back()); weight = w - weight; m_lower += weight*rational(mutex.size()-1); + sum2 += weight*rational(mutex.size()); add_soft(soft, weight); mutex.pop_back(); while (!mutex.empty() && get_weight(mutex.back()) == w) { @@ -310,6 +314,7 @@ public: } weight = w; } + SASSERT(sum1 == sum2); } lbool check_sat_hill_climb(expr_ref_vector& asms1) { @@ -398,7 +403,7 @@ public: while (is_sat == l_false) { core.reset(); s().get_unsat_core(core); - //verify_core(core); + // verify_core(core); model_ref mdl; get_mus_model(mdl); is_sat = minimize_core(core); @@ -772,8 +777,6 @@ public: for (unsigned i = 0; i < m_soft.size(); ++i) { m_assignment[i] = is_true(m_soft[i]); } - - DEBUG_CODE(verify_assignment();); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 07bb8385b..1335685ff 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -181,6 +181,43 @@ namespace opt { clear_state(); } + void context::get_hard_constraints(expr_ref_vector& hard) { + hard.append(m_scoped_state.m_hard); + } + + expr_ref context::get_objective(unsigned i) { + SASSERT(i < num_objectives()); + objective const& o = m_scoped_state.m_objectives[i]; + expr_ref result(m), zero(m); + expr_ref_vector args(m); + switch (o.m_type) { + case O_MAXSMT: + zero = m_arith.mk_numeral(rational(0), false); + for (unsigned i = 0; i < o.m_terms.size(); ++i) { + args.push_back(m.mk_ite(o.m_terms[i], zero, m_arith.mk_numeral(o.m_weights[i], false))); + } + result = m_arith.mk_add(args.size(), args.c_ptr()); + break; + case O_MAXIMIZE: + result = o.m_term; + if (m_arith.is_arith_expr(result)) { + result = m_arith.mk_uminus(result); + } + else if (m_bv.is_bv(result)) { + result = m_bv.mk_bv_neg(result); + } + else { + UNREACHABLE(); + } + break; + case O_MINIMIZE: + result = o.m_term; + break; + } + return result; + } + + unsigned context::add_soft_constraint(expr* f, rational const& w, symbol const& id) { clear_state(); return m_scoped_state.add(f, w, id); @@ -1328,14 +1365,21 @@ namespace opt { } std::string context::to_string() const { + return to_string(m_scoped_state.m_hard, m_scoped_state.m_objectives); + } + + std::string context::to_string_internal() const { + return to_string(m_hard_constraints, m_objectives); + } + + std::string context::to_string(expr_ref_vector const& hard, vector const& objectives) const { smt2_pp_environment_dbg env(m); ast_pp_util visitor(m); std::ostringstream out; -#define PP(_e_) ast_smt2_pp(out, _e_, env); - visitor.collect(m_scoped_state.m_hard); + visitor.collect(hard); - for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { - objective const& obj = m_scoped_state.m_objectives[i]; + for (unsigned i = 0; i < objectives.size(); ++i) { + objective const& obj = objectives[i]; switch(obj.m_type) { case O_MAXIMIZE: case O_MINIMIZE: @@ -1351,33 +1395,34 @@ namespace opt { } visitor.display_decls(out); - visitor.display_asserts(out, m_scoped_state.m_hard, m_pp_neat); - for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { - objective const& obj = m_scoped_state.m_objectives[i]; + visitor.display_asserts(out, hard, m_pp_neat); + for (unsigned i = 0; i < objectives.size(); ++i) { + objective const& obj = objectives[i]; switch(obj.m_type) { case O_MAXIMIZE: out << "(maximize "; - PP(obj.m_term); + ast_smt2_pp(out, obj.m_term, env); out << ")\n"; break; case O_MINIMIZE: out << "(minimize "; - PP(obj.m_term); + ast_smt2_pp(out, obj.m_term, env); out << ")\n"; break; case O_MAXSMT: for (unsigned j = 0; j < obj.m_terms.size(); ++j) { out << "(assert-soft "; - PP(obj.m_terms[j]); + ast_smt2_pp(out, obj.m_terms[j], env); rational w = obj.m_weights[j]; - if (w.is_int()) { - out << " :weight " << w; - } - else { - out << " :dweight " << w; - } + + w.display_decimal(out << " :weight ", 3, true); if (obj.m_id != symbol::null) { - out << " :id " << obj.m_id; + if (is_smt2_quoted_symbol(obj.m_id)) { + out << " :id " << mk_smt2_quoted_symbol(obj.m_id); + } + else { + out << " :id " << obj.m_id; + } } out << ")\n"; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index ac1fe8e7a..18af756bf 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -175,6 +175,8 @@ namespace opt { unsigned add_objective(app* t, bool is_max); void add_hard_constraint(expr* f); + void get_hard_constraints(expr_ref_vector& hard); + expr_ref get_objective(unsigned i); virtual void push(); virtual void pop(unsigned n); @@ -208,7 +210,7 @@ namespace opt { std::string to_string() const; - virtual unsigned num_objectives() { return m_objectives.size(); } + virtual unsigned num_objectives() { return m_scoped_state.m_objectives.size(); } virtual expr_ref mk_gt(unsigned i, model_ref& model); virtual expr_ref mk_ge(unsigned i, model_ref& model); virtual expr_ref mk_le(unsigned i, model_ref& model); @@ -284,6 +286,9 @@ namespace opt { void display_objective(std::ostream& out, objective const& obj) const; void display_bounds(std::ostream& out, bounds_t const& b) const; + std::string to_string(expr_ref_vector const& hard, vector const& objectives) const; + std::string to_string_internal() const; + void validate_lex(); diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h index 17c5a51bf..5b7f630b4 100644 --- a/src/opt/opt_sls_solver.h +++ b/src/opt/opt_sls_solver.h @@ -90,19 +90,6 @@ namespace opt { virtual void get_labels(svector & r) { m_solver->get_labels(r); } - virtual void set_cancel(bool f) { - m_solver->set_cancel(f); - m_pb2bv.set_cancel(f); - #pragma omp critical (sls_solver) - { - if (m_bvsls) { - m_bvsls->set_cancel(f); - } - if (m_pbsls) { - m_pbsls->set_cancel(f); - } - } - } virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } @@ -203,14 +190,11 @@ namespace opt { } void pbsls_opt(model_ref& mdl) { - #pragma omp critical (sls_solver) - { - if (m_pbsls) { - m_pbsls->reset(); - } - else { - m_pbsls = alloc(smt::pb_sls, m); - } + if (m_pbsls) { + m_pbsls->reset(); + } + else { + m_pbsls = alloc(smt::pb_sls, m); } m_pbsls->set_model(mdl); m_pbsls->updt_params(m_params); @@ -226,10 +210,7 @@ namespace opt { } void bvsls_opt(model_ref& mdl) { - #pragma omp critical (sls_solver) - { - m_bvsls = alloc(bvsls_opt_engine, m, m_params); - } + m_bvsls = alloc(bvsls_opt_engine, m, m_params); assertions2sls(); expr_ref objective = soft2bv(m_soft, m_weights); TRACE("opt", tout << objective << "\n";); diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index e44782a31..ef90aac4c 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -373,7 +373,7 @@ namespace smt { expr* n = vars[i]; bool neg = m_manager.is_not(n, n); if (b_internalized(n)) { - lits.insert(literal(get_bool_var(n), !neg).index()); + lits.insert(literal(get_bool_var(n), neg).index()); } } while (!lits.empty()) { diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index d4880f7d7..94ce453b4 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1281,7 +1281,7 @@ namespace smt { The deletion event handler is ignored if binary clause optimization is applicable. */ clause * context::mk_clause(unsigned num_lits, literal * lits, justification * j, clause_kind k, clause_del_eh * del_eh) { - TRACE("mk_clause", tout << "creating clause:\n"; display_literals(tout, num_lits, lits); tout << "\n";); + TRACE("mk_clause", tout << "creating clause:\n"; display_literals_verbose(tout, num_lits, lits); tout << "\n";); switch (k) { case CLS_AUX: { literal_buffer simp_lits; diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 3819f05cb..df39b4186 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -222,6 +222,12 @@ namespace smt { m_imp->assert_expr(e); } + void kernel::assert_expr(expr_ref_vector const& es) { + for (unsigned i = 0; i < es.size(); ++i) { + m_imp->assert_expr(es[i]); + } + } + void kernel::assert_expr(expr * e, proof * pr) { m_imp->assert_expr(e, pr); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index 0fec4a21b..ea09081ec 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -70,7 +70,8 @@ namespace smt { This method uses the "asserted" proof as a justification for e. */ void assert_expr(expr * e); - + + void assert_expr(expr_ref_vector const& es); /** \brief Assert the given assertion with the given proof as a justification. */ diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 163452d47..d2db3a603 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1709,7 +1709,7 @@ namespace smt { SASSERT(!maintain_integrality || valid_assignment()); SASSERT(satisfy_bounds()); } - TRACE("opt", display(tout);); + TRACE("opt_verbose", display(tout);); return (best_efforts>0 || ctx.get_cancel_flag())?BEST_EFFORT:result; } diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index d3b1f0f10..c06f82c8b 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -1385,7 +1385,7 @@ namespace smt { m_branch_cut_counter++; // TODO: add giveup code if (m_branch_cut_counter % m_params.m_arith_branch_cut_ratio == 0) { - TRACE("opt", display(tout);); + TRACE("opt_verbose", display(tout);); move_non_base_vars_to_bounds(); if (!make_feasible()) { TRACE("arith_int", tout << "failed to move variables to bounds.\n";); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index d47ecaa4e..dd91ffbfb 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -704,8 +704,8 @@ namespace smt { bool bounded = false; unsigned n = 0; numeral range; - for (unsigned i = 0; i < m_nl_monomials.size(); i++) { - theory_var v = m_nl_monomials[i]; + for (unsigned j = 0; j < m_nl_monomials.size(); ++j) { + theory_var v = m_nl_monomials[j]; if (is_real(v)) continue; bool computed_epsilon = false; @@ -2336,8 +2336,8 @@ namespace smt { bool theory_arith::max_min_nl_vars() { var_set already_found; svector vars; - for (unsigned i = 0; i < m_nl_monomials.size(); i++) { - theory_var v = m_nl_monomials[i]; + for (unsigned j = 0; j < m_nl_monomials.size(); ++j) { + theory_var v = m_nl_monomials[j]; mark_var(v, vars, already_found); expr * n = var2expr(v); SASSERT(is_pure_monomial(n)); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 5273e6b66..d4f7bf30e 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -321,7 +321,8 @@ namespace smt { if (m_simplex.upper_valid(v)) { m_simplex.get_upper(v, last_bound); if (m_mpq_inf_mgr.gt(bound, last_bound)) { - literal lit = m_explain_upper.get(v, null_literal); + literal lit = m_explain_upper.get(v, null_literal); + TRACE("pb", tout << ~lit << " " << ~explain << "\n";); get_context().mk_clause(~lit, ~explain, justify(~lit, ~explain)); return false; } @@ -342,6 +343,7 @@ namespace smt { m_simplex.get_lower(v, last_bound); if (m_mpq_inf_mgr.gt(last_bound, bound)) { literal lit = m_explain_lower.get(v, null_literal); + TRACE("pb", tout << ~lit << " " << ~explain << "\n";); get_context().mk_clause(~lit, ~explain, justify(~lit, ~explain)); return false; } @@ -405,6 +407,7 @@ namespace smt { if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); } + TRACE("pb", tout << lits << "\n";); ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); return false; @@ -515,11 +518,10 @@ namespace smt { ++log; n *= 2; } - unsigned th = args.size()*log; // 10* + unsigned th = args.size()*log; c->m_compilation_threshold = th; - IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threhshold to " << th << ")\n";); + IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threshold to " << th << ")\n";); TRACE("pb", tout << "compilation threshold: " << th << "\n";); - //compile_ineq(*c); } else { c->m_compilation_threshold = UINT_MAX; @@ -1247,9 +1249,9 @@ namespace smt { literal_vector in; for (unsigned i = 0; i < num_args; ++i) { rational n = c.coeff(i); - lbool val = ctx.get_assignment(c.lit()); - if (val != l_undef && - ctx.get_assign_level(thl) == ctx.get_base_level()) { + literal lit = c.lit(i); + lbool val = ctx.get_assignment(lit); + if (val != l_undef && ctx.get_assign_level(lit) == ctx.get_base_level()) { if (val == l_true) { unsigned m = n.get_unsigned(); if (k < m) { @@ -1264,38 +1266,35 @@ namespace smt { n -= rational::one(); } } + + TRACE("pb", tout << in << " >= " << k << "\n";); - unsigned num_compiled_vars, num_compiled_clauses; + + psort_expr ps(ctx, *this); + psort_nw sortnw(ps); + sortnw.m_stats.reset(); if (ctx.get_assignment(thl) == l_true && ctx.get_assign_level(thl) == ctx.get_base_level()) { - psort_expr ps(ctx, *this); - psort_nw sortnw(ps); - sortnw.m_stats.reset(); at_least_k = sortnw.ge(false, k, in.size(), in.c_ptr()); + TRACE("pb", tout << ~thl << " " << at_least_k << "\n";); ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k)); - num_compiled_vars = sortnw.m_stats.m_num_compiled_vars; - num_compiled_clauses = sortnw.m_stats.m_num_compiled_clauses; } else { - psort_expr ps(ctx, *this); - psort_nw sortnw(ps); - sortnw.m_stats.reset(); literal at_least_k = sortnw.ge(true, k, in.size(), in.c_ptr()); + TRACE("pb", tout << ~thl << " " << at_least_k << "\n";); ctx.mk_clause(~thl, at_least_k, justify(~thl, at_least_k)); ctx.mk_clause(~at_least_k, thl, justify(thl, ~at_least_k)); - num_compiled_vars = sortnw.m_stats.m_num_compiled_vars; - num_compiled_clauses = sortnw.m_stats.m_num_compiled_clauses; } - m_stats.m_num_compiled_vars += num_compiled_vars; - m_stats.m_num_compiled_clauses += num_compiled_clauses; + m_stats.m_num_compiled_vars += sortnw.m_stats.m_num_compiled_vars; + m_stats.m_num_compiled_clauses += sortnw.m_stats.m_num_compiled_clauses; + IF_VERBOSE(1, verbose_stream() << "(smt.pb compile sorting network bound: " << k << " literals: " << in.size() << " clauses: " << num_compiled_clauses << " vars: " << num_compiled_vars << ")\n";); - TRACE("pb", tout << thl << "\n";); // auxiliary clauses get removed when popping scopes. // we have to recompile the circuit after back-tracking. c.m_compiled = l_false; @@ -1305,7 +1304,6 @@ namespace smt { void theory_pb::init_search_eh() { - m_to_compile.reset(); } void theory_pb::push_scope_eh() { @@ -1334,6 +1332,7 @@ namespace smt { m_ineq_rep.erase(r_info.m_rep); } } + m_to_compile.erase(c); dealloc(c); } m_ineqs_lim.resize(new_lim); @@ -1459,6 +1458,7 @@ namespace smt { if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); } + TRACE("pb", tout << lits << "\n";); ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); } @@ -1765,6 +1765,7 @@ namespace smt { for (unsigned i = 0; i < m_ineq_literals.size(); ++i) { m_ineq_literals[i].neg(); } + TRACE("pb", tout << m_ineq_literals << "\n";); ctx.mk_clause(m_ineq_literals.size(), m_ineq_literals.c_ptr(), justify(m_ineq_literals), CLS_AUX_LEMMA, 0); break; default: { diff --git a/src/tactic/arith/bv2int_rewriter.h b/src/tactic/arith/bv2int_rewriter.h index 0f68257f1..15a425857 100644 --- a/src/tactic/arith/bv2int_rewriter.h +++ b/src/tactic/arith/bv2int_rewriter.h @@ -34,7 +34,7 @@ class bv2int_rewriter_ctx { public: bv2int_rewriter_ctx(ast_manager& m, params_ref const& p) : - m_side_conditions(m), m_trail(m) { update_params(p); } + m_max_size(UINT_MAX), m_side_conditions(m), m_trail(m) { update_params(p); } void reset() { m_side_conditions.reset(); m_trail.reset(); m_power2.reset(); } void add_side_condition(expr* e) { m_side_conditions.push_back(e); } diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp index 5019b6550..096e52981 100644 --- a/src/tactic/arith/card2bv_tactic.cpp +++ b/src/tactic/arith/card2bv_tactic.cpp @@ -18,500 +18,22 @@ Notes: --*/ #include"tactical.h" #include"cooperate.h" -#include"rewriter_def.h" #include"ast_smt2_pp.h" -#include"expr_substitution.h" #include"card2bv_tactic.h" -#include"pb_rewriter.h" +#include"pb2bv_rewriter.h" #include"ast_util.h" #include"ast_pp.h" - -namespace pb { - unsigned card2bv_rewriter::get_num_bits(func_decl* f) { - rational r(0); - unsigned sz = f->get_arity(); - for (unsigned i = 0; i < sz; ++i) { - r += pb.get_coeff(f, i); - } - r = r > pb.get_k(f)? r : pb.get_k(f); - return r.get_num_bits(); - } - - card2bv_rewriter::card2bv_rewriter(ast_manager& m): - m(m), - au(m), - pb(m), - bv(m), - m_sort(*this), - m_lemmas(m), - m_trail(m) - {} - - void card2bv_rewriter::mk_assert(func_decl * f, unsigned sz, expr * const* args, expr_ref & result, expr_ref_vector& lemmas) { - m_lemmas.reset(); - SASSERT(f->get_family_id() == pb.get_family_id()); - if (is_or(f)) { - result = m.mk_or(sz, args); - } - else if (is_and(f)) { - result = m.mk_and(sz, args); - } - else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - result = m_sort.eq(pb.get_k(f).get_unsigned(), sz, args); - } - else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - result = m_sort.le(false, pb.get_k(f).get_unsigned(), sz, args); - } - else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) { - result = m_sort.ge(false, pb.get_k(f).get_unsigned(), sz, args); - } - else { - br_status st = mk_shannon(f, sz, args, result); - if (st == BR_FAILED) { - mk_bv(f, sz, args, result); - } - } - lemmas.append(m_lemmas); - } - - std::ostream& card2bv_rewriter::pp(std::ostream& out, literal lit) { - return out << mk_ismt2_pp(lit, m); - } - - card2bv_rewriter::literal card2bv_rewriter::trail(literal l) { - m_trail.push_back(l); - return l; - } - card2bv_rewriter::literal card2bv_rewriter::fresh() { - return trail(m.mk_fresh_const("sn", m.mk_bool_sort())); - } - - void card2bv_rewriter::mk_clause(unsigned n, literal const* lits) { - m_lemmas.push_back(mk_or(m, n, lits)); - } - - - br_status card2bv_rewriter::mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { - if (f->get_family_id() == null_family_id) { - if (sz == 1) { - // Expecting minimize/maximize. - func_decl_ref fd(m); - fd = m.mk_func_decl(f->get_name(), m.get_sort(args[0]), f->get_range()); - result = m.mk_app(fd.get(), args[0]); - return BR_DONE; - } - else - return BR_FAILED; - } - else if (f->get_family_id() == m.get_basic_family_id()) { - result = m.mk_app(f, sz, args); - return BR_DONE; - } - else if (f->get_family_id() == pb.get_family_id()) { - if (is_or(f)) { - result = m.mk_or(sz, args); - return BR_DONE; - } - if (is_and(f)) { - result = m.mk_and(sz, args); - return BR_DONE; - } - if (is_atmost1(f, sz, args, result)) { - return BR_DONE; - } - br_status st = mk_shannon(f, sz, args, result); - if (st == BR_FAILED) { - mk_bv(f, sz, args, result); - return BR_DONE; - } - else { - return st; - } - } - // NSB: review - // we should remove this code and rely on a layer above to deal with - // whatever it accomplishes. It seems to break types. - // - else if (f->get_family_id() == au.get_family_id()) { - if (f->get_decl_kind() == OP_ADD) { - unsigned bits = 0; - for (unsigned i = 0; i < sz; i++) { - rational val1, val2; - if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) { - bits += val1.get_num_bits(); - } - else if (m.is_ite(args[i]) && - au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() && - au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) { - bits++; - } - else - return BR_FAILED; - } - - result = 0; - for (unsigned i = 0; i < sz; i++) { - rational val1, val2; - expr * q; - if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) - q = bv.mk_numeral(val1, bits); - else - q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits)); - result = (i == 0) ? q : bv.mk_bv_add(result.get(), q); - } - return BR_DONE; - } - else - return BR_FAILED; - } - else - return BR_FAILED; - } - - expr_ref card2bv_rewriter::mk_atmost1(unsigned n, expr * const* xs) { - expr_ref_vector result(m), in(m); - in.append(n, xs); - unsigned inc_size = 4; - while (!in.empty()) { - expr_ref_vector ors(m); - unsigned i = 0; - unsigned n = in.size(); - bool last = n <= inc_size; - for (; i + inc_size < n; i += inc_size) { - mk_at_most_1_small(last, inc_size, in.c_ptr() + i, result, ors); - } - if (i < n) { - mk_at_most_1_small(last, n - i, in.c_ptr() + i, result, ors); - } - if (last) { - break; - } - in.reset(); - in.append(ors); - } - return mk_and(result); - } - - void card2bv_rewriter::mk_at_most_1_small(bool last, unsigned n, literal const* xs, expr_ref_vector& result, expr_ref_vector& ors) { - if (!last) { - ors.push_back(m.mk_or(n, xs)); - } - for (unsigned i = 0; i < n; ++i) { - for (unsigned j = i + 1; j < n; ++j) { - result.push_back(m.mk_not(m.mk_and(xs[i], xs[j]))); - } - } - } - - bool card2bv_rewriter::is_atmost1(func_decl* f, unsigned sz, expr * const* args, expr_ref& result) { - switch (f->get_decl_kind()) { - case OP_AT_MOST_K: - case OP_PB_LE: - if (pb.get_k(f).is_one() && pb.has_unit_coefficients(f)) { - result = mk_atmost1(sz, args); - return true; - } - return false; - case OP_AT_LEAST_K: - case OP_PB_GE: - if (pb.get_k(f) == rational(sz-1) && pb.has_unit_coefficients(f)) { - expr_ref_vector nargs(m); - for (unsigned i = 0; i < sz; ++i) { - nargs.push_back(mk_not(args[i])); - } - result = mk_atmost1(nargs.size(), nargs.c_ptr()); - return true; - } - return false; - case OP_PB_EQ: - return false; - default: - UNREACHABLE(); - return false; - } - } - - bool card2bv_rewriter::is_or(func_decl* f) { - switch (f->get_decl_kind()) { - case OP_AT_MOST_K: - case OP_PB_LE: - return false; - case OP_AT_LEAST_K: - case OP_PB_GE: - return pb.get_k(f).is_one(); - case OP_PB_EQ: - return false; - default: - UNREACHABLE(); - return false; - } - } - - bool card2bv_rewriter::is_and(func_decl* f) { - return false; - } - - void card2bv_rewriter::mk_bv(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { - expr_ref zero(m), a(m), b(m); - expr_ref_vector es(m); - unsigned bw = get_num_bits(f); - zero = bv.mk_numeral(rational(0), bw); - for (unsigned i = 0; i < sz; ++i) { - es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), bw), zero)); - } - switch (es.size()) { - case 0: a = zero; break; - case 1: a = es[0].get(); break; - default: - a = es[0].get(); - for (unsigned i = 1; i < es.size(); ++i) { - a = bv.mk_bv_add(a, es[i].get()); - } - break; - } - b = bv.mk_numeral(pb.get_k(f), bw); - - switch (f->get_decl_kind()) { - case OP_AT_MOST_K: - case OP_PB_LE: - UNREACHABLE(); - result = bv.mk_ule(a, b); - break; - case OP_AT_LEAST_K: - UNREACHABLE(); - case OP_PB_GE: - result = bv.mk_ule(b, a); - break; - case OP_PB_EQ: - result = m.mk_eq(a, b); - break; - default: - UNREACHABLE(); - } - TRACE("card2bv", tout << result << "\n";); - } - - struct argc_t { - expr* m_arg; - rational m_coeff; - argc_t():m_arg(0), m_coeff(0) {} - argc_t(expr* arg, rational const& r): m_arg(arg), m_coeff(r) {} - }; - struct argc_gt { - bool operator()(argc_t const& a, argc_t const& b) const { - return a.m_coeff > b.m_coeff; - } - }; - struct argc_entry { - unsigned m_index; - rational m_k; - expr* m_value; - argc_entry(unsigned i, rational const& k): m_index(i), m_k(k), m_value(0) {} - argc_entry():m_index(0), m_k(0), m_value(0) {} - - struct eq { - bool operator()(argc_entry const& a, argc_entry const& b) const { - return a.m_index == b.m_index && a.m_k == b.m_k; - } - }; - struct hash { - unsigned operator()(argc_entry const& a) const { - return a.m_index ^ a.m_k.hash(); - } - }; - }; - typedef hashtable argc_cache; - - br_status card2bv_rewriter::mk_shannon( - func_decl * f, unsigned sz, expr * const* args, expr_ref & result) { - - unsigned max_clauses = sz*10; - vector argcs; - for (unsigned i = 0; i < sz; ++i) { - argcs.push_back(argc_t(args[i], pb.get_coeff(f, i))); - } - std::sort(argcs.begin(), argcs.end(), argc_gt()); - DEBUG_CODE( - for (unsigned i = 0; i + 1 < sz; ++i) { - SASSERT(argcs[i].m_coeff >= argcs[i+1].m_coeff); - } - ); - result = m.mk_app(f, sz, args); - TRACE("card2bv", tout << result << "\n";); - argc_cache cache; - expr_ref_vector trail(m); - vector todo_k; - unsigned_vector todo_i; - todo_k.push_back(pb.get_k(f)); - todo_i.push_back(0); - decl_kind kind = f->get_decl_kind(); - argc_entry entry1; - while (!todo_i.empty()) { - SASSERT(todo_i.size() == todo_k.size()); - if (cache.size() > max_clauses) { - return BR_FAILED; - } - unsigned i = todo_i.back(); - rational k = todo_k.back(); - argc_entry entry(i, k); - if (cache.contains(entry)) { - todo_i.pop_back(); - todo_k.pop_back(); - continue; - } - SASSERT(i < sz); - SASSERT(!k.is_neg()); - rational const& coeff = argcs[i].m_coeff; - expr* arg = argcs[i].m_arg; - if (i + 1 == sz) { - switch(kind) { - case OP_AT_MOST_K: - case OP_PB_LE: - if (coeff <= k) { - entry.m_value = m.mk_true(); - } - else { - entry.m_value = negate(arg); - trail.push_back(entry.m_value); - } - break; - case OP_AT_LEAST_K: - case OP_PB_GE: - if (k.is_zero()) { - entry.m_value = m.mk_true(); - } - else if (coeff < k) { - entry.m_value = m.mk_false(); - } - else if (coeff.is_zero()) { - entry.m_value = m.mk_true(); - } - else { - SASSERT(coeff >= k && k.is_pos()); - entry.m_value = arg; - } - break; - case OP_PB_EQ: - if (coeff == k) { - entry.m_value = arg; - } - else if (k.is_zero()) { - entry.m_value = negate(arg); - trail.push_back(entry.m_value); - } - else { - entry.m_value = m.mk_false(); - } - break; - } - todo_i.pop_back(); - todo_k.pop_back(); - cache.insert(entry); - continue; - } - entry.m_index++; - expr* lo = 0, *hi = 0; - if (cache.find(entry, entry1)) { - lo = entry1.m_value; - } - else { - todo_i.push_back(i+1); - todo_k.push_back(k); - } - entry.m_k -= coeff; - if (kind != OP_PB_EQ && !entry.m_k.is_pos()) { - switch (kind) { - case OP_AT_MOST_K: - case OP_PB_LE: - hi = m.mk_false(); - break; - case OP_AT_LEAST_K: - case OP_PB_GE: - hi = m.mk_true(); - break; - default: - UNREACHABLE(); - } - } - else if (cache.find(entry, entry1)) { - hi = entry1.m_value; - } - else { - todo_i.push_back(i+1); - todo_k.push_back(entry.m_k); - } - if (hi && lo) { - todo_i.pop_back(); - todo_k.pop_back(); - entry.m_index = i; - entry.m_k = k; - entry.m_value = mk_ite(arg, hi, lo); - trail.push_back(entry.m_value); - cache.insert(entry); - } - } - argc_entry entry(0, pb.get_k(f)); - VERIFY(cache.find(entry, entry)); - result = entry.m_value; - TRACE("card2bv", tout << result << "\n";); - return BR_DONE; - } - - expr* card2bv_rewriter::negate(expr* e) { - if (m.is_not(e, e)) return e; - return m.mk_not(e); - } - - expr* card2bv_rewriter::mk_ite(expr* c, expr* hi, expr* lo) { - while (m.is_not(c, c)) { - std::swap(hi, lo); - } - if (hi == lo) return hi; - if (m.is_true(hi) && m.is_false(lo)) return c; - if (m.is_false(hi) && m.is_true(lo)) return negate(c); - if (m.is_true(hi)) return m.mk_or(c, lo); - if (m.is_false(lo)) return m.mk_and(c, hi); - if (m.is_false(hi)) return m.mk_and(negate(c), lo); - if (m.is_true(lo)) return m.mk_implies(c, hi); - return m.mk_ite(c, hi, lo); - } - - void card_pb_rewriter::rewrite(expr* e, expr_ref& result) { - if (pb.is_eq(e)) { - app* a = to_app(e); - ast_manager& m = m_lemmas.get_manager(); - unsigned sz = a->get_num_args(); - expr_ref_vector args(m); - expr_ref tmp(m); - for (unsigned i = 0; i < sz; ++i) { - (*this)(a->get_arg(i), tmp); - args.push_back(tmp); - } - m_cfg.m_r.mk_assert(a->get_decl(), sz, args.c_ptr(), result, m_lemmas); - } - else { - (*this)(e, result); - } - } - -}; - -template class rewriter_tpl; - +#include"filter_model_converter.h" class card2bv_tactic : public tactic { ast_manager & m; params_ref m_params; - th_rewriter m_rw1; - pb::card_pb_rewriter m_rw2; public: card2bv_tactic(ast_manager & m, params_ref const & p): m(m), - m_params(p), - m_rw1(m), - m_rw2(m) { + m_params(p) { } virtual tactic * translate(ast_manager & m) { @@ -538,9 +60,8 @@ public: SASSERT(g->is_well_sorted()); mc = 0; pc = 0; core = 0; result.reset(); tactic_report report("card2bv", *g); - m_rw1.reset(); - m_rw2.reset(); - m_rw2.lemmas().reset(); + th_rewriter rw1(m, m_params); + pb2bv_rewriter rw2(m, m_params); if (g->inconsistent()) { result.push_back(g.get()); @@ -550,18 +71,28 @@ public: expr_ref new_f1(m), new_f2(m); proof_ref new_pr1(m), new_pr2(m); for (unsigned idx = 0; !g->inconsistent() && idx < g->size(); idx++) { - m_rw1(g->form(idx), new_f1, new_pr1); + rw1(g->form(idx), new_f1, new_pr1); TRACE("card2bv", tout << "Rewriting " << mk_ismt2_pp(new_f1.get(), m) << std::endl;); - m_rw2.rewrite(new_f1, new_f2); + rw2(new_f1, new_f2, new_pr2); if (m.proofs_enabled()) { new_pr1 = m.mk_modus_ponens(g->pr(idx), new_pr1); - new_pr2 = m.mk_rewrite(new_f1, new_f2); new_pr1 = m.mk_modus_ponens(new_pr1, new_pr2); } g->update(idx, new_f2, new_pr1, g->dep(idx)); } - for (unsigned i = 0; i < m_rw2.lemmas().size(); ++i) { - g->assert_expr(m_rw2.lemmas()[i].get()); + expr_ref_vector fmls(m); + rw2.flush_side_constraints(fmls); + for (unsigned i = 0; !g->inconsistent() && i < fmls.size(); ++i) { + g->assert_expr(fmls[i].get()); + } + + func_decl_ref_vector const& fns = rw2.fresh_constants(); + if (!fns.empty()) { + filter_model_converter* filter = alloc(filter_model_converter, m); + for (unsigned i = 0; i < fns.size(); ++i) { + filter->insert(fns[i]); + } + mc = filter; } g->inc_depth(); diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index 4c3790af3..6348ddd74 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -29,10 +29,11 @@ Notes: #include"filter_model_converter.h" #include"pb2bv_model_converter.h" #include"pb2bv_tactic.h" +#include"ast_pp.h" class pb2bv_tactic : public tactic { public: - struct non_pb {}; + struct non_pb { expr* e; non_pb(expr* e) : e(e) {}}; struct only_01_visitor { typedef rational numeral; @@ -48,7 +49,7 @@ public: void throw_non_pb(expr * n) { TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";); - throw non_pb(); + throw non_pb(n); } void operator()(var * n) { @@ -575,7 +576,7 @@ private: void throw_non_pb(expr * n) { TRACE("pb2bv", tout << "Not pseudo-Boolean: " << mk_ismt2_pp(n, m) << "\n";); - throw non_pb(); + throw non_pb(n); } // check if polynomial is encoding @@ -910,8 +911,8 @@ private: try { quick_pb_check(g); } - catch (non_pb) { - throw tactic_exception("goal is in a fragment unsupported by pb2bv"); + catch (non_pb& p) { + throw_tactic(p.e); } unsigned size = g->size(); @@ -940,8 +941,8 @@ private: new_exprs.push_back(new_f); } } - catch (non_pb) { - throw tactic_exception("goal is in a fragment unsupported by pb2bv"); + catch (non_pb& p) { + throw_tactic(p.e); } for (unsigned idx = 0; idx < size; idx++) @@ -966,6 +967,12 @@ private: TRACE("pb2bv", g->display(tout);); SASSERT(g->is_well_sorted()); } + + void throw_tactic(expr* e) { + std::stringstream strm; + strm << "goal is in a fragment unsupported by pb2bv. Offending expression: " << mk_pp(e, m); + throw tactic_exception(strm.str().c_str()); + } }; imp * m_imp; diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index d7d6c9811..2ccbe9712 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -29,7 +29,7 @@ Revision History: #include "extension_model_converter.h" #include "var_subst.h" #include "ast_util.h" -#include "fd_rewriter.h" +#include "enum2bv_rewriter.h" class dt2bv_tactic : public tactic { @@ -40,7 +40,6 @@ class dt2bv_tactic : public tactic { bv_util m_bv; obj_hashtable m_fd_sorts; obj_hashtable m_non_fd_sorts; - obj_map* m_translate; bool is_fd(expr* a) { return is_fd(get_sort(a)); } @@ -99,11 +98,11 @@ class dt2bv_tactic : public tactic { sort_pred m_is_fd; public: - dt2bv_tactic(ast_manager& m, params_ref const& p, obj_map* tr): - m(m), m_params(p), m_dt(m), m_bv(m), m_translate(tr), m_is_fd(*this) {} + dt2bv_tactic(ast_manager& m, params_ref const& p): + m(m), m_params(p), m_dt(m), m_bv(m), m_is_fd(*this) {} virtual tactic * translate(ast_manager & m) { - return alloc(dt2bv_tactic, m, m_params, 0); + return alloc(dt2bv_tactic, m, m_params); } virtual void updt_params(params_ref const & p) { @@ -133,7 +132,7 @@ public: if (!m_fd_sorts.empty()) { ref ext = alloc(extension_model_converter, m); ref filter = alloc(filter_model_converter, m); - fd_rewriter rw(m, m_params); + enum2bv_rewriter rw(m, m_params); rw.set_is_fd(&m_is_fd); expr_ref new_curr(m); proof_ref new_pr(m); @@ -154,9 +153,6 @@ public: obj_map::iterator it = rw.enum2bv().begin(), end = rw.enum2bv().end(); for (; it != end; ++it) { filter->insert(it->m_value); - if (m_translate) { - m_translate->insert(it->m_key, it->m_value); - } } } { @@ -182,6 +178,6 @@ public: }; -tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p, obj_map* tr) { - return alloc(dt2bv_tactic, m, p, tr); +tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p) { + return alloc(dt2bv_tactic, m, p); } diff --git a/src/tactic/bv/dt2bv_tactic.h b/src/tactic/bv/dt2bv_tactic.h index fd5aacda6..10ce0724f 100644 --- a/src/tactic/bv/dt2bv_tactic.h +++ b/src/tactic/bv/dt2bv_tactic.h @@ -24,7 +24,7 @@ Revision History: class ast_manager; class tactic; -tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref(), obj_map* tr = 0); +tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref()); /* ADD_TACTIC("dt2bv", "eliminate finite domain data-types. Replace by bit-vectors.", "mk_dt2bv_tactic(m, p)") diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp new file mode 100644 index 000000000..f7236351c --- /dev/null +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -0,0 +1,296 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + bounded_int2bv_solver.cpp + +Abstract: + + This solver identifies bounded integers and rewrites them to bit-vectors. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ + +#include "bounded_int2bv_solver.h" +#include "solver_na2as.h" +#include "tactic.h" +#include "pb2bv_rewriter.h" +#include "filter_model_converter.h" +#include "extension_model_converter.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" +#include "bound_manager.h" +#include "bv2int_rewriter.h" +#include "expr_safe_replace.h" +#include "bv_decl_plugin.h" +#include "arith_decl_plugin.h" + +class bounded_int2bv_solver : public solver_na2as { + ast_manager& m; + params_ref m_params; + bv_util m_bv; + arith_util m_arith; + expr_ref_vector m_assertions; + ref m_solver; + ptr_vector m_bounds; + func_decl_ref_vector m_bv_fns; + func_decl_ref_vector m_int_fns; + unsigned_vector m_bv_fns_lim; + obj_map m_int2bv; + obj_map m_bv2int; + obj_map m_bv2offset; + bv2int_rewriter_ctx m_rewriter_ctx; + bv2int_rewriter_star m_rewriter; + +public: + + bounded_int2bv_solver(ast_manager& m, params_ref const& p, solver* s): + solver_na2as(m), + m(m), + m_params(p), + m_bv(m), + m_arith(m), + m_assertions(m), + m_solver(s), + m_bv_fns(m), + m_int_fns(m), + m_rewriter_ctx(m, p), + m_rewriter(m, m_rewriter_ctx) + { + m_bounds.push_back(alloc(bound_manager, m)); + } + + virtual ~bounded_int2bv_solver() { + while (!m_bounds.empty()) { + dealloc(m_bounds.back()); + m_bounds.pop_back(); + } + } + + virtual solver* translate(ast_manager& m, params_ref const& p) { + return alloc(bounded_int2bv_solver, m, p, m_solver->translate(m, p)); + } + + virtual void assert_expr(expr * t) { + m_assertions.push_back(t); + } + + virtual void push_core() { + flush_assertions(); + m_solver->push(); + m_bv_fns_lim.push_back(m_bv_fns.size()); + m_bounds.push_back(alloc(bound_manager, m)); + } + + virtual void pop_core(unsigned n) { + m_assertions.reset(); + m_solver->pop(n); + + if (n > 0) { + SASSERT(n <= m_bv_fns_lim.size()); + unsigned new_sz = m_bv_fns_lim.size() - n; + unsigned lim = m_bv_fns_lim[new_sz]; + for (unsigned i = m_int_fns.size(); i > lim; ) { + --i; + m_int2bv.erase(m_int_fns[i].get()); + m_bv2int.erase(m_bv_fns[i].get()); + m_bv2offset.erase(m_bv_fns[i].get()); + } + m_bv_fns_lim.resize(new_sz); + m_bv_fns.resize(lim); + m_int_fns.resize(lim); + } + + while (n > 0) { + dealloc(m_bounds.back()); + m_bounds.pop_back(); + --n; + } + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + flush_assertions(); + return m_solver->check_sat(num_assumptions, assumptions); + } + + virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } + virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } + virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } + virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } + virtual void get_model(model_ref & mdl) { + m_solver->get_model(mdl); + if (mdl) { + extend_model(mdl); + filter_model(mdl); + } + } + virtual proof * get_proof() { return m_solver->get_proof(); } + virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } + virtual void get_labels(svector & r) { m_solver->get_labels(r); } + virtual ast_manager& get_manager() const { return m; } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + flush_assertions(); + expr_ref_vector bvars(m); + for (unsigned i = 0; i < vars.size(); ++i) { + expr* v = vars[i]; + func_decl* f; + rational offset; + if (is_app(v) && is_uninterp_const(v) && m_int2bv.find(to_app(v)->get_decl(), f)) { + bvars.push_back(m.mk_const(f)); + } + else { + bvars.push_back(v); + } + } + lbool r = m_solver->get_consequences(asms, bvars, consequences); + + // translate bit-vector consequences back to integer values + for (unsigned i = 0; i < consequences.size(); ++i) { + expr* a, *b, *u, *v; + func_decl* f; + rational num; + unsigned bvsize; + rational offset; + VERIFY(m.is_implies(consequences[i].get(), a, b)); + if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_bv2int.find(to_app(u)->get_decl(), f) && m_bv.is_numeral(v, num, bvsize)) { + SASSERT(num.is_unsigned()); + expr_ref head(m); + VERIFY (m_bv2offset.find(to_app(u)->get_decl(), offset)); + // f + offset == num + // f == num - offset + head = m.mk_eq(m.mk_const(f), m_arith.mk_numeral(num + offset, true)); + consequences[i] = m.mk_implies(a, head); + } + } + return r; + + } + +private: + + void filter_model(model_ref& mdl) const { + if (m_bv_fns.empty()) { + return; + } + filter_model_converter filter(m); + func_decl_ref_vector const& fns = m_bv_fns; + for (unsigned i = 0; i < m_bv_fns.size(); ++i) { + filter.insert(m_bv_fns[i]); + } + filter(mdl, 0); + } + + void extend_model(model_ref& mdl) { + extension_model_converter ext(m); + obj_map::iterator it = m_int2bv.begin(), end = m_int2bv.end(); + for (; it != end; ++it) { + rational offset; + VERIFY (m_bv2offset.find(it->m_value, offset)); + expr_ref value(m_bv.mk_bv2int(m.mk_const(it->m_value)), m); + if (!offset.is_zero()) { + value = m_arith.mk_add(value, m_arith.mk_numeral(offset, true)); + } + TRACE("int2bv", tout << mk_pp(it->m_key, m) << " " << value << "\n";); + ext.insert(it->m_key, value); + } + ext(mdl, 0); + } + + void accumulate_sub(expr_safe_replace& sub) { + for (unsigned i = 0; i < m_bounds.size(); ++i) { + accumulate_sub(sub, *m_bounds[i]); + } + } + + void accumulate_sub(expr_safe_replace& sub, bound_manager& bm) { + bound_manager::iterator it = bm.begin(), end = bm.end(); + for (; it != end; ++it) { + expr* e = *it; + rational lo, hi; + bool s1, s2; + SASSERT(is_uninterp_const(e)); + func_decl* f = to_app(e)->get_decl(); + + if (bm.has_lower(e, lo, s1) && bm.has_upper(e, hi, s2) && lo <= hi && !s1 && !s2) { + func_decl* fbv; + rational offset; + if (!m_int2bv.find(f, fbv)) { + rational n = hi - lo + rational::one(); + unsigned num_bits = get_num_bits(n); + expr_ref b(m); + b = m.mk_fresh_const("b", m_bv.mk_sort(num_bits)); + fbv = to_app(b)->get_decl(); + offset = lo; + m_int2bv.insert(f, fbv); + m_bv2int.insert(fbv, f); + m_bv2offset.insert(fbv, offset); + m_bv_fns.push_back(fbv); + m_int_fns.push_back(f); + unsigned shift; + if (!offset.is_zero() && !n.is_power_of_two(shift)) { + m_assertions.push_back(m_bv.mk_ule(b, m_bv.mk_numeral(n-rational::one(), num_bits))); + } + } + else { + VERIFY(m_bv2offset.find(fbv, offset)); + } + expr_ref t(m.mk_const(fbv), m); + t = m_bv.mk_bv2int(t); + if (!offset.is_zero()) { + t = m_arith.mk_add(t, m_arith.mk_numeral(lo, true)); + } + sub.insert(e, t); + } + } + } + + unsigned get_num_bits(rational const& k) { + SASSERT(!k.is_neg()); + SASSERT(k.is_int()); + rational two(2); + rational bound(1); + unsigned num_bits = 1; + while (bound <= k) { + ++num_bits; + bound *= two; + } + return num_bits; + } + + void flush_assertions() { + bound_manager& bm = *m_bounds.back(); + for (unsigned i = 0; i < m_assertions.size(); ++i) { + bm(m_assertions[i].get()); + } + expr_safe_replace sub(m); + accumulate_sub(sub); + proof_ref proof(m); + expr_ref fml1(m), fml2(m); + if (sub.empty()) { + m_solver->assert_expr(m_assertions); + } + else { + for (unsigned i = 0; i < m_assertions.size(); ++i) { + sub(m_assertions[i].get(), fml1); + m_rewriter(fml1, fml2, proof); + m_solver->assert_expr(fml2); + TRACE("int2bv", tout << fml2 << "\n";); + } + } + m_assertions.reset(); + } +}; + +solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s) { + return alloc(bounded_int2bv_solver, m, p, s); +} diff --git a/src/tactic/portfolio/bounded_int2bv_solver.h b/src/tactic/portfolio/bounded_int2bv_solver.h new file mode 100644 index 000000000..5fcf2cd65 --- /dev/null +++ b/src/tactic/portfolio/bounded_int2bv_solver.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + bounded_int2bv_solver.h + +Abstract: + + Finite domain solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ +#ifndef BOUNDED_INT2BV_SOLVER_H_ +#define BOUNDED_INT2BV_SOLVER_H_ + +#include"ast.h" +#include"params.h" + +class solver; + +solver * mk_bounded_int2bv_solver(ast_manager & m, params_ref const & p, solver* s); + +#endif diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp new file mode 100644 index 000000000..369402114 --- /dev/null +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -0,0 +1,162 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + enum2bv_solver.cpp + +Abstract: + + Finite domain solver. + + Enumeration data-types are translated into bit-vectors, and then + the incremental sat-solver is applied to the resulting assertions. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-17 + +Notes: + +--*/ + +#include "solver_na2as.h" +#include "tactic.h" +#include "bv_decl_plugin.h" +#include "datatype_decl_plugin.h" +#include "enum2bv_rewriter.h" +#include "extension_model_converter.h" +#include "filter_model_converter.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" +#include "enum2bv_solver.h" + +class enum2bv_solver : public solver_na2as { + ast_manager& m; + params_ref m_params; + ref m_solver; + enum2bv_rewriter m_rewriter; + +public: + + enum2bv_solver(ast_manager& m, params_ref const& p, solver* s): + solver_na2as(m), + m(m), + m_params(p), + m_solver(s), + m_rewriter(m, p) + { + } + + virtual ~enum2bv_solver() {} + + virtual solver* translate(ast_manager& m, params_ref const& p) { + return alloc(enum2bv_solver, m, p, m_solver->translate(m, p)); + } + + virtual void assert_expr(expr * t) { + expr_ref tmp(t, m); + expr_ref_vector bounds(m); + proof_ref tmp_proof(m); + m_rewriter(t, tmp, tmp_proof); + m_solver->assert_expr(tmp); + m_rewriter.flush_side_constraints(bounds); + m_solver->assert_expr(bounds); + } + + virtual void push_core() { + m_rewriter.push(); + m_solver->push(); + } + + virtual void pop_core(unsigned n) { + m_solver->pop(n); + m_rewriter.pop(n); + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + return m_solver->check_sat(num_assumptions, assumptions); + } + + virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } + virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } + virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } + virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } + virtual void get_model(model_ref & mdl) { + m_solver->get_model(mdl); + if (mdl) { + extend_model(mdl); + filter_model(mdl); + } + } + virtual proof * get_proof() { return m_solver->get_proof(); } + virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } + virtual void get_labels(svector & r) { m_solver->get_labels(r); } + virtual ast_manager& get_manager() const { return m; } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + + datatype_util dt(m); + bv_util bv(m); + + // translate enumeration constants to bit-vectors. + expr_ref_vector bvars(m), conseq(m); + for (unsigned i = 0; i < vars.size(); ++i) { + func_decl* f; + if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { + bvars.push_back(m.mk_const(f)); + } + else { + bvars.push_back(vars[i]); + } + } + lbool r = m_solver->get_consequences(asms, bvars, consequences); + std::cout << consequences.size() << "\n"; + + + // translate bit-vector consequences back to enumeration types + for (unsigned i = 0; i < consequences.size(); ++i) { + expr* a, *b, *u, *v; + func_decl* f; + rational num; + unsigned bvsize; + VERIFY(m.is_implies(consequences[i].get(), a, b)); + if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { + SASSERT(num.is_unsigned()); + expr_ref head(m); + ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); + head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); + consequences[i] = m.mk_implies(a, head); + } + } + return r; + } + + void filter_model(model_ref& mdl) { + filter_model_converter filter(m); + obj_map::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end(); + for (; it != end; ++it) { + filter.insert(it->m_value); + } + filter(mdl, 0); + } + + void extend_model(model_ref& mdl) { + extension_model_converter ext(m); + obj_map::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end(); + for (; it != end; ++it) { + ext.insert(it->m_key, it->m_value); + + } + ext(mdl, 0); + } + +}; + +solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s) { + return alloc(enum2bv_solver, m, p, s); +} diff --git a/src/tactic/portfolio/enum2bv_solver.h b/src/tactic/portfolio/enum2bv_solver.h new file mode 100644 index 000000000..b113c6747 --- /dev/null +++ b/src/tactic/portfolio/enum2bv_solver.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + enum2bv_solver.h + +Abstract: + + Finite domain solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-17 + +Notes: + +--*/ +#ifndef ENUM2BV_SOLVER_H_ +#define ENUM2BV_SOLVER_H_ + +#include"ast.h" +#include"params.h" + +class solver; + +solver * mk_enum2bv_solver(ast_manager & m, params_ref const & p, solver* s); + +#endif diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp index 9447c158c..a534337bc 100644 --- a/src/tactic/portfolio/fd_solver.cpp +++ b/src/tactic/portfolio/fd_solver.cpp @@ -9,9 +9,6 @@ Abstract: Finite domain solver. - Enumeration data-types are translated into bit-vectors, and then - the incremental sat-solver is applied to the resulting assertions. - Author: Nikolaj Bjorner (nbjorner) 2016-10-17 @@ -21,141 +18,16 @@ Notes: --*/ #include "fd_solver.h" -#include "solver_na2as.h" #include "tactic.h" #include "inc_sat_solver.h" -#include "bv_decl_plugin.h" -#include "datatype_decl_plugin.h" -#include "fd_rewriter.h" -#include "extension_model_converter.h" -#include "filter_model_converter.h" -#include "ast_pp.h" -#include "model_smt2_pp.h" - -class fd_solver : public solver_na2as { - ast_manager& m; - params_ref m_params; - ref m_solver; - fd_rewriter m_rewriter; - -public: - - fd_solver(ast_manager& m, params_ref const& p): - solver_na2as(m), - m(m), - m_params(p), - m_solver(mk_inc_sat_solver(m, p)), - m_rewriter(m, p) - { - } - - virtual ~fd_solver() {} - - virtual solver* translate(ast_manager& m, params_ref const& p) { - return alloc(fd_solver, m, p); - } - - virtual void assert_expr(expr * t) { - expr_ref tmp(t, m); - expr_ref_vector bounds(m); - proof_ref tmp_proof(m); - m_rewriter(t, tmp, tmp_proof); - m_solver->assert_expr(tmp); - m_rewriter.flush_side_constraints(bounds); - m_solver->assert_expr(bounds); - } - - virtual void push_core() { - m_rewriter.push(); - m_solver->push(); - } - - virtual void pop_core(unsigned n) { - m_solver->pop(n); - m_rewriter.pop(n); - } - - virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { - return m_solver->check_sat(num_assumptions, assumptions); - } - - virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } - virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } - virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } - virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } - virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } - virtual void get_model(model_ref & mdl) { - m_solver->get_model(mdl); - if (mdl) { - extend_model(mdl); - filter_model(mdl); - } - } - virtual proof * get_proof() { return m_solver->get_proof(); } - virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } - virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } - virtual void get_labels(svector & r) { m_solver->get_labels(r); } - virtual ast_manager& get_manager() const { return m; } - virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } - - virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { - - datatype_util dt(m); - bv_util bv(m); - - // translate enumeration constants to bit-vectors. - expr_ref_vector bvars(m), conseq(m); - for (unsigned i = 0; i < vars.size(); ++i) { - func_decl* f; - if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { - bvars.push_back(m.mk_const(f)); - } - else { - bvars.push_back(vars[i]); - } - } - lbool r = m_solver->get_consequences(asms, bvars, consequences); - - // translate bit-vector consequences back to enumeration types - for (unsigned i = 0; i < consequences.size(); ++i) { - expr* a, *b, *u, *v; - func_decl* f; - rational num; - unsigned bvsize; - VERIFY(m.is_implies(consequences[i].get(), a, b)); - if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { - SASSERT(num.is_unsigned()); - expr_ref head(m); - ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); - head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); - consequences[i] = m.mk_implies(a, head); - } - } - return r; - } - - void filter_model(model_ref& mdl) { - filter_model_converter filter(m); - obj_map::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end(); - for (; it != end; ++it) { - filter.insert(it->m_value); - } - filter(mdl, 0); - } - - void extend_model(model_ref& mdl) { - extension_model_converter ext(m); - obj_map::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end(); - for (; it != end; ++it) { - ext.insert(it->m_key, it->m_value); - - } - ext(mdl, 0); - } - -}; +#include "enum2bv_solver.h" +#include "pb2bv_solver.h" +#include "bounded_int2bv_solver.h" solver * mk_fd_solver(ast_manager & m, params_ref const & p) { - return alloc(fd_solver, m, p); + solver* s = mk_inc_sat_solver(m, p); + s = mk_enum2bv_solver(m, p, s); + s = mk_pb2bv_solver(m, p, s); + s = mk_bounded_int2bv_solver(m, p, s); + return s; } diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp new file mode 100644 index 000000000..bfd533e8a --- /dev/null +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -0,0 +1,127 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + pb2bv_solver.cpp + +Abstract: + + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ + +#include "pb2bv_solver.h" +#include "solver_na2as.h" +#include "tactic.h" +#include "pb2bv_rewriter.h" +#include "filter_model_converter.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" + +class pb2bv_solver : public solver_na2as { + ast_manager& m; + params_ref m_params; + expr_ref_vector m_assertions; + ref m_solver; + pb2bv_rewriter m_rewriter; + +public: + + pb2bv_solver(ast_manager& m, params_ref const& p, solver* s): + solver_na2as(m), + m(m), + m_params(p), + m_assertions(m), + m_solver(s), + m_rewriter(m, p) + { + } + + virtual ~pb2bv_solver() {} + + virtual solver* translate(ast_manager& m, params_ref const& p) { + return alloc(pb2bv_solver, m, p, m_solver->translate(m, p)); + } + + virtual void assert_expr(expr * t) { + m_assertions.push_back(t); + } + + virtual void push_core() { + flush_assertions(); + m_rewriter.push(); + m_solver->push(); + } + + virtual void pop_core(unsigned n) { + m_assertions.reset(); + m_solver->pop(n); + m_rewriter.pop(n); + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + flush_assertions(); + return m_solver->check_sat(num_assumptions, assumptions); + } + + virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } + virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } + virtual void collect_statistics(statistics & st) const { + m_rewriter.collect_statistics(st); + m_solver->collect_statistics(st); + } + virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } + virtual void get_model(model_ref & mdl) { + m_solver->get_model(mdl); + if (mdl) { + filter_model(mdl); + } + } + virtual proof * get_proof() { return m_solver->get_proof(); } + virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } + virtual void get_labels(svector & r) { m_solver->get_labels(r); } + virtual ast_manager& get_manager() const { return m; } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + flush_assertions(); + return m_solver->get_consequences(asms, vars, consequences); } + + void filter_model(model_ref& mdl) { + if (m_rewriter.fresh_constants().empty()) { + return; + } + filter_model_converter filter(m); + func_decl_ref_vector const& fns = m_rewriter.fresh_constants(); + for (unsigned i = 0; i < fns.size(); ++i) { + filter.insert(fns[i]); + } + filter(mdl, 0); + } + +private: + void flush_assertions() { + proof_ref proof(m); + expr_ref fml(m); + expr_ref_vector fmls(m); + for (unsigned i = 0; i < m_assertions.size(); ++i) { + m_rewriter(m_assertions[i].get(), fml, proof); + m_solver->assert_expr(fml); + } + m_rewriter.flush_side_constraints(fmls); + m_solver->assert_expr(fmls); + m_assertions.reset(); + } +}; + +solver * mk_pb2bv_solver(ast_manager & m, params_ref const & p, solver* s) { + return alloc(pb2bv_solver, m, p, s); +} diff --git a/src/tactic/portfolio/pb2bv_solver.h b/src/tactic/portfolio/pb2bv_solver.h new file mode 100644 index 000000000..e861e769b --- /dev/null +++ b/src/tactic/portfolio/pb2bv_solver.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + pb2bv_solver.h + +Abstract: + + Pseudo-Boolean to bit-vector solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-23 + +Notes: + +--*/ +#ifndef PB2BV_SOLVER_H_ +#define PB2BV_SOLVER_H_ + +#include"ast.h" +#include"params.h" + +class solver; + +solver * mk_pb2bv_solver(ast_manager & m, params_ref const & p, solver* s); + +#endif diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp index 8c35bcfb1..febff0151 100644 --- a/src/test/get_consequences.cpp +++ b/src/test/get_consequences.cpp @@ -51,85 +51,8 @@ static void test1() { std::cout << conseq << "\n"; } -static void test2() { - ast_manager m; - reg_decl_plugins(m); - bv_util bv(m); - datatype_util dtutil(m); - params_ref p; - datatype_decl_plugin & dt = *(static_cast(m.get_plugin(m.get_family_id("datatype")))); - sort_ref_vector new_sorts(m); - constructor_decl* R = mk_constructor_decl(symbol("R"), symbol("is-R"), 0, 0); - constructor_decl* G = mk_constructor_decl(symbol("G"), symbol("is-G"), 0, 0); - constructor_decl* B = mk_constructor_decl(symbol("B"), symbol("is-B"), 0, 0); - constructor_decl* constrs[3] = { R, G, B }; - datatype_decl * enum_sort = mk_datatype_decl(symbol("RGB"), 3, constrs); - VERIFY(dt.mk_datatypes(1, &enum_sort, new_sorts)); - del_constructor_decls(3, constrs); - sort* rgb = new_sorts[0].get(); - - expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb); - ptr_vector const& enums = *dtutil.get_datatype_constructors(rgb); - expr_ref r = expr_ref(m.mk_const(enums[0]), m); - expr_ref g = expr_ref(m.mk_const(enums[1]), m); - expr_ref b = expr_ref(m.mk_const(enums[2]), m); - expr_ref val(m); - - // Eliminate enumeration data-types: - goal_ref gl = alloc(goal, m); - gl->assert_expr(m.mk_not(m.mk_eq(x, r))); - gl->assert_expr(m.mk_not(m.mk_eq(x, b))); - gl->display(std::cout); - obj_map tr; - obj_map rev_tr; - ref dt2bv = mk_dt2bv_tactic(m, p, &tr); - goal_ref_buffer result; - model_converter_ref mc; - proof_converter_ref pc; - expr_dependency_ref core(m); - (*dt2bv)(gl, result, mc, pc, core); - - // Collect translations from enumerations to bit-vectors - obj_map::iterator it = tr.begin(), end = tr.end(); - for (; it != end; ++it) { - rev_tr.insert(it->m_value, it->m_key); - } - - // Create bit-vector implication problem - val = m.mk_const(tr.find(to_app(x)->get_decl())); - std::cout << val << "\n"; - ptr_vector fmls; - result[0]->get_formulas(fmls); - ref solver = mk_inc_sat_solver(m, p); - for (unsigned i = 0; i < fmls.size(); ++i) { - solver->assert_expr(fmls[i]); - } - expr_ref_vector asms(m), vars(m), conseq(m); - vars.push_back(val); - - // retrieve consequences - solver->get_consequences(asms, vars, conseq); - - // Convert consequences over bit-vectors to enumeration types. - std::cout << conseq << "\n"; - for (unsigned i = 0; i < conseq.size(); ++i) { - expr* a, *b, *u, *v; - func_decl* f; - rational num; - unsigned bvsize; - VERIFY(m.is_implies(conseq[i].get(), a, b)); - if (m.is_eq(b, u, v) && rev_tr.find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { - SASSERT(num.is_unsigned()); - expr_ref head(m); - head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); - conseq[i] = m.mk_implies(a, head); - } - } - std::cout << conseq << "\n"; -} - -void test3() { +void test2() { ast_manager m; reg_decl_plugins(m); bv_util bv(m); @@ -189,6 +112,4 @@ void test3() { void tst_get_consequences() { test1(); test2(); - test3(); - } diff --git a/src/test/main.cpp b/src/test/main.cpp index 9c6cdd668..320eddd7b 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -229,6 +229,7 @@ int main(int argc, char ** argv) { TST_ARGV(ddnf); TST(model_evaluator); TST(get_consequences); + TST(pb2bv); //TST_ARGV(hs); } diff --git a/src/test/pb2bv.cpp b/src/test/pb2bv.cpp new file mode 100644 index 000000000..c114997c5 --- /dev/null +++ b/src/test/pb2bv.cpp @@ -0,0 +1,195 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +--*/ + +#include "trace.h" +#include "vector.h" +#include "ast.h" +#include "ast_pp.h" +#include "statistics.h" +#include "reg_decl_plugins.h" +#include "pb2bv_rewriter.h" +#include "smt_kernel.h" +#include "model_smt2_pp.h" +#include "smt_params.h" +#include "ast_util.h" +#include "pb_decl_plugin.h" +#include "th_rewriter.h" +#include "fd_solver.h" +#include "solver.h" + +static void test1() { + ast_manager m; + reg_decl_plugins(m); + pb_util pb(m); + params_ref p; + pb2bv_rewriter rw(m, p); + expr_ref_vector vars(m); + unsigned N = 5; + for (unsigned i = 0; i < N; ++i) { + std::stringstream strm; + strm << "b" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + } + + for (unsigned k = 1; k <= N; ++k) { + expr_ref fml(m), result(m); + proof_ref proof(m); + fml = pb.mk_at_least_k(vars.size(), vars.c_ptr(), k); + rw(fml, result, proof); + std::cout << fml << " |-> " << result << "\n"; + } + expr_ref_vector lemmas(m); + rw.flush_side_constraints(lemmas); + std::cout << lemmas << "\n"; +} + +static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector const& coeffs, unsigned k, unsigned kind) { + pb_util pb(m); + params_ref p; + pb2bv_rewriter rw(m, p); + unsigned N = vars.size(); + expr_ref fml1(m), fml2(m), result1(m), result2(m); + proof_ref proof(m); + expr_ref_vector lemmas(m); + th_rewriter th_rw(m); + + switch (kind) { + case 0: fml1 = pb.mk_ge(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + } + rw(fml1, result1, proof); + rw.flush_side_constraints(lemmas); + std::cout << lemmas << "\n"; + for (unsigned values = 0; values < static_cast(1 << N); ++values) { + smt_params fp; + smt::kernel solver(m, fp); + expr_ref_vector tf(m); + for (unsigned i = 0; i < N; ++i) { + bool is_true = 0 != (values & (1 << i)); + tf.push_back(is_true ? m.mk_true() : m.mk_false()); + solver.assert_expr(is_true ? vars[i] : m.mk_not(vars[i])); + } + + solver.assert_expr(lemmas); + switch (kind) { + case 0: fml2 = pb.mk_ge(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + case 1: fml2 = pb.mk_le(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + default: fml2 = pb.mk_eq(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + } + std::cout << fml1 << " " << fml2 << "\n"; + th_rw(fml2, result2, proof); + SASSERT(m.is_true(result2) || m.is_false(result2)); + lbool res = solver.check(); + SASSERT(res == l_true); + solver.assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get()); + res = solver.check(); + SASSERT(res == l_false); + } +} + +static void test_semantics(ast_manager& m, expr_ref_vector const& vars, vector const& coeffs, unsigned k) { + test_semantics(m, vars, coeffs, k, 0); + test_semantics(m, vars, coeffs, k, 1); + test_semantics(m, vars, coeffs, k, 2); +} + +static void test2() { + ast_manager m; + reg_decl_plugins(m); + expr_ref_vector vars(m); + unsigned N = 4; + for (unsigned i = 0; i < N; ++i) { + std::stringstream strm; + strm << "b" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + } + for (unsigned coeff = 0; coeff < static_cast(1 << N); ++coeff) { + vector coeffs; + for (unsigned i = 0; i < N; ++i) { + bool is_one = 0 != (coeff & (1 << i)); + coeffs.push_back(is_one ? rational(1) : rational(2)); + } + for (unsigned i = 0; i <= N; ++i) { + test_semantics(m, vars, coeffs, i); + } + } +} + + +static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector const& coeffs, unsigned k, unsigned kind) { + pb_util pb(m); + params_ref p; + unsigned N = vars.size(); + expr_ref fml1(m), fml2(m), result1(m), result2(m); + proof_ref proof(m); + th_rewriter th_rw(m); + + switch (kind) { + case 0: fml1 = pb.mk_ge(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + case 1: fml1 = pb.mk_le(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + default: fml1 = pb.mk_eq(vars.size(), coeffs.c_ptr(), vars.c_ptr(), rational(k)); break; + } + result1 = m.mk_fresh_const("xx", m.mk_bool_sort()); + for (unsigned values = 0; values < static_cast(1 << N); ++values) { + ref slv = mk_fd_solver(m, p); + expr_ref_vector tf(m); + for (unsigned i = 0; i < N; ++i) { + bool is_true = 0 != (values & (1 << i)); + tf.push_back(is_true ? m.mk_true() : m.mk_false()); + slv->assert_expr(is_true ? vars[i] : m.mk_not(vars[i])); + } + slv->assert_expr(m.mk_eq(result1, fml1)); + + switch (kind) { + case 0: fml2 = pb.mk_ge(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + case 1: fml2 = pb.mk_le(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + default: fml2 = pb.mk_eq(tf.size(), coeffs.c_ptr(), tf.c_ptr(), rational(k)); break; + } + std::cout << fml1 << " " << fml2 << "\n"; + th_rw(fml2, result2, proof); + SASSERT(m.is_true(result2) || m.is_false(result2)); + lbool res = slv->check_sat(0,0); + SASSERT(res == l_true); + slv->assert_expr(m.is_true(result2) ? m.mk_not(result1) : result1.get()); + res = slv->check_sat(0,0); + SASSERT(res == l_false); + } +} + +static void test_solver_semantics(ast_manager& m, expr_ref_vector const& vars, vector const& coeffs, unsigned k) { + test_solver_semantics(m, vars, coeffs, k, 0); + test_solver_semantics(m, vars, coeffs, k, 1); + test_solver_semantics(m, vars, coeffs, k, 2); +} + +static void test3() { + ast_manager m; + reg_decl_plugins(m); + expr_ref_vector vars(m); + unsigned N = 4; + for (unsigned i = 0; i < N; ++i) { + std::stringstream strm; + strm << "b" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort())); + } + for (unsigned coeff = 0; coeff < static_cast(1 << N); ++coeff) { + vector coeffs; + for (unsigned i = 0; i < N; ++i) { + bool is_one = 0 != (coeff & (1 << i)); + coeffs.push_back(is_one ? rational(1) : rational(2)); + } + for (unsigned i = 0; i <= N; ++i) { + test_solver_semantics(m, vars, coeffs, i); + } + } +} + +void tst_pb2bv() { + test1(); + test2(); + test3(); +} + diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index 57e818542..8b2aadee3 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -332,31 +332,106 @@ void test_sorting5(unsigned n, unsigned k) { test_sorting_ge(n, k); } -void test_at_most_1(unsigned n) { +expr_ref naive_at_most1(expr_ref_vector const& xs) { + ast_manager& m = xs.get_manager(); + expr_ref_vector clauses(m); + for (unsigned i = 0; i < xs.size(); ++i) { + for (unsigned j = i + 1; j < xs.size(); ++j) { + clauses.push_back(m.mk_not(m.mk_and(xs[i], xs[j]))); + } + } + return mk_and(clauses); +} + +void test_at_most_1(unsigned n, bool full) { ast_manager m; reg_decl_plugins(m); expr_ref_vector in(m), out(m); for (unsigned i = 0; i < n; ++i) { in.push_back(m.mk_fresh_const("a",m.mk_bool_sort())); } - + ast_ext2 ext(m); + psort_nw sn(ext); + expr_ref result1(m), result2(m); + result1 = sn.le(full, 1, in.size(), in.c_ptr()); + result2 = naive_at_most1(in); + + std::cout << "clauses: " << ext.m_clauses << "\n-----\n"; + + smt_params fp; + smt::kernel solver(m, fp); + for (unsigned i = 0; i < ext.m_clauses.size(); ++i) { + solver.assert_expr(ext.m_clauses[i].get()); + } + lbool res; + if (full) { + solver.push(); + solver.assert_expr(m.mk_not(m.mk_eq(result1, result2))); + + std::cout << result1 << "\n"; + + res = solver.check(); + SASSERT(res == l_false); + + solver.pop(1); + } + + if (n >= 9) return; + for (unsigned i = 0; i < static_cast(1 << n); ++i) { + std::cout << "checking: " << n << ": " << i << "\n"; + solver.push(); + unsigned k = 0; + for (unsigned j = 0; j < n; ++j) { + bool is_true = (i & (1 << j)) != 0; + expr_ref atom(m); + atom = is_true ? in[j].get() : m.mk_not(in[j].get()); + solver.assert_expr(atom); + std::cout << atom << "\n"; + if (is_true) ++k; + } + res = solver.check(); + SASSERT(res == l_true); + if (k > 1) { + solver.assert_expr(result1); + } + else if (!full) { + solver.pop(1); + continue; + } + else { + solver.assert_expr(m.mk_not(result1)); + } + res = solver.check(); + SASSERT(res == l_false); + solver.pop(1); + } +} + + +static void test_at_most1() { + ast_manager m; + reg_decl_plugins(m); + expr_ref_vector in(m), out(m); + for (unsigned i = 0; i < 5; ++i) { + in.push_back(m.mk_fresh_const("a",m.mk_bool_sort())); + } + in[4] = in[3]; + ast_ext2 ext(m); psort_nw sn(ext); expr_ref result(m); - result = sn.le(false, 1, in.size(), in.c_ptr()); + result = sn.le(true, 1, in.size(), in.c_ptr()); std::cout << result << "\n"; std::cout << ext.m_clauses << "\n"; } void tst_sorting_network() { - test_at_most_1(1); - test_at_most_1(2); - test_at_most_1(3); - test_at_most_1(4); - test_at_most_1(5); - test_at_most_1(10); - return; + for (unsigned i = 1; i < 17; ++i) { + test_at_most_1(i, true); + test_at_most_1(i, false); + } + test_at_most1(); test_sorting_eq(11,7); for (unsigned n = 3; n < 20; n += 2) { diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp index df4d207a6..feb051033 100644 --- a/src/util/mpq.cpp +++ b/src/util/mpq.cpp @@ -153,7 +153,7 @@ void mpq_manager::display_smt2(std::ostream & out, mpq const & a, bool de } template -void mpq_manager::display_decimal(std::ostream & out, mpq const & a, unsigned prec) { +void mpq_manager::display_decimal(std::ostream & out, mpq const & a, unsigned prec, bool truncate) { mpz n1, d1, v1; get_numerator(a, n1); get_denominator(a, d1); @@ -177,7 +177,7 @@ void mpq_manager::display_decimal(std::ostream & out, mpq const & a, unsi if (is_zero(n1)) goto end; // number is precise } - out << "?"; + if (!truncate) out << "?"; end: del(ten); del(n1); del(d1); del(v1); } diff --git a/src/util/mpq.h b/src/util/mpq.h index 0a643c650..093cc0a44 100644 --- a/src/util/mpq.h +++ b/src/util/mpq.h @@ -265,7 +265,7 @@ public: void display_smt2(std::ostream & out, mpq const & a, bool decimal) const; - void display_decimal(std::ostream & out, mpq const & a, unsigned prec); + void display_decimal(std::ostream & out, mpq const & a, unsigned prec, bool truncate = false); void add(mpz const & a, mpz const & b, mpz & c) { mpz_manager::add(a, b, c); } diff --git a/src/util/rational.h b/src/util/rational.h index fc25837c6..ba447fca6 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -86,7 +86,7 @@ public: void display(std::ostream & out) const { return m().display(out, m_val); } - void display_decimal(std::ostream & out, unsigned prec) const { return m().display_decimal(out, m_val, prec); } + void display_decimal(std::ostream & out, unsigned prec, bool truncate = false) const { return m().display_decimal(out, m_val, prec, truncate); } bool is_uint64() const { return m().is_uint64(m_val); } diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index 0a1c0ad55..0f5d2838e 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -226,7 +226,12 @@ Notes: m_t = EQ; card(k+1, n, xs, out); SASSERT(out.size() >= k+1); - return ctx.mk_min(out[k-1], ctx.mk_not(out[k])); + if (k == 0) { + return ctx.mk_not(out[k]); + } + else { + return ctx.mk_min(out[k-1], ctx.mk_not(out[k])); + } } } @@ -234,19 +239,28 @@ Notes: private: literal mk_at_most_1(bool full, unsigned n, literal const* xs) { + TRACE("pb", tout << (full?"full":"partial") << " "; + for (unsigned i = 0; i < n; ++i) tout << xs[i] << " "; + tout << "\n";); + + if (!full && n >= 4) { + return mk_at_most_1_bimander(n, xs); + } literal_vector in(n, xs); literal result = fresh(); unsigned inc_size = 4; + literal_vector ands; + ands.push_back(result); while (!in.empty()) { literal_vector ors; unsigned i = 0; unsigned n = in.size(); bool last = n <= inc_size; for (; i + inc_size < n; i += inc_size) { - mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ors); + mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ands, ors); } if (i < n) { - mk_at_most_1_small(full, last, n - i, in.c_ptr() + i, result, ors); + mk_at_most_1_small(full, last, n - i, in.c_ptr() + i, result, ands, ors); } if (last) { break; @@ -255,10 +269,20 @@ Notes: in.append(ors); ors.reset(); } + if (full) { + add_clause(ands); + } return result; } - void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ors) { + void mk_at_most_1_small(bool full, bool last, unsigned n, literal const* xs, literal result, literal_vector& ands, literal_vector& ors) { + SASSERT(n > 0); + if (n == 1) { + if (!last) { + ors.push_back(xs[0]); + } + return; + } if (!last) { literal ex = fresh(); for (unsigned j = 0; j < n; ++j) { @@ -271,16 +295,59 @@ Notes: } ors.push_back(ex); } + // result => xs[0] + ... + xs[n-1] <= 1 for (unsigned i = 0; i < n; ++i) { for (unsigned j = i + 1; j < n; ++j) { add_clause(ctx.mk_not(result), ctx.mk_not(xs[i]), ctx.mk_not(xs[j])); } - if (full) { - add_clause(result, xs[i]); + } + // xs[0] + ... + xs[n-1] <= 1 => and_x + if (full) { + literal and_i = fresh(); + for (unsigned i = 0; i < n; ++i) { + literal_vector lits; + lits.push_back(and_i); + for (unsigned j = 0; j < n; ++j) { + if (j != i) lits.push_back(xs[j]); + } + add_clause(lits); } + ands.push_back(ctx.mk_not(and_i)); } } + literal mk_at_most_1_bimander(unsigned n, literal const* xs) { + literal_vector in(n, xs); + literal result = fresh(); + unsigned inc_size = 2; + bool last = false; + bool full = false; + literal_vector ors, ands; + unsigned i = 0; + for (; i + inc_size < n; i += inc_size) { + mk_at_most_1_small(full, last, inc_size, in.c_ptr() + i, result, ands, ors); + } + if (i < n) { + mk_at_most_1_small(full, last, n - i, in.c_ptr() + i, result, ands, ors); + } + + unsigned nbits = 0; + while (static_cast(1 << nbits) < ors.size()) { + ++nbits; + } + literal_vector bits; + for (unsigned k = 0; k < nbits; ++k) { + bits.push_back(fresh()); + } + for (i = 0; i < ors.size(); ++i) { + for (unsigned k = 0; k < nbits; ++k) { + bool bit_set = (i & (static_cast(1 << k))) != 0; + add_clause(ctx.mk_not(result), ctx.mk_not(ors[i]), bit_set ? bits[k] : ctx.mk_not(bits[k])); + } + } + return result; + } + std::ostream& pp(std::ostream& out, unsigned n, literal const* lits) { for (unsigned i = 0; i < n; ++i) ctx.pp(out, lits[i]) << " "; return out; @@ -344,9 +411,13 @@ Notes: literal lits[2] = { l1, l2 }; add_clause(2, lits); } + void add_clause(literal_vector const& lits) { + add_clause(lits.size(), lits.c_ptr()); + } void add_clause(unsigned n, literal const* ls) { m_stats.m_num_compiled_clauses++; literal_vector tmp(n, ls); + TRACE("pb", for (unsigned i = 0; i < n; ++i) tout << ls[i] << " "; tout << "\n";); ctx.mk_clause(n, tmp.c_ptr()); } @@ -383,7 +454,7 @@ Notes: } void card(unsigned k, unsigned n, literal const* xs, literal_vector& out) { - TRACE("pb", tout << "card k:" << k << " n: " << n << "\n";); + TRACE("pb", tout << "card k: " << k << " n: " << n << "\n";); if (n <= k) { psort_nw::sorting(n, xs, out); } @@ -397,7 +468,7 @@ Notes: card(k, n-l, xs + l, out2); smerge(k, out1.size(), out1.c_ptr(), out2.size(), out2.c_ptr(), out); } - TRACE("pb", tout << "card k:" << k << " n: " << n << "\n"; + TRACE("pb", tout << "card k: " << k << " n: " << n << "\n"; pp(tout << "in:", n, xs) << "\n"; pp(tout << "out:", out) << "\n";); @@ -743,7 +814,7 @@ Notes: if (j < b) { ls.push_back(as[i]); ls.push_back(bs[j]); - add_clause(ls.size(), ls.c_ptr()); + add_clause(ls); ls.pop_back(); ls.pop_back(); } @@ -804,7 +875,7 @@ Notes: pp(tout, lits) << "\n";); SASSERT(k + offset <= n); if (k == 0) { - add_clause(lits.size(), lits.c_ptr()); + add_clause(lits); return; } for (unsigned i = offset; i < n - k + 1; ++i) {