From a7bb41fd499556f3d30e50f06fcf4dfb0274d177 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Aug 2017 09:19:35 -0700 Subject: [PATCH] fix build issues Signed-off-by: Nikolaj Bjorner --- .../transforms/dl_mk_quantifier_instantiation.cpp | 1 + src/smt/asserted_formulas.cpp | 4 +++- src/smt/asserted_formulas.h | 13 +++++++------ 3 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index f32840c49..74d15bcdf 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -26,6 +26,7 @@ Revision History: #include "muz/transforms/dl_mk_quantifier_instantiation.h" #include "muz/base/dl_context.h" #include "ast/pattern/pattern_inference.h" +#include "ast/rewriter/rewriter_def.h" namespace datalog { diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index b475ee778..eac5f7c10 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -56,7 +56,8 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p): m_macro_manager(m), m_bit2int(m), m_bv_sharing(m), - m_inconsistent(false){ + m_inconsistent(false), + m_has_quantifiers(false) { m_bsimp = 0; m_bvsimp = 0; @@ -143,6 +144,7 @@ void asserted_formulas::set_eliminate_and(bool flag) { void asserted_formulas::assert_expr(expr * e, proof * _in_pr) { if (inconsistent()) return; + m_has_quantifiers |= ::has_quantifiers(e); if (!m_params.m_preprocess) { push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs); return; diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 093680fd9..eaed4e405 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -19,17 +19,17 @@ Revision History: #ifndef ASSERTED_FORMULAS_H_ #define ASSERTED_FORMULAS_H_ -#include "smt/params/smt_params.h" +#include "util/statistics.h" +#include "ast/static_features.h" #include "ast/simplifier/simplifier.h" #include "ast/simplifier/basic_simplifier_plugin.h" -#include "ast/static_features.h" +#include "ast/simplifier/maximise_ac_sharing.h" +#include "ast/simplifier/bit2int.h" #include "ast/macros/macro_manager.h" #include "ast/macros/macro_finder.h" #include "ast/normal_forms/defined_names.h" -#include "ast/simplifier/maximise_ac_sharing.h" -#include "ast/simplifier/bit2int.h" -#include "util/statistics.h" #include "ast/pattern/pattern_inference.h" +#include "smt/params/smt_params.h" class arith_simplifier_plugin; class bv_simplifier_plugin; @@ -55,6 +55,7 @@ class asserted_formulas { maximise_bv_sharing m_bv_sharing; bool m_inconsistent; + bool m_has_quantifiers; struct scope { unsigned m_asserted_formulas_lim; @@ -128,7 +129,7 @@ public: void display_ll(std::ostream & out, ast_mark & pp_visited) const; void collect_statistics(statistics & st) const; // TODO: improve precision of the following method. - bool has_quantifiers() const { return m_simplifier.visited_quantifier(); /* approximation */ } + bool has_quantifiers() const { return m_has_quantifiers; } // ----------------------------------- //