From 2751cbc2703c49d9d38a624db9baf3a63a71bc6a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Sep 2017 22:36:36 -0500 Subject: [PATCH] n/a Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 6 +++++ src/sat/sat_solver.cpp | 7 +++--- src/sat/sat_solver/inc_sat_solver.cpp | 13 ++++++---- src/sat/tactic/sat_tactic.cpp | 35 +++++++++++++-------------- src/smt/smt_internalizer.cpp | 12 ++------- src/smt/theory_dense_diff_logic_def.h | 14 ++++++----- src/smt/theory_diff_logic_def.h | 1 - src/test/ddnf.cpp | 16 +++++++++++- src/test/main.cpp | 1 + src/test/sorting_network.cpp | 17 +++++++------ 10 files changed, 70 insertions(+), 52 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index fa3b06649..260d49174 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1549,13 +1549,19 @@ void cmd_context::display_dimacs() { if (m_solver) { try { gparams::set("sat.dimacs.display", "true"); + params_ref p; + m_solver->updt_params(p); m_solver->check_sat(0, nullptr); } catch (...) { gparams::set("sat.dimacs.display", "false"); + params_ref p; + m_solver->updt_params(p); throw; } gparams::set("sat.dimacs.display", "false"); + params_ref p; + m_solver->updt_params(p); } } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 2fa0c46f0..63f1badb7 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -724,6 +724,8 @@ namespace sat { pop_to_base_level(); IF_VERBOSE(2, verbose_stream() << "(sat.sat-solver)\n";); SASSERT(scope_lvl() == 0); + SASSERT(m_config.m_dimacs_display); + std::cout << "display dimacs: " << m_config.m_dimacs_display << "\n"; if (m_config.m_dimacs_display) { display_dimacs(std::cout); for (unsigned i = 0; i < num_lits; ++lits) { @@ -1249,10 +1251,7 @@ namespace sat { } void solver::sort_watch_lits() { - vector::iterator it = m_watches.begin(); - vector::iterator end = m_watches.end(); - for (; it != end; ++it) { - watch_list & wlist = *it; + for (watch_list & wlist : m_watches) { std::stable_sort(wlist.begin(), wlist.end(), watched_lt()); } } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 69645d705..be418cbc4 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -162,6 +162,11 @@ public: if (r != l_true) return r; r = m_solver.check(m_asms.size(), m_asms.c_ptr()); + if (r == l_undef && m_solver.get_config().m_dimacs_display) { + for (auto const& kv : m_map) { + std::cout << "c " << kv.m_value << " " << mk_pp(kv.m_key, m) << "\n"; + } + } switch (r) { case l_true: @@ -643,14 +648,12 @@ private: } sat::model const & ll_m = m_solver.get_model(); model_ref md = alloc(model, m); - atom2bool_var::iterator it = m_map.begin(); - atom2bool_var::iterator end = m_map.end(); - for (; it != end; ++it) { - expr * n = it->m_key; + for (auto const& kv : m_map) { + expr * n = kv.m_key; if (is_app(n) && to_app(n)->get_num_args() > 0) { continue; } - sat::bool_var v = it->m_value; + sat::bool_var v = kv.m_value; switch (sat::value_at(v, ll_m)) { case l_true: md->register_decl(to_app(n)->get_decl(), m.mk_true()); diff --git a/src/sat/tactic/sat_tactic.cpp b/src/sat/tactic/sat_tactic.cpp index 9b706597d..4a6171f70 100644 --- a/src/sat/tactic/sat_tactic.cpp +++ b/src/sat/tactic/sat_tactic.cpp @@ -16,11 +16,11 @@ Author: Notes: --*/ +#include "ast/ast_pp.h" #include "tactic/tactical.h" +#include "tactic/filter_model_converter.h" #include "sat/tactic/goal2sat.h" #include "sat/sat_solver.h" -#include "tactic/filter_model_converter.h" -#include "ast/ast_smt2_pp.h" #include "model/model_v2_pp.h" class sat_tactic : public tactic { @@ -56,11 +56,9 @@ class sat_tactic : public tactic { sat::literal_vector assumptions; m_goal2sat(*g, m_params, m_solver, map, dep2asm); TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n"; - atom2bool_var::iterator it = map.begin(); - atom2bool_var::iterator end = map.end(); - for (; it != end; ++it) { - if (!is_uninterp_const(it->m_key)) - tout << mk_ismt2_pp(it->m_key, m) << "\n"; + for (auto const& kv : map) { + if (!is_uninterp_const(kv.m_key)) + tout << mk_ismt2_pp(kv.m_key, m) << "\n"; }); g->reset(); g->m().compact_memory(); @@ -70,6 +68,11 @@ class sat_tactic : public tactic { TRACE("sat_dimacs", m_solver.display_dimacs(tout);); dep2assumptions(dep2asm, assumptions); lbool r = m_solver.check(assumptions.size(), assumptions.c_ptr()); + if (r == l_undef && m_solver.get_config().m_dimacs_display) { + for (auto const& kv : map) { + std::cout << "c " << kv.m_value << " " << mk_pp(kv.m_key, g->m()) << "\n"; + } + } if (r == l_false) { expr_dependency * lcore = 0; if (produce_core) { @@ -90,11 +93,9 @@ class sat_tactic : public tactic { model_ref md = alloc(model, m); sat::model const & ll_m = m_solver.get_model(); TRACE("sat_tactic", for (unsigned i = 0; i < ll_m.size(); i++) tout << i << ":" << ll_m[i] << " "; tout << "\n";); - atom2bool_var::iterator it = map.begin(); - atom2bool_var::iterator end = map.end(); - for (; it != end; ++it) { - expr * n = it->m_key; - sat::bool_var v = it->m_value; + for (auto const& kv : map) { + expr * n = kv.m_key; + sat::bool_var v = kv.m_value; TRACE("sat_tactic", tout << "extracting value of " << mk_ismt2_pp(n, m) << "\nvar: " << v << "\n";); switch (sat::value_at(v, ll_m)) { case l_true: @@ -126,17 +127,15 @@ class sat_tactic : public tactic { void dep2assumptions(obj_map& dep2asm, sat::literal_vector& assumptions) { - obj_map::iterator it = dep2asm.begin(), end = dep2asm.end(); - for (; it != end; ++it) { - assumptions.push_back(it->m_value); + for (auto const& kv : dep2asm) { + assumptions.push_back(kv.m_value); } } void mk_asm2dep(obj_map& dep2asm, u_map& lit2asm) { - obj_map::iterator it = dep2asm.begin(), end = dep2asm.end(); - for (; it != end; ++it) { - lit2asm.insert(it->m_value.index(), it->m_key); + for (auto const& kv : dep2asm) { + lit2asm.insert(kv.m_value.index(), kv.m_key); } } }; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 58b391ac2..5a8a313ba 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -201,16 +201,8 @@ namespace smt { TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m_manager);); svector sorted_exprs; top_sort_expr(n, sorted_exprs); - TRACE("deep_internalize", - svector::const_iterator it = sorted_exprs.begin(); - svector::const_iterator end = sorted_exprs.end(); - for (; it != end; ++it) { - tout << "#" << it->first->get_id() << " " << it->second << "\n"; - }); - svector::const_iterator it = sorted_exprs.begin(); - svector::const_iterator end = sorted_exprs.end(); - for (; it != end; ++it) - internalize(it->first, it->second); + TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; ); + for (auto & kv : sorted_exprs) internalize(kv.first, kv.second); } SASSERT(m_manager.is_bool(n)); if (is_gate(m_manager, n)) { diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index ad7727a89..064bdd433 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -151,14 +151,15 @@ namespace smt { m_autil.is_numeral(rhs, _k); numeral offset(_k); app * s, * t; - if (m_autil.is_add(lhs) && to_app(lhs)->get_num_args() == 2 && is_times_minus_one(to_app(lhs)->get_arg(1), s)) { - t = to_app(to_app(lhs)->get_arg(0)); + expr *arg1, *arg2; + if (m_autil.is_add(lhs, arg1, arg2) && is_times_minus_one(arg2, s)) { + t = to_app(arg1); } - else if (m_autil.is_add(lhs) && to_app(lhs)->get_num_args() == 2 && is_times_minus_one(to_app(lhs)->get_arg(0), s)) { - t = to_app(to_app(lhs)->get_arg(1)); + else if (m_autil.is_add(lhs, arg1, arg2) && is_times_minus_one(arg1, s)) { + t = to_app(arg2); } - else if (m_autil.is_mul(lhs) && to_app(lhs)->get_num_args() == 2 && m_autil.is_minus_one(to_app(lhs)->get_arg(0))) { - s = to_app(to_app(lhs)->get_arg(1)); + else if (m_autil.is_mul(lhs, arg1, arg2) && m_autil.is_minus_one(arg1)) { + s = to_app(arg2); t = mk_zero_for(s); } else if (!m_autil.is_arith_expr(lhs)) { @@ -170,6 +171,7 @@ namespace smt { found_non_diff_logic_expr(n); return false; } + TRACE("arith", tout << expr_ref(lhs, get_manager()) << " " << expr_ref(s, get_manager()) << " " << expr_ref(t, get_manager()) << "\n";); source = internalize_term_core(s); target = internalize_term_core(t); if (source == null_theory_var || target == null_theory_var) { diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 02cc8860f..a7153234c 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -733,7 +733,6 @@ theory_var theory_diff_logic::mk_term(app* n) { source = mk_var(a); for (unsigned i = 0; i < n->get_num_args(); ++i) { expr* arg = n->get_arg(i); - std::cout << "internalize: " << mk_pp(arg, get_manager()) << " " << ctx.e_internalized(arg) << "\n"; if (!ctx.e_internalized(arg)) { ctx.internalize(arg, false); } diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index 3f8e748be..09f1a4cf9 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -200,6 +200,20 @@ void tst_ddnf(char ** argv, int argc, int& i) { dealloc(ddnf); } - +void tst_ddnf1() { + enable_trace("ddnf"); + unsigned W = 2; + datalog::ddnf_core ddnf(W); + tbv_manager& tbvm = ddnf.get_tbv_manager(); + tbv* tXX = tbvm.allocate("xx"); + tbv* t1X = tbvm.allocate("1x"); + tbv* tX1 = tbvm.allocate("x1"); + tbv* t11 = tbvm.allocate("11"); + ddnf.insert(*tXX); + ddnf.insert(*t11); + ddnf.insert(*tX1); + ddnf.insert(*t1X); + ddnf.display(std::cout); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index d0d0aac5b..03fbba1df 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -237,6 +237,7 @@ int main(int argc, char ** argv) { TST(sat_user_scope); TST(pdr); TST_ARGV(ddnf); + TST(ddnf1); TST(model_evaluator); TST_ARGV(lp); TST(get_consequences); diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index 2984e94e2..1062057f6 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -6,16 +6,14 @@ Copyright (c) 2015 Microsoft Corporation #include "util/trace.h" #include "util/vector.h" +#include "util/sorting_network.h" #include "ast/ast.h" #include "ast/ast_pp.h" #include "ast/reg_decl_plugins.h" -#include "util/sorting_network.h" -#include "smt/smt_kernel.h" -#include "model/model_smt2_pp.h" -#include "smt/params/smt_params.h" #include "ast/ast_util.h" - - +#include "model/model_smt2_pp.h" +#include "smt/smt_kernel.h" +#include "smt/params/smt_params.h" struct ast_ext { ast_manager& m; @@ -388,7 +386,6 @@ void test_at_most_1(unsigned n, bool full) { std::cout << atom << "\n"; if (is_true) ++k; } - VERIFY(l_false == solver.check()); if (k > 1) { solver.assert_expr(result1); } @@ -427,6 +424,12 @@ void tst_sorting_network() { test_at_most_1(i, true); test_at_most_1(i, false); } + + for (unsigned n = 2; n < 20; ++n) { + std::cout << "verify eq-1 out of " << n << "\n"; + test_sorting_eq(n, 1); + } + test_at_most1(); test_sorting_eq(11,7);