diff options
Diffstat (limited to 'src/theory/arith')
53 files changed, 256 insertions, 823 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 5b3c87b3d..71ac18e84 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -15,17 +15,18 @@ ** \todo document this file **/ -#include "cvc4autoconfig.h" +#include <cfloat> +#include <cmath> +#include <map> +#include <math.h> +#include "base/output.h" +#include "cvc4autoconfig.h" #include "theory/arith/approx_simplex.h" -#include "theory/arith/normal_form.h" #include "theory/arith/constraint.h" #include "theory/arith/cut_log.h" #include "theory/arith/matrix.h" -#include <math.h> -#include <cmath> -#include <cfloat> -#include <map> +#include "theory/arith/normal_form.h" using namespace std; diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h index 808b64703..064887787 100644 --- a/src/theory/arith/approx_simplex.h +++ b/src/theory/arith/approx_simplex.h @@ -19,14 +19,13 @@ #include "cvc4_private.h" #pragma once +#include <vector> -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" -#include "util/rational.h" #include "theory/arith/delta_rational.h" -//#include "theory/arith/linear_equality.h" #include "util/dense_map.h" -#include <vector> +#include "util/rational.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/arith_heuristic_pivot_rule.cpp b/src/theory/arith/arith_heuristic_pivot_rule.cpp deleted file mode 100644 index 8ef2385c7..000000000 --- a/src/theory/arith/arith_heuristic_pivot_rule.cpp +++ /dev/null @@ -1,41 +0,0 @@ -/********************* */ -/*! \file arith_heuristic_pivot_rule.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/arith/arith_heuristic_pivot_rule.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) { - switch(rule) { - case MINIMUM_AMOUNT: - out << "MINIMUM_AMOUNT"; - break; - case VAR_ORDER: - out << "VAR_ORDER"; - break; - case MAXIMUM_AMOUNT: - out << "MAXIMUM_AMOUNT"; - break; - default: - out << "ArithHeuristicPivotRule!UNKNOWN"; - } - - return out; -} - -}/* CVC4 namespace */ - diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/theory/arith/arith_heuristic_pivot_rule.h deleted file mode 100644 index a64a7c846..000000000 --- a/src/theory/arith/arith_heuristic_pivot_rule.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file arith_heuristic_pivot_rule.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H -#define __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H - -#include <iostream> - -namespace CVC4 { - -typedef enum { - VAR_ORDER, - MINIMUM_AMOUNT, - MAXIMUM_AMOUNT, - SUM_METRIC -} ErrorSelectionRule; - -std::ostream& operator<<(std::ostream& out, ErrorSelectionRule rule) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */ diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 2b31831e2..cd180e59e 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -15,15 +15,18 @@ ** \todo document this file **/ -#include "smt/options.h" #include "theory/arith/arith_ite_utils.h" -#include "theory/arith/normal_form.h" + +#include <ostream> + +#include "base/output.h" +#include "options/smt_options.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/normal_form.h" #include "theory/ite_utilities.h" -#include "theory/theory_model.h" #include "theory/rewriter.h" #include "theory/substitutions.h" -#include <ostream> +#include "theory/theory_model.h" using namespace std; diff --git a/src/theory/arith/arith_propagation_mode.cpp b/src/theory/arith/arith_propagation_mode.cpp deleted file mode 100644 index 119761906..000000000 --- a/src/theory/arith/arith_propagation_mode.cpp +++ /dev/null @@ -1,44 +0,0 @@ -/********************* */ -/*! \file arith_propagation_mode.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/arith/arith_propagation_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, ArithPropagationMode mode) { - switch(mode) { - case NO_PROP: - out << "NO_PROP"; - break; - case UNATE_PROP: - out << "UNATE_PROP"; - break; - case BOUND_INFERENCE_PROP: - out << "BOUND_INFERENCE_PROP"; - break; - case BOTH_PROP: - out << "BOTH_PROP"; - break; - default: - out << "ArithPropagationMode!UNKNOWN"; - } - - return out; -} - -}/* CVC4 namespace */ - diff --git a/src/theory/arith/arith_propagation_mode.h b/src/theory/arith/arith_propagation_mode.h deleted file mode 100644 index fe8f8c9cc..000000000 --- a/src/theory/arith/arith_propagation_mode.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file arith_propagation_mode.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H -#define __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H - -#include <iostream> - -namespace CVC4 { - -typedef enum { - NO_PROP, - UNATE_PROP, - BOUND_INFERENCE_PROP, - BOTH_PROP -} ArithPropagationMode; - -std::ostream& operator<<(std::ostream& out, ArithPropagationMode rule) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */ diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a85fd024f..ca286d53a 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -15,14 +15,15 @@ ** \todo document this file **/ -#include "theory/theory.h" -#include "theory/arith/normal_form.h" -#include "theory/arith/arith_rewriter.h" -#include "theory/arith/arith_utilities.h" - -#include <vector> #include <set> #include <stack> +#include <vector> + +#include "base/output.h" +#include "theory/arith/arith_rewriter.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/normal_form.h" +#include "theory/theory.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp index a7767e38b..383c6b418 100644 --- a/src/theory/arith/arith_static_learner.cpp +++ b/src/theory/arith/arith_static_learner.cpp @@ -15,18 +15,16 @@ ** \todo document this file **/ -#include "theory/rewriter.h" +#include <vector> -#include "theory/arith/arith_utilities.h" +#include "base/output.h" +#include "expr/convenience_node_builders.h" +#include "expr/expr.h" +#include "options/arith_options.h" #include "theory/arith/arith_static_learner.h" -#include "theory/arith/options.h" - +#include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" - -#include "expr/expr.h" -#include "expr/convenience_node_builders.h" - -#include <vector> +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index 7a1a1a6db..2b0ee9dad 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -20,13 +20,12 @@ #ifndef __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H #define __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H +#include <set> -#include "util/statistics_registry.h" -#include "theory/arith/arith_utilities.h" - -#include "context/context.h" #include "context/cdtrail_hashmap.h" -#include <set> +#include "context/context.h" +#include "expr/statistics_registry.h" +#include "theory/arith/arith_utilities.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/arith_unate_lemma_mode.cpp b/src/theory/arith/arith_unate_lemma_mode.cpp deleted file mode 100644 index bb6066bb4..000000000 --- a/src/theory/arith/arith_unate_lemma_mode.cpp +++ /dev/null @@ -1,44 +0,0 @@ -/********************* */ -/*! \file arith_unate_lemma_mode.cpp - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/arith/arith_unate_lemma_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode mode) { - switch(mode) { - case NO_PRESOLVE_LEMMAS: - out << "NO_PRESOLVE_LEMMAS"; - break; - case INEQUALITY_PRESOLVE_LEMMAS: - out << "INEQUALITY_PRESOLVE_LEMMAS"; - break; - case EQUALITY_PRESOLVE_LEMMAS: - out << "EQUALITY_PRESOLVE_LEMMAS"; - break; - case ALL_PRESOLVE_LEMMAS: - out << "ALL_PRESOLVE_LEMMAS"; - break; - default: - out << "ArithUnateLemmaMode!UNKNOWN"; - } - - return out; -} - -}/* CVC4 namespace */ - diff --git a/src/theory/arith/arith_unate_lemma_mode.h b/src/theory/arith/arith_unate_lemma_mode.h deleted file mode 100644 index 5e1362bcb..000000000 --- a/src/theory/arith/arith_unate_lemma_mode.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file arith_unate_lemma_mode.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H -#define __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H - -#include <iostream> - -namespace CVC4 { - -typedef enum { - NO_PRESOLVE_LEMMAS, - INEQUALITY_PRESOLVE_LEMMAS, - EQUALITY_PRESOLVE_LEMMAS, - ALL_PRESOLVE_LEMMAS -} ArithUnateLemmaMode; - -std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode rule) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */ diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 9d32916cc..ffa896012 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -19,16 +19,17 @@ #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H -#include "util/rational.h" -#include "util/integer.h" -#include "util/dense_map.h" -#include "expr/node.h" -#include "theory/arith/delta_rational.h" -#include "theory/arith/arithvar.h" -#include "context/cdhashset.h" #include <ext/hash_map> #include <vector> +#include "context/cdhashset.h" +#include "expr/node.h" +#include "theory/arith/arithvar.h" +#include "theory/arith/delta_rational.h" +#include "util/dense_map.h" +#include "util/integer.h" +#include "util/rational.h" + namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index dd049e94f..9e4dab4c3 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -22,10 +22,10 @@ #pragma once #include <vector> + #include "util/index.h" #include "util/rational.h" - namespace CVC4 { namespace theory { namespace arith { @@ -43,4 +43,3 @@ extern bool debugIsASet(const ArithVarVec& variables); }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 5b92a8809..737cc9e7b 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -15,9 +15,9 @@ ** \todo document this file **/ - +#include "base/output.h" +#include "options/arith_options.h" #include "theory/arith/attempt_solution_simplex.h" -#include "theory/arith/options.h" #include "theory/arith/constraint.h" using namespace std; diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h index 4d94169c9..88d29f6b0 100644 --- a/src/theory/arith/attempt_solution_simplex.h +++ b/src/theory/arith/attempt_solution_simplex.h @@ -53,7 +53,7 @@ #pragma once -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "theory/arith/approx_simplex.h" diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h index c1f0ce545..b5e0124c1 100644 --- a/src/theory/arith/bound_counts.h +++ b/src/theory/arith/bound_counts.h @@ -19,8 +19,9 @@ #pragma once #include <stdint.h> + +#include "base/cvc4_assert.h" #include "theory/arith/arithvar.h" -#include "util/cvc4_assert.h" #include "util/dense_map.h" namespace CVC4 { diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index 734c605c6..d180ceab5 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -19,12 +19,11 @@ #pragma once #include "expr/node.h" -#include "util/rational.h" - -#include "theory/arith/theory_arith_private_forward.h" #include "theory/arith/arithvar.h" #include "theory/arith/bound_counts.h" #include "theory/arith/constraint_forward.h" +#include "theory/arith/theory_arith_private_forward.h" +#include "util/rational.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 8a145ffc2..964c92eb5 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -14,10 +14,10 @@ ** \todo document this file **/ +#include "base/output.h" +#include "theory/arith/arith_utilities.h" #include "theory/arith/congruence_manager.h" - #include "theory/arith/constraint.h" -#include "theory/arith/arith_utilities.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 7ecfd21cf..2fc9c47ed 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -19,19 +19,16 @@ #pragma once +#include "context/cdlist.h" +#include "context/cdmaybe.h" +#include "context/cdo.h" +#include "context/cdtrail_queue.h" +#include "context/context.h" +#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/partial_model.h" - #include "theory/uf/equality_engine.h" - -#include "context/cdo.h" -#include "context/cdlist.h" -#include "context/context.h" -#include "context/cdtrail_queue.h" -#include "context/cdmaybe.h" - -#include "util/statistics_registry.h" #include "util/dense_map.h" namespace CVC4 { diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 4acf86d43..f13565a7f 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -15,15 +15,15 @@ ** \todo document this file **/ -#include "cvc4_private.h" -#include "theory/arith/constraint.h" -#include "theory/arith/arith_utilities.h" -#include "theory/arith/normal_form.h" +#include <ostream> +#include <algorithm> +#include "base/output.h" #include "proof/proof.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/constraint.h" +#include "theory/arith/normal_form.h" -#include <ostream> -#include <algorithm> using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp index d855caee8..d94e1c760 100644 --- a/src/theory/arith/cut_log.cpp +++ b/src/theory/arith/cut_log.cpp @@ -15,17 +15,17 @@ ** \todo document this file **/ -#include "cvc4autoconfig.h" - +#include <cmath> +#include <limits.h> +#include <map> +#include <math.h> -#include "theory/arith/cut_log.h" +#include "base/output.h" +#include "cvc4autoconfig.h" #include "theory/arith/approx_simplex.h" -#include "theory/arith/normal_form.h" #include "theory/arith/constraint.h" -#include <math.h> -#include <cmath> -#include <map> -#include <limits.h> +#include "theory/arith/cut_log.h" +#include "theory/arith/normal_form.h" using namespace std; diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 9ce017488..bbed13418 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -20,15 +20,16 @@ #pragma once +#include <ext/hash_map> +#include <map> +#include <set> +#include <vector> + #include "expr/kind.h" -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/arith/constraint_forward.h" #include "util/dense_map.h" -#include <vector> -#include <map> -#include <set> -#include <ext/hash_map> namespace CVC4 { namespace theory { diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index a9d919c21..5f67847d8 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -17,14 +17,13 @@ #include "cvc4_private.h" -#include "util/integer.h" -#include "util/rational.h" -#include "util/exception.h" - +#pragma once #include <ostream> -#pragma once +#include "base/exception.h" +#include "util/integer.h" +#include "util/rational.h" namespace CVC4 { diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 7e50dad87..f8b8e0e7b 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -14,11 +14,12 @@ ** A Diophantine equation solver for the theory of arithmetic. **/ -#include "theory/arith/dio_solver.h" -#include "theory/arith/options.h" - #include <iostream> +#include "base/output.h" +#include "options/arith_options.h" +#include "theory/arith/dio_solver.h" + using namespace std; namespace CVC4 { diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 9b96acf48..626160b03 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -16,22 +16,22 @@ #include "cvc4_private.h" + #ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H #define __CVC4__THEORY__ARITH__DIO_SOLVER_H -#include "context/context.h" -#include "context/cdo.h" +#include <utility> +#include <vector> + +#include "base/output.h" #include "context/cdlist.h" +#include "context/cdo.h" #include "context/cdqueue.h" - +#include "context/context.h" +#include "expr/statistics_registry.h" +#include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "util/rational.h" -#include "theory/arith/normal_form.h" - -#include "util/statistics_registry.h" - -#include <vector> -#include <utility> namespace CVC4 { namespace theory { diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 234b33e97..32f81ded8 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -15,10 +15,10 @@ ** \todo document this file **/ - -#include "theory/arith/dual_simplex.h" -#include "theory/arith/options.h" +#include "base/output.h" +#include "options/arith_options.h" #include "theory/arith/constraint.h" +#include "theory/arith/dual_simplex.h" using namespace std; diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h index 53f627081..d6bf57bb0 100644 --- a/src/theory/arith/dual_simplex.h +++ b/src/theory/arith/dual_simplex.h @@ -48,12 +48,11 @@ ** These are theory valid and are currently turned into lemmas **/ - #include "cvc4_private.h" #pragma once -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" namespace CVC4 { diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h index 5843e0f7b..f12e38c12 100644 --- a/src/theory/arith/error_set.h +++ b/src/theory/arith/error_set.h @@ -20,36 +20,18 @@ #pragma once +#include <vector> + +#include "expr/statistics_registry.h" +#include "options/arith_heuristic_pivot_rule.h" #include "theory/arith/arithvar.h" #include "theory/arith/bound_counts.h" +#include "theory/arith/callbacks.h" #include "theory/arith/delta_rational.h" #include "theory/arith/partial_model.h" -#include "theory/arith/arith_heuristic_pivot_rule.h" #include "theory/arith/tableau_sizes.h" -#include "theory/arith/callbacks.h" - -#include "util/statistics_registry.h" #include "util/bin_heap.h" -// #if CVC4_GCC_HAS_PB_DS_BUG -// // Unfortunate bug in some older GCCs (e.g., v4.2): -// // http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612 -// // Requires some header-hacking to work around -// # define __throw_container_error inline __throw_container_error -// # define __throw_insert_error inline __throw_insert_error -// # define __throw_join_error inline __throw_join_error -// # define __throw_resize_error inline __throw_resize_error -// # include <ext/pb_ds/exception.hpp> -// # undef __throw_container_error -// # undef __throw_insert_error -// # undef __throw_join_error -// # undef __throw_resize_error -// #endif /* CVC4_GCC_HAS_PB_DS_BUG */ - -// #include <ext/pb_ds/priority_queue.hpp> - -#include <vector> - namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index d21bb8f8b..229dc379c 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -14,13 +14,12 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ - - #include "theory/arith/fc_simplex.h" -#include "theory/arith/options.h" -#include "theory/arith/constraint.h" -#include "util/statistics_registry.h" +#include "base/output.h" +#include "expr/statistics_registry.h" +#include "options/arith_options.h" +#include "theory/arith/constraint.h" using namespace std; diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index b6c0c4f62..471804003 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -52,10 +52,11 @@ #pragma once +#include <stdint.h> + +#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "util/dense_map.h" -#include "util/statistics_registry.h" -#include <stdint.h> namespace CVC4 { namespace theory { diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h index 55486080a..770d9d1b3 100644 --- a/src/theory/arith/infer_bounds.h +++ b/src/theory/arith/infer_bounds.h @@ -19,13 +19,15 @@ #pragma once -#include "util/maybe.h" -#include "util/integer.h" -#include "util/rational.h" +#include <ostream> + #include "expr/node.h" #include "theory/arith/delta_rational.h" #include "theory/theory.h" -#include <ostream> +#include "util/integer.h" +#include "util/maybe.h" +#include "util/rational.h" + namespace CVC4 { namespace theory { diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index bd252bf49..d8888bd75 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -15,8 +15,9 @@ **/ -#include "theory/arith/linear_equality.h" +#include "base/output.h" #include "theory/arith/constraint.h" +#include "theory/arith/linear_equality.h" using namespace std; diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 99ec6e52c..d7c9c038c 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -29,16 +29,15 @@ #pragma once -#include "theory/arith/delta_rational.h" +#include "expr/statistics_registry.h" +#include "options/arith_options.h" #include "theory/arith/arithvar.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/tableau.h" #include "theory/arith/constraint_forward.h" +#include "theory/arith/delta_rational.h" +#include "theory/arith/partial_model.h" #include "theory/arith/simplex_update.h" -#include "theory/arith/options.h" - +#include "theory/arith/tableau.h" #include "util/maybe.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index 6c218eb0b..647df886f 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -19,13 +19,14 @@ #pragma once -#include "util/index.h" -#include "util/dense_map.h" -#include "theory/arith/arithvar.h" - #include <queue> -#include <vector> #include <utility> +#include <vector> + +#include "base/output.h" +#include "theory/arith/arithvar.h" +#include "util/dense_map.h" +#include "util/index.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index fda34960a..e22a5e2e3 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -15,9 +15,11 @@ ** \todo document this file **/ +#include <list> + +#include "base/output.h" #include "theory/arith/normal_form.h" #include "theory/arith/arith_utilities.h" -#include <list> #include "theory/theory.h" using namespace std; diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 97813338f..eeb56f597 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -20,19 +20,20 @@ #ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H #define __CVC4__THEORY__ARITH__NORMAL_FORM_H -#include "expr/node.h" -#include "expr/node_self_iterator.h" -#include "util/rational.h" -#include "theory/arith/delta_rational.h" -//#include "theory/arith/arith_utilities.h" - -#include <list> #include <algorithm> +#include <list> #if IS_SORTED_IN_GNUCXX_NAMESPACE # include <ext/algorithm> #endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */ +#include "base/output.h" +#include "expr/node.h" +#include "expr/node_self_iterator.h" +#include "theory/arith/delta_rational.h" +#include "util/rational.h" + + namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/options b/src/theory/arith/options deleted file mode 100644 index ea9658eb3..000000000 --- a/src/theory/arith/options +++ /dev/null @@ -1,164 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module ARITH "theory/arith/options.h" Arithmetic theory - -option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::theory::arith::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_unate_lemma_mode.h" - determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help) - -option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::theory::arith::stringToArithPropagationMode :default BOTH_PROP :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_propagation_mode.h" - turns on arithmetic propagation (default is 'old', see --arith-prop=help) - -# The maximum number of difference pivots to do per invocation of simplex. -# If this is negative, the number of pivots done is the number of variables. -# If this is not set by the user, different logics are free to chose different -# defaults. -option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write - the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection - -# The maximum number of variable order pivots to do per invocation of simplex. -# If this is negative, the number of pivots done is unlimited. -# If this is not set by the user, different logics are free to chose different -# defaults. -expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write - limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule - -option arithErrorSelectionRule --error-selection-rule=RULE ErrorSelectionRule :handler CVC4::theory::arith::stringToErrorSelectionRule :default MINIMUM_AMOUNT :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_heuristic_pivot_rule.h" - change the pivot rule for the basic variable (default is 'min', see --pivot-rule help) - -# The number of pivots before simplex rechecks every basic variable for a conflict -option arithSimplexCheckPeriod --simplex-check-period=N uint16_t :default 200 - the number of pivots to do in simplex before rechecking for a conflict on all variables - -# This is the pivots per basic variable that can be done using heuristic choices -# before variable order must be used. -# If this is not set by the user, different logics are free to chose different -# defaults. -option arithPivotThreshold --pivot-threshold=N uint16_t :default 2 :read-write - sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order - -option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16 - sets the maximum row length to be used in propagation - -option arithDioSolver /--disable-dio-solver bool :default true - turns off Linear Diophantine Equation solver (Griggio, JSAT 2012) - -# Whether to split (= x y) into (and (<= x y) (>= x y)) in -# arithmetic preprocessing. -option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-equalities bool :default false :read-write - turns on the preprocessing rewrite turning equalities into a conjunction of inequalities -/turns off the preprocessing rewrite turning equalities into a conjunction of inequalities - - -option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default false - turns on the preprocessing step of attempting to infer bounds on miplib problems -/turns off the preprocessing step of attempting to infer bounds on miplib problems - -option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1 - do substitution for miplib 'tmp' vars if defined in <= N eliminated vars - -option doCutAllBounded --cut-all-bounded bool :default false :read-write - turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds -/turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds - -option maxCutsInContext --maxCutsInContext unsigned :default 65535 - maximum cuts in a given context before signalling a restart - -option revertArithModels --revert-arith-models-on-unsat bool :default false - revert the arithmetic model to a known safe model on unsat if one is cached - -option havePenalties --fc-penalties bool :default false :read-write - turns on degenerate pivot penalties -/turns off degenerate pivot penalties - -option useFC --use-fcsimplex bool :default false :read-write - use focusing and converging simplex (FMCAD 2013 submission) - -option useSOI --use-soi bool :default false :read-write - use sum of infeasibility simplex (FMCAD 2013 submission) - -option restrictedPivots --restrict-pivots bool :default true :read-write - have a pivot cap for simplex at effort levels below fullEffort - -option collectPivots --collect-pivot-stats bool :default false :read-write - collect the pivot history - -option useApprox --use-approx bool :default false :read-write - attempt to use an approximate solver - -option maxApproxDepth --approx-branch-depth int16_t :default 200 :read-write - maximum branch depth the approximate solver is allowed to take - -option exportDioDecompositions --dio-decomps bool :default false :read-write - let skolem variables for integer divisibility constraints leak from the dio solver - -option newProp --new-prop bool :default false :read-write - use the new row propagation system - -option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write - rows shorter than this are propagated as clauses - -option soiQuickExplain --soi-qe bool :default false :read-write - use quick explain to minimize the sum of infeasibility conflicts - -option rewriteDivk rewrite-divk --rewrite-divk bool :default false :read-write - rewrite division and mod when by a constant into linear terms - -option trySolveIntStandardEffort --se-solve-int bool :default false - attempt to use the approximate solve integer method on standard effort - -option replayFailureLemma --lemmas-on-replay-failure bool :default false - attempt to use external lemmas if approximate solve integer failed - -option dioSolverTurns --dio-turns int :default 10 - turns in a row dio solver cutting gets - -option rrTurns --rr-turns int :default 3 - round robin turn - -option dioRepeat --dio-repeat bool :default false - handle dio solver constraints in mass or one at a time - -option replayEarlyCloseDepths --replay-early-close-depth int :default 1 - multiples of the depths to try to close the approx log eagerly - -option replayFailurePenalty --replay-failure-penalty int :default 100 - number of solve integer attempts to skips after a numeric failure - -option replayNumericFailurePenalty --replay-num-err-penalty int :default 4194304 - number of solve integer attempts to skips after a numeric failure - -option replayRejectCutSize --replay-reject-cut unsigned :default 25500 - maximum complexity of any coefficient while replaying cuts - -option lemmaRejectCutSize --replay-lemma-reject-cut unsigned :default 25500 - maximum complexity of any coefficient while outputing replaying cut lemmas - -option soiApproxMajorFailure --replay-soi-major-threshold double :default .01 - threshold for a major tolerance failure by the approximate solver - -option soiApproxMajorFailurePen --replay-soi-major-threshold-pen int :default 50 - threshold for a major tolerance failure by the approximate solver - -option soiApproxMinorFailure --replay-soi-minor-threshold double :default .0001 - threshold for a minor tolerance failure by the approximate solver - -option soiApproxMinorFailurePen --replay-soi-minor-threshold-pen int :default 10 - threshold for a minor tolerance failure by the approximate solver - -option ppAssertMaxSubSize --pp-assert-max-sub-size unsigned :default 2 - threshold for substituting an equality in ppAssert - -option maxReplayTree --max-replay-tree int :default 512 - threshold for attempting to replay a tree - - -option pbRewrites --pb-rewrites bool :default false - apply pseudo boolean rewrites - -option pbRewriteThreshold --pb-rewrite-threshold int :default 256 - threshold of number of pseudoboolean variables to have before doing rewrites - -endmodule diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h deleted file mode 100644 index 57b9661ba..000000000 --- a/src/theory/arith/options_handlers.h +++ /dev/null @@ -1,122 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Kshitij Bansal, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Custom handlers and predicates for arithmetic options - ** - ** Custom handlers and predicates for arithmetic options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H - -#include <string> - -namespace CVC4 { -namespace theory { -namespace arith { - -static const std::string arithUnateLemmasHelp = "\ -Unate lemmas are generated before SAT search begins using the relationship\n\ -of constant terms and polynomials.\n\ -Modes currently supported by the --unate-lemmas option:\n\ -+ none \n\ -+ ineqs \n\ - Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\ -+ eqs \n\ - Outputs lemmas of the general forms\n\ - (= p c) implies (<= p d) for c < d, or\n\ - (= p c) implies (not (= p d)) for c != d.\n\ -+ all \n\ - A combination of inequalities and equalities.\n\ -"; - -static const std::string propagationModeHelp = "\ -This decides on kind of propagation arithmetic attempts to do during the search.\n\ -+ none\n\ -+ unate\n\ - use constraints to do unate propagation\n\ -+ bi (Bounds Inference)\n\ - infers bounds on basic variables using the upper and lower bounds of the\n\ - non-basic variables in the tableau.\n\ -+both\n\ -"; - -static const std::string errorSelectionRulesHelp = "\ -This decides on the rule used by simplex during heuristic rounds\n\ -for deciding the next basic variable to select.\n\ -Heuristic pivot rules available:\n\ -+min\n\ - The minimum abs() value of the variable's violation of its bound. (default)\n\ -+max\n\ - The maximum violation the bound\n\ -+varord\n\ - The variable order\n\ -"; - -inline ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "all") { - return ALL_PRESOLVE_LEMMAS; - } else if(optarg == "none") { - return NO_PRESOLVE_LEMMAS; - } else if(optarg == "ineqs") { - return INEQUALITY_PRESOLVE_LEMMAS; - } else if(optarg == "eqs") { - return EQUALITY_PRESOLVE_LEMMAS; - } else if(optarg == "help") { - puts(arithUnateLemmasHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --unate-lemmas: `") + - optarg + "'. Try --unate-lemmas help."); - } -} - -inline ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "none") { - return NO_PROP; - } else if(optarg == "unate") { - return UNATE_PROP; - } else if(optarg == "bi") { - return BOUND_INFERENCE_PROP; - } else if(optarg == "both") { - return BOTH_PROP; - } else if(optarg == "help") { - puts(propagationModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --arith-prop: `") + - optarg + "'. Try --arith-prop help."); - } -} - -inline ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "min") { - return MINIMUM_AMOUNT; - } else if(optarg == "varord") { - return VAR_ORDER; - } else if(optarg == "max") { - return MAXIMUM_AMOUNT; - } else if(optarg == "help") { - puts(errorSelectionRulesHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") + - optarg + "'. Try --heuristic-pivot-rule help."); - } -} - -}/* CVC4::theory::arith namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H */ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index cb853953f..0124ee0f9 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -15,11 +15,10 @@ ** \todo document this file **/ - -#include "theory/arith/partial_model.h" -#include "util/output.h" +#include "base/output.h" #include "theory/arith/constraint.h" #include "theory/arith/normal_form.h" +#include "theory/arith/partial_model.h" using namespace std; diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp index 829952c5e..c09b0180a 100644 --- a/src/theory/arith/pseudoboolean_proc.cpp +++ b/src/theory/arith/pseudoboolean_proc.cpp @@ -15,9 +15,10 @@ ** \todo document this file **/ -#include "theory/arith/pseudoboolean_proc.h" -#include "theory/arith/normal_form.h" +#include "base/output.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/normal_form.h" +#include "theory/arith/pseudoboolean_proc.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h index 665f1aa06..d1e10f695 100644 --- a/src/theory/arith/pseudoboolean_proc.h +++ b/src/theory/arith/pseudoboolean_proc.h @@ -19,17 +19,16 @@ #pragma once +#include <ext/hash_set> #include <vector> -#include "util/rational.h" -#include "util/maybe.h" -#include "expr/node.h" -#include "context/context.h" -#include "context/cdo.h" #include "context/cdhashmap.h" - +#include "context/cdo.h" +#include "context/context.h" +#include "expr/node.h" #include "theory/substitutions.h" -#include <ext/hash_set> +#include "util/maybe.h" +#include "util/rational.h" namespace CVC4 { namespace theory { @@ -107,4 +106,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 49664e0ea..24c6ce432 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -16,9 +16,10 @@ **/ -#include "theory/arith/simplex.h" -#include "theory/arith/options.h" +#include "base/output.h" +#include "options/arith_options.h" #include "theory/arith/constraint.h" +#include "theory/arith/simplex.h" using namespace std; diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 2d7fc597a..f39006788 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -53,15 +53,14 @@ #pragma once +#include "expr/result.h" #include "theory/arith/arithvar.h" -#include "theory/arith/error_set.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/tableau.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/error_set.h" #include "theory/arith/linear_equality.h" - +#include "theory/arith/partial_model.h" +#include "theory/arith/tableau.h" #include "util/dense_map.h" -#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 0d07c5ffc..765e6a00d 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -14,15 +14,15 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ +#include "theory/arith/soi_simplex.h" +#include <algorithm> -#include "theory/arith/soi_simplex.h" -#include "theory/arith/options.h" +#include "base/output.h" +#include "expr/statistics_registry.h" +#include "options/arith_options.h" #include "theory/arith/constraint.h" -#include "util/statistics_registry.h" - -#include <algorithm> using namespace std; diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h index 6dd6373d4..b08d7794b 100644 --- a/src/theory/arith/soi_simplex.h +++ b/src/theory/arith/soi_simplex.h @@ -52,10 +52,11 @@ #pragma once +#include <stdint.h> + +#include "expr/statistics_registry.h" #include "theory/arith/simplex.h" #include "util/dense_map.h" -#include "util/statistics_registry.h" -#include <stdint.h> namespace CVC4 { namespace theory { diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index 231eb1562..744dda6b7 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -15,6 +15,7 @@ ** \todo document this file **/ +#include "base/output.h" #include "theory/arith/tableau.h" using namespace std; diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index c6750f61b..77187c798 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -19,11 +19,12 @@ #pragma once -#include "util/dense_map.h" -#include "util/rational.h" +#include <vector> + #include "theory/arith/arithvar.h" #include "theory/arith/matrix.h" -#include <vector> +#include "util/dense_map.h" +#include "util/rational.h" namespace CVC4 { namespace theory { @@ -161,4 +162,3 @@ private: }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp index fdd9ff16a..64bae22fe 100644 --- a/src/theory/arith/tableau_sizes.cpp +++ b/src/theory/arith/tableau_sizes.cpp @@ -15,6 +15,7 @@ ** \todo document this file **/ +#include "base/output.h" #include "theory/arith/tableau_sizes.h" #include "theory/arith/tableau.h" diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 565c69514..1e3b21b17 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -16,9 +16,10 @@ **/ #include "theory/arith/theory_arith.h" -#include "theory/arith/theory_arith_private.h" + +#include "options/smt_options.h" #include "theory/arith/infer_bounds.h" -#include "smt/options.h" +#include "theory/arith/theory_arith_private.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c9c45af2f..ab800f10d 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -17,71 +17,59 @@ #include "theory/arith/theory_arith_private.h" -#include "expr/node.h" -#include "expr/kind.h" -#include "expr/metakind.h" -#include "expr/node_builder.h" +#include <stdint.h> -#include "context/context.h" -#include "context/cdlist.h" +#include <map> +#include <queue> +#include <vector> + +#include "base/output.h" #include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" +#include "context/cdlist.h" #include "context/cdqueue.h" - -#include "theory/valuation.h" -#include "theory/rewriter.h" - -#include "util/rational.h" -#include "util/integer.h" -#include "util/boolean_simplification.h" -#include "util/dense_map.h" -#include "util/statistics_registry.h" -#include "util/result.h" - -#include "smt/logic_request.h" +#include "context/context.h" +#include "expr/kind.h" +#include "expr/metakind.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/result.h" +#include "expr/statistics_registry.h" +#include "options/arith_options.h" +#include "options/smt_options.h" // for incrementalSolving() #include "smt/logic_exception.h" -#include "smt/options.h" // for incrementalSolving() - -#include "theory/arith/arithvar.h" -#include "theory/arith/cut_log.h" -#include "theory/arith/delta_rational.h" -#include "theory/arith/matrix.h" +#include "smt/logic_request.h" +#include "smt_util/boolean_simplification.h" +#include "theory/arith/approx_simplex.h" +#include "theory/arith/arith_ite_utils.h" +#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_rewriter.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/linear_equality.h" -#include "theory/arith/simplex.h" #include "theory/arith/arith_static_learner.h" -#include "theory/arith/dio_solver.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/congruence_manager.h" - -#include "theory/arith/approx_simplex.h" #include "theory/arith/constraint.h" - -#include "theory/ite_utilities.h" -#include "theory/arith/arith_ite_utils.h" - -#include "theory/arith/arith_utilities.h" +#include "theory/arith/constraint.h" +#include "theory/arith/cut_log.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/delta_rational.h" +#include "theory/arith/dio_solver.h" +#include "theory/arith/linear_equality.h" +#include "theory/arith/matrix.h" #include "theory/arith/matrix.h" - -#include "theory/arith/arith_rewriter.h" -#include "theory/arith/constraint.h" -#include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" -#include "theory/theory_model.h" - -#include "theory/arith/options.h" -#include "theory/quantifiers/options.h" - - +#include "theory/arith/partial_model.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/simplex.h" +#include "theory/arith/theory_arith.h" +#include "theory/ite_utilities.h" #include "theory/quantifiers/bounded_integers.h" - -#include <stdint.h> - -#include <vector> -#include <map> -#include <queue> +#include "theory/rewriter.h" +#include "theory/theory_model.h" +#include "theory/valuation.h" +#include "util/dense_map.h" +#include "util/integer.h" +#include "util/rational.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 4c539c60d..0c2a704e8 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -17,70 +17,56 @@ #pragma once -#include "theory/arith/theory_arith_private_forward.h" - -#include "expr/node.h" -#include "expr/kind.h" -#include "expr/metakind.h" -#include "expr/node_builder.h" +#include <map> +#include <queue> +#include <stdint.h> +#include <vector> -#include "context/context.h" -#include "context/cdlist.h" #include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" +#include "context/cdlist.h" #include "context/cdqueue.h" - -#include "theory/valuation.h" -#include "theory/rewriter.h" - -#include "util/rational.h" -#include "util/integer.h" -#include "util/boolean_simplification.h" -#include "util/dense_map.h" -#include "util/statistics_registry.h" -#include "util/result.h" - +#include "context/context.h" +#include "expr/kind.h" +#include "expr/metakind.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/result.h" +#include "expr/statistics_registry.h" +#include "options/arith_options.h" #include "smt/logic_exception.h" - - - -#include "theory/arith/arithvar.h" -#include "theory/arith/delta_rational.h" -#include "theory/arith/matrix.h" +#include "smt_util/boolean_simplification.h" +#include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_rewriter.h" -#include "theory/arith/partial_model.h" -#include "theory/arith/linear_equality.h" #include "theory/arith/arith_static_learner.h" -#include "theory/arith/dio_solver.h" -#include "theory/arith/congruence_manager.h" - -#include "theory/arith/simplex.h" -#include "theory/arith/dual_simplex.h" -#include "theory/arith/fc_simplex.h" -#include "theory/arith/soi_simplex.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/arithvar.h" #include "theory/arith/attempt_solution_simplex.h" - +#include "theory/arith/congruence_manager.h" +#include "theory/arith/constraint.h" #include "theory/arith/constraint.h" - -#include "theory/arith/arith_utilities.h" #include "theory/arith/delta_rational.h" +#include "theory/arith/delta_rational.h" +#include "theory/arith/dio_solver.h" +#include "theory/arith/dual_simplex.h" +#include "theory/arith/fc_simplex.h" #include "theory/arith/infer_bounds.h" -#include "theory/arith/partial_model.h" +#include "theory/arith/linear_equality.h" +#include "theory/arith/matrix.h" #include "theory/arith/matrix.h" - -#include "theory/arith/arith_rewriter.h" -#include "theory/arith/constraint.h" -#include "theory/arith/theory_arith.h" #include "theory/arith/normal_form.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/partial_model.h" +#include "theory/arith/simplex.h" +#include "theory/arith/soi_simplex.h" +#include "theory/arith/theory_arith.h" +#include "theory/arith/theory_arith_private_forward.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" - -#include "theory/arith/options.h" - -#include <stdint.h> - -#include <vector> -#include <map> -#include <queue> +#include "theory/valuation.h" +#include "util/dense_map.h" +#include "util/integer.h" +#include "util/rational.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h index f661e18d3..c4501fc43 100644 --- a/src/theory/arith/type_enumerator.h +++ b/src/theory/arith/type_enumerator.h @@ -19,11 +19,11 @@ #ifndef __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H #define __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H +#include "expr/kind.h" +#include "expr/type_node.h" +#include "theory/type_enumerator.h" #include "util/integer.h" #include "util/rational.h" -#include "theory/type_enumerator.h" -#include "expr/type_node.h" -#include "expr/kind.h" namespace CVC4 { namespace theory { |