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<watch_list>::iterator it = m_watches.begin();
- vector<watch_list>::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<expr, sat::literal>& dep2asm,
sat::literal_vector& assumptions) {
- obj_map<expr, sat::literal>::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<expr, sat::literal>& dep2asm,
u_map<expr*>& lit2asm) {
- obj_map<expr, sat::literal>::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<expr_bool_pair> sorted_exprs;
top_sort_expr(n, sorted_exprs);
- TRACE("deep_internalize",
- svector<expr_bool_pair>::const_iterator it = sorted_exprs.begin();
- svector<expr_bool_pair>::const_iterator end = sorted_exprs.end();
- for (; it != end; ++it) {
- tout << "#" << it->first->get_id() << " " << it->second << "\n";
- });
- svector<expr_bool_pair>::const_iterator it = sorted_exprs.begin();
- svector<expr_bool_pair>::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<Ext>::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);