From 58198d7cb69df67b0c7974f55109613839975300 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Oct 2016 15:45:39 -0400 Subject: [PATCH] add consequence finding to inc-sat-solver Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/pb_rewriter.cpp | 15 --------------- src/smt/theory_pb.cpp | 2 +- 2 files changed, 1 insertion(+), 16 deletions(-) diff --git a/src/ast/rewriter/pb_rewriter.cpp b/src/ast/rewriter/pb_rewriter.cpp index 74062fbfa..d233604f9 100644 --- a/src/ast/rewriter/pb_rewriter.cpp +++ b/src/ast/rewriter/pb_rewriter.cpp @@ -278,21 +278,6 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons tout << result << "\n"; ); -#if 0 - static unsigned num_changes = 0; - static unsigned num_calls = 0; - static unsigned inc = 1; - { - expr_ref tmp(m); - tmp = m.mk_app(f, num_args, args); - num_calls++; - if (tmp != result) ++num_changes; - if (num_calls > inc) { - std::cout << num_calls << " " << num_changes << "\n"; - inc *= 2; - } - } -#endif TRACE("pb_validate", validate_rewrite(f, num_args, args, result);); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 2461a9db2..90cd020c3 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -519,7 +519,7 @@ namespace smt { c->m_compilation_threshold = th; IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threhshold to " << th << ")\n";); TRACE("pb", tout << "compilation threshold: " << th << "\n";); - compile_ineq(*c); + //compile_ineq(*c); } else { c->m_compilation_threshold = UINT_MAX;