mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

n/a

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-23 22:36:36 -05:00
parent 95ee4c94f1
commit 2751cbc270
10 changed files with 70 additions and 52 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/cmd_context/cmd_context.cpp
View file

@ -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);
}
}

7
src/sat/sat_solver.cpp
View file

@ -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());
}
}

13
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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());

35
src/sat/tactic/sat_tactic.cpp
View file

@ -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);
}
}
};

12
src/smt/smt_internalizer.cpp
View file

@ -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)) {

14
src/smt/theory_dense_diff_logic_def.h
View file

@ -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) {

1
src/smt/theory_diff_logic_def.h
View file

@ -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);
}

16
src/test/ddnf.cpp
View file

@ -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);
}

1
src/test/main.cpp
View file

@ -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);

17
src/test/sorting_network.cpp
View file

@ -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);