mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

tidy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-09 08:24:14 -08:00
parent d2d42f9810
commit 0fd4c4fb06
1 changed files with 0 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/smt/theory_seq.cpp
View file

@ -5083,35 +5083,9 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
TRACE("seq", ctx.display_literals_verbose(tout << "assert:\n", lits) << "\n";);
m_new_propagation = true;
++m_stats.m_add_axiom;
#if 0
static unsigned level = 0;
if (level == 0) {
level++;
disable_trace("seq");
kernel k(m, ctx.get_fparams());
expr_ref tmp(m);
for (literal lit: lits) {
ctx.literal2expr(~lit, tmp);
k.assert_expr(tmp);
}
lbool r = k.check();
enable_trace("seq");
if (r == l_true) {
k.display(std::cout); std::cout << "\n";
TRACE("seq", k.display(tout << "sat\n"); tout << "\n";);
}
level--;
}
#endif
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
#if 0
void theory_seq::dump_axiom(literal_vector const& lits) {
display_lemma_as_smt_problem(std::cout << "; lemma\n", lits.size(), lits.c_ptr());
}
#endif
expr_ref theory_seq::coalesce_chars(expr* const& e) {
context& ctx = get_context();