mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

bmc/farkas/smt2 pattern printing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-11 09:34:15 -07:00
parent 27a5bd5b83
commit 89ca9aa5bd
4 changed files with 22 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

14
lib/ast_smt_pp.cpp
View file

@ -602,12 +602,22 @@ class smt_printer {
}
}
m_out << " :pat { ";
if (m_is_smt2) {
m_out << " :pattern ( ";
}
else {
m_out << " :pat { ";
}
for (unsigned j = 0; j < pat->get_num_args(); ++j) {
print_no_lets(pat->get_arg(j));
m_out << " ";
}
m_out << "}";
if (m_is_smt2) {
m_out << ")";
}
else {
m_out << "}";
}
}
if (m_is_smt2 && q->get_num_patterns() > 0) {
m_out << ")";

7
lib/dl_bmc_engine.cpp
View file

@ -27,6 +27,7 @@ Revision History:
#include "dl_decl_plugin.h"
#include "bool_rewriter.h"
#include "model_smt2_pp.h"
#include "ast_smt_pp.h"
namespace datalog {
bmc::bmc(context& ctx):
@ -711,7 +712,11 @@ namespace datalog {
md->eval(trace, trace);
md->eval(path, path);
IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n";);
IF_VERBOSE(2, m_solver.display(verbose_stream()); verbose_stream() << "\n";);
ast_smt_pp pp(m);
for (unsigned i = 0; i < m_solver.size(); ++i) {
pp.add_assumption(m_solver.get_formulas()[i]);
}
IF_VERBOSE(2, pp.display_smt2(verbose_stream(), m.mk_true()); verbose_stream() << "\n";);
m_answer = get_proof(md, to_app(trace), to_app(path));
is_sat = l_true;
}

3
lib/dl_check_table.cpp
View file

@ -96,6 +96,9 @@ namespace datalog {
(*m_tocheck)(tocheck(tgt), tocheck(src), tocheck(delta));
(*m_checker)(checker(tgt), checker(src), checker(delta));
get(tgt).well_formed();
if (delta) {
get(*delta).well_formed();
}
}
};

2
lib/pdr_farkas_learner.cpp
View file

@ -329,7 +329,7 @@ namespace pdr {
m_ctx->pop(1);
IF_VERBOSE(3, {
for (unsigned i = 0; i < lemmas.size(); ++i) {
for (unsigned i = 0; i < ilemmas.size(); ++i) {
verbose_stream() << "B': " << mk_pp(ilemmas[i].get(), m) << "\n";
}
});