From bee4716a850f96283c3f71bda67d44c4f93df429 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Feb 2018 12:56:30 -0800 Subject: [PATCH] lia2card simplifications, move up before elim01 (which could be deprecated) Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb_rewriter.cpp | 3 +++ src/opt/opt_context.cpp | 4 ++-- src/opt/opt_parse.cpp | 27 +++++++++++++++++++++++- src/sat/sat_big.cpp | 9 +++++++- src/tactic/arith/lia2card_tactic.cpp | 6 ++++-- src/tactic/portfolio/parallel_tactic.cpp | 4 ++++ src/util/util.h | 12 +++++++---- 7 files changed, 55 insertions(+), 10 deletions(-) diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 8bf7f2078..42efb3c6c 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -272,6 +272,9 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons else if (k.is_one() && all_unit && m_args.size() == 1) { result = m_args.back(); } + else if (slack == k) { + result = mk_and(m, sz, m_args.c_ptr()); + } else { result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k); } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 9e72d24dc..e62a1c647 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -735,8 +735,8 @@ namespace opt { tactic_ref tac1, tac2, tac3, tac4; if (optp.elim_01()) { tac1 = mk_dt2bv_tactic(m); - tac2 = mk_elim01_tactic(m); - tac3 = mk_lia2card_tactic(m); + tac2 = mk_lia2card_tactic(m); + tac3 = mk_elim01_tactic(m); tac4 = mk_eq2bv_tactic(m); params_ref lia_p; lia_p.set_bool("compile_equality", optp.pb_compile_equality()); diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp index 5ca1faed6..758379517 100644 --- a/src/opt/opt_parse.cpp +++ b/src/opt/opt_parse.cpp @@ -386,6 +386,26 @@ private: in.skip_line(); continue; } + bool neg = false; + if (c == '-') { + in.next(); + c = in.ch(); + m_buffer.reset(); + m_buffer.push_back('-'); + if (is_num(c)) { + neg = true; + } + else { + while (!is_ws(c) && !in.eof()) { + m_buffer.push_back(c); + in.next(); + c = in.ch(); + } + m_buffer.push_back(0); + m_tokens.push_back(asymbol(symbol(m_buffer.c_ptr()), in.line())); + continue; + } + } if (is_num(c)) { rational n(0); @@ -405,6 +425,7 @@ private: } } if (div > 1) n = n / rational(div); + if (neg) n.neg(); m_tokens.push_back(asymbol(n, in.line())); continue; } @@ -453,6 +474,7 @@ private: c == '{' || c == '}' || c == ',' || + c == '_' || c == '.' || c == ';' || c == '?' || @@ -687,13 +709,16 @@ private: tok.next(2); } } - if (peek_le(1) && tok.peek_num(2)) { + else if (peek_le(1) && tok.peek_num(2)) { v = peek(0); tok.next(2); rational rhs = tok.get_num(0); update_upper(v, rhs); tok.next(1); } + else { + error("bound expected"); + } } void update_lower(rational const& r, symbol const& v) { diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 9c2bef50e..b7dc0bf8a 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -28,7 +28,7 @@ namespace sat { void big::init(solver& s, bool learned) { init_adding_edges(s.num_vars(), learned); unsigned num_lits = m_num_vars * 2; - literal_vector lits; + literal_vector lits, r; SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size()); for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) { literal u = to_literal(l_idx); @@ -41,6 +41,13 @@ namespace sat { m_roots[v.index()] = false; edges.push_back(v); } +#if 0 + if (w.is_ext_constraint() && + s.m_ext && + s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), r)) { + IF_VERBOSE(0, verbose_stream() << "extended binary " << r.size() << "\n";); + } +#endif } } done_adding_edges(); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 4e97b1e57..bc7e3a4ee 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -160,6 +160,9 @@ public: expr_ref_vector xs(m); expr_ref last_v(m); if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card"); + if (hi == 0) { + return expr_ref(a.mk_int(0), m); + } if (lo > 0) { xs.push_back(a.mk_int(lo)); } @@ -183,7 +186,7 @@ public: expr_ref_vector axioms(m); expr_safe_replace rep(m); - tactic_report report("cardinality-intro", *g); + tactic_report report("lia2card", *g); bound_manager bounds(m); bounds(*g); @@ -205,7 +208,6 @@ public: expr_ref new_curr(m), tmp(m); proof_ref new_pr(m); rep(g->form(i), tmp); - if (tmp == g->form(i)) continue; m_rw(tmp, new_curr, new_pr); if (m.proofs_enabled() && !new_pr) { new_pr = m.mk_rewrite(g->form(i), new_curr); diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index f4982c2c2..4a5af3679 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -242,6 +242,7 @@ class parallel_tactic : public tactic { lbool simplify() { lbool r = l_undef; if (m_depth == 1) { + IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-1)\n";); set_simplify_params(true, true); // retain PB, retain blocked r = get_solver().check_sat(0,0); if (r != l_undef) return r; @@ -255,9 +256,11 @@ class parallel_tactic : public tactic { m_solver->set_model_converter(mc.get()); m_solver->assert_expr(fmls); } + IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-2)\n";); set_simplify_params(false, true); // remove PB, retain blocked r = get_solver().check_sat(0,0); if (r != l_undef) return r; + IF_VERBOSE(2, verbose_stream() << "(parallel.tactic simplify-3)\n";); set_simplify_params(false, false); // remove any PB, remove blocked r = get_solver().check_sat(0,0); return r; @@ -398,6 +401,7 @@ private: cube.reset(); cube.append(s.split_cubes(1)); SASSERT(cube.size() <= 1); + IF_VERBOSE(2, verbose_stream() << "(sat.parallel :split-cube " << cube.size() << ")\n";); if (!s.cubes().empty()) m_queue.add_task(s.clone()); if (!cube.empty()) s.assert_cube(cube.get(0)); s.inc_depth(1); diff --git a/src/util/util.h b/src/util/util.h index 931ea34b4..6da289071 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -197,13 +197,17 @@ bool is_threaded(); } \ } } ((void) 0) +#ifdef _NO_OMP_ +#define LOCK_CODE(CODE) CODE; +#else #define LOCK_CODE(CODE) \ { \ - __pragma(omp critical (verbose_lock)) \ - { \ - CODE; \ - } \ + __pragma(omp critical (verbose_lock)) \ + { \ + CODE; \ + } \ } +#endif template struct default_eq {