From ab4fbe40b67b630203ed688269e98b6427b58b89 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 3 May 2017 17:45:56 -0400
Subject: [PATCH] cleanup
---
.gitignore | 1 -
src/ast/ast_smt2_pp.h | 2 +-
src/ast/ast_smt_pp.cpp | 1 -
src/ast/rewriter/rewriter.txt | 1 -
src/parsers/smt2/smt2parser.cpp | 3 +--
src/smt/smt_context.cpp | 7 +------
src/smt/smt_theory.h | 16 ++++++++--------
7 files changed, 11 insertions(+), 20 deletions(-)
diff --git a/.gitignore b/.gitignore
index 7cc289168..cc1c2a754 100644
--- a/.gitignore
+++ b/.gitignore
@@ -86,4 +86,3 @@ src/*/*/CMakeLists.txt
src/*/*/*/CMakeLists.txt
src/api/dotnet/cmake_install_gac.cmake.in
src/api/dotnet/cmake_uninstall_gac.cmake.in
-
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 244594461..f2d177041 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -55,8 +55,8 @@ public:
virtual format_ns::format * pp_bv_literal(app * t, bool use_bv_lits, bool bv_neg);
virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec);
virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits);
- virtual format_ns::format * pp_string_literal(app * t);
virtual format_ns::format * pp_datalog_literal(app * t);
+ virtual format_ns::format * pp_string_literal(app * t);
virtual format_ns::format * pp_sort(sort * s);
virtual format_ns::format * pp_fdecl_ref(func_decl * f);
format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len) const;
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index f41350dc5..706f65ac4 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -406,7 +406,6 @@ class smt_printer {
void visit_app(app* n) {
rational val;
- const char *str;
bool is_int, pos;
buffer<symbol> names;
unsigned bv_size;
diff --git a/src/ast/rewriter/rewriter.txt b/src/ast/rewriter/rewriter.txt
index a7a9e5eff..9eb016af2 100644
--- a/src/ast/rewriter/rewriter.txt
+++ b/src/ast/rewriter/rewriter.txt
@@ -8,7 +8,6 @@ The following classes implement theory specific rewriting rules:
- datatype_rewriter
- fpa_rewriter
- seq_rewriter
- - str_rewriter
Each of them provide the method
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result)
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 491aca8ba..1486f6e6c 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -66,8 +66,7 @@ namespace smt2 {
scoped_ptr<bv_util> m_bv_util;
scoped_ptr<arith_util> m_arith_util;
- scoped_ptr<seq_util> m_seq_util;
-
+ scoped_ptr<seq_util> m_seq_util;
scoped_ptr<pattern_validator> m_pattern_validator;
scoped_ptr<var_shifter> m_var_shifter;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 68a9f980d..535ae3b1e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1714,12 +1714,6 @@ namespace smt {
for (unsigned i = 0; i < m_th_eq_propagation_queue.size() && !inconsistent(); i++) {
new_th_eq curr = m_th_eq_propagation_queue[i];
theory * th = get_theory(curr.m_th_id);
- TRACE("t_str_eq_bug", tout
- << "th->name = " << th->get_name() << std::endl
- << "m_th_id = " << curr.m_th_id << std::endl
- << "m_lhs = " << curr.m_lhs << std::endl
- << "m_rhs = " << curr.m_rhs << std::endl
- << std::endl;);
SASSERT(th);
th->new_eq_eh(curr.m_lhs, curr.m_rhs);
#ifdef Z3DEBUG
@@ -3042,6 +3036,7 @@ namespace smt {
// not counting any literals that get assigned by this method
// this relies on bcp() to give us its old m_qhead and therefore
// bcp() should always be called before this method
+
unsigned assigned_literal_end = m_assigned_literals.size();
for (; qhead < assigned_literal_end; ++qhead) {
literal l = m_assigned_literals[qhead];
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index 7dd2819e4..67091c601 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -185,6 +185,14 @@ namespace smt {
virtual void add_theory_assumptions(expr_ref_vector & assumptions) {
}
+ /**
+ \brief This method is called from the smt_context when an unsat core is generated.
+ The theory may change the answer to UNKNOWN by returning l_undef from this method.
+ */
+ virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) {
+ return l_false;
+ }
+
/**
\brief This method is invoked before the search starts.
*/
@@ -200,14 +208,6 @@ namespace smt {
return FC_DONE;
}
- /**
- \brief This method is called from the smt_context when an unsat core is generated.
- The theory may change the answer to UNKNOWN by returning l_undef from this method.
- */
- virtual lbool validate_unsat_core(expr_ref_vector & unsat_core) {
- return l_false;
- }
-
/**
\brief Parametric theories (e.g. Arrays) should implement this method.
See example in context::is_shared