mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

test hilbert-basis with fdds and checked integers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-26 17:31:59 -07:00
parent 00e79e6b6b
commit 5c4003b4e5
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -212,7 +212,6 @@ namespace datalog {
ast_manager & m;
params_ref m_params;
rule_ref_vector m_rules;
th_rewriter m_theory_rewriter;
bit_blaster_rewriter m_blaster;
expand_mkbv m_rewriter;
@ -220,7 +219,6 @@ namespace datalog {
bool blast(expr_ref& fml) {
proof_ref pr(m);
expr_ref fml1(m), fml2(m);
m_theory_rewriter(fml);
m_blaster(fml, fml1, pr);
m_rewriter(fml1, fml2);
TRACE("dl", tout << mk_pp(fml, m) << " -> " << mk_pp(fml1, m) << " -> " << mk_pp(fml2, m) << "\n";);
@ -243,7 +241,6 @@ namespace datalog {
m(ctx.get_manager()),
m_params(ctx.get_params().p),
m_rules(ctx.get_rule_manager()),
m_theory_rewriter(m, m_params),
m_blaster(m, m_params),
m_rewriter(m, ctx, m_rules) {
m_params.set_bool("blast_full", true);