From a02a794c383ae2381e1210f53174cefb8d94e615 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 3 Mar 2021 17:50:45 +0100 Subject: [PATCH] More cleanup of includes to reduce compilation times (#6037) Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files. --- src/base/exception.cpp | 8 ++ src/base/exception.h | 11 +-- src/base/listener.cpp | 4 - src/decision/decision_engine.cpp | 1 + src/decision/decision_engine.h | 9 +- src/decision/justification_heuristic.cpp | 99 ++++++++++--------- src/decision/justification_heuristic.h | 46 +++++---- src/expr/buffered_proof_generator.h | 2 +- src/expr/dtype.cpp | 2 + src/expr/kind_template.cpp | 2 + src/expr/lazy_proof.cpp | 1 + src/expr/lazy_proof.h | 5 +- src/expr/lazy_proof_chain.cpp | 1 + src/expr/lazy_proof_chain.h | 1 - src/expr/node.cpp | 3 +- src/expr/proof.cpp | 2 + src/expr/proof.h | 3 +- src/expr/proof_checker.cpp | 1 + src/expr/proof_checker.h | 3 +- src/expr/proof_ensure_closed.cpp | 4 + src/expr/proof_ensure_closed.h | 5 +- src/expr/proof_generator.cpp | 3 + src/expr/proof_generator.h | 2 +- src/expr/proof_node_algorithm.cpp | 2 + src/expr/proof_node_algorithm.h | 4 +- src/expr/proof_node_manager.cpp | 2 + src/expr/proof_node_manager.h | 7 +- src/expr/proof_node_to_sexpr.cpp | 2 + src/expr/proof_node_to_sexpr.h | 4 +- src/expr/proof_node_updater.cpp | 1 + src/expr/proof_node_updater.h | 9 +- src/expr/proof_step_buffer.cpp | 2 + src/expr/proof_step_buffer.h | 3 +- src/expr/record.h | 1 - src/expr/sequence.cpp | 1 + src/expr/subs.cpp | 2 + src/expr/sygus_datatype.cpp | 2 + src/expr/symbol_manager.h | 1 - src/expr/tconv_seq_proof_generator.cpp | 4 + src/expr/tconv_seq_proof_generator.h | 3 +- src/expr/term_canonize.cpp | 2 + src/expr/term_context_node.h | 2 +- src/expr/term_context_stack.cpp | 2 + src/expr/term_conversion_proof_generator.cpp | 3 + src/expr/term_conversion_proof_generator.h | 5 +- src/expr/type.cpp | 1 + src/expr/type_checker_template.cpp | 2 + src/expr/type_checker_util.h | 2 + src/expr/type_matcher.h | 1 - src/options/language.cpp | 5 + src/options/language.h | 11 +-- src/options/open_ostream.h | 4 +- src/options/options_handler.h | 5 +- src/preprocessing/assertion_pipeline.cpp | 1 + src/preprocessing/assertion_pipeline.h | 10 +- src/preprocessing/passes/ackermann.cpp | 6 +- src/preprocessing/passes/ackermann.h | 4 +- src/preprocessing/passes/apply_substs.cpp | 2 + src/preprocessing/passes/apply_substs.h | 4 +- src/preprocessing/passes/bool_to_bv.cpp | 3 + src/preprocessing/passes/bool_to_bv.h | 3 +- src/preprocessing/passes/bv_abstraction.cpp | 3 + src/preprocessing/passes/bv_abstraction.h | 1 - src/preprocessing/passes/bv_eager_atoms.cpp | 3 + src/preprocessing/passes/bv_eager_atoms.h | 1 - src/preprocessing/passes/bv_gauss.cpp | 9 +- src/preprocessing/passes/bv_gauss.h | 2 +- src/preprocessing/passes/bv_intro_pow2.cpp | 2 + src/preprocessing/passes/bv_intro_pow2.h | 1 - src/preprocessing/passes/bv_to_bool.cpp | 3 + src/preprocessing/passes/bv_to_bool.h | 3 +- src/preprocessing/passes/bv_to_int.cpp | 4 + src/preprocessing/passes/bv_to_int.h | 10 +- .../passes/extended_rewriter_pass.cpp | 2 + .../passes/extended_rewriter_pass.h | 1 - .../passes/foreign_theory_rewrite.cpp | 3 + .../passes/foreign_theory_rewrite.h | 6 +- src/preprocessing/passes/fun_def_fmf.cpp | 5 + src/preprocessing/passes/fun_def_fmf.h | 3 +- src/preprocessing/passes/global_negate.cpp | 1 + src/preprocessing/passes/global_negate.h | 2 +- src/preprocessing/passes/ho_elim.cpp | 1 + src/preprocessing/passes/ho_elim.h | 6 +- src/preprocessing/passes/int_to_bv.cpp | 2 + src/preprocessing/passes/int_to_bv.h | 1 - src/preprocessing/passes/ite_removal.cpp | 4 + src/preprocessing/passes/ite_removal.h | 4 - src/preprocessing/passes/ite_simp.cpp | 5 + src/preprocessing/passes/ite_simp.h | 2 +- src/preprocessing/passes/miplib_trick.cpp | 5 + src/preprocessing/passes/miplib_trick.h | 2 +- src/preprocessing/passes/nl_ext_purify.cpp | 3 + src/preprocessing/passes/nl_ext_purify.h | 1 - src/preprocessing/passes/non_clausal_simp.cpp | 8 +- src/preprocessing/passes/non_clausal_simp.h | 17 +++- .../passes/pseudo_boolean_processor.cpp | 2 + .../passes/pseudo_boolean_processor.h | 2 - .../passes/quantifier_macros.cpp | 4 + src/preprocessing/passes/quantifier_macros.h | 3 - .../passes/quantifiers_preprocess.cpp | 2 + .../passes/quantifiers_preprocess.h | 1 - src/preprocessing/passes/real_to_int.cpp | 3 + src/preprocessing/passes/real_to_int.h | 2 - src/preprocessing/passes/rewrite.cpp | 1 + src/preprocessing/passes/rewrite.h | 1 - src/preprocessing/passes/sep_skolem_emp.cpp | 2 + src/preprocessing/passes/sep_skolem_emp.h | 1 - src/preprocessing/passes/sort_infer.cpp | 4 + src/preprocessing/passes/sort_infer.h | 6 -- src/preprocessing/passes/static_learning.cpp | 3 + src/preprocessing/passes/static_learning.h | 1 - src/preprocessing/passes/strings_eager_pp.cpp | 3 +- src/preprocessing/passes/strings_eager_pp.h | 1 - src/preprocessing/passes/sygus_inference.cpp | 3 + src/preprocessing/passes/sygus_inference.h | 3 - src/preprocessing/passes/synth_rew_rules.cpp | 3 + src/preprocessing/passes/synth_rew_rules.h | 1 - .../passes/theory_preprocess.cpp | 6 +- src/preprocessing/passes/theory_preprocess.h | 1 - .../passes/theory_rewrite_eq.cpp | 2 + src/preprocessing/passes/theory_rewrite_eq.h | 2 +- .../passes/unconstrained_simplifier.cpp | 4 + .../passes/unconstrained_simplifier.h | 7 +- src/preprocessing/preprocessing_pass.cpp | 6 +- src/preprocessing/preprocessing_pass.h | 8 +- .../preprocessing_pass_context.h | 16 +-- .../preprocessing_pass_registry.h | 5 +- src/preprocessing/util/ite_utilities.cpp | 1 + src/preprocessing/util/ite_utilities.h | 6 +- src/printer/let_binding.h | 1 - src/printer/printer.h | 1 - src/proof/cnf_proof.h | 4 +- src/proof/proof_manager.h | 2 - src/prop/bvminisat/simp/SimpSolver.h | 7 +- src/prop/cnf_stream.h | 4 +- src/prop/minisat/core/Solver.h | 1 + src/prop/prop_engine.cpp | 33 ++++--- src/prop/prop_engine.h | 23 +---- src/prop/prop_proof_manager.cpp | 2 + src/prop/prop_proof_manager.h | 2 + src/prop/sat_proof_manager.h | 8 +- src/prop/theory_proxy.h | 5 +- src/smt/abduction_solver.cpp | 2 + src/smt/assertions.cpp | 1 + src/smt/assertions.h | 4 +- src/smt/check_models.cpp | 2 + src/smt/check_models.h | 5 +- src/smt/command.h | 3 - src/smt/dump_manager.h | 6 +- src/smt/expand_definitions.cpp | 2 + src/smt/expand_definitions.h | 14 ++- src/smt/interpolation_solver.cpp | 2 + src/smt/managed_ostreams.h | 5 +- src/smt/model.h | 6 +- src/smt/model_blocker.cpp | 2 + src/smt/model_blocker.h | 5 +- src/smt/node_command.cpp | 2 + src/smt/options_manager.h | 4 +- src/smt/preprocess_proof_generator.cpp | 2 + src/smt/preprocess_proof_generator.h | 2 - src/smt/preprocessor.cpp | 2 + src/smt/preprocessor.h | 6 +- src/smt/process_assertions.cpp | 3 + src/smt/process_assertions.h | 10 +- src/smt/proof_manager.cpp | 4 + src/smt/proof_manager.h | 11 +-- src/smt/proof_post_processor.cpp | 1 + src/smt/proof_post_processor.h | 1 + src/smt/smt_engine.cpp | 2 + src/smt/smt_engine.h | 2 - src/smt/smt_solver.cpp | 27 ++--- src/smt/term_formula_removal.cpp | 3 + src/smt/term_formula_removal.h | 12 +-- src/theory/arith/delta_rational.cpp | 2 + src/theory/arith/nl/iand_solver.cpp | 1 + .../booleans/proof_circuit_propagator.cpp | 2 + src/theory/bv/bitblast/bitblaster.h | 1 + src/theory/bv/bv_solver_bitblast.h | 1 + src/theory/datatypes/sygus_datatype_utils.cpp | 2 + src/theory/datatypes/theory_datatypes.cpp | 1 + src/theory/inference_id.cpp | 2 + src/theory/lazy_tree_proof_generator.cpp | 1 + .../quantifiers/single_inv_partition.cpp | 2 + .../quantifiers/sygus/cegis_core_connective.h | 3 +- src/theory/quantifiers/sygus/sygus_abduct.cpp | 2 + .../quantifiers/sygus/sygus_interpol.cpp | 2 + src/theory/quantifiers/sygus/sygus_utils.cpp | 2 + .../quantifiers/sygus/term_database_sygus.cpp | 1 + src/theory/quantifiers/sygus_sampler.cpp | 1 + src/theory/strings/regexp_operation.cpp | 2 + src/theory/strings/theory_strings_utils.cpp | 2 + src/theory/theory_engine.cpp | 2 + src/theory/theory_engine_proof_generator.cpp | 4 + src/theory/theory_id.cpp | 2 + src/theory/uf/cardinality_extension.cpp | 2 + src/theory/uf/eq_proof.cpp | 1 + src/theory/uf/theory_uf.cpp | 1 + src/util/bitvector.h | 2 + src/util/cardinality.cpp | 1 + src/util/integer_gmp_imp.h | 6 +- src/util/poly_util.cpp | 1 + src/util/rational_gmp_imp.h | 2 +- src/util/result.cpp | 1 + src/util/result.h | 3 +- src/util/safe_print.cpp | 3 + src/util/safe_print.h | 5 +- src/util/sampler.cpp | 3 + src/util/sampler.h | 1 - src/util/sexpr.h | 2 - src/util/string.h | 4 +- .../preprocessing/pass_bv_gauss_white.cpp | 1 + test/unit/prop/cnf_stream_white.cpp | 1 + test/unit/util/cardinality_black.cpp | 1 + test/unit/util/integer_black.cpp | 1 + 214 files changed, 571 insertions(+), 343 deletions(-) diff --git a/src/base/exception.cpp b/src/base/exception.cpp index cddef79fd..ad50ec351 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -20,6 +20,7 @@ #include #include #include +#include #include #include "base/check.h" @@ -28,6 +29,13 @@ using namespace std; namespace CVC4 { +std::string Exception::toString() const +{ + std::stringstream ss; + toStream(ss); + return ss.str(); +} + thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = nullptr; LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {} diff --git a/src/base/exception.h b/src/base/exception.h index 8a89c99fc..815e4011f 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -19,12 +19,8 @@ #ifndef CVC4__EXCEPTION_H #define CVC4__EXCEPTION_H -#include -#include #include #include -#include -#include #include namespace CVC4 { @@ -61,12 +57,7 @@ class CVC4_PUBLIC Exception : public std::exception { * toString(), there is no stream, so the parameters are default * and you'll get exprs and types printed using the AST language. */ - std::string toString() const - { - std::stringstream ss; - toStream(ss); - return ss.str(); - } + std::string toString() const; /** * Printing: feel free to redefine toStream(). When overridden in diff --git a/src/base/listener.cpp b/src/base/listener.cpp index 72f9ee086..6e9d659fd 100644 --- a/src/base/listener.cpp +++ b/src/base/listener.cpp @@ -16,10 +16,6 @@ #include "base/listener.h" -#include - -#include "base/check.h" - namespace CVC4 { Listener::Listener(){} diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index e1327c0a7..2cebfa447 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -20,6 +20,7 @@ #include "expr/node.h" #include "options/decision_options.h" #include "options/smt_options.h" +#include "util/resource_manager.h" using namespace std; diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 914636fe9..74a230e29 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -19,18 +19,15 @@ #ifndef CVC4__DECISION__DECISION_ENGINE_H #define CVC4__DECISION__DECISION_ENGINE_H -#include - #include "base/output.h" +#include "context/cdo.h" #include "decision/decision_strategy.h" #include "expr/node.h" #include "prop/cnf_stream.h" -#include "prop/prop_engine.h" +#include "prop/sat_solver.h" #include "prop/sat_solver_types.h" -#include "smt/smt_engine_scope.h" -#include "smt/term_formula_removal.h" +#include "util/result.h" -using namespace std; using namespace CVC4::prop; using namespace CVC4::decision; diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 1d0b386e3..4950f4f3d 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -18,15 +18,18 @@ **/ #include "justification_heuristic.h" +#include "decision/decision_attributes.h" +#include "decision/decision_engine.h" #include "expr/kind.h" #include "expr/node_manager.h" #include "options/decision_options.h" -#include "theory/rewriter.h" -#include "smt/term_formula_removal.h" #include "smt/smt_statistics_registry.h" +#include "smt/term_formula_removal.h" +#include "theory/rewriter.h" #include "util/random.h" namespace CVC4 { +namespace decision { JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, context::UserContext* uc, @@ -67,8 +70,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) { if(options::decisionThreshold() > 0) { bool stopSearchTmp = false; - SatLiteral lit = getNextThresh(stopSearchTmp, options::decisionThreshold()); - if(lit != undefSatLiteral) { + prop::SatLiteral lit = + getNextThresh(stopSearchTmp, options::decisionThreshold()); + if (lit != prop::undefSatLiteral) + { Assert(stopSearchTmp == false); return lit; } @@ -88,9 +93,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D for(JustifiedSet::key_iterator i = d_justified.key_begin(); i != d_justified.key_end(); ++i) { TNode n = *i; - SatLiteral l = d_decisionEngine->hasSatLiteral(n) ? - d_decisionEngine->getSatLiteral(n) : -1; - SatValue v = tryGetSatValue(n); + prop::SatLiteral l = d_decisionEngine->hasSatLiteral(n) + ? d_decisionEngine->getSatLiteral(n) + : -1; + prop::SatValue v = tryGetSatValue(n); Trace("justified") <<"{ "<setResult(SAT_VALUE_TRUE); + if (d_curThreshold == 0) d_decisionEngine->setResult(prop::SAT_VALUE_TRUE); return prop::undefSatLiteral; } - -inline void computeXorIffDesiredValues -(Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2) +inline void computeXorIffDesiredValues(Kind k, + prop::SatValue desiredVal, + prop::SatValue& desiredVal1, + prop::SatValue& desiredVal2) { Assert(k == kind::EQUAL || k == kind::XOR); bool shouldInvert = - (desiredVal == SAT_VALUE_TRUE && k == kind::EQUAL) || - (desiredVal == SAT_VALUE_FALSE && k == kind::XOR); + (desiredVal == prop::SAT_VALUE_TRUE && k == kind::EQUAL) + || (desiredVal == prop::SAT_VALUE_FALSE && k == kind::XOR); - if(desiredVal1 == SAT_VALUE_UNKNOWN && - desiredVal2 == SAT_VALUE_UNKNOWN) { + if (desiredVal1 == prop::SAT_VALUE_UNKNOWN + && desiredVal2 == prop::SAT_VALUE_UNKNOWN) + { // CHOICE: pick one of them arbitarily - desiredVal1 = SAT_VALUE_FALSE; + desiredVal1 = prop::SAT_VALUE_FALSE; } if(desiredVal2 == SAT_VALUE_UNKNOWN) { @@ -214,9 +222,9 @@ bool JustificationHeuristic::checkJustified(TNode n) DecisionWeight JustificationHeuristic::getExploredThreshold(TNode n) { - return - d_exploredThreshold.find(n) == d_exploredThreshold.end() ? - numeric_limits::max() : d_exploredThreshold[n]; + return d_exploredThreshold.find(n) == d_exploredThreshold.end() + ? std::numeric_limits::max() + : d_exploredThreshold[n]; } void JustificationHeuristic::setExploredThreshold(TNode n) @@ -263,36 +271,36 @@ DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity } else { if(k == kind::OR) { - dW1 = numeric_limits::max(), dW2 = 0; + dW1 = std::numeric_limits::max(), dW2 = 0; for(TNode::iterator i=n.begin(); i != n.end(); ++i) { - dW1 = min(dW1, getWeightPolarized(*i, true)); - dW2 = max(dW2, getWeightPolarized(*i, false)); + dW1 = std::min(dW1, getWeightPolarized(*i, true)); + dW2 = std::max(dW2, getWeightPolarized(*i, false)); } } else if(k == kind::AND) { - dW1 = 0, dW2 = numeric_limits::max(); + dW1 = 0, dW2 = std::numeric_limits::max(); for(TNode::iterator i=n.begin(); i != n.end(); ++i) { - dW1 = max(dW1, getWeightPolarized(*i, true)); - dW2 = min(dW2, getWeightPolarized(*i, false)); + dW1 = std::max(dW1, getWeightPolarized(*i, true)); + dW2 = std::min(dW2, getWeightPolarized(*i, false)); } } else if(k == kind::IMPLIES) { - dW1 = min(getWeightPolarized(n[0], false), - getWeightPolarized(n[1], true)); - dW2 = max(getWeightPolarized(n[0], true), - getWeightPolarized(n[1], false)); + dW1 = std::min(getWeightPolarized(n[0], false), + getWeightPolarized(n[1], true)); + dW2 = std::max(getWeightPolarized(n[0], true), + getWeightPolarized(n[1], false)); } else if(k == kind::NOT) { dW1 = getWeightPolarized(n[0], false); dW2 = getWeightPolarized(n[0], true); } else { dW1 = 0; for(TNode::iterator i=n.begin(); i != n.end(); ++i) { - dW1 = max(dW1, getWeightPolarized(*i, true)); - dW1 = max(dW1, getWeightPolarized(*i, false)); + dW1 = std::max(dW1, getWeightPolarized(*i, true)); + dW1 = std::max(dW1, getWeightPolarized(*i, false)); } dW2 = dW1; } } - d_weightCache[n] = make_pair(dW1, dW2); + d_weightCache[n] = std::make_pair(dW1, dW2); } return polarity ? d_weightCache[n].get().first : d_weightCache[n].get().second; } @@ -315,7 +323,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) { { DecisionWeight dW = 0; for (TNode::iterator i = n.begin(); i != n.end(); ++i) - dW = max(dW, getWeight(*i)); + dW = std::max(dW, getWeight(*i)); n.setAttribute(DecisionWeightAttr(), dW); } else if (combiningFn == options::DecisionWeightInternal::SUM @@ -323,7 +331,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) { { DecisionWeight dW = 0; for (TNode::iterator i = n.begin(); i != n.end(); ++i) - dW = max(dW, getWeight(*i)); + dW = std::max(dW, getWeight(*i)); n.setAttribute(DecisionWeightAttr(), dW); } else @@ -334,7 +342,7 @@ DecisionWeight JustificationHeuristic::getWeight(TNode n) { return n.getAttribute(DecisionWeightAttr()); } -typedef vector ChildList; +typedef std::vector ChildList; TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) { if(options::decisionUseWeight()) { // TODO: Optimize storing & access @@ -389,7 +397,7 @@ void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l) SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]); if (it2 != d_skolemAssertions.end()) { - l.push_back(make_pair(n[i], (*it2).second)); + l.push_back(std::make_pair(n[i], (*it2).second)); Assert(n[i].getNumChildren() == 0); } if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end()) @@ -610,8 +618,8 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TN { if(options::decisionUseWeight() && getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) { - swap(node1, node2); - swap(desiredVal1, desiredVal2); + std::swap(node1, node2); + std::swap(desiredVal1, desiredVal2); } if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) { @@ -635,8 +643,8 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TN { if(options::decisionUseWeight() && getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) { - swap(node1, node2); - swap(desiredVal1, desiredVal2); + std::swap(node1, node2); + std::swap(desiredVal1, desiredVal2); } bool noSplitter = true; @@ -722,4 +730,5 @@ JustificationHeuristic::handleEmbeddedSkolems(TNode node) return noSplitter ? NO_SPLITTER : DONT_KNOW; } -} /* namespace CVC4 */ +} /* namespace decision */ +} /* namespace CVC4 */ \ No newline at end of file diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 0a16759e1..1cf2810fd 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -24,16 +24,17 @@ #define CVC4__DECISION__JUSTIFICATION_HEURISTIC #include +#include #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdlist.h" -#include "decision/decision_attributes.h" -#include "decision/decision_engine.h" +#include "context/cdo.h" #include "decision/decision_strategy.h" #include "expr/node.h" -#include "preprocessing/assertion_pipeline.h" +#include "options/decision_weight.h" #include "prop/sat_solver_types.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace decision { @@ -42,12 +43,17 @@ class JustificationHeuristic : public ITEDecisionStrategy { // TRUE FALSE MEH enum SearchResult {FOUND_SPLITTER, NO_SPLITTER, DONT_KNOW}; - typedef std::vector > SkolemList; + typedef std::vector > SkolemList; typedef context::CDHashMap SkolemCache; typedef std::vector ChildList; - typedef context::CDHashMap,TNodeHashFunction> ChildCache; + typedef context:: + CDHashMap, TNodeHashFunction> + ChildCache; typedef context::CDHashMap SkolemMap; - typedef context::CDHashMap,TNodeHashFunction> WeightCache; + typedef context::CDHashMap, + TNodeHashFunction> + WeightCache; // being 'justified' is monotonic with respect to decisions typedef context::CDHashSet JustifiedSet; @@ -91,7 +97,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { std::unordered_set d_visitedComputeSkolems; /** current decision for the recursive call */ - SatLiteral d_curDecision; + prop::SatLiteral d_curDecision; /** current threshold for the recursive call */ DecisionWeight d_curThreshold; @@ -136,12 +142,12 @@ public: /* getNext with an option to specify threshold */ prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold); - SatLiteral findSplitter(TNode node, SatValue desiredVal); + prop::SatLiteral findSplitter(TNode node, prop::SatValue desiredVal); /** * Do all the hard work. */ - SearchResult findSplitterRec(TNode node, SatValue value); + SearchResult findSplitterRec(TNode node, prop::SatValue value); /* Helper functions */ void setJustified(TNode); @@ -151,7 +157,7 @@ public: void setPrvsIndex(int); int getPrvsIndex(); DecisionWeight getWeightPolarized(TNode n, bool polarity); - DecisionWeight getWeightPolarized(TNode n, SatValue); + DecisionWeight getWeightPolarized(TNode n, prop::SatValue); static DecisionWeight getWeight(TNode); bool compareByWeightFalse(TNode, TNode); bool compareByWeightTrue(TNode, TNode); @@ -159,7 +165,7 @@ public: /* If literal exists corresponding to the node return that. Otherwise an UNKNOWN */ - SatValue tryGetSatValue(Node n); + prop::SatValue tryGetSatValue(Node n); /* Get list of all term-ITEs for the atomic formula v */ JustificationHeuristic::SkolemList getSkolems(TNode n); @@ -176,13 +182,17 @@ public: /* Compute all term-removal skolems in a node recursively */ void computeSkolems(TNode n, SkolemList& l); - SearchResult handleAndOrEasy(TNode node, SatValue desiredVal); - SearchResult handleAndOrHard(TNode node, SatValue desiredVal); - SearchResult handleBinaryEasy(TNode node1, SatValue desiredVal1, - TNode node2, SatValue desiredVal2); - SearchResult handleBinaryHard(TNode node1, SatValue desiredVal1, - TNode node2, SatValue desiredVal2); - SearchResult handleITE(TNode node, SatValue desiredVal); + SearchResult handleAndOrEasy(TNode node, prop::SatValue desiredVal); + SearchResult handleAndOrHard(TNode node, prop::SatValue desiredVal); + SearchResult handleBinaryEasy(TNode node1, + prop::SatValue desiredVal1, + TNode node2, + prop::SatValue desiredVal2); + SearchResult handleBinaryHard(TNode node1, + prop::SatValue desiredVal1, + TNode node2, + prop::SatValue desiredVal2); + SearchResult handleITE(TNode node, prop::SatValue desiredVal); SearchResult handleEmbeddedSkolems(TNode node); };/* class JustificationHeuristic */ diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h index da80891a2..15ae6ea83 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/expr/buffered_proof_generator.h @@ -19,11 +19,11 @@ #include "context/cdhashmap.h" #include "expr/proof_generator.h" -#include "expr/proof_step_buffer.h" namespace CVC4 { class ProofNodeManager; +class ProofStep; /** * The proof generator for buffered steps. This class is a context-dependent diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index f94f0063a..5451edc02 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -13,6 +13,8 @@ **/ #include "expr/dtype.h" +#include + #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/type_matcher.h" diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index 0bda68b7b..e82e614b3 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include + #include "expr/kind.h" namespace CVC4 { diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 8d8d2741f..9c6d0e290 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -15,6 +15,7 @@ #include "expr/lazy_proof.h" #include "expr/proof_ensure_closed.h" +#include "expr/proof_node.h" #include "expr/proof_node_manager.h" using namespace CVC4::kind; diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index 83dc90e4d..7c39164fe 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -17,14 +17,11 @@ #ifndef CVC4__EXPR__LAZY_PROOF_H #define CVC4__EXPR__LAZY_PROOF_H -#include -#include - #include "expr/proof.h" -#include "expr/proof_generator.h" namespace CVC4 { +class ProofGenerator; class ProofNodeManager; /** diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index f80ab099c..0e5e8c376 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -16,6 +16,7 @@ #include "expr/proof.h" #include "expr/proof_ensure_closed.h" +#include "expr/proof_node.h" #include "expr/proof_node_algorithm.h" #include "expr/proof_node_manager.h" #include "options/proof_options.h" diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 1604bf182..e1b0f3cd0 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -17,7 +17,6 @@ #ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H #define CVC4__EXPR__LAZY_PROOF_CHAIN_H -#include #include #include "context/cdhashmap.h" diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 1aca73d2e..eee8d0136 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -15,8 +15,9 @@ **/ #include "expr/node.h" -#include #include +#include +#include #include "base/exception.h" #include "base/output.h" diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index b512b5869..6596f6c5f 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -14,6 +14,8 @@ #include "expr/proof.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" #include "expr/proof_node_manager.h" using namespace CVC4::kind; diff --git a/src/expr/proof.h b/src/expr/proof.h index 3a26f0975..abb0b9b37 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -17,17 +17,16 @@ #ifndef CVC4__EXPR__PROOF_H #define CVC4__EXPR__PROOF_H -#include #include #include "context/cdhashmap.h" #include "expr/node.h" #include "expr/proof_generator.h" -#include "expr/proof_node.h" #include "expr/proof_step_buffer.h" namespace CVC4 { +class ProofNode; class ProofNodeManager; /** diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index dc87d1795..a5655c9db 100644 --- a/src/expr/proof_checker.cpp +++ b/src/expr/proof_checker.cpp @@ -14,6 +14,7 @@ #include "expr/proof_checker.h" +#include "expr/proof_node.h" #include "expr/skolem_manager.h" #include "options/proof_options.h" #include "smt/smt_statistics_registry.h" diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index ab9c24434..200a1839d 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -20,12 +20,13 @@ #include #include "expr/node.h" -#include "expr/proof_node.h" +#include "expr/proof_rule.h" #include "util/statistics_registry.h" namespace CVC4 { class ProofChecker; +class ProofNode; /** A virtual base class for checking a proof rule */ class ProofRuleChecker diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp index 6eebcd3ec..183ff0d5b 100644 --- a/src/expr/proof_ensure_closed.cpp +++ b/src/expr/proof_ensure_closed.cpp @@ -14,6 +14,10 @@ #include "expr/proof_ensure_closed.h" +#include + +#include "expr/proof_generator.h" +#include "expr/proof_node.h" #include "expr/proof_node_algorithm.h" #include "options/proof_options.h" #include "options/smt_options.h" diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h index 7b970a71a..c54a5dfd5 100644 --- a/src/expr/proof_ensure_closed.h +++ b/src/expr/proof_ensure_closed.h @@ -18,11 +18,12 @@ #define CVC4__EXPR__PROOF_ENSURE_CLOSED_H #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node.h" namespace CVC4 { +class ProofGenerator; +class ProofNode; + /** * Debug check closed on Trace c. Context ctx is string for debugging. * This method throws an assertion failure if pg cannot provide a closed diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index d2206a570..31af09b7f 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -14,7 +14,10 @@ #include "expr/proof_generator.h" +#include + #include "expr/proof.h" +#include "expr/proof_node.h" #include "expr/proof_node_algorithm.h" #include "options/smt_options.h" diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 869f226b8..3b376d77c 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -18,11 +18,11 @@ #define CVC4__EXPR__PROOF_GENERATOR_H #include "expr/node.h" -#include "expr/proof_node.h" namespace CVC4 { class CDProof; +class ProofNode; /** An overwrite policy for CDProof */ enum class CDPOverwrite : uint32_t diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp index 2af296813..751dcc39e 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/expr/proof_node_algorithm.cpp @@ -14,6 +14,8 @@ #include "expr/proof_node_algorithm.h" +#include "expr/proof_node.h" + namespace CVC4 { namespace expr { diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index 43d06ea91..af8de066d 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -20,9 +20,11 @@ #include #include "expr/node.h" -#include "expr/proof_node.h" namespace CVC4 { + +class ProofNode; + namespace expr { /** diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index f5e15f6d6..91858f239 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -15,6 +15,8 @@ #include "expr/proof_node_manager.h" #include "expr/proof.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" #include "expr/proof_node_algorithm.h" #include "options/proof_options.h" #include "theory/rewriter.h" diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 3ad56c92d..e7be50065 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -19,11 +19,14 @@ #include -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "expr/node.h" +#include "expr/proof_rule.h" namespace CVC4 { +class ProofChecker; +class ProofNode; + /** * A manager for proof node objects. This is a trusted interface for creating * and updating ProofNode objects. diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp index fbfc3e3d4..6830326ba 100644 --- a/src/expr/proof_node_to_sexpr.cpp +++ b/src/expr/proof_node_to_sexpr.cpp @@ -15,7 +15,9 @@ #include "expr/proof_node_to_sexpr.h" #include +#include +#include "expr/proof_node.h" #include "options/proof_options.h" using namespace CVC4::kind; diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h index 3e0d42a7d..e6c003d10 100644 --- a/src/expr/proof_node_to_sexpr.h +++ b/src/expr/proof_node_to_sexpr.h @@ -20,10 +20,12 @@ #include #include "expr/node.h" -#include "expr/proof_node.h" +#include "expr/proof_rule.h" namespace CVC4 { +class ProofNode; + /** A class to convert ProofNode objects to s-expressions */ class ProofNodeToSExpr { diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index e0f096075..f421ff4f3 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -17,6 +17,7 @@ #include "expr/lazy_proof.h" #include "expr/proof_ensure_closed.h" #include "expr/proof_node_algorithm.h" +#include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 9814c8166..2df668384 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -18,14 +18,17 @@ #define CVC4__EXPR__PROOF_NODE_UPDATER_H #include -#include +#include -#include "expr/proof.h" +#include "expr/node.h" #include "expr/proof_node.h" -#include "expr/proof_node_manager.h" namespace CVC4 { +class CDProof; +class ProofNode; +class ProofNodeManager; + /** * A virtual callback class for updating ProofNode. An example use case of this * class is to eliminate a proof rule by expansion. diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp index bb02aeb20..4c99855df 100644 --- a/src/expr/proof_step_buffer.cpp +++ b/src/expr/proof_step_buffer.cpp @@ -14,6 +14,8 @@ #include "expr/proof_step_buffer.h" +#include "expr/proof_checker.h" + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h index 4e463a7b3..1b09a8f96 100644 --- a/src/expr/proof_step_buffer.h +++ b/src/expr/proof_step_buffer.h @@ -20,11 +20,12 @@ #include #include "expr/node.h" -#include "expr/proof_checker.h" #include "expr/proof_rule.h" namespace CVC4 { +class ProofChecker; + /** * Information for constructing a step in a CDProof. Notice that the conclusion * of the proof step is intentionally not included in this data structure. diff --git a/src/expr/record.h b/src/expr/record.h index 4e1ff6772..1ab84c30c 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -19,7 +19,6 @@ #ifndef CVC4__RECORD_H #define CVC4__RECORD_H -#include #include #include #include diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index f65558184..68c4985bb 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -14,6 +14,7 @@ #include "expr/sequence.h" +#include #include #include "expr/node.h" diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index 541db1ac5..3ca75050a 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -14,6 +14,8 @@ #include "expr/subs.h" +#include + #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index 3401e55f7..e67a1befe 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -14,6 +14,8 @@ #include "expr/sygus_datatype.h" +#include + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index fa5732854..73018d7ca 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -19,7 +19,6 @@ #include #include -#include #include #include "api/cvc4cpp.h" diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp index 8bd850488..105c811d4 100644 --- a/src/expr/tconv_seq_proof_generator.cpp +++ b/src/expr/tconv_seq_proof_generator.cpp @@ -14,6 +14,10 @@ #include "expr/tconv_seq_proof_generator.h" +#include + +#include "expr/proof_node_manager.h" + namespace CVC4 { TConvSeqProofGenerator::TConvSeqProofGenerator( diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h index 95499d6b8..9197028d6 100644 --- a/src/expr/tconv_seq_proof_generator.h +++ b/src/expr/tconv_seq_proof_generator.h @@ -20,11 +20,12 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" #include "theory/trust_node.h" namespace CVC4 { +class ProofNodeManager; + /** * The term conversion sequence proof generator. This is used for maintaining * a fixed sequence of proof generators that provide proofs for rewrites diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp index e5ebd0209..91f7f3190 100644 --- a/src/expr/term_canonize.cpp +++ b/src/expr/term_canonize.cpp @@ -14,6 +14,8 @@ #include "expr/term_canonize.h" +#include + // TODO #1216: move the code in this include #include "theory/quantifiers/term_util.h" diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h index ff8187bbc..061cf1ed2 100644 --- a/src/expr/term_context_node.h +++ b/src/expr/term_context_node.h @@ -18,11 +18,11 @@ #define CVC4__EXPR__TERM_CONTEXT_NODE_H #include "expr/node.h" -#include "expr/term_context.h" namespace CVC4 { class TCtxStack; +class TermContext; /** * A (term-context) sensitive term. This is a wrapper around a Node that diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp index 64cab7035..f35514fa6 100644 --- a/src/expr/term_context_stack.cpp +++ b/src/expr/term_context_stack.cpp @@ -14,6 +14,8 @@ #include "expr/term_context_stack.h" +#include "expr/term_context.h" + namespace CVC4 { TCtxStack::TCtxStack(const TermContext* tctx) : d_tctx(tctx) {} diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index d37ccf914..a47214ae1 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -14,6 +14,9 @@ #include "expr/term_conversion_proof_generator.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" +#include "expr/term_context.h" #include "expr/term_context_stack.h" using namespace CVC4::kind; diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index dcf8b3fa4..4d6a169cb 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -20,11 +20,12 @@ #include "context/cdhashmap.h" #include "expr/lazy_proof.h" #include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "expr/term_context.h" namespace CVC4 { +class ProofNodeManager; +class TermContext; + /** A policy for how rewrite steps are applied in TConvProofGenerator */ enum class TConvPolicy : uint32_t { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index dadbdc91d..cbc15e153 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -16,6 +16,7 @@ #include "expr/type.h" #include +#include #include #include diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index e7685dba8..f5a729b36 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -14,6 +14,8 @@ ** TypeChecker implementation. **/ +#include + #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" #include "expr/type_checker.h" diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h index 312ffe53a..32c1254de 100644 --- a/src/expr/type_checker_util.h +++ b/src/expr/type_checker_util.h @@ -19,6 +19,8 @@ #include "cvc4_private.h" +#include + #include "expr/kind.h" #include "expr/node.h" #include "expr/node_manager.h" diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h index 47fc36eee..126175582 100644 --- a/src/expr/type_matcher.h +++ b/src/expr/type_matcher.h @@ -19,7 +19,6 @@ #include -#include "expr/node.h" #include "expr/type_node.h" namespace CVC4 { diff --git a/src/options/language.cpp b/src/options/language.cpp index c2eb13852..ee6da3e48 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -16,6 +16,11 @@ #include "options/language.h" +#include + +#include "base/exception.h" +#include "options/option_exception.h" + namespace CVC4 { namespace language { diff --git a/src/options/language.h b/src/options/language.h index b34ac378e..e1e4dfed3 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -19,12 +19,9 @@ #ifndef CVC4__LANGUAGE_H #define CVC4__LANGUAGE_H -#include +#include #include -#include "base/exception.h" -#include "options/option_exception.h" - namespace CVC4 { namespace language { @@ -182,9 +179,9 @@ bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC; bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC; /** - * Is the language smtlib 2.5 or above? If exact=true, then this method returns - * false if the input language is not exactly SMT-LIB 2.6. - */ + * Is the language smtlib 2.5 or above? If exact=true, then this method returns + * false if the input language is not exactly SMT-LIB 2.5. + */ bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC; bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC; /** diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h index 6b6a1afb7..b62c56898 100644 --- a/src/options/open_ostream.h +++ b/src/options/open_ostream.h @@ -20,13 +20,11 @@ #ifndef CVC4__OPEN_OSTREAM_H #define CVC4__OPEN_OSTREAM_H +#include #include -#include #include #include -#include "options/option_exception.h" - namespace CVC4 { class OstreamOpener { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 07e629976..9652c9f8e 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -22,17 +22,18 @@ #include #include -#include "base/modal_exception.h" #include "options/base_handlers.h" #include "options/bv_options.h" #include "options/decision_options.h" #include "options/language.h" #include "options/option_exception.h" -#include "options/options.h" #include "options/printer_modes.h" #include "options/quantifiers_options.h" namespace CVC4 { + +class Options; + namespace options { /** diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 4bc3323e5..250c0639c 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -18,6 +18,7 @@ #include "expr/node_manager.h" #include "options/smt_options.h" #include "proof/proof_manager.h" +#include "smt/preprocess_proof_generator.h" #include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 9d65329b0..408c0718c 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -21,13 +21,15 @@ #include #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "smt/preprocess_proof_generator.h" -#include "smt/term_formula_removal.h" #include "theory/trust_node.h" namespace CVC4 { + +class ProofGenerator; +namespace smt { +class PreprocessProofGenerator; +} + namespace preprocessing { using IteSkolemMap = std::unordered_map; diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index a092a8778..f8efa5de9 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -22,11 +22,15 @@ **/ #include "preprocessing/passes/ackermann.h" + #include + #include "base/check.h" #include "expr/node_algorithm.h" #include "options/options.h" #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" using namespace CVC4; using namespace CVC4::theory; @@ -197,7 +201,7 @@ size_t getBVSkolemSize(size_t capacity) * a sufficient bit-vector size. * Populate usVarsToBVVars so that it maps variables with uninterpreted sort to * the fresh skolem BV variables. variables */ -void collectUSortsToBV(const unordered_set& vars, +void collectUSortsToBV(const std::unordered_set& vars, const USortToBVSizeMap& usortCardinality, SubstitutionMap& usVarsToBVVars) { diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h index cd0d059e4..e28a1ca2d 100644 --- a/src/preprocessing/passes/ackermann.h +++ b/src/preprocessing/passes/ackermann.h @@ -27,9 +27,11 @@ #define CVC4__PREPROCESSING__PASSES__ACKERMANN_H #include + #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" +#include "theory/logic_info.h" +#include "theory/substitutions.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index c93895e79..0369dd0ed 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -18,6 +18,8 @@ #include "preprocessing/passes/apply_substs.h" #include "context/cdo.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/rewriter.h" #include "theory/substitutions.h" diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h index 781fcc79e..197e08eaf 100644 --- a/src/preprocessing/passes/apply_substs.h +++ b/src/preprocessing/passes/apply_substs.h @@ -21,10 +21,12 @@ #define CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { + +class PreprocessingPassContext; + namespace passes { class ApplySubsts : public PreprocessingPass diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp index 47a504d59..6a1d76fad 100644 --- a/src/preprocessing/passes/bool_to_bv.cpp +++ b/src/preprocessing/passes/bool_to_bv.cpp @@ -19,7 +19,10 @@ #include "base/map_util.h" #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory.h" diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h index c5e6f3801..917954da6 100644 --- a/src/preprocessing/passes/bool_to_bv.h +++ b/src/preprocessing/passes/bool_to_bv.h @@ -18,10 +18,9 @@ #ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H #define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H +#include "expr/node.h" #include "options/bv_options.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" -#include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp index ebc169e42..67951d441 100644 --- a/src/preprocessing/passes/bv_abstraction.cpp +++ b/src/preprocessing/passes/bv_abstraction.cpp @@ -26,8 +26,11 @@ #include #include "options/bv_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/bv/theory_bv.h" #include "theory/rewriter.h" +#include "theory/theory_engine.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h index a49bdae2c..f9d633bbc 100644 --- a/src/preprocessing/passes/bv_abstraction.h +++ b/src/preprocessing/passes/bv_abstraction.h @@ -27,7 +27,6 @@ #define CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp index 460ef2597..c521f736c 100644 --- a/src/preprocessing/passes/bv_eager_atoms.cpp +++ b/src/preprocessing/passes/bv_eager_atoms.cpp @@ -18,6 +18,9 @@ #include "preprocessing/passes/bv_eager_atoms.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/theory_engine.h" #include "theory/theory_model.h" namespace CVC4 { diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h index 4c1bb136c..e0b063654 100644 --- a/src/preprocessing/passes/bv_eager_atoms.h +++ b/src/preprocessing/passes/bv_eager_atoms.h @@ -21,7 +21,6 @@ #define CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp index 02a08b133..d8b309609 100644 --- a/src/preprocessing/passes/bv_gauss.cpp +++ b/src/preprocessing/passes/bv_gauss.cpp @@ -17,16 +17,17 @@ #include "preprocessing/passes/bv_gauss.h" +#include +#include + #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "util/bitvector.h" -#include -#include - - using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h index 0b614251f..3b8197f9b 100644 --- a/src/preprocessing/passes/bv_gauss.h +++ b/src/preprocessing/passes/bv_gauss.h @@ -20,8 +20,8 @@ #ifndef CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H #define CVC4__PREPROCESSING__PASSES__BV_GAUSS_ELIM_H +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp index 1e14e5b4b..573d36207 100644 --- a/src/preprocessing/passes/bv_intro_pow2.cpp +++ b/src/preprocessing/passes/bv_intro_pow2.cpp @@ -20,6 +20,8 @@ #include +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h index 92bdc2fc7..a270baa64 100644 --- a/src/preprocessing/passes/bv_intro_pow2.h +++ b/src/preprocessing/passes/bv_intro_pow2.h @@ -22,7 +22,6 @@ #define CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp index ac8b01d74..cf156692b 100644 --- a/src/preprocessing/passes/bv_to_bool.cpp +++ b/src/preprocessing/passes/bv_to_bool.cpp @@ -23,7 +23,10 @@ #include "expr/node.h" #include "expr/node_visitor.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" #include "theory/theory.h" diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h index 5054edfc4..a19116e77 100644 --- a/src/preprocessing/passes/bv_to_bool.h +++ b/src/preprocessing/passes/bv_to_bool.h @@ -19,9 +19,8 @@ #ifndef CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H #define CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" -#include "theory/bv/theory_bv_utils.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index 704214d06..5043718ca 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -18,6 +18,7 @@ #include "preprocessing/passes/bv_to_int.h" #include +#include #include #include #include @@ -26,6 +27,8 @@ #include "expr/node_traversal.h" #include "options/smt_options.h" #include "options/uf_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" #include "theory/rewriter.h" @@ -34,6 +37,7 @@ namespace CVC4 { namespace preprocessing { namespace passes { +using namespace std; using namespace CVC4::theory; using namespace CVC4::theory::bv; diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index dd830d7cf..edcc84622 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -69,10 +69,8 @@ #define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H #include "context/cdhashmap.h" -#include "context/cdo.h" -#include "context/context.h" +#include "context/cdhashset.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" #include "theory/arith/nl/iand_utils.h" namespace CVC4 { @@ -104,7 +102,7 @@ class BVToInt : public PreprocessingPass * @return a node representing the shift. * */ - Node createShiftNode(vector children, + Node createShiftNode(std::vector children, uint64_t bvsize, bool isLeftShift); @@ -209,7 +207,7 @@ class BVToInt : public PreprocessingPass */ Node reconstructNode(Node originalNode, TypeNode resultType, - const vector& translated_children); + const std::vector& translated_children); /** * A useful utility function. @@ -247,7 +245,7 @@ class BVToInt : public PreprocessingPass * that have children. */ Node translateWithChildren(Node original, - const vector& translated_children); + const std::vector& translated_children); /** * Performs the actual translation to integers for nodes diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp index 95e107328..381e1b589 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.cpp +++ b/src/preprocessing/passes/extended_rewriter_pass.cpp @@ -17,6 +17,8 @@ #include "preprocessing/passes/extended_rewriter_pass.h" #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/quantifiers/extended_rewrite.h" namespace CVC4 { diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h index f4314a123..22b4d2da6 100644 --- a/src/preprocessing/passes/extended_rewriter_pass.h +++ b/src/preprocessing/passes/extended_rewriter_pass.h @@ -20,7 +20,6 @@ #define CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp index c7bed4d31..6e898a3c2 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.cpp +++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp @@ -17,6 +17,9 @@ #include "preprocessing/passes/foreign_theory_rewrite.h" #include "expr/node_traversal.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/rewriter.h" #include "theory/strings/arith_entail.h" namespace CVC4 { diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h index 2a882641e..aca3d0cfe 100644 --- a/src/preprocessing/passes/foreign_theory_rewrite.h +++ b/src/preprocessing/passes/foreign_theory_rewrite.h @@ -20,10 +20,8 @@ #define CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H #include "context/cdhashmap.h" -#include "context/cdo.h" -#include "context/context.h" +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { @@ -57,7 +55,7 @@ class ForeignTheoryRewrite : public PreprocessingPass /** construct a node with the same operator as originalNode whose children are * processedChildren */ - static Node reconstructNode(Node originalNode, vector newChildren); + static Node reconstructNode(Node originalNode, std::vector newChildren); /** A cache to store the simplified nodes */ CDNodeMap d_cache; }; diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index 8c7a71021..1657aeafa 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -14,11 +14,16 @@ #include "preprocessing/passes/fun_def_fmf.h" +#include + #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "proof/proof_manager.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h index 36d1166b7..d091d9db4 100644 --- a/src/preprocessing/passes/fun_def_fmf.h +++ b/src/preprocessing/passes/fun_def_fmf.h @@ -16,12 +16,11 @@ #define CVC4__PREPROCESSING__PASSES__FUN_DEF_FMF_H #include -#include #include +#include "context/cdlist.h" #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp index 00ca1efd3..de7a7fb47 100644 --- a/src/preprocessing/passes/global_negate.cpp +++ b/src/preprocessing/passes/global_negate.cpp @@ -17,6 +17,7 @@ #include #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" using namespace std; diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h index af8ae5048..b59303870 100644 --- a/src/preprocessing/passes/global_negate.h +++ b/src/preprocessing/passes/global_negate.h @@ -25,8 +25,8 @@ #ifndef CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H #define CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index 8cf4ad2ed..1f64e2e87 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -18,6 +18,7 @@ #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" #include "theory/uf/theory_uf_rewriter.h" diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h index a1dc05b83..01683d2f5 100644 --- a/src/preprocessing/passes/ho_elim.h +++ b/src/preprocessing/passes/ho_elim.h @@ -19,8 +19,12 @@ #ifndef __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H #define __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H +#include +#include +#include + +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index 5b0465772..2e237df2b 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -25,6 +25,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -32,6 +33,7 @@ namespace CVC4 { namespace preprocessing { namespace passes { +using namespace std; using namespace CVC4::theory; using NodeMap = std::unordered_map; diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h index 208e7ab6a..a2085d6eb 100644 --- a/src/preprocessing/passes/int_to_bv.h +++ b/src/preprocessing/passes/int_to_bv.h @@ -22,7 +22,6 @@ #define CVC4__PREPROCESSING__PASSES__INT_TO_BV_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index f788338be..b82535804 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -18,6 +18,10 @@ #include "preprocessing/passes/ite_removal.h" #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "proof/proof_manager.h" +#include "prop/prop_engine.h" #include "theory/rewriter.h" #include "theory/theory_preprocessor.h" diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h index 2b8a05fe4..a7ed87752 100644 --- a/src/preprocessing/passes/ite_removal.h +++ b/src/preprocessing/passes/ite_removal.h @@ -20,11 +20,7 @@ #ifndef CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H #define CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H -#include -#include - #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp index 2a1f4c3e6..6ed149895 100644 --- a/src/preprocessing/passes/ite_simp.cpp +++ b/src/preprocessing/passes/ite_simp.cpp @@ -17,10 +17,15 @@ #include #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" #include "smt_util/nary_builder.h" #include "theory/arith/arith_ite_utils.h" +#include "theory/rewriter.h" +#include "theory/theory_engine.h" +using namespace std; using namespace CVC4; using namespace CVC4::theory; diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h index fe1dfa6e0..603e7889e 100644 --- a/src/preprocessing/passes/ite_simp.h +++ b/src/preprocessing/passes/ite_simp.h @@ -18,7 +18,7 @@ #define CVC4__PREPROCESSING__PASSES__ITE_SIMP_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" +#include "preprocessing/util/ite_utilities.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 50dbc4a27..20a5fdbb0 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -15,14 +15,18 @@ #include "preprocessing/passes/miplib_trick.h" +#include #include #include "expr/node_self_iterator.h" #include "options/arith_options.h" #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_statistics_registry.h" #include "smt_util/boolean_simplification.h" #include "theory/booleans/circuit_propagator.h" +#include "theory/theory_engine.h" #include "theory/theory_model.h" #include "theory/trust_substitutions.h" @@ -30,6 +34,7 @@ namespace CVC4 { namespace preprocessing { namespace passes { +using namespace std; using namespace CVC4::theory; namespace { diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h index f7be87f18..99fd766ca 100644 --- a/src/preprocessing/passes/miplib_trick.h +++ b/src/preprocessing/passes/miplib_trick.h @@ -18,8 +18,8 @@ #ifndef CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H #define CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index 88bdf2e5c..553a85036 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -16,11 +16,14 @@ #include "preprocessing/passes/nl_ext_purify.h" +#include "preprocessing/assertion_pipeline.h" +#include "theory/rewriter.h" namespace CVC4 { namespace preprocessing { namespace passes { +using namespace std; using namespace CVC4::theory; Node NlExtPurify::purifyNlTerms(TNode n, diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h index 5c7c5776e..df06dc22d 100644 --- a/src/preprocessing/passes/nl_ext_purify.h +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -25,7 +25,6 @@ #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 8cff66d72..6d6cfac41 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -20,7 +20,13 @@ #include "context/cdo.h" #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "smt/preprocess_proof_generator.h" #include "smt/smt_statistics_registry.h" +#include "theory/booleans/circuit_propagator.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" #include "theory/theory_model.h" #include "theory/trust_substitutions.h" @@ -289,7 +295,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << "Resize non-clausal learned literals to " << j << std::endl; learned_literals.resize(j); - unordered_set s; + std::unordered_set s; for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { Node assertion = (*assertionsToPreprocess)[i]; diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index f94eb2d70..9539b6fd8 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -17,16 +17,23 @@ #ifndef CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H #define CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H -#include - -#include "expr/lazy_proof.h" +#include "context/cdlist.h" #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" -#include "smt/preprocess_proof_generator.h" #include "theory/trust_node.h" namespace CVC4 { + +class LazyCDProof; +class ProofNodeManager; + +namespace smt { +class PreprocessProofGenerator; +} +namespace theory { +class TrustSubstitutionMap; +} + namespace preprocessing { namespace passes { diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp index 2720d2f0b..a9396c570 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.cpp +++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp @@ -18,6 +18,8 @@ #include "preprocessing/passes/pseudo_boolean_processor.h" #include "base/output.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h index 03137dac5..b1338bb38 100644 --- a/src/preprocessing/passes/pseudo_boolean_processor.h +++ b/src/preprocessing/passes/pseudo_boolean_processor.h @@ -25,10 +25,8 @@ #include "context/cdhashmap.h" #include "context/cdo.h" -#include "context/context.h" #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" #include "theory/substitutions.h" #include "util/maybe.h" #include "util/rational.h" diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index ea73b7958..4e4d30649 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -20,6 +20,9 @@ #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "proof/proof_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/arith/arith_msum.h" @@ -29,6 +32,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4::theory; diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h index c5e557a9e..d5396be7d 100644 --- a/src/preprocessing/passes/quantifier_macros.h +++ b/src/preprocessing/passes/quantifier_macros.h @@ -18,12 +18,9 @@ #define CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H #include -#include #include #include "expr/node.h" -#include "expr/type_node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp index 6daafff2d..5caf37611 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.cpp +++ b/src/preprocessing/passes/quantifiers_preprocess.cpp @@ -20,6 +20,7 @@ #include "preprocessing/passes/quantifiers_preprocess.h" #include "base/output.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/rewriter.h" @@ -27,6 +28,7 @@ namespace CVC4 { namespace preprocessing { namespace passes { +using namespace std; using namespace CVC4::theory; QuantifiersPreprocess::QuantifiersPreprocess(PreprocessingPassContext* preprocContext) diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h index 43fce22b3..ad18a382c 100644 --- a/src/preprocessing/passes/quantifiers_preprocess.h +++ b/src/preprocessing/passes/quantifiers_preprocess.h @@ -23,7 +23,6 @@ #define CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp index 672e281d7..f7995c2d7 100644 --- a/src/preprocessing/passes/real_to_int.cpp +++ b/src/preprocessing/passes/real_to_int.cpp @@ -18,6 +18,8 @@ #include +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/arith/arith_msum.h" #include "theory/rewriter.h" #include "theory/theory_model.h" @@ -26,6 +28,7 @@ namespace CVC4 { namespace preprocessing { namespace passes { +using namespace std; using namespace CVC4::theory; Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector& var_eq) diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h index 9fd8aca53..bab6f604c 100644 --- a/src/preprocessing/passes/real_to_int.h +++ b/src/preprocessing/passes/real_to_int.h @@ -19,12 +19,10 @@ #ifndef CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H #define CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H -#include #include #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp index b8c9498e1..0684dde81 100644 --- a/src/preprocessing/passes/rewrite.cpp +++ b/src/preprocessing/passes/rewrite.cpp @@ -16,6 +16,7 @@ #include "preprocessing/passes/rewrite.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h index 76493958a..73ce82873 100644 --- a/src/preprocessing/passes/rewrite.h +++ b/src/preprocessing/passes/rewrite.h @@ -20,7 +20,6 @@ #define CVC4__PREPROCESSING__PASSES__REWRITE_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index ef2014b8a..20720668c 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -20,6 +20,7 @@ #include #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/quantifiers/quant_util.h" #include "theory/rewriter.h" #include "theory/theory.h" @@ -28,6 +29,7 @@ namespace CVC4 { namespace preprocessing { namespace passes { +using namespace std; using namespace CVC4::theory; namespace { diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h index 912fd1b60..50ea641e2 100644 --- a/src/preprocessing/passes/sep_skolem_emp.h +++ b/src/preprocessing/passes/sep_skolem_emp.h @@ -19,7 +19,6 @@ #define CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 918b13140..8e75acf9e 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -16,9 +16,13 @@ #include "options/smt_options.h" #include "options/uf_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "smt/dump_manager.h" +#include "smt/smt_engine_scope.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" +#include "theory/theory_engine.h" using namespace std; diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h index 1a18b6fd1..23a910780 100644 --- a/src/preprocessing/passes/sort_infer.h +++ b/src/preprocessing/passes/sort_infer.h @@ -15,13 +15,7 @@ #ifndef CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ #define CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ -#include -#include -#include - -#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index d48857396..26055f718 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -18,7 +18,10 @@ #include #include "expr/node.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/rewriter.h" +#include "theory/theory_engine.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h index c86ebf90f..5c0ec816d 100644 --- a/src/preprocessing/passes/static_learning.h +++ b/src/preprocessing/passes/static_learning.h @@ -19,7 +19,6 @@ #define CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp index 69cb8914c..ddc7f4e21 100644 --- a/src/preprocessing/passes/strings_eager_pp.cpp +++ b/src/preprocessing/passes/strings_eager_pp.cpp @@ -14,8 +14,9 @@ #include "preprocessing/passes/strings_eager_pp.h" -#include "theory/strings/theory_strings_preprocess.h" +#include "preprocessing/assertion_pipeline.h" #include "theory/rewriter.h" +#include "theory/strings/theory_strings_preprocess.h" using namespace CVC4::theory; diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h index 299260c61..8679a6f70 100644 --- a/src/preprocessing/passes/strings_eager_pp.h +++ b/src/preprocessing/passes/strings_eager_pp.h @@ -18,7 +18,6 @@ #define CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index caf63b0ec..933efbfde 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -14,6 +14,8 @@ #include "preprocessing/passes/sygus_inference.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" @@ -21,6 +23,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace std; diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h index 31d94efd2..4a67ae224 100644 --- a/src/preprocessing/passes/sygus_inference.h +++ b/src/preprocessing/passes/sygus_inference.h @@ -15,13 +15,10 @@ #ifndef CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ #define CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ -#include -#include #include #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index 7b54fee61..b899b2de7 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -15,10 +15,13 @@ #include "preprocessing/passes/synth_rew_rules.h" +#include + #include "expr/sygus_datatype.h" #include "expr/term_canonize.h" #include "options/base_options.h" #include "options/quantifiers_options.h" +#include "preprocessing/assertion_pipeline.h" #include "printer/printer.h" #include "theory/quantifiers/candidate_rewrite_database.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index 5613c1b22..3721f9457 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -17,7 +17,6 @@ #define CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 22ae14762..04d761d2f 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -17,6 +17,10 @@ #include "preprocessing/passes/theory_preprocess.h" #include "options/smt_options.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "proof/proof_manager.h" +#include "prop/prop_engine.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" @@ -35,7 +39,7 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); IteSkolemMap& imap = assertions->getIteSkolemMap(); - PropEngine* propEngine = d_preprocContext->getPropEngine(); + prop::PropEngine* propEngine = d_preprocContext->getPropEngine(); // Remove all of the ITE occurrences and normalize for (unsigned i = 0, size = assertions->size(); i < size; ++i) { diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h index 49597828d..1635d4c3b 100644 --- a/src/preprocessing/passes/theory_preprocess.h +++ b/src/preprocessing/passes/theory_preprocess.h @@ -20,7 +20,6 @@ #define CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp index 68de75194..95f70d0f6 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.cpp +++ b/src/preprocessing/passes/theory_rewrite_eq.cpp @@ -14,6 +14,8 @@ #include "preprocessing/passes/theory_rewrite_eq.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" #include "theory/theory_engine.h" using namespace CVC4::theory; diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index bc4027310..c15f5e36e 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.h +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -17,8 +17,8 @@ #ifndef CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H #define CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H +#include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" #include "theory/trust_node.h" namespace CVC4 { diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 6ebf1b8c8..e50548ff8 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -19,6 +19,9 @@ #include "preprocessing/passes/unconstrained_simplifier.h" #include "expr/dtype.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/logic_info.h" #include "theory/rewriter.h" @@ -27,6 +30,7 @@ namespace CVC4 { namespace preprocessing { namespace passes { +using namespace std; using namespace CVC4::theory; UnconstrainedSimplifier::UnconstrainedSimplifier( diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h index ebfe51e79..b4d18a424 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.h +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -23,17 +23,16 @@ #include #include -#include -#include "context/context.h" #include "expr/node.h" #include "preprocessing/preprocessing_pass.h" -#include "preprocessing/preprocessing_pass_context.h" -#include "theory/logic_info.h" #include "theory/substitutions.h" #include "util/statistics_registry.h" namespace CVC4 { +namespace context { +class Context; +} namespace preprocessing { namespace passes { diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 169f10c9d..3eec24414 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -16,9 +16,13 @@ #include "preprocessing/preprocessing_pass.h" +#include "preprocessing/assertion_pipeline.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "printer/printer.h" #include "smt/dump.h" +#include "smt/output_manager.h" +#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" -#include "printer/printer.h" namespace CVC4 { namespace preprocessing { diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index b8ddb9846..3970ee8d3 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -33,14 +33,14 @@ #include -#include "preprocessing/assertion_pipeline.h" -#include "preprocessing/preprocessing_pass_context.h" -#include "smt/smt_engine_scope.h" -#include "theory/logic_info.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace preprocessing { +class AssertionPipeline; +class PreprocessingPassContext; + /** * Preprocessing passes return a result which indicates whether a conflict has * been detected during preprocessing. diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index c22a69255..2db213caf 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -21,18 +21,20 @@ #ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H #define CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H -#include "context/cdo.h" -#include "context/context.h" -#include "decision/decision_engine.h" -#include "preprocessing/util/ite_utilities.h" +#include "context/cdhashset.h" #include "smt/smt_engine.h" -#include "smt/term_formula_removal.h" -#include "theory/booleans/circuit_propagator.h" -#include "theory/theory_engine.h" #include "theory/trust_substitutions.h" #include "util/resource_manager.h" namespace CVC4 { +class SmtEngine; +class TheoryEngine; +namespace theory::booleans { +class CircuitPropagator; +} +namespace prop { +class PropEngine; +} namespace preprocessing { class PreprocessingPassContext diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h index ce5c5da22..01bbab3a6 100644 --- a/src/preprocessing/preprocessing_pass_registry.h +++ b/src/preprocessing/preprocessing_pass_registry.h @@ -19,15 +19,14 @@ #ifndef CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H #define CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H -#include +#include #include #include -#include "preprocessing/preprocessing_pass.h" - namespace CVC4 { namespace preprocessing { +class PreprocessingPass; class PreprocessingPassContext; /** diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 7e05af698..33d5cb826 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -21,6 +21,7 @@ #include +#include "preprocessing/assertion_pipeline.h" #include "preprocessing/passes/rewrite.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h index c82bf7958..fbe94302f 100644 --- a/src/preprocessing/util/ite_utilities.h +++ b/src/preprocessing/util/ite_utilities.h @@ -27,16 +27,16 @@ #include #include "expr/node.h" -#include "preprocessing/assertion_pipeline.h" #include "util/hash.h" #include "util/statistics_registry.h" namespace CVC4 { namespace preprocessing { + +class AssertionPipeline; + namespace util { -class IncomingArcCounter; -class TermITEHeightCounter; class ITECompressor; class ITESimplifier; class ITECareSimplifier; diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h index 45a09d07f..1572ab014 100644 --- a/src/printer/let_binding.h +++ b/src/printer/let_binding.h @@ -17,7 +17,6 @@ #ifndef CVC4__PRINTER__LET_BINDING_H #define CVC4__PRINTER__LET_BINDING_H -#include #include #include "context/cdhashmap.h" diff --git a/src/printer/printer.h b/src/printer/printer.h index 0a5ed1eac..dba29e524 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -19,7 +19,6 @@ #ifndef CVC4__PRINTER__PRINTER_H #define CVC4__PRINTER__PRINTER_H -#include #include #include "expr/node.h" diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 286c4e0bf..acbfbb2a2 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -21,14 +21,12 @@ #ifndef CVC4__CNF_PROOF_H #define CVC4__CNF_PROOF_H -#include #include #include #include "context/cdhashmap.h" #include "proof/clause_id.h" -#include "proof/sat_proof.h" -#include "util/maybe.h" +#include "proof/proof_manager.h" namespace CVC4 { namespace prop { diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index c7eb2282b..f05fb0386 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -19,7 +19,6 @@ #ifndef CVC4__PROOF_MANAGER_H #define CVC4__PROOF_MANAGER_H -#include #include #include #include @@ -28,7 +27,6 @@ #include "context/cdhashset.h" #include "expr/node.h" #include "proof/clause_id.h" -#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h index 9907b8d72..c76878da4 100644 --- a/src/prop/bvminisat/simp/SimpSolver.h +++ b/src/prop/bvminisat/simp/SimpSolver.h @@ -21,13 +21,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef BVMinisat_SimpSolver_h #define BVMinisat_SimpSolver_h -#include "context/context.h" #include "proof/clause_id.h" #include "prop/bvminisat/core/Solver.h" #include "prop/bvminisat/mtl/Queue.h" -#include "util/statistics_registry.h" namespace CVC4 { + +namespace context { +class Context; +} + namespace BVMinisat { //================================================================================================= diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 69cbb0241..92bdd66ee 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -32,7 +32,7 @@ #include "proof/proof_manager.h" #include "prop/proof_cnf_stream.h" #include "prop/registrar.h" -#include "prop/theory_proxy.h" +#include "prop/sat_solver_types.h" namespace CVC4 { @@ -41,6 +41,8 @@ class OutputManager; namespace prop { class ProofCnfStream; +class PropEngine; +class SatSolver; /** A policy for how literals for formulas are handled in cnf_stream */ enum class FormulaLitPolicy : uint32_t diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 8fa489f65..f685017a7 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -36,6 +36,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "prop/minisat/utils/Options.h" #include "prop/sat_proof_manager.h" #include "theory/theory.h" +#include "util/resource_manager.h" namespace CVC4 { template class TSatProof; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 738b4dc9c..473449179 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -32,6 +32,7 @@ #include "proof/proof_manager.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" +#include "prop/prop_proof_manager.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" @@ -83,7 +84,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_resourceManager(rm), d_outMgr(outMgr) { - Debug("prop") << "Constructing the PropEngine" << endl; + Debug("prop") << "Constructing the PropEngine" << std::endl; d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm)); d_decisionEngine->init(); // enable appropriate strategies @@ -146,7 +147,7 @@ void PropEngine::finishInit() } PropEngine::~PropEngine() { - Debug("prop") << "Destructing the PropEngine" << endl; + Debug("prop") << "Destructing the PropEngine" << std::endl; d_decisionEngine->shutdown(); d_decisionEngine.reset(nullptr); delete d_cnfStream; @@ -179,7 +180,7 @@ void PropEngine::notifyPreprocessedAssertions( void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "assertFormula(" << node << ")" << endl; + Debug("prop") << "assertFormula(" << node << ")" << std::endl; d_decisionEngine->addAssertion(node); assertInternal(node, false, false, true); } @@ -187,7 +188,7 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertSkolemDefinition(TNode node, TNode skolem) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "assertFormula(" << node << ")" << endl; + Debug("prop") << "assertFormula(" << node << ")" << std::endl; d_decisionEngine->addSkolemDefinition(node, skolem); assertInternal(node, false, false, true); } @@ -235,7 +236,7 @@ void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn, bool removable) { Node node = trn.getNode(); - Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl; bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; Assert(!isProofEnabled() || trn.getGenerator() != nullptr); assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator()); @@ -292,7 +293,7 @@ void PropEngine::assertLemmasInternal( } void PropEngine::requirePhase(TNode n, bool phase) { - Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl; + Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << std::endl; Assert(n.getType().isBoolean()); SatLiteral lit = d_cnfStream->getLiteral(n); @@ -307,26 +308,26 @@ bool PropEngine::isDecision(Node lit) const { void PropEngine::printSatisfyingAssignment(){ const CnfStream::NodeToLiteralMap& transCache = d_cnfStream->getTranslationCache(); - Debug("prop-value") << "Literal | Value | Expr" << endl + Debug("prop-value") << "Literal | Value | Expr" << std::endl << "----------------------------------------" - << "-----------------" << endl; + << "-----------------" << std::endl; for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(), end = transCache.end(); i != end; ++i) { - pair curr = *i; + std::pair curr = *i; SatLiteral l = curr.second; if(!l.isNegated()) { Node n = curr.first; SatValue value = d_satSolver->modelValue(l); - Debug("prop-value") << "'" << l << "' " << value << " " << n << endl; + Debug("prop-value") << "'" << l << "' " << value << " " << n << std::endl; } } } Result PropEngine::checkSat() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; - Debug("prop") << "PropEngine::checkSat()" << endl; + Debug("prop") << "PropEngine::checkSat()" << std::endl; // Mark that we are in the checkSat ScopedBool scopedBool(d_inCheckSat); @@ -360,7 +361,7 @@ Result PropEngine::checkSat() { printSatisfyingAssignment(); } - Debug("prop") << "PropEngine::checkSat() => " << result << endl; + Debug("prop") << "PropEngine::checkSat() => " << result << std::endl; if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) { return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE); } @@ -491,20 +492,20 @@ void PropEngine::push() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; d_satSolver->push(); - Debug("prop") << "push()" << endl; + Debug("prop") << "push()" << std::endl; } void PropEngine::pop() { Assert(!d_inCheckSat) << "Sat solver in solve()!"; d_satSolver->pop(); - Debug("prop") << "pop()" << endl; + Debug("prop") << "pop()" << std::endl; } void PropEngine::resetTrail() { d_satSolver->resetTrail(); - Debug("prop") << "resetTrail()" << endl; + Debug("prop") << "resetTrail()" << std::endl; } unsigned PropEngine::getAssertionLevel() const @@ -522,7 +523,7 @@ void PropEngine::interrupt() d_interrupted = true; d_satSolver->interrupt(); - Debug("prop") << "interrupt()" << endl; + Debug("prop") << "interrupt()" << std::endl; } void PropEngine::spendResource(ResourceManager::Resource r) diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index d0c75a924..834f35d90 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -21,22 +21,11 @@ #ifndef CVC4__PROP_ENGINE_H #define CVC4__PROP_ENGINE_H -#include - -#include "base/modal_exception.h" +#include "context/cdlist.h" #include "expr/node.h" -#include "options/options.h" -#include "proof/proof_manager.h" -#include "prop/minisat/core/Solver.h" -#include "prop/minisat/minisat.h" -#include "prop/proof_cnf_stream.h" -#include "prop/prop_proof_manager.h" -#include "prop/sat_solver_types.h" +#include "theory/output_channel.h" #include "theory/trust_node.h" -#include "theory/theory_inference_manager.h" -#include "util/resource_manager.h" #include "util/result.h" -#include "util/unsafe_interrupt_exception.h" namespace CVC4 { @@ -45,16 +34,12 @@ class DecisionEngine; class OutputManager; class TheoryEngine; -namespace theory { - class TheoryRegistrar; -}/* CVC4::theory namespace */ - namespace prop { class CnfStream; class CDCLTSatSolverInterface; - -class PropEngine; +class ProofCnfStream; +class PropPfManager; /** * PropEngine is the abstraction of a Sat Solver, providing methods for diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index 3c18dc896..c19d09bb9 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -16,6 +16,8 @@ #include "expr/proof_ensure_closed.h" #include "expr/proof_node_algorithm.h" +#include "prop/prop_proof_manager.h" +#include "prop/sat_solver.h" namespace CVC4 { namespace prop { diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index fc0151bcd..2e0d997df 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -27,6 +27,8 @@ namespace CVC4 { namespace prop { +class CDCLTSatSolverInterface; + /** * This class is responsible for managing the proof output of PropEngine, both * building and checking it. diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 0555e7ba7..e05923268 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -21,10 +21,7 @@ #include "expr/buffered_proof_generator.h" #include "expr/lazy_proof_chain.h" #include "expr/node.h" -#include "expr/proof.h" -#include "expr/proof_node_manager.h" #include "prop/minisat/core/SolverTypes.h" -#include "prop/cnf_stream.h" #include "prop/sat_solver_types.h" namespace Minisat { @@ -32,8 +29,13 @@ class Solver; } namespace CVC4 { + +class ProofNodeManager; + namespace prop { +class CnfStream; + /** * This class is responsible for managing the proof production of the SAT * solver. It tracks resolutions produced during solving and stores them, diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index ac79cf967..049232868 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -23,19 +23,16 @@ // Optional blocks below will be unconditionally included #define CVC4_USE_MINISAT -#include #include -#include "context/cdhashmap.h" #include "context/cdqueue.h" #include "expr/node.h" #include "prop/registrar.h" -#include "prop/sat_solver.h" +#include "prop/sat_solver_types.h" #include "theory/theory.h" #include "theory/theory_preprocessor.h" #include "theory/trust_node.h" #include "util/resource_manager.h" -#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 3f03c00e2..6a326ed2e 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -14,6 +14,8 @@ #include "smt/abduction_solver.h" +#include + #include "options/smt_options.h" #include "smt/smt_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 6776b06e2..5c1e1b879 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -19,6 +19,7 @@ #include "options/language.h" #include "options/smt_options.h" #include "proof/proof_manager.h" +#include "smt/abstract_values.h" #include "smt/smt_engine.h" using namespace CVC4::theory; diff --git a/src/smt/assertions.h b/src/smt/assertions.h index 5ce2556a7..bba4d2e29 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -20,14 +20,14 @@ #include #include "context/cdlist.h" -#include "context/context.h" #include "expr/node.h" #include "preprocessing/assertion_pipeline.h" -#include "smt/abstract_values.h" namespace CVC4 { namespace smt { +class AbstractValues; + /** * Contains all information pertaining to the assertions of an SMT engine. * diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 310201f47..b211c61c2 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -15,8 +15,10 @@ #include "smt/check_models.h" #include "options/smt_options.h" +#include "smt/model.h" #include "smt/node_command.h" #include "smt/preprocessor.h" +#include "smt/smt_solver.h" #include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/theory_engine.h" diff --git a/src/smt/check_models.h b/src/smt/check_models.h index 14af41b27..f9d527867 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -19,12 +19,13 @@ #include "context/cdlist.h" #include "expr/node.h" -#include "smt/model.h" -#include "smt/smt_solver.h" namespace CVC4 { namespace smt { +class Model; +class SmtSolver; + /** * This utility is responsible for checking the current model. */ diff --git a/src/smt/command.h b/src/smt/command.h index c11012944..a2230e12a 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -23,7 +23,6 @@ #define CVC4__COMMAND_H #include -#include #include #include #include @@ -40,8 +39,6 @@ class Term; } // namespace api class SymbolManager; -class UnsatCore; -class SmtEngine; class Command; class CommandStatus; diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h index 192bb2324..c7a05e21b 100644 --- a/src/smt/dump_manager.h +++ b/src/smt/dump_manager.h @@ -20,13 +20,17 @@ #include #include -#include "context/cdlist.h" +#include "context/context.h" #include "expr/node.h" namespace CVC4 { class NodeCommand; +namespace context { +class UserContext; +} + namespace smt { /** diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp index c2c4b6fd2..c01b5a243 100644 --- a/src/smt/expand_definitions.cpp +++ b/src/smt/expand_definitions.cpp @@ -18,8 +18,10 @@ #include #include "expr/node_manager_attributes.h" +#include "preprocessing/assertion_pipeline.h" #include "smt/defined_function.h" #include "smt/smt_engine.h" +#include "smt/smt_engine_stats.h" #include "theory/theory_engine.h" using namespace CVC4::preprocessing; diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index 486aa0c3a..0c2f9b2d5 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -20,17 +20,23 @@ #include #include "expr/node.h" -#include "expr/term_conversion_proof_generator.h" -#include "preprocessing/assertion_pipeline.h" -#include "smt/smt_engine_stats.h" -#include "util/resource_manager.h" +#include "theory/trust_node.h" namespace CVC4 { +class ProofNodeManager; +class ResourceManager; class SmtEngine; +class TConvProofGenerator; + +namespace preprocessing { +class AssertionPipeline; +} namespace smt { +struct SmtEngineStatistics; + /** * Module in charge of expanding definitions for an SMT engine. * diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 09ddfde75..965f49855 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -14,6 +14,8 @@ #include "smt/interpolation_solver.h" +#include + #include "options/smt_options.h" #include "smt/smt_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index d4cf33554..2482f77ef 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -22,11 +22,10 @@ #include -#include "options/open_ostream.h" -#include "smt/update_ostream.h" - namespace CVC4 { +class OstreamOpener; + /** This abstracts the management of ostream memory and initialization. */ class ManagedOstream { public: diff --git a/src/smt/model.h b/src/smt/model.h index e7c2434a6..277803499 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -21,13 +21,15 @@ #include #include "expr/node.h" -#include "theory/theory_model.h" -#include "util/cardinality.h" namespace CVC4 { class SmtEngine; +namespace theory { +class TheoryModel; +} + namespace smt { class Model; diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index cabd7bd20..95c9f1d18 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -18,6 +18,8 @@ #include "expr/node.h" #include "expr/node_algorithm.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" +#include "theory/theory_model.h" using namespace CVC4::kind; diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 5c45a6a56..6c453987e 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -21,10 +21,13 @@ #include "expr/node.h" #include "options/smt_options.h" -#include "theory/theory_model.h" namespace CVC4 { +namespace theory { +class TheoryModel; +} + /** * A utility for blocking the current model. */ diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index 33b5d9953..3fc3a2e0c 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -16,6 +16,8 @@ #include "smt/node_command.h" +#include + #include "printer/printer.h" namespace CVC4 { diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h index 983b98b34..81b935f36 100644 --- a/src/smt/options_manager.h +++ b/src/smt/options_manager.h @@ -15,15 +15,15 @@ #ifndef CVC4__SMT__OPTIONS_MANAGER_H #define CVC4__SMT__OPTIONS_MANAGER_H -#include "options/options.h" #include "options/options_listener.h" #include "smt/managed_ostreams.h" namespace CVC4 { -class SmtEngine; class LogicInfo; +class Options; class ResourceManager; +class SmtEngine; namespace smt { diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index ef80ebdae..261450dbb 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -16,6 +16,8 @@ #include "smt/preprocess_proof_generator.h" #include "expr/proof.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" #include "options/proof_options.h" #include "theory/rewriter.h" diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index 01d9c89da..312e58453 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -20,12 +20,10 @@ #include #include "context/cdhashmap.h" -#include "context/cdlist.h" #include "expr/lazy_proof.h" #include "expr/proof_set.h" #include "expr/proof_generator.h" #include "expr/proof_node_manager.h" -#include "theory/eager_proof_generator.h" #include "theory/trust_node.h" namespace CVC4 { diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 3e4ef0cdd..e5e9b98f4 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -19,8 +19,10 @@ #include "smt/abstract_values.h" #include "smt/assertions.h" #include "smt/dump.h" +#include "smt/preprocess_proof_generator.h" #include "smt/smt_engine.h" +using namespace std; using namespace CVC4::theory; using namespace CVC4::kind; diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 22b585e05..ece5fb5a8 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -17,14 +17,16 @@ #ifndef CVC4__SMT__PREPROCESSOR_H #define CVC4__SMT__PREPROCESSOR_H -#include +#include -#include "preprocessing/preprocessing_pass_context.h" #include "smt/expand_definitions.h" #include "smt/process_assertions.h" #include "theory/booleans/circuit_propagator.h" namespace CVC4 { +namespace preprocessing { +class PreprocessingPassContext; +} namespace smt { class AbstractValues; diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 0c01abbbb..23890d9fc 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -31,10 +31,13 @@ #include "printer/printer.h" #include "smt/defined_function.h" #include "smt/dump.h" +#include "smt/expand_definitions.h" #include "smt/smt_engine.h" +#include "smt/smt_engine_stats.h" #include "theory/logic_info.h" #include "theory/theory_engine.h" +using namespace std; using namespace CVC4::preprocessing; using namespace CVC4::theory; using namespace CVC4::kind; diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index ca834459d..891ef93f1 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -17,17 +17,14 @@ #ifndef CVC4__SMT__PROCESS_ASSERTIONS_H #define CVC4__SMT__PROCESS_ASSERTIONS_H -#include +#include -#include "context/cdhashmap.h" #include "context/cdlist.h" #include "expr/node.h" #include "expr/type_node.h" #include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/assertions.h" -#include "smt/expand_definitions.h" -#include "smt/smt_engine_stats.h" #include "util/resource_manager.h" namespace CVC4 { @@ -36,6 +33,9 @@ class SmtEngine; namespace smt { +class ExpandDefs; +struct SmtEngineStatistics; + /** * Module in charge of processing assertions for an SMT engine. * @@ -54,7 +54,7 @@ class ProcessAssertions { /** The types for the recursive function definitions */ typedef context::CDList NodeList; - typedef unordered_map NodeToBoolHashMap; + typedef std::unordered_map NodeToBoolHashMap; public: ProcessAssertions(SmtEngine& smt, diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index cb7943aed..2f7683e7c 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -14,11 +14,15 @@ #include "smt/proof_manager.h" +#include "expr/proof_checker.h" #include "expr/proof_node_algorithm.h" +#include "expr/proof_node_manager.h" #include "options/base_options.h" #include "options/proof_options.h" #include "smt/assertions.h" #include "smt/defined_function.h" +#include "smt/preprocess_proof_generator.h" +#include "smt/proof_post_processor.h" namespace CVC4 { namespace smt { diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index a6f284cad..abb984ea9 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -18,22 +18,21 @@ #define CVC4__SMT__PROOF_MANAGER_H #include "context/cdhashmap.h" -#include "context/cdlist.h" #include "expr/node.h" -#include "expr/proof_checker.h" -#include "expr/proof_node.h" -#include "expr/proof_node_manager.h" -#include "smt/preprocess_proof_generator.h" -#include "smt/proof_post_processor.h" namespace CVC4 { +class ProofChecker; +class ProofNode; +class ProofNodeManager; class SmtEngine; namespace smt { class Assertions; class DefinedFunction; +class PreprocessProofGenerator; +class ProofPostproccess; /** * This class is responsible for managing the proof output of SmtEngine, as diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 0898096f5..f7811911b 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -14,6 +14,7 @@ #include "smt/proof_post_processor.h" +#include "expr/proof_node_manager.h" #include "expr/skolem_manager.h" #include "options/proof_options.h" #include "options/smt_options.h" diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index de74d4869..b3e636b58 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -22,6 +22,7 @@ #include "expr/proof_node_updater.h" #include "smt/witness_form.h" +#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 80d7b96fa..891349809 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -34,11 +34,13 @@ #include "printer/printer.h" #include "proof/proof_manager.h" #include "proof/unsat_core.h" +#include "prop/prop_engine.h" #include "smt/abduction_solver.h" #include "smt/abstract_values.h" #include "smt/assertions.h" #include "smt/check_models.h" #include "smt/defined_function.h" +#include "smt/dump.h" #include "smt/dump_manager.h" #include "smt/interpolation_solver.h" #include "smt/listeners.h" diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8974e5e60..50e45c52f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -887,8 +887,6 @@ class CVC4_PUBLIC SmtEngine /* ....................................................................... */ private: /* ....................................................................... */ - /** The type of our internal assertion list */ - typedef context::CDList AssertionList; // disallow copy/assignment SmtEngine(const SmtEngine&) = delete; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 996a51e90..9b5871139 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -20,9 +20,12 @@ #include "smt/preprocessor.h" #include "smt/smt_engine.h" #include "smt/smt_engine_state.h" +#include "smt/smt_engine_stats.h" #include "theory/theory_engine.h" #include "theory/theory_traits.h" +using namespace std; + namespace CVC4 { namespace smt { @@ -67,12 +70,12 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine(d_theoryEngine.get(), - d_smt.getContext(), - d_smt.getUserContext(), - d_rm, - d_smt.getOutputManager(), - d_pnm)); + d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), + d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_smt.getOutputManager(), + d_pnm)); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -88,12 +91,12 @@ void SmtSolver::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine(d_theoryEngine.get(), - d_smt.getContext(), - d_smt.getUserContext(), - d_rm, - d_smt.getOutputManager(), - d_pnm)); + d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), + d_smt.getContext(), + d_smt.getUserContext(), + d_rm, + d_smt.getOutputManager(), + d_pnm)); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 5f08efb14..133d1e692 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -18,8 +18,11 @@ #include #include "expr/attribute.h" +#include "expr/lazy_proof.h" #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" +#include "expr/term_context_stack.h" +#include "expr/term_conversion_proof_generator.h" #include "options/smt_options.h" #include "proof/proof_manager.h" diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 803021fc3..c2a88d718 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -18,22 +18,22 @@ #pragma once -#include +#include #include #include "context/cdinsert_hashmap.h" #include "context/context.h" -#include "expr/lazy_proof.h" #include "expr/node.h" -#include "expr/term_context_stack.h" -#include "expr/term_conversion_proof_generator.h" -#include "theory/eager_proof_generator.h" +#include "expr/term_context.h" #include "theory/trust_node.h" -#include "util/bool.h" #include "util/hash.h" namespace CVC4 { +class LazyCDProof; +class ProofNodeManager; +class TConvProofGenerator; + class RemoveTermFormulas { public: RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr); diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index f5a9a2a75..8107136c3 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -18,6 +18,8 @@ #include "theory/arith/delta_rational.h" +#include + using namespace std; namespace CVC4 { diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 6487b48ec..5e34aebc7 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -22,6 +22,7 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" #include "util/iand.h" using namespace CVC4::kind; diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index bc4e0c8ae..01b834482 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -16,6 +16,8 @@ #include "theory/booleans/proof_circuit_propagator.h" +#include + #include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index d71fae8d0..a1763d081 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -31,6 +31,7 @@ #include "prop/sat_solver_types.h" #include "smt/smt_engine_scope.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" +#include "theory/theory.h" #include "theory/valuation.h" #include "util/resource_manager.h" diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 4eec45e4b..94f74a638 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -21,6 +21,7 @@ #include +#include "context/cdqueue.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "theory/bv/bitblast/simple_bitblaster.h" diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 6169d3752..e11f773a3 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -16,6 +16,8 @@ #include "theory/datatypes/sygus_datatype_utils.h" +#include + #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9105cdfd6..97600f76f 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -16,6 +16,7 @@ #include "theory/datatypes/theory_datatypes.h" #include +#include #include "base/check.h" #include "expr/dtype.h" diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index fda694e3d..94f90bc46 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -14,6 +14,8 @@ #include "theory/inference_id.h" +#include + namespace CVC4 { namespace theory { diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/theory/lazy_tree_proof_generator.cpp index 126ce60b9..b6155f19e 100644 --- a/src/theory/lazy_tree_proof_generator.cpp +++ b/src/theory/lazy_tree_proof_generator.cpp @@ -18,6 +18,7 @@ #include "expr/node.h" #include "expr/proof_generator.h" +#include "expr/proof_node.h" #include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index f1307f142..842ef59bf 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -14,6 +14,8 @@ **/ #include "theory/quantifiers/single_inv_partition.h" +#include + #include "expr/node_algorithm.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index cdc43658d..69adc9a4b 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -18,11 +18,12 @@ #define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H #include + #include "expr/node.h" #include "expr/node_trie.h" - #include "theory/evaluator.h" #include "theory/quantifiers/sygus/cegis.h" +#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 67f02b558..e56312362 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/sygus/sygus_abduct.h" +#include + #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 3edec96c7..9f8ac0e3c 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/sygus/sygus_interpol.h" +#include + #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "options/smt_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp index ca87e1049..d793fb718 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.cpp +++ b/src/theory/quantifiers/sygus/sygus_utils.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/sygus/sygus_utils.h" +#include + #include "expr/node_algorithm.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 275e9a27f..a5be5871f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index a72054f6d..c835369b7 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/lazy_trie.h" +#include "theory/rewriter.h" #include "util/bitvector.h" #include "util/random.h" #include "util/sampler.h" diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 24d2e00bd..21480e8ec 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -16,6 +16,8 @@ #include "theory/strings/regexp_operation.h" +#include + #include "expr/node_algorithm.h" #include "options/strings_options.h" #include "theory/rewriter.h" diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index b807fe1b3..4338d38c4 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -16,6 +16,8 @@ #include "theory/strings/theory_strings_utils.h" +#include + #include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/arith_entail.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e49ca8b05..07b23525e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -16,6 +16,8 @@ #include "theory/theory_engine.h" +#include + #include "base/map_util.h" #include "decision/decision_engine.h" #include "expr/attribute.h" diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index 2ba0a49ff..1eb191fd7 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -14,6 +14,10 @@ #include "theory/theory_engine_proof_generator.h" +#include + +#include "expr/proof_node.h" + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp index e9111db8c..5859b5c99 100644 --- a/src/theory/theory_id.cpp +++ b/src/theory/theory_id.cpp @@ -17,6 +17,8 @@ #include "theory/theory_id.h" +#include + #include "base/check.h" #include "lib/ffs.h" diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 94402e2d9..d2fc4cf9e 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -14,6 +14,8 @@ #include "theory/uf/cardinality_extension.h" +#include + #include "options/smt_options.h" #include "options/uf_options.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 58d5f4924..7a164c196 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -17,6 +17,7 @@ #include "base/configuration.h" #include "expr/proof.h" +#include "expr/proof_checker.h" #include "options/uf_options.h" namespace CVC4 { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index db8b89d89..e6e809533 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -18,6 +18,7 @@ #include "theory/uf/theory_uf.h" #include +#include #include "expr/node_algorithm.h" #include "expr/proof_node_manager.h" diff --git a/src/util/bitvector.h b/src/util/bitvector.h index b1a27929a..a5ef3a607 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -20,7 +20,9 @@ #define CVC4__BITVECTOR_H #include +#include +#include "base/exception.h" #include "util/integer.h" namespace CVC4 { diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index f78b076de..bf3a8ef2b 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -17,6 +17,7 @@ #include "util/cardinality.h" #include +#include #include "base/check.h" #include "base/exception.h" diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index fe05dc982..cca141094 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -20,13 +20,11 @@ #ifndef CVC4__INTEGER_H #define CVC4__INTEGER_H +#include + #include -#include #include -#include "base/exception.h" -#include "util/gmp_util.h" - namespace CVC4 { class Rational; diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp index ad769b779..2e2f200a3 100644 --- a/src/util/poly_util.cpp +++ b/src/util/poly_util.cpp @@ -27,6 +27,7 @@ #include #include +#include #include "base/check.h" #include "maybe.h" diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index f166d9cdc..f6c9a1e44 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -24,7 +24,7 @@ #include -#include "base/exception.h" +#include "util/gmp_util.h" #include "util/integer.h" #include "util/maybe.h" diff --git a/src/util/result.cpp b/src/util/result.cpp index f4e4d13c7..09445fa3b 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -18,6 +18,7 @@ #include #include #include +#include #include #include "base/check.h" diff --git a/src/util/result.h b/src/util/result.h index 96fe919d0..d0b0896bc 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -19,10 +19,9 @@ #ifndef CVC4__RESULT_H #define CVC4__RESULT_H -#include +#include #include -#include "base/exception.h" #include "options/language.h" namespace CVC4 { diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp index f45849736..aa2918cde 100644 --- a/src/util/safe_print.cpp +++ b/src/util/safe_print.cpp @@ -20,8 +20,11 @@ #include "safe_print.h" +#include #include +#include + /* Size of buffers used */ #define BUFFER_SIZE 20 diff --git a/src/util/safe_print.h b/src/util/safe_print.h index 6f72569bb..b98b4f3e9 100644 --- a/src/util/safe_print.h +++ b/src/util/safe_print.h @@ -40,10 +40,7 @@ #include #include -#include - -#include "lib/clock_gettime.h" -#include "util/result.h" +#include namespace CVC4 { diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp index 20dfb92a7..8b1a2c3db 100644 --- a/src/util/sampler.cpp +++ b/src/util/sampler.cpp @@ -17,8 +17,11 @@ #include "util/sampler.h" +#include + #include "base/check.h" #include "util/bitvector.h" +#include "util/random.h" namespace CVC4 { diff --git a/src/util/sampler.h b/src/util/sampler.h index 8968f5dc7..dad6605a5 100644 --- a/src/util/sampler.h +++ b/src/util/sampler.h @@ -21,7 +21,6 @@ #define CVC4__UTIL_FLOATINGPOINT_SAMPLER_H #include "util/floatingpoint.h" -#include "util/random.h" namespace CVC4 { diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 3bcf36abf..5c47fa4fd 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -26,12 +26,10 @@ #ifndef CVC4__SEXPR_H #define CVC4__SEXPR_H -#include #include #include #include -#include "base/exception.h" #include "options/language.h" #include "util/integer.h" #include "util/rational.h" diff --git a/src/util/string.h b/src/util/string.h index 9e503bb07..f908c2f0f 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -17,10 +17,10 @@ #ifndef CVC4__UTIL__STRING_H #define CVC4__UTIL__STRING_H -#include -#include +#include #include #include + #include "util/rational.h" namespace CVC4 { diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 1a3412186..5e2e80e4a 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -20,6 +20,7 @@ #include "context/context.h" #include "expr/node.h" #include "expr/node_manager.h" +#include "preprocessing/assertion_pipeline.h" #include "preprocessing/passes/bv_gauss.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp index 569c8a0e1..ceaf69423 100644 --- a/test/unit/prop/cnf_stream_white.cpp +++ b/test/unit/prop/cnf_stream_white.cpp @@ -19,6 +19,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/registrar.h" +#include "prop/sat_solver.h" #include "prop/theory_proxy.h" #include "test_smt.h" #include "theory/arith/theory_arith.h" diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp index 832965836..c5ffe0b87 100644 --- a/test/unit/util/cardinality_black.cpp +++ b/test/unit/util/cardinality_black.cpp @@ -17,6 +17,7 @@ #include #include +#include "base/exception.h" #include "test.h" #include "util/cardinality.h" #include "util/integer.h" diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp index 41497a7a4..f447246e2 100644 --- a/test/unit/util/integer_black.cpp +++ b/test/unit/util/integer_black.cpp @@ -17,6 +17,7 @@ #include #include +#include "base/exception.h" #include "test.h" #include "util/integer.h" -- 2.30.2