diff options
Diffstat (limited to 'src/theory')
195 files changed, 1693 insertions, 3409 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 { diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index f3c6385e5..d9f77d50f 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -18,17 +18,18 @@ #ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H #define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H -#include "util/backtrackable.h" -#include "context/cdlist.h" -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "util/statistics_registry.h" -#include "util/ntuple.h" #include <ext/hash_set> #include <ext/hash_map> #include <iostream> #include <map> +#include "context/backtrackable.h" +#include "context/cdlist.h" +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "expr/statistics_registry.h" +#include "util/ntuple.h" + namespace CVC4 { namespace theory { namespace arrays { diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index c18492a58..d5f313ca1 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -35,7 +35,7 @@ operator STORE 3 "array store; first parameter is an array term, second is the s constant STORE_ALL \ ::CVC4::ArrayStoreAll \ ::CVC4::ArrayStoreAllHashFunction \ - "util/array_store_all.h" \ + "expr/array_store_all.h" \ "array store-all; payload is an instance of the CVC4::ArrayStoreAll class (this is not supported by arrays decision procedure yet, but it is used for returned array models)" # used internally by array theory diff --git a/src/theory/arrays/options b/src/theory/arrays/options deleted file mode 100644 index 8ed80c1f1..000000000 --- a/src/theory/arrays/options +++ /dev/null @@ -1,32 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module ARRAYS "theory/arrays/options.h" Arrays theory - -option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-write - turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper) - -option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write - turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination) - -option arraysModelBased --arrays-model-based bool :default false :read-write - turn on model-based array solver - -option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write - turn on eager index splitting for generated array lemmas - -option arraysEagerLemmas --arrays-eager-lemmas bool :default false :read-write - turn on eager lemma generation for arrays - -option arraysConfig --arrays-config int :default 0 :read-write - set different array option configurations - for developers only - -option arraysReduceSharing --arrays-reduce-sharing bool :default false :read-write - use model information to reduce size of care graph for arrays - -option arraysPropagate --arrays-prop int :default 2 :read-write - propagation effort for arrays: 0 is none, 1 is some, 2 is full - -endmodule diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp index 1743e3b30..0d04ce097 100644 --- a/src/theory/arrays/static_fact_manager.cpp +++ b/src/theory/arrays/static_fact_manager.cpp @@ -18,9 +18,9 @@ #include <iostream> -#include "theory/arrays/static_fact_manager.h" -#include "util/cvc4_assert.h" +#include "base/cvc4_assert.h" #include "expr/node.h" +#include "theory/arrays/static_fact_manager.h" using namespace std; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index d872ab42c..5af7f02db 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -14,17 +14,18 @@ ** Implementation of the theory of arrays. **/ - #include "theory/arrays/theory_arrays.h" -#include "theory/valuation.h" -#include "expr/kind.h" + #include <map> + +#include "expr/kind.h" +#include "options/arrays_options.h" +#include "options/smt_options.h" +#include "smt/logic_exception.h" +#include "smt_util/command.h" #include "theory/rewriter.h" -#include "expr/command.h" #include "theory/theory_model.h" -#include "theory/arrays/options.h" -#include "smt/options.h" -#include "smt/logic_exception.h" +#include "theory/valuation.h" using namespace std; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index b2e039912..717c654d2 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -19,13 +19,13 @@ #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_H -#include "theory/theory.h" -#include "theory/arrays/array_info.h" -#include "util/statistics_registry.h" -#include "theory/uf/equality_engine.h" #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdqueue.h" +#include "expr/statistics_registry.h" +#include "theory/arrays/array_info.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp index 9e6978c92..3f71b350e 100644 --- a/src/theory/arrays/union_find.cpp +++ b/src/theory/arrays/union_find.cpp @@ -18,9 +18,9 @@ #include <iostream> -#include "theory/arrays/union_find.h" -#include "util/cvc4_assert.h" +#include "base/cvc4_assert.h" #include "expr/node.h" +#include "theory/arrays/union_find.h" using namespace std; diff --git a/src/theory/booleans/boolean_term_conversion_mode.cpp b/src/theory/booleans/boolean_term_conversion_mode.cpp deleted file mode 100644 index b8647eb3c..000000000 --- a/src/theory/booleans/boolean_term_conversion_mode.cpp +++ /dev/null @@ -1,41 +0,0 @@ -/********************* */ -/*! \file boolean_term_conversion_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 <iostream> -#include "theory/booleans/boolean_term_conversion_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) { - switch(mode) { - case theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: - out << "BOOLEAN_TERM_CONVERT_TO_BITVECTORS"; - break; - case theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES: - out << "BOOLEAN_TERM_CONVERT_TO_DATATYPES"; - break; - case theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE: - out << "BOOLEAN_TERM_CONVERT_NATIVE"; - break; - default: - out << "BooleanTermConversionMode!UNKNOWN"; - } - - return out; -} - -}/* CVC4 namespace */ diff --git a/src/theory/booleans/boolean_term_conversion_mode.h b/src/theory/booleans/boolean_term_conversion_mode.h deleted file mode 100644 index 5671dea13..000000000 --- a/src/theory/booleans/boolean_term_conversion_mode.h +++ /dev/null @@ -1,53 +0,0 @@ -/********************* */ -/*! \file boolean_term_conversion_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_private.h" - -#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H -#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H - -#include <iostream> - -namespace CVC4 { -namespace theory { -namespace booleans { - -typedef enum { - /** - * Convert Boolean terms to bitvectors of size 1. - */ - BOOLEAN_TERM_CONVERT_TO_BITVECTORS, - /** - * Convert Boolean terms to enumerations in the Datatypes theory. - */ - BOOLEAN_TERM_CONVERT_TO_DATATYPES, - /** - * Convert Boolean terms to enumerations in the Datatypes theory IF - * used in a datatypes context, otherwise to a bitvector of size 1. - */ - BOOLEAN_TERM_CONVERT_NATIVE - -} BooleanTermConversionMode; - -}/* CVC4::theory::booleans namespace */ -}/* CVC4::theory namespace */ - -std::ostream& operator<<(std::ostream& out, theory::booleans::BooleanTermConversionMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */ diff --git a/src/theory/booleans/options b/src/theory/booleans/options deleted file mode 100644 index 6c571f30e..000000000 --- a/src/theory/booleans/options +++ /dev/null @@ -1,11 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module BOOLEANS "theory/booleans/options.h" Boolean theory - -option booleanTermConversionMode boolean-term-conversion-mode --boolean-term-conversion-mode=MODE CVC4::theory::booleans::BooleanTermConversionMode :default CVC4::theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS :include "theory/booleans/boolean_term_conversion_mode.h" :handler CVC4::theory::booleans::stringToBooleanTermConversionMode :handler-include "theory/booleans/options_handlers.h" - policy for converting Boolean terms - -endmodule diff --git a/src/theory/booleans/options_handlers.h b/src/theory/booleans/options_handlers.h deleted file mode 100644 index 8cad689eb..000000000 --- a/src/theory/booleans/options_handlers.h +++ /dev/null @@ -1,65 +0,0 @@ -/********************* */ -/*! \file options_handlers.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_private.h" - -#ifndef __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H - -#include <string> - -namespace CVC4 { -namespace theory { -namespace booleans { - -static const std::string booleanTermConversionModeHelp = "\ -Boolean term conversion modes currently supported by the\n\ ---boolean-term-conversion-mode option:\n\ -\n\ -bitvectors [default]\n\ -+ Boolean terms are converted to bitvectors of size 1.\n\ -\n\ -datatypes\n\ -+ Boolean terms are converted to enumerations in the Datatype theory.\n\ -\n\ -native\n\ -+ Boolean terms are converted in a \"natural\" way depending on where they\n\ - are used. If in a datatype context, they are converted to an enumeration.\n\ - Elsewhere, they are converted to a bitvector of size 1.\n\ -"; - -inline BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "bitvectors") { - return BOOLEAN_TERM_CONVERT_TO_BITVECTORS; - } else if(optarg == "datatypes") { - return BOOLEAN_TERM_CONVERT_TO_DATATYPES; - } else if(optarg == "native") { - return BOOLEAN_TERM_CONVERT_NATIVE; - } else if(optarg == "help") { - puts(booleanTermConversionModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") + - optarg + "'. Try --boolean-term-conversion-mode help."); - } -} - -}/* CVC4::theory::booleans namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__BOOLEANS__OPTIONS_HANDLERS_H */ diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 8e1661e28..a286f1605 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -18,7 +18,7 @@ #include "theory/booleans/theory_bool.h" #include "theory/booleans/circuit_propagator.h" #include "theory/valuation.h" -#include "util/boolean_simplification.h" +#include "smt_util/boolean_simplification.h" #include "theory/substitutions.h" #include <vector> diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 44474c18a..c0f955861 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -266,7 +266,7 @@ well-founded SORT_TYPE \ constant UNINTERPRETED_CONSTANT \ ::CVC4::UninterpretedConstant \ ::CVC4::UninterpretedConstantHashFunction \ - "util/uninterpreted_constant.h" \ + "expr/uninterpreted_constant.h" \ "the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::UninterpretedConstant class (used in models)" typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule enumerator SORT_TYPE \ @@ -306,7 +306,7 @@ parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjuct constant CHAIN_OP \ ::CVC4::Chain \ ::CVC4::ChainHashFunction \ - "util/chain.h" \ + "expr/chain.h" \ "the chained operator; payload is an instance of the CVC4::Chain class" constant TYPE_CONSTANT \ @@ -339,7 +339,7 @@ typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule constant SUBTYPE_TYPE \ ::CVC4::Predicate \ ::CVC4::PredicateHashFunction \ - "util/predicate.h" \ + "expr/predicate.h" \ "predicate subtype; payload is an instance of the CVC4::Predicate class" cardinality SUBTYPE_TYPE \ "::CVC4::theory::builtin::SubtypeProperties::computeCardinality(%TYPE%)" \ diff --git a/src/theory/builtin/options b/src/theory/builtin/options deleted file mode 100644 index 699f361c9..000000000 --- a/src/theory/builtin/options +++ /dev/null @@ -1,8 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module BUILTIN "theory/builtin/options.h" Builtin theory - -endmodule diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index 516d6a06b..e91c7e411 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -16,7 +16,8 @@ **/ #include "theory/builtin/theory_builtin_rewriter.h" -#include "util/chain.h" + +#include "expr/chain.h" using namespace std; diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index c9585c46f..635cf7dc7 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -19,11 +19,11 @@ #ifndef __CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H #define __CVC4__THEORY__BUILTIN__TYPE_ENUMERATOR_H -#include "util/integer.h" -#include "util/uninterpreted_constant.h" -#include "theory/type_enumerator.h" -#include "expr/type_node.h" #include "expr/kind.h" +#include "expr/type_node.h" +#include "expr/uninterpreted_constant.h" +#include "theory/type_enumerator.h" +#include "util/integer.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index c414ac749..f05520306 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -12,12 +12,13 @@ ** [[ Add lengthier description here ]] ** \todo document this file **/ - #include "theory/bv/abstraction.h" + +#include "options/bv_options.h" +#include "smt_util/dump.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" -#include "theory/bv/options.h" -#include "util/dump.h" + using namespace CVC4; using namespace CVC4::theory; @@ -28,10 +29,10 @@ using namespace std; using namespace CVC4::theory::bv::utils; bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) { - Debug("bv-abstraction") << "AbstractionModule::applyAbstraction\n"; + Debug("bv-abstraction") << "AbstractionModule::applyAbstraction\n"; TimerStat::CodeTimer abstractionTimer(d_statistics.d_abstractionTime); - + for (unsigned i = 0; i < assertions.size(); ++i) { if (assertions[i].getKind() == kind::OR) { for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) { diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h index 2e86c834d..6b4d5a7dc 100644 --- a/src/theory/bv/abstraction.h +++ b/src/theory/bv/abstraction.h @@ -14,22 +14,22 @@ ** Bitvector theory. **/ +#include "cvc4_private.h" #ifndef __CVC4__THEORY__BV__ABSTRACTION_H #define __CVC4__THEORY__BV__ABSTRACTION_H -#include "cvc4_private.h" #include <ext/hash_map> #include <ext/hash_set> + #include "expr/node.h" +#include "expr/statistics_registry.h" #include "theory/substitutions.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { namespace bv { - typedef std::vector<TNode> ArgsVec; class AbstractionModule { diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp index 6270995ef..f07bd49f7 100644 --- a/src/theory/bv/aig_bitblaster.cpp +++ b/src/theory/bv/aig_bitblaster.cpp @@ -14,11 +14,11 @@ ** Bitblaster for the lazy bv solver. **/ -#include "cvc4_private.h" #include "bitblaster_template.h" +#include "cvc4_private.h" +#include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" -#include "theory/bv/options.h" #ifdef CVC4_USE_ABC diff --git a/src/theory/bv/bitblast_mode.cpp b/src/theory/bv/bitblast_mode.cpp deleted file mode 100644 index 51c0290af..000000000 --- a/src/theory/bv/bitblast_mode.cpp +++ /dev/null @@ -1,55 +0,0 @@ -/********************* */ -/*! \file bitblast_mode.cpp - ** \verbatim - ** Original author: Liana Hadarean - ** 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 Bitblast modes for bit-vector solver. - ** - ** Bitblast modes for bit-vector solver. - **/ - -#include "theory/bv/bitblast_mode.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) { - switch(mode) { - case theory::bv::BITBLAST_MODE_LAZY: - out << "BITBLAST_MODE_LAZY"; - break; - case theory::bv::BITBLAST_MODE_EAGER: - out << "BITBLAST_MODE_EAGER"; - break; - default: - out << "BitblastMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) { - switch(mode) { - case theory::bv::BITVECTOR_SLICER_ON: - out << "BITVECTOR_SLICER_ON"; - break; - case theory::bv::BITVECTOR_SLICER_OFF: - out << "BITVECTOR_SLICER_OFF"; - break; - case theory::bv::BITVECTOR_SLICER_AUTO: - out << "BITVECTOR_SLICER_AUTO"; - break; - default: - out << "BvSlicerMode:UNKNOWN![" << unsigned(mode) << "]"; - } - - return out; -} - - -}/* CVC4 namespace */ diff --git a/src/theory/bv/bitblast_mode.h b/src/theory/bv/bitblast_mode.h deleted file mode 100644 index 89ecdc381..000000000 --- a/src/theory/bv/bitblast_mode.h +++ /dev/null @@ -1,72 +0,0 @@ -/********************* */ -/*! \file bitblast_mode.h - ** \verbatim - ** Original author: Liana Hadarean - ** 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 Bitblasting modes for bit-vector solver. - ** - ** Bitblasting modes for bit-vector solver. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H -#define __CVC4__THEORY__BV__BITBLAST_MODE_H - -#include <iostream> - -namespace CVC4 { -namespace theory { -namespace bv { - -/** Enumeration of bit-blasting modes */ -enum BitblastMode { - - /** - * Lazy bit-blasting that separates boolean reasoning - * from term reasoning. - */ - BITBLAST_MODE_LAZY, - - /** - * Bit-blast eagerly to the bit-vector SAT solver. - */ - BITBLAST_MODE_EAGER -};/* enum BitblastMode */ - -/** Enumeration of bit-vector equality slicer mode */ -enum BvSlicerMode { - - /** - * Force the slicer on. - */ - BITVECTOR_SLICER_ON, - - /** - * Slicer off. - */ - BITVECTOR_SLICER_OFF, - - /** - * Auto enable slicer if problem has only equalities. - */ - BITVECTOR_SLICER_AUTO - -};/* enum BvSlicerMode */ - - -}/* CVC4::theory::bv namespace */ -}/* CVC4::theory namespace */ - -std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */ diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index d42c4a8c9..b93d0561e 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -23,12 +23,13 @@ #include "expr/node.h" #include <vector> #include <ext/hash_map> + #include "context/cdhashmap.h" #include "bitblast_strategies_template.h" +#include "expr/resource_manager.h" #include "prop/sat_solver.h" #include "theory/valuation.h" #include "theory/theory_registrar.h" -#include "util/resource_manager.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 0c087ddb9..66b1c4182 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -14,9 +14,9 @@ ** Eager bit-blasting solver. **/ -#include "theory/bv/bv_eager_solver.h" +#include "options/bv_options.h" #include "theory/bv/bitblaster_template.h" -#include "theory/bv/options.h" +#include "theory/bv/bv_eager_solver.h" using namespace std; using namespace CVC4; diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h index 01d772cb9..261a0b1c4 100644 --- a/src/theory/bv/bv_quick_check.h +++ b/src/theory/bv/bv_quick_check.h @@ -22,10 +22,10 @@ #include <vector> #include <ext/hash_map> -#include "expr/node.h" #include "context/cdo.h" +#include "expr/node.h" +#include "expr/statistics_registry.h" #include "prop/sat_solver_types.h" -#include "util/statistics_registry.h" #include "theory/bv/theory_bv_utils.h" namespace CVC4 { diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index e6e3120f5..4531be040 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -14,14 +14,13 @@ ** Algebraic solver. **/ -#include "util/boolean_simplification.h" -#include "theory/theory_model.h" - -#include "theory/bv/options.h" -#include "theory/bv/theory_bv.h" -#include "theory/bv/bv_subtheory_algebraic.h" +#include "options/bv_options.h" +#include "smt_util/boolean_simplification.h" #include "theory/bv/bv_quick_check.h" +#include "theory/bv/bv_subtheory_algebraic.h" +#include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/theory_model.h" using namespace std; diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp index 7e3ed46c8..1d0342c08 100644 --- a/src/theory/bv/bv_subtheory_bitblast.cpp +++ b/src/theory/bv/bv_subtheory_bitblast.cpp @@ -14,24 +14,24 @@ ** Algebraic solver. **/ +#include "decision/decision_attributes.h" +#include "options/decision_options.h" +#include "options/bv_options.h" +#include "theory/bv/abstraction.h" +#include "theory/bv/bitblaster_template.h" +#include "theory/bv/bv_quick_check.h" #include "theory/bv/bv_subtheory_bitblast.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/bv/bitblaster_template.h" -#include "theory/bv/bv_quick_check.h" -#include "theory/bv/options.h" -#include "theory/bv/abstraction.h" -#include "theory/decision_attributes.h" -#include "decision/options.h" - using namespace std; -using namespace CVC4; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; using namespace CVC4::theory::bv::utils; +namespace CVC4 { +namespace theory { +namespace bv { + BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv) : SubtheorySolver(c, bv), d_bitblaster(new TLazyBitblaster(c, bv, "lazy")), @@ -78,8 +78,8 @@ void BitblastSolver::preRegister(TNode node) { CodeTimer weightComputationTime(d_bv->d_statistics.d_weightComputationTimer); d_bitblastQueue.push_back(node); if ((options::decisionUseWeight() || options::decisionThreshold() != 0) && - !node.hasAttribute(theory::DecisionWeightAttr())) { - node.setAttribute(theory::DecisionWeightAttr(),computeAtomWeight(node)); + !node.hasAttribute(decision::DecisionWeightAttr())) { + node.setAttribute(decision::DecisionWeightAttr(),computeAtomWeight(node)); } } } @@ -277,3 +277,7 @@ void BitblastSolver::setConflict(TNode conflict) { } d_bv->setConflict(final_conflict); } + +}/* namespace CVC4::theory::bv */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp index 6ae0ffb71..ef4d24e82 100644 --- a/src/theory/bv/bv_subtheory_core.cpp +++ b/src/theory/bv/bv_subtheory_core.cpp @@ -16,12 +16,12 @@ #include "theory/bv/bv_subtheory_core.h" +#include "options/bv_options.h" +#include "options/smt_options.h" +#include "theory/bv/slicer.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/bv/slicer.h" #include "theory/theory_model.h" -#include "theory/bv/options.h" -#include "smt/options.h" using namespace std; using namespace CVC4; diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp index 55dcbb03a..054e43b7c 100644 --- a/src/theory/bv/bv_subtheory_inequality.cpp +++ b/src/theory/bv/bv_subtheory_inequality.cpp @@ -15,10 +15,11 @@ **/ #include "theory/bv/bv_subtheory_inequality.h" + +#include "options/smt_options.h" #include "theory/bv/theory_bv.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" -#include "smt/options.h" using namespace std; using namespace CVC4; @@ -232,4 +233,3 @@ InequalitySolver::Statistics::Statistics() InequalitySolver::Statistics::~Statistics() { StatisticsRegistry::unregisterStat(&d_numCallstoCheck); } - diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp index 06a1d4a44..00e6f9ff8 100644 --- a/src/theory/bv/bv_to_bool.cpp +++ b/src/theory/bv/bv_to_bool.cpp @@ -13,11 +13,10 @@ ** ** Preprocessing pass that lifts bit-vectors of size 1 to booleans. **/ - - -#include "util/node_visitor.h" #include "theory/bv/bv_to_bool.h" +#include "smt_util/node_visitor.h" + using namespace std; using namespace CVC4; using namespace CVC4::theory; diff --git a/src/theory/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h index b266b591b..46b2d5c6e 100644 --- a/src/theory/bv/bv_to_bool.h +++ b/src/theory/bv/bv_to_bool.h @@ -15,12 +15,13 @@ **/ #include "cvc4_private.h" -#include "theory/bv/theory_bv_utils.h" -#include "util/statistics_registry.h" #ifndef __CVC4__THEORY__BV__BV_TO_BOOL_H #define __CVC4__THEORY__BV__BV_TO_BOOL_H +#include "expr/statistics_registry.h" +#include "theory/bv/theory_bv_utils.h" + namespace CVC4 { namespace theory { namespace bv { diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp index 3f076bd4c..ec2bfd9c0 100644 --- a/src/theory/bv/eager_bitblaster.cpp +++ b/src/theory/bv/eager_bitblaster.cpp @@ -9,27 +9,31 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief + ** \brief ** - ** Bitblaster for the eager bv solver. + ** Bitblaster for the eager bv solver. **/ #include "cvc4_private.h" -#include "theory/bv/bitblaster_template.h" -#include "theory/bv/options.h" -#include "theory/theory_model.h" -#include "theory/bv/theory_bv.h" +#include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" +#include "theory/bv/bitblaster_template.h" +#include "theory/bv/theory_bv.h" +#include "theory/theory_model.h" using namespace CVC4; using namespace CVC4::theory; -using namespace CVC4::theory::bv; +using namespace CVC4::theory::bv; + +namespace CVC4 { +namespace theory { +namespace bv { void BitblastingRegistrar::preRegister(Node n) { - d_bitblaster->bbAtom(n); + d_bitblaster->bbAtom(n); }; EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) @@ -38,12 +42,12 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv) , d_bbAtoms() , d_variables() { - d_bitblastingRegistrar = new BitblastingRegistrar(this); + d_bitblastingRegistrar = new BitblastingRegistrar(this); d_nullContext = new context::Context(); d_satSolver = prop::SatSolverFactory::createMinisat(d_nullContext, "EagerBitblaster"); d_cnfStream = new prop::TseitinCnfStream(d_satSolver, d_bitblastingRegistrar, d_nullContext); - + MinisatEmptyNotify* notify = new MinisatEmptyNotify(); d_satSolver->setNotify(notify); } @@ -68,7 +72,7 @@ void EagerBitblaster::bbFormula(TNode node) { void EagerBitblaster::bbAtom(TNode node) { node = node.getKind() == kind::NOT? node[0] : node; if (node.getKind() == kind::BITVECTOR_BITOF) - return; + return; if (hasBBAtom(node)) { return; } @@ -83,18 +87,18 @@ void EagerBitblaster::bbAtom(TNode node) { // asserting that the atom is true iff the definition holds Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb); - AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); + AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); storeBBAtom(node, atom_definition); d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null()); } void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) { // no need to store the definition for the lazy bit-blaster - d_bbAtoms.insert(atom); + d_bbAtoms.insert(atom); } bool EagerBitblaster::hasBBAtom(TNode atom) const { - return d_bbAtoms.find(atom) != d_bbAtoms.end(); + return d_bbAtoms.find(atom) != d_bbAtoms.end(); } void EagerBitblaster::bbTerm(TNode node, Bits& bits) { @@ -161,7 +165,7 @@ Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) { if (!hasBBTerm(a)) { return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node(); } - + Bits bits; getBBTerm(a, bits); Integer value(0); @@ -191,9 +195,9 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { (var.isVar() && var.getType().isBoolean())) { // only shared terms could not have been bit-blasted Assert (hasBBTerm(var) || isSharedTerm(var)); - + Node const_value = getModelFromSatSolver(var, fullModel); - + if(const_value != Node()) { Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= " << var << " " @@ -207,3 +211,7 @@ void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) { bool EagerBitblaster::isSharedTerm(TNode node) { return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); } + +} /* namespace CVC4::theory::bv; */ +} /* namespace CVC4::theory; */ +} /* namespace CVC4; */ diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp index 59ecc7385..3c2b4ed78 100644 --- a/src/theory/bv/lazy_bitblaster.cpp +++ b/src/theory/bv/lazy_bitblaster.cpp @@ -14,17 +14,17 @@ ** Bitblaster for the lazy bv solver. **/ -#include "cvc4_private.h" #include "bitblaster_template.h" -#include "theory_bv_utils.h" -#include "theory/rewriter.h" +#include "cvc4_private.h" +#include "options/bv_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" +#include "theory/bv/abstraction.h" #include "theory/bv/theory_bv.h" -#include "theory/bv/options.h" +#include "theory/rewriter.h" #include "theory/theory_model.h" -#include "theory/bv/abstraction.h" +#include "theory_bv_utils.h" using namespace CVC4; using namespace CVC4::theory; diff --git a/src/theory/bv/options b/src/theory/bv/options deleted file mode 100644 index eba4608d2..000000000 --- a/src/theory/bv/options +++ /dev/null @@ -1,69 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module BV "theory/bv/options.h" Bitvector theory - -# Option to set the bit-blasting mode (lazy, eager) - -option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :handler CVC4::theory::bv::stringToBitblastMode :default CVC4::theory::bv::BITBLAST_MODE_LAZY :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h" - choose bitblasting mode, see --bitblast=help - -# Options for eager bit-blasting - -option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild CVC4::theory::bv::setBitblastAig :predicate-include "theory/bv/options_handlers.h" :read-write - bitblast by first converting to AIG (implies --bitblast=eager) -expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig :link-smt bitblast-aig - abc command to run AIG simplifications (implies --bitblast-aig, default is "balance;drw") - -# Options for lazy bit-blasting - -option bitvectorPropagate --bv-propagate bool :default true :read-write :link --bitblast=lazy - use bit-vector propagation in the bit-blaster - -option bitvectorEqualitySolver --bv-eq-solver bool :default true :read-write :link --bitblast=lazy - use the equality engine for the bit-vector theory (only if --bitblast=lazy) - -option bitvectorEqualitySlicer --bv-eq-slicer=MODE CVC4::theory::bv::BvSlicerMode :handler CVC4::theory::bv::stringToBvSlicerMode :default CVC4::theory::bv::BITVECTOR_SLICER_OFF :read-write :include "theory/bv/bitblast_mode.h" :handler-include "theory/bv/options_handlers.h" :read-write :link --bv-eq-solver - turn on the slicing equality solver for the bit-vector theory (only if --bitblast=lazy) - -option bitvectorInequalitySolver --bv-inequality-solver bool :default true :read-write :link --bitblast=lazy - turn on the inequality solver for the bit-vector theory (only if --bitblast=lazy) - -option bitvectorAlgebraicSolver --bv-algebraic-solver bool :default true :read-write :link --bitblast=lazy - turn on the algebraic solver for the bit-vector theory (only if --bitblast=lazy) - -expert-option bitvectorAlgebraicBudget --bv-algebraic-budget unsigned :default 1500 :read-write :link --bv-algebraic-solver - the budget allowed for the algebraic solver in number of SAT conflicts - -# General options - -option bitvectorToBool --bv-to-bool bool :default false :read-write - lift bit-vectors of size 1 to booleans when possible - -option bitvectorDivByZeroConst --bv-div-zero-const bool :default false :read-write - always return -1 on division by zero - -expert-option bvExtractArithRewrite --bv-extract-arith bool :default false :read-write - enable rewrite pushing extract [i:0] over arithmetic operations (can blow up) - -expert-option bvAbstraction --bv-abstraction bool :default false :read-write - mcm benchmark abstraction - -expert-option skolemizeArguments --bv-skolemize bool :default false :read-write - skolemize arguments for bv abstraction (only does something if --bv-abstraction is on) - -expert-option bvNumFunc --bv-num-func=NUM unsigned :default 1 - number of function symbols in conflicts that are generalized - -expert-option bvEagerExplanations --bv-eager-explanations bool :default false :read-write - compute bit-blasting propagation explanations eagerly - -expert-option bitvectorQuickXplain --bv-quick-xplain bool :default false - minimize bv conflicts using the QuickXplain algorithm - -expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false - introduce bitvector powers of two as a preprocessing pass - -endmodule diff --git a/src/theory/bv/options_handlers.h b/src/theory/bv/options_handlers.h deleted file mode 100644 index a7a7101d2..000000000 --- a/src/theory/bv/options_handlers.h +++ /dev/null @@ -1,160 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Liana Hadarean - ** 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 Custom handlers and predicates for TheoryBV options - ** - ** Custom handlers and predicates for TheoryBV options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__BV__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__BV__OPTIONS_HANDLERS_H - -#include "theory/bv/bitblast_mode.h" -#include "main/options.h" - -namespace CVC4 { -namespace theory { -namespace bv { - -inline void abcEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) { -#ifndef CVC4_USE_ABC - if(value) { - std::stringstream ss; - ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support"; - throw OptionException(ss.str()); - } -#endif /* CVC4_USE_ABC */ -} - -inline void abcEnabledBuild(std::string option, std::string value, SmtEngine* smt) throw(OptionException) { -#ifndef CVC4_USE_ABC - if(!value.empty()) { - std::stringstream ss; - ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support"; - throw OptionException(ss.str()); - } -#endif /* CVC4_USE_ABC */ -} - -static const std::string bitblastingModeHelp = "\ -Bit-blasting modes currently supported by the --bitblast option:\n\ -\n\ -lazy (default)\n\ -+ Separate boolean structure and term reasoning betwen the core\n\ - SAT solver and the bv SAT solver\n\ -\n\ -eager\n\ -+ Bitblast eagerly to bv SAT solver\n\ -"; - -inline BitblastMode stringToBitblastMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "lazy") { - if (!options::bitvectorPropagate.wasSetByUser()) { - options::bitvectorPropagate.set(true); - } - if (!options::bitvectorEqualitySolver.wasSetByUser()) { - options::bitvectorEqualitySolver.set(true); - } - if (!options::bitvectorEqualitySlicer.wasSetByUser()) { - if (options::incrementalSolving() || - options::produceModels()) { - options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_OFF); - } else { - options::bitvectorEqualitySlicer.set(BITVECTOR_SLICER_AUTO); - } - } - - if (!options::bitvectorInequalitySolver.wasSetByUser()) { - options::bitvectorInequalitySolver.set(true); - } - if (!options::bitvectorAlgebraicSolver.wasSetByUser()) { - options::bitvectorAlgebraicSolver.set(true); - } - return BITBLAST_MODE_LAZY; - } else if(optarg == "eager") { - - if (options::incrementalSolving() && - options::incrementalSolving.wasSetByUser()) { - throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\ - Try --bitblast=lazy")); - } - - if (!options::bitvectorToBool.wasSetByUser()) { - options::bitvectorToBool.set(true); - } - - if (!options::bvAbstraction.wasSetByUser() && - !options::skolemizeArguments.wasSetByUser()) { - options::bvAbstraction.set(true); - options::skolemizeArguments.set(true); - } - return BITBLAST_MODE_EAGER; - } else if(optarg == "help") { - puts(bitblastingModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --bitblast: `") + - optarg + "'. Try --bitblast=help."); - } -} - -static const std::string bvSlicerModeHelp = "\ -Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\ -\n\ -auto (default)\n\ -+ Turn slicer on if input has only equalities over core symbols\n\ -\n\ -on\n\ -+ Turn slicer on\n\ -\n\ -off\n\ -+ Turn slicer off\n\ -"; - -inline BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - - if(optarg == "auto") { - return BITVECTOR_SLICER_AUTO; - } else if(optarg == "on") { - return BITVECTOR_SLICER_ON; - } else if(optarg == "off") { - return BITVECTOR_SLICER_OFF; - } else if(optarg == "help") { - puts(bitblastingModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --bv-eq-slicer: `") + - optarg + "'. Try --bv-eq-slicer=help."); - } -} - -inline void setBitblastAig(std::string option, bool arg, SmtEngine* smt) throw(OptionException) { - if(arg) { - if(options::bitblastMode.wasSetByUser()) { - if(options::bitblastMode() != BITBLAST_MODE_EAGER) { - throw OptionException("bitblast-aig must be used with eager bitblaster"); - } - } else { - options::bitblastMode.set(stringToBitblastMode("", "eager", smt)); - } - if(!options::bitvectorAigSimplifications.wasSetByUser()) { - options::bitvectorAigSimplifications.set("balance;drw"); - } - } -} - -}/* CVC4::theory::bv namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__BV__OPTIONS_HANDLERS_H */ diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index a7587bedf..d31ff50d1 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -14,10 +14,11 @@ ** Bitvector theory. **/ +#include "options/bv_options.h" #include "theory/bv/slicer.h" #include "theory/bv/theory_bv_utils.h" #include "theory/rewriter.h" -#include "theory/bv/options.h" + using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::bv; diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h index 7b55054bc..5ecc2a788 100644 --- a/src/theory/bv/slicer.h +++ b/src/theory/bv/slicer.h @@ -16,17 +16,19 @@ #include "cvc4_private.h" +#include <math.h> #include <vector> #include <list> #include <ext/hash_map> -#include <math.h> -#include "util/bitvector.h" -#include "util/statistics_registry.h" -#include "util/index.h" #include "expr/node.h" +#include "expr/statistics_registry.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" +#include "util/index.h" + + #ifndef __CVC4__THEORY__BV__SLICER_BV_H #define __CVC4__THEORY__BV__SLICER_BV_H diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 95a483d34..4039fceec 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -11,24 +11,25 @@ ** ** [[ Add lengthier description here ]] ** \todo document this file -**/ + **/ -#include "smt/options.h" #include "theory/bv/theory_bv.h" -#include "theory/bv/theory_bv_utils.h" + +#include "options/bv_options.h" +#include "options/smt_options.h" +#include "theory/bv/abstraction.h" +#include "theory/bv/bv_eager_solver.h" +#include "theory/bv/bv_subtheory_algebraic.h" +#include "theory/bv/bv_subtheory_bitblast.h" +#include "theory/bv/bv_subtheory_core.h" +#include "theory/bv/bv_subtheory_inequality.h" #include "theory/bv/slicer.h" -#include "theory/valuation.h" -#include "theory/bv/options.h" #include "theory/bv/theory_bv_rewrite_rules_normalization.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" -#include "theory/bv/bv_subtheory_core.h" -#include "theory/bv/bv_subtheory_inequality.h" -#include "theory/bv/bv_subtheory_algebraic.h" -#include "theory/bv/bv_subtheory_bitblast.h" -#include "theory/bv/bv_eager_solver.h" #include "theory/bv/theory_bv_rewriter.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" -#include "theory/bv/abstraction.h" +#include "theory/valuation.h" using namespace CVC4; using namespace CVC4::theory; diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 193de55db..4b3649a86 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -14,18 +14,19 @@ ** Bitvector theory. **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__BV__THEORY_BV_H #define __CVC4__THEORY__BV__THEORY_BV_H -#include "cvc4_private.h" -#include "theory/theory.h" -#include "context/context.h" -#include "context/cdlist.h" #include "context/cdhashset.h" +#include "context/cdlist.h" +#include "context/context.h" +#include "expr/statistics_registry.h" +#include "theory/bv/bv_subtheory.h" #include "theory/bv/theory_bv_utils.h" -#include "util/statistics_registry.h" +#include "theory/theory.h" #include "util/hash.h" -#include "theory/bv/bv_subtheory.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 768923ee6..f5e2a2077 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -15,15 +15,17 @@ ** \todo document this file **/ -#pragma once - #include "cvc4_private.h" -#include "theory/theory.h" + +#pragma once + +#include <sstream> + #include "context/context.h" -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" +#include "smt_util/command.h" #include "theory/bv/theory_bv_utils.h" -#include "expr/command.h" -#include <sstream> +#include "theory/theory.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index bc1b92dce..0911b6ccf 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -19,6 +19,7 @@ #pragma once +#include "theory/rewriter.h" #include "theory/bv/theory_bv_rewrite_rules.h" #include "theory/bv/theory_bv_utils.h" diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index f2adea411..2c82943ce 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -15,15 +15,15 @@ ** \todo document this file **/ -#include "theory/theory.h" -#include "theory/bv/options.h" -#include "theory/bv/theory_bv_rewriter.h" +#include "options/bv_options.h" #include "theory/bv/theory_bv_rewrite_rules.h" +#include "theory/bv/theory_bv_rewrite_rules_constant_evaluation.h" #include "theory/bv/theory_bv_rewrite_rules_core.h" +#include "theory/bv/theory_bv_rewrite_rules_normalization.h" #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h" -#include "theory/bv/theory_bv_rewrite_rules_constant_evaluation.h" #include "theory/bv/theory_bv_rewrite_rules_simplification.h" -#include "theory/bv/theory_bv_rewrite_rules_normalization.h" +#include "theory/bv/theory_bv_rewriter.h" +#include "theory/theory.h" using namespace CVC4; using namespace CVC4::theory; @@ -682,6 +682,3 @@ Node TheoryBVRewriter::eliminateBVSDiv(TNode node) { >::apply(node); return result; } - - - diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 3f0fa8194..7e5d429fd 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -20,8 +20,8 @@ #ifndef __CVC4__THEORY__BV__THEORY_BV_REWRITER_H #define __CVC4__THEORY__BV__THEORY_BV_REWRITER_H +#include "expr/statistics_registry.h" #include "theory/rewriter.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index d2025b1b8..f57ccec48 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -16,24 +16,23 @@ **/ #include "theory/bv/theory_bv_utils.h" -#include "theory/decision_attributes.h" #include "theory/theory.h" -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::bv; -using namespace CVC4::theory::bv::utils; +namespace CVC4 { +namespace theory { +namespace bv { +namespace utils { -bool CVC4::theory::bv::utils::isCoreTerm(TNode term, TNodeBoolMap& cache) { - term = term.getKind() == kind::NOT ? term[0] : term; - TNodeBoolMap::const_iterator it = cache.find(term); +bool isCoreTerm(TNode term, TNodeBoolMap& cache) { + term = term.getKind() == kind::NOT ? term[0] : term; + TNodeBoolMap::const_iterator it = cache.find(term); if (it != cache.end()) { return it->second; } - + if (term.getNumChildren() == 0) return true; - + if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) { Kind k = term.getKind(); if (k != kind::CONST_BITVECTOR && @@ -52,21 +51,21 @@ bool CVC4::theory::bv::utils::isCoreTerm(TNode term, TNodeBoolMap& cache) { return false; } } - - cache[term]= true; + + cache[term]= true; return true; } -bool CVC4::theory::bv::utils::isEqualityTerm(TNode term, TNodeBoolMap& cache) { - term = term.getKind() == kind::NOT ? term[0] : term; - TNodeBoolMap::const_iterator it = cache.find(term); +bool isEqualityTerm(TNode term, TNodeBoolMap& cache) { + term = term.getKind() == kind::NOT ? term[0] : term; + TNodeBoolMap::const_iterator it = cache.find(term); if (it != cache.end()) { return it->second; } - + if (term.getNumChildren() == 0) return true; - + if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, term) == THEORY_BV) { Kind k = term.getKind(); if (k != kind::CONST_BITVECTOR && @@ -83,13 +82,13 @@ bool CVC4::theory::bv::utils::isEqualityTerm(TNode term, TNodeBoolMap& cache) { return false; } } - - cache[term]= true; + + cache[term]= true; return true; } -uint64_t CVC4::theory::bv::utils::numNodes(TNode node, NodeSet& seen) { +uint64_t numNodes(TNode node, NodeSet& seen) { if (seen.find(node) != seen.end()) return 0; @@ -101,9 +100,7 @@ uint64_t CVC4::theory::bv::utils::numNodes(TNode node, NodeSet& seen) { return size; } - - -void CVC4::theory::bv::utils::collectVariables(TNode node, NodeSet& vars) { +void collectVariables(TNode node, NodeSet& vars) { if (vars.find(node) != vars.end()) return; @@ -115,3 +112,8 @@ void CVC4::theory::bv::utils::collectVariables(TNode node, NodeSet& vars) { collectVariables(node[i], vars); } } + +}/* CVC4::theory::bv::utils namespace */ +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h index 1d835dd23..db98ef66b 100644 --- a/src/theory/bv/type_enumerator.h +++ b/src/theory/bv/type_enumerator.h @@ -19,11 +19,11 @@ #ifndef __CVC4__THEORY__BV__TYPE_ENUMERATOR_H #define __CVC4__THEORY__BV__TYPE_ENUMERATOR_H +#include "expr/kind.h" +#include "expr/type_node.h" +#include "theory/type_enumerator.h" #include "util/bitvector.h" #include "util/integer.h" -#include "theory/type_enumerator.h" -#include "expr/type_node.h" -#include "expr/kind.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index bd44f66a9..dc57f6b47 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -19,10 +19,10 @@ #ifndef __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H #define __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H +#include "expr/node_manager_attributes.h" +#include "options/datatypes_options.h" #include "theory/rewriter.h" -#include "theory/datatypes/options.h" #include "theory/type_enumerator.h" -#include "expr/node_manager_attributes.h" namespace CVC4 { namespace theory { @@ -625,4 +625,3 @@ public: }/* CVC4 namespace */ #endif /* __CVC4__THEORY__DATATYPES__DATATYPES_REWRITER_H */ - diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 3ab29f334..5f0466d30 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -15,11 +15,11 @@ **/ -#include "theory/datatypes/datatypes_sygus.h" -#include "theory/datatypes/datatypes_rewriter.h" #include "expr/node_manager.h" +#include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/datatypes/datatypes_sygus.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/options.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h index 4eac3d1c6..415bd6e4b 100644 --- a/src/theory/datatypes/datatypes_sygus.h +++ b/src/theory/datatypes/datatypes_sygus.h @@ -19,10 +19,11 @@ #ifndef __CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_H #define __CVC4__THEORY__DATATYPES__DATATYPES_SYGUS_H -#include "expr/node.h" -#include "util/datatype.h" #include <iostream> #include <map> + +#include "expr/node.h" +#include "expr/datatype.h" #include "context/context.h" #include "context/cdchunk_list.h" #include "context/cdhashmap.h" @@ -30,11 +31,10 @@ namespace CVC4 { namespace theory { - namespace quantifiers { class TermDbSygus; -} - +} /* namespace quantifiers */ + namespace datatypes { class SygusSplit diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index a4cd0d124..749d6b58a 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -41,15 +41,15 @@ parameterized APPLY_TESTER TESTER_TYPE 1 "tester application; first parameter is constant DATATYPE_TYPE \ ::CVC4::Datatype \ "::CVC4::DatatypeHashFunction" \ - "util/datatype.h" \ + "expr/datatype.h" \ "a datatype type" cardinality DATATYPE_TYPE \ "%TYPE%.getConst<Datatype>().getCardinality()" \ - "util/datatype.h" + "expr/datatype.h" well-founded DATATYPE_TYPE \ "%TYPE%.getConst<Datatype>().isWellFounded()" \ "%TYPE%.getConst<Datatype>().mkGroundTerm(%TYPE%.toType())" \ - "util/datatype.h" + "expr/datatype.h" enumerator DATATYPE_TYPE \ "::CVC4::theory::datatypes::DatatypesEnumerator" \ @@ -58,11 +58,11 @@ enumerator DATATYPE_TYPE \ operator PARAMETRIC_DATATYPE 1: "parametric datatype" cardinality PARAMETRIC_DATATYPE \ "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \ - "util/datatype.h" + "expr/datatype.h" well-founded PARAMETRIC_DATATYPE \ "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \ "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \ - "util/datatype.h" + "expr/datatype.h" enumerator PARAMETRIC_DATATYPE \ "::CVC4::theory::datatypes::DatatypesEnumerator" \ @@ -73,7 +73,7 @@ parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \ constant ASCRIPTION_TYPE \ ::CVC4::AscriptionType \ ::CVC4::AscriptionTypeHashFunction \ - "util/ascription_type.h" \ + "expr/ascription_type.h" \ "a type parameter for type ascription; payload is an instance of the CVC4::AscriptionType class" typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule @@ -126,7 +126,7 @@ typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule constant RECORD_TYPE \ ::CVC4::Record \ ::CVC4::RecordHashFunction \ - "util/record.h" \ + "expr/record.h" \ "record type" cardinality RECORD_TYPE \ "::CVC4::theory::datatypes::TupleProperties::computeCardinality(%TYPE%)" \ @@ -146,7 +146,7 @@ construle RECORD ::CVC4::theory::datatypes::RecordProperties constant RECORD_SELECT_OP \ ::CVC4::RecordSelect \ ::CVC4::RecordSelectHashFunction \ - "util/record.h" \ + "expr/record.h" \ "operator for a record select; payload is an instance CVC4::RecordSelect class" parameterized RECORD_SELECT RECORD_SELECT_OP 1 "record select; first parameter is a RECORD_SELECT_OP, second is a record term to select from" typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule @@ -154,7 +154,7 @@ typerule RECORD_SELECT ::CVC4::theory::datatypes::RecordSelectTypeRule constant RECORD_UPDATE_OP \ ::CVC4::RecordUpdate \ ::CVC4::RecordUpdateHashFunction \ - "util/record.h" \ + "expr/record.h" \ "operator for a record update; payload is an instance CVC4::RecordSelect class" parameterized RECORD_UPDATE RECORD_UPDATE_OP 2 "record update; first parameter is a RECORD_UPDATE_OP (which references a field), second is a record term to update, third is the element to store in the record in the given field" typerule RECORD_UPDATE ::CVC4::theory::datatypes::RecordUpdateTypeRule diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options deleted file mode 100644 index 6da0fe244..000000000 --- a/src/theory/datatypes/options +++ /dev/null @@ -1,23 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module DATATYPES "theory/datatypes/options.h" Datatypes theory - -# How to handle selectors applied to incorrect constructors. If this option is set, -# then we do not rewrite such a selector term to an arbitrary ground term. -# For example, by default cvc4 considers cdr( nil ) = nil. If this option is set, then -# cdr( nil ) has no set value. -expert-option dtRewriteErrorSel --dt-rewrite-error-sel bool :default false :read-write - rewrite incorrectly applied selectors to arbitrary ground term -option dtForceAssignment --dt-force-assignment bool :default false :read-write - force the datatypes solver to give specific values to all datatypes terms before answering sat -option dtBinarySplit --dt-binary-split bool :default false - do binary splits for datatype constructor types -option cdtBisimilar --cdt-bisimilar bool :default true - do bisimilarity check for co-datatypes -option dtCyclic --dt-cyclic bool :default true - do cyclicity check for datatypes - -endmodule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index af8e5c503..1962d2e31 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -13,26 +13,24 @@ ** ** Implementation of the theory of datatypes. **/ +#include "theory/datatypes/theory_datatypes.h" +#include <map> -#include "theory/datatypes/theory_datatypes.h" -#include "theory/valuation.h" +#include "base/cvc4_assert.h" +#include "expr/datatype.h" #include "expr/kind.h" -#include "util/datatype.h" -#include "util/cvc4_assert.h" +#include "options/datatypes_options.h" +#include "options/quantifiers_options.h" +#include "options/smt_options.h" +#include "smt/boolean_terms.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" +#include "theory/quantifiers_engine.h" #include "theory/theory_model.h" -#include "smt/options.h" -#include "smt/boolean_terms.h" -#include "theory/datatypes/options.h" #include "theory/type_enumerator.h" +#include "theory/valuation.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers_engine.h" - - -#include <map> using namespace std; using namespace CVC4; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index b452e02d1..bbbf799bd 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -19,16 +19,16 @@ #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H -#include "theory/theory.h" -#include "util/datatype.h" -#include "util/hash.h" -#include "theory/uf/equality_engine.h" -#include "theory/datatypes/datatypes_sygus.h" - #include <ext/hash_set> #include <iostream> #include <map> + #include "context/cdchunk_list.h" +#include "expr/datatype.h" +#include "theory/datatypes/datatypes_sygus.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" +#include "util/hash.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 15d1c6c9e..23e68a6a8 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -19,7 +19,7 @@ #ifndef __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H #define __CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H -#include "util/matcher.h" +#include "expr/matcher.h" //#include "expr/attribute.h" namespace CVC4 { diff --git a/src/theory/decision_attributes.h b/src/theory/decision_attributes.h deleted file mode 100644 index 1ea1bb21d..000000000 --- a/src/theory/decision_attributes.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file decision_attributes.h - ** \verbatim - ** Original author: Kshitij Bansal - ** Major contributors: Morgan Deters - ** 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 Rewriter attributes - ** - ** Rewriter attributes. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__DECISION_ATTRIBUTES -#define __CVC4__THEORY__DECISION_ATTRIBUTES - -#include "expr/attribute.h" - -namespace CVC4 { -namespace decision { -typedef uint64_t DecisionWeight; -} -namespace theory { -namespace attr { - struct DecisionWeightTag {}; -}/* CVC4::theory::attr namespace */ - -typedef expr::Attribute<attr::DecisionWeightTag, decision::DecisionWeight> DecisionWeightAttr; - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__DECISION_ATTRIBUTES */ diff --git a/src/theory/fp/options b/src/theory/fp/options deleted file mode 100644 index 3fee94d1d..000000000 --- a/src/theory/fp/options +++ /dev/null @@ -1,8 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module FP "theory/fp/options.h" Fp - -endmodule diff --git a/src/theory/fp/options_handlers.h b/src/theory/fp/options_handlers.h deleted file mode 100644 index f1a86e396..000000000 --- a/src/theory/fp/options_handlers.h +++ /dev/null @@ -1,14 +0,0 @@ -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__FP__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__FP__OPTIONS_HANDLERS_H - -namespace CVC4 { -namespace theory { -namespace fp { - -}/* CVC4::theory::fp namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__FP__OPTIONS_HANDLERS_H */ diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index ba9823541..59ff4692f 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -25,12 +25,11 @@ ** ]] **/ -#include "theory/fp/theory_fp_rewriter.h" - -#include "util/cvc4_assert.h" - #include <algorithm> +#include "base/cvc4_assert.h" +#include "theory/fp/theory_fp_rewriter.h" + namespace CVC4 { namespace theory { namespace fp { diff --git a/src/theory/idl/options b/src/theory/idl/options deleted file mode 100644 index c1c9edcef..000000000 --- a/src/theory/idl/options +++ /dev/null @@ -1,12 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module IDL "theory/idl/options.h" Idl - -option idlRewriteEq --enable-idl-rewrite-equalities/--disable-idl-rewrite-equalities bool :default false :read-write - enable rewriting equalities into two inequalities in IDL solver (default is disabled) -/disable rewriting equalities into two inequalities in IDL solver (default is disabled) - -endmodule diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index 55dec35e9..427ac577c 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -16,12 +16,14 @@ **/ #include "theory/idl/theory_idl.h" -#include "theory/idl/options.h" -#include "theory/rewriter.h" #include <set> #include <queue> +#include "options/idl_options.h" +#include "theory/rewriter.h" + + using namespace std; using namespace CVC4; diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index ee7e5db12..6c59146e1 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -29,7 +29,7 @@ #ifndef __CVC4__THEORY__INTERRUPTED_H #define __CVC4__THEORY__INTERRUPTED_H -#include "util/exception.h" +#include "base/exception.h" namespace CVC4 { namespace theory { diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index d4abdbf35..27fce3071 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -22,11 +22,12 @@ #ifndef __CVC4__ITE_UTILITIES_H #define __CVC4__ITE_UTILITIES_H -#include <vector> #include <ext/hash_map> #include <ext/hash_set> +#include <vector> + #include "expr/node.h" -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 1df304061..15600fefc 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -15,14 +15,17 @@ ** A class giving information about a logic (group of theory modules and ** configuration information). **/ +#include "theory/logic_info.h" #include <string> #include <cstring> #include <sstream> +#include "base/cvc4_assert.h" #include "expr/kind.h" -#include "theory/logic_info.h" -#include "util/cvc4_assert.h" + +#warning "TODO: Remove logic_info_forward.h" + using namespace std; using namespace CVC4::theory; diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index f4527648a..9cecc88b7 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -24,6 +24,7 @@ #include <string> #include <vector> #include "expr/kind.h" +#include "options/logic_info_forward.h" namespace CVC4 { @@ -338,4 +339,3 @@ std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) CVC4_PUBLIC; }/* CVC4 namespace */ #endif /* __CVC4__LOGIC_INFO_H */ - diff --git a/src/theory/options b/src/theory/options deleted file mode 100644 index 9944264c8..000000000 --- a/src/theory/options +++ /dev/null @@ -1,15 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module THEORY "theory/options.h" Theory layer - -expert-option theoryOfMode theoryof-mode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h" :read-write - mode for Theory::theoryof() - -option - use-theory --use-theory=NAME argument :handler CVC4::theory::useTheory :handler-include "theory/options_handlers.h" - use alternate theory implementation NAME (--use-theory=help for a list) -option theoryAlternates ::std::map<std::string,bool> :include <map> :read-write - -endmodule diff --git a/src/theory/options_handlers.h b/src/theory/options_handlers.h deleted file mode 100644 index 4b0cd94a5..000000000 --- a/src/theory/options_handlers.h +++ /dev/null @@ -1,69 +0,0 @@ -/********************* */ -/*! \file options_handlers.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 Custom handlers and predicates for TheoryEngine options - ** - ** Custom handlers and predicates for TheoryEngine options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__OPTIONS_HANDLERS_H - -#include "expr/metakind.h" - -namespace CVC4 { -namespace theory { - -static const std::string theoryOfModeHelp = "\ -TheoryOf modes currently supported by the --theoryof-mode option:\n\ -\n\ -type (default) \n\ -+ type variables, constants and equalities by type\n\ -\n\ -term \n\ -+ type variables as uninterpreted, equalities by the parametric theory\n\ -"; - -inline TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, SmtEngine* smt) { - if(optarg == "type") { - return THEORY_OF_TYPE_BASED; - } else if(optarg == "term") { - return THEORY_OF_TERM_BASED; - } else if(optarg == "help") { - puts(theoryOfModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --theoryof-mode: `") + - optarg + "'. Try --theoryof-mode help."); - } -} - -inline void useTheory(std::string option, std::string optarg, SmtEngine* smt) { - if(optarg == "help") { - puts(useTheoryHelp); - exit(1); - } - if(useTheoryValidate(optarg)) { - std::map<std::string, bool> m = options::theoryAlternates(); - m[optarg] = true; - options::theoryAlternates.set(m); - } else { - throw OptionException(std::string("unknown option for ") + option + ": `" + - optarg + "'. Try --use-theory help."); - } -} - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__OPTIONS_HANDLERS_H */ diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 2da0f0467..34a5a7dbd 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -19,10 +19,10 @@ #ifndef __CVC4__THEORY__OUTPUT_CHANNEL_H #define __CVC4__THEORY__OUTPUT_CHANNEL_H -#include "util/cvc4_assert.h" -#include "theory/interrupted.h" -#include "util/resource_manager.h" +#include "base/cvc4_assert.h" +#include "expr/resource_manager.h" #include "smt/logic_exception.h" +#include "theory/interrupted.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index f047276b0..b18676cbc 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -13,9 +13,9 @@ **/ +#include "options/quantifiers_options.h" #include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 2fd595a9f..ceab8394f 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -14,12 +14,12 @@ ** This class manages integer bounds for quantifiers **/ +#include "options/quantifiers_options.h" #include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/options.h" using namespace CVC4; using namespace std; @@ -425,4 +425,3 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node bool BoundedIntegers::isGroundRange(Node f, Node v) { return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar(); } - diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index b67c4bd56..0cdb22be4 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -12,13 +12,13 @@ ** \brief Implementation of theory uf candidate generator class **/ +#include "options/quantifiers_options.h" #include "theory/quantifiers/candidate_generator.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/options.h" +#include "theory/theory_engine.h" +#include "theory/uf/theory_uf.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index 398ae1ffe..81fe00674 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -12,14 +12,14 @@ ** \brief counterexample guided instantiation class ** **/ - #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/first_order_model.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" -#include "util/datatype.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 6fcfdbc58..8274561ca 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -17,11 +17,11 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H #define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_INSTANTIATION_H -#include "context/cdhashmap.h" #include "context/cdchunk_list.h" -#include "theory/quantifiers_engine.h" +#include "context/cdhashmap.h" +#include "options/quantifiers_modes.h" #include "theory/quantifiers/ce_guided_single_inv.h" -#include "theory/quantifiers/modes.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index f533a2bbb..7ef23077f 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -12,18 +12,18 @@ ** \brief utility for processing single invocation synthesis conjectures ** **/ - #include "theory/quantifiers/ce_guided_single_inv.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" #include "theory/quantifiers/ce_guided_single_inv_ei.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/datatypes/datatypes_rewriter.h" -#include "util/datatype.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; @@ -1186,4 +1186,4 @@ void SingleInvocationPartition::debugPrint( const char * c ) { Trace(c) << std::endl; } -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp index 18252e190..f45285851 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp @@ -13,12 +13,12 @@ ** **/ -#include "theory/quantifiers/ce_guided_single_inv_ei.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/ce_guided_single_inv_ei.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; @@ -44,4 +44,4 @@ bool CegEntailmentInfer::getEntailedConjecture( Node& conj, Node& exp ) { return false; } -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 8fd935368..6ba5bed02 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -12,18 +12,18 @@ ** \brief utility for processing single invocation synthesis conjectures ** **/ - #include "theory/quantifiers/ce_guided_single_inv_sol.h" -#include "theory/quantifiers/ce_guided_single_inv.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" +#include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/ce_guided_single_inv.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/datatypes/datatypes_rewriter.h" -#include "util/datatype.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 7c10da90c..cea90621d 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -11,16 +11,16 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation **/ - #include "theory/quantifiers/ceg_instantiator.h" -#include "theory/arith/theory_arith.h" + +#include "options/quantifiers_options.h" +#include "smt_util/ite_removal.h" #include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" -#include "util/ite_removal.h" +#include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" //#define MBP_STRICT_ASSERTIONS diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 9504bd407..5b3c5263f 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -18,8 +18,8 @@ #ifndef __CVC4__CEG_INSTANTIATOR_H #define __CVC4__CEG_INSTANTIATOR_H +#include "expr/statistics_registry.h" #include "theory/quantifiers_engine.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 1cdad589b..8e083ae1e 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -13,12 +13,12 @@ ** **/ +#include "options/quantifiers_options.h" #include "theory/quantifiers/conjecture_generator.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/first_order_model.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 36d055b69..095e7868e 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -12,13 +12,13 @@ ** \brief Implementation of model engine model class **/ +#include "options/quantifiers_options.h" +#include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/ambqi_builder.h" -#include "theory/quantifiers/options.h" +#include "theory/quantifiers/term_database.h" #define USE_INDEX_ORDERING diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index c3a723fce..02c6bbba8 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -12,9 +12,9 @@ ** \brief Implementation of full model check class **/ -#include "theory/quantifiers/full_model_check.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/options.h" +#include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/term_database.h" using namespace std; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index f4e8861dc..89c2d4868 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -11,15 +11,15 @@ ** ** [[ Add lengthier description here ]] ** \todo document this file -**/ - + **/ #include "theory/quantifiers/inst_match_generator.h" -#include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/term_database.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/candidate_generator.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" #include "theory/quantifiers_engine.h" -#include "theory/quantifiers/options.h" -#include "util/datatype.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index eff1c0d9b..a4632398d 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -11,17 +11,17 @@ ** ** \brief Implementation of counterexample-guided quantifier instantiation strategies **/ - #include "theory/quantifiers/inst_strategy_cbqi.h" -#include "theory/arith/theory_arith.h" + +#include "options/quantifiers_options.h" +#include "smt_util/ite_removal.h" #include "theory/arith/partial_model.h" +#include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" -#include "util/ite_removal.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index d14b85111..b8bc25c6a 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -18,11 +18,10 @@ #ifndef __CVC4__INST_STRATEGY_CBQI_H #define __CVC4__INST_STRATEGY_CBQI_H -#include "theory/quantifiers/instantiation_engine.h" +#include "expr/statistics_registry.h" #include "theory/arith/arithvar.h" #include "theory/quantifiers/ceg_instantiator.h" - -#include "util/statistics_registry.h" +#include "theory/quantifiers/instantiation_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 9237d95c2..299eb51fd 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -14,11 +14,11 @@ #include "theory/quantifiers/inst_strategy_e_matching.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/inst_match_generator.h" #include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4; @@ -652,4 +652,3 @@ bool FullSaturation::process( Node f, bool fullEffort ){ void FullSaturation::registerQuantifier( Node q ) { } - diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h index 2f7e7dcf1..a19bcca76 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/inst_strategy_e_matching.h @@ -17,14 +17,12 @@ #ifndef __CVC4__INST_STRATEGY_E_MATCHING_H #define __CVC4__INST_STRATEGY_E_MATCHING_H -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/trigger.h" - #include "context/context.h" #include "context/context_mm.h" - -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" #include "theory/quantifiers/instantiation_engine.h" +#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 16cecb657..88a67e3c8 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -14,12 +14,12 @@ #include "theory/quantifiers/instantiation_engine.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/inst_strategy_e_matching.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 163005806..a5e3dada8 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -14,16 +14,17 @@ ** This class implements quantifiers macro definitions. **/ +#include "theory/quantifiers/macros.h" + #include <vector> -#include "theory/quantifiers/macros.h" -#include "theory/rewriter.h" +#include "options/quantifiers_modes.h" +#include "options/quantifiers_options.h" #include "proof/proof_manager.h" #include "smt/smt_engine_scope.h" -#include "theory/quantifiers/modes.h" -#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/rewriter.h" using namespace CVC4; using namespace std; @@ -485,4 +486,4 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { } } } -}
\ No newline at end of file +} diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 79b995ef0..dc18548a5 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -12,18 +12,19 @@ ** \brief Implementation of model builder class **/ +#include "theory/quantifiers/model_builder.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_model.h" #include "theory/uf/theory_uf_strong_solver.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/model_builder.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/trigger.h" -#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; @@ -745,5 +746,3 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; } } - - diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index f5a063eb8..6a21a50e5 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -13,16 +13,17 @@ **/ #include "theory/quantifiers/model_engine.h" + +#include "options/quantifiers_options.h" +#include "theory/quantifiers/ambqi_builder.h" +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_strong_solver.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/ambqi_builder.h" using namespace std; using namespace CVC4; @@ -335,5 +336,3 @@ ModelEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas); StatisticsRegistry::unregisterStat(&d_mbqi_inst_lemmas); } - - diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp deleted file mode 100644 index 253f23561..000000000 --- a/src/theory/quantifiers/modes.cpp +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file modes.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** 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 <iostream> -#include "theory/quantifiers/modes.h" - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) { - switch(mode) { - case theory::quantifiers::INST_WHEN_PRE_FULL: - out << "INST_WHEN_PRE_FULL"; - break; - case theory::quantifiers::INST_WHEN_FULL: - out << "INST_WHEN_FULL"; - break; - case theory::quantifiers::INST_WHEN_FULL_LAST_CALL: - out << "INST_WHEN_FULL_LAST_CALL"; - break; - case theory::quantifiers::INST_WHEN_LAST_CALL: - out << "INST_WHEN_LAST_CALL"; - break; - default: - out << "InstWhenMode!UNKNOWN"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) { - switch(mode) { - case theory::quantifiers::LITERAL_MATCH_NONE: - out << "LITERAL_MATCH_NONE"; - break; - case theory::quantifiers::LITERAL_MATCH_PREDICATE: - out << "LITERAL_MATCH_PREDICATE"; - break; - case theory::quantifiers::LITERAL_MATCH_EQUALITY: - out << "LITERAL_MATCH_EQUALITY"; - break; - default: - out << "LiteralMatchMode!UNKNOWN"; - } - - return out; -} - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { - switch(mode) { - case theory::quantifiers::MBQI_GEN_EVAL: - out << "MBQI_GEN_EVAL"; - break; - case theory::quantifiers::MBQI_NONE: - out << "MBQI_NONE"; - break; - case theory::quantifiers::MBQI_FMC: - out << "MBQI_FMC"; - break; - case theory::quantifiers::MBQI_ABS: - out << "MBQI_ABS"; - break; - case theory::quantifiers::MBQI_TRUST: - out << "MBQI_TRUST"; - break; - default: - out << "MbqiMode!UNKNOWN"; - } - return out; -} - -}/* CVC4 namespace */ - diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h deleted file mode 100644 index 01d3f0c22..000000000 --- a/src/theory/quantifiers/modes.h +++ /dev/null @@ -1,173 +0,0 @@ -/********************* */ -/*! \file modes.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** 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__QUANTIFIERS__MODES_H -#define __CVC4__THEORY__QUANTIFIERS__MODES_H - -#include <iostream> - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -typedef enum { - /** Apply instantiation round before full effort (possibly at standard effort) */ - INST_WHEN_PRE_FULL, - /** Apply instantiation round at full effort or above */ - INST_WHEN_FULL, - /** Apply instantiation round at full effort, after all other theories finish, or above */ - INST_WHEN_FULL_DELAY, - /** Apply instantiation round at full effort half the time, and last call always */ - INST_WHEN_FULL_LAST_CALL, - /** Apply instantiation round at full effort after all other theories finish half the time, and last call always */ - INST_WHEN_FULL_DELAY_LAST_CALL, - /** Apply instantiation round at last call only */ - INST_WHEN_LAST_CALL, -} InstWhenMode; - -typedef enum { - /** Do not consider polarity of patterns */ - LITERAL_MATCH_NONE, - /** Consider polarity of boolean predicates only */ - LITERAL_MATCH_PREDICATE, - /** Consider polarity of boolean predicates, as well as equalities */ - LITERAL_MATCH_EQUALITY, -} LiteralMatchMode; - -typedef enum { - /** mbqi from CADE 24 paper */ - MBQI_GEN_EVAL, - /** no mbqi */ - MBQI_NONE, - /** default, mbqi from Section 5.4.2 of AJR thesis */ - MBQI_FMC, - /** mbqi with integer intervals */ - MBQI_FMC_INTERVAL, - /** abstract mbqi algorithm */ - MBQI_ABS, - /** mbqi trust (produce no instantiations) */ - MBQI_TRUST, -} MbqiMode; - -typedef enum { - /** default, apply at full effort */ - QCF_WHEN_MODE_DEFAULT, - /** apply at last call */ - QCF_WHEN_MODE_LAST_CALL, - /** apply at standard effort */ - QCF_WHEN_MODE_STD, - /** apply based on heuristics */ - QCF_WHEN_MODE_STD_H, -} QcfWhenMode; - -typedef enum { - /** default, use qcf for conflicts only */ - QCF_CONFLICT_ONLY, - /** use qcf for conflicts and propagations */ - QCF_PROP_EQ, - /** use qcf for conflicts, propagations and heuristic instantiations */ - QCF_PARTIAL, - /** use qcf for model checking */ - QCF_MC, -} QcfMode; - -typedef enum { - /** use but do not trust */ - USER_PAT_MODE_USE, - /** default, if patterns are supplied for a quantifier, use only those */ - USER_PAT_MODE_TRUST, - /** resort to user patterns only when necessary */ - USER_PAT_MODE_RESORT, - /** ignore user patterns */ - USER_PAT_MODE_IGNORE, - /** interleave use/resort for user patterns */ - USER_PAT_MODE_INTERLEAVE, -} UserPatMode; - -typedef enum { - /** default for trigger selection */ - TRIGGER_SEL_DEFAULT, - /** only consider minimal terms for triggers */ - TRIGGER_SEL_MIN, - /** only consider maximal terms for triggers */ - TRIGGER_SEL_MAX, -} TriggerSelMode; - -typedef enum CVC4_PUBLIC { - /** default : prenex quantifiers without user patterns */ - PRENEX_NO_USER_PAT, - /** prenex all */ - PRENEX_ALL, - /** prenex none */ - PRENEX_NONE, -} PrenexQuantMode; - -typedef enum { - /** enforce fairness by UF corresponding to datatypes size */ - CEGQI_FAIR_UF_DT_SIZE, - /** enforce fairness by datatypes size */ - CEGQI_FAIR_DT_SIZE, - /** enforce fairness by datatypes height bound */ - CEGQI_FAIR_DT_HEIGHT_PRED, - /** do not use fair strategy for CEGQI */ - CEGQI_FAIR_NONE, -} CegqiFairMode; - -typedef enum { - /** consider all terms in master equality engine */ - TERM_DB_ALL, - /** consider only relevant terms */ - TERM_DB_RELEVANT, -} TermDbMode; - -typedef enum { - /** do not lift ITEs in quantified formulas */ - ITE_LIFT_QUANT_MODE_NONE, - /** only lift ITEs in quantified formulas if reduces the term size */ - ITE_LIFT_QUANT_MODE_SIMPLE, - /** lift ITEs */ - ITE_LIFT_QUANT_MODE_ALL, -} IteLiftQuantMode; - -typedef enum { - /** synthesize I( x ) */ - SYGUS_INV_TEMPL_MODE_NONE, - /** synthesize ( pre( x ) V I( x ) ) */ - SYGUS_INV_TEMPL_MODE_PRE, - /** synthesize ( post( x ) ^ I( x ) ) */ - SYGUS_INV_TEMPL_MODE_POST, -} SygusInvTemplMode; - -typedef enum { - /** infer all definitions */ - MACROS_QUANT_MODE_ALL, - /** infer ground definitions */ - MACROS_QUANT_MODE_GROUND, - /** infer ground uf definitions */ - MACROS_QUANT_MODE_GROUND_UF, -} MacrosQuantMode; - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ - -std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC; - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__MODES_H */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options deleted file mode 100644 index 065da0d5a..000000000 --- a/src/theory/quantifiers/options +++ /dev/null @@ -1,297 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers - -#### rewriter options - -# Whether to mini-scope quantifiers. -# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to -# ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) -option miniscopeQuant --miniscope-quant bool :default true :read-write - miniscope quantifiers -# Whether to mini-scope quantifiers based on formulas with no free variables. -# For example, forall x. ( P( x ) V Q ) will be rewritten to -# ( forall x. P( x ) ) V Q -option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write - miniscope quantifiers for ground subformulas -option quantSplit --quant-split bool :default true - apply splitting to quantified formulas based on variable disjoint disjuncts -option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h" - prenex mode for quantified formulas -# Whether to variable-eliminate quantifiers. -# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to -# forall y. P( c, y ) -option varElimQuant --var-elim-quant bool :default true - enable simple variable elimination for quantified formulas -option dtVarExpandQuant --dt-var-exp-quant bool :default true - expand datatype variables bound to one constructor in quantifiers -#ite lift mode for quantified formulas -option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h" - ite lifting mode for quantified formulas -option condVarSplitQuant --cond-var-split-quant bool :default true - split quantified formulas that lead to variable eliminations -option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false - aggressive split quantified formulas that lead to variable eliminations -option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false - split ites with dt testers as conditions -# Whether to CNF quantifier bodies -# option cnfQuant --cnf-quant bool :default false -# apply CNF conversion to quantified formulas -option nnfQuant --nnf-quant bool :default true - apply NNF conversion to quantified formulas -# Whether to pre-skolemize quantifier bodies. -# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to -# forall x. P( x ) => f( S( x ) ) = x -option preSkolemQuant --pre-skolem-quant bool :read-write :default false - apply skolemization eagerly to bodies of quantified formulas -option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true - apply skolemization to nested quantified formulass -option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true - apply skolemization to quantified formulas aggressively -option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false - perform aggressive miniscoping for quantifiers -option elimTautQuant --elim-taut-quant bool :default true - eliminate tautological disjuncts of quantified formulas -option purifyQuant --purify-quant bool :default false - purify quantified formulas - -#### E-matching options - -option eMatching --e-matching bool :read-write :default true - whether to do heuristic E-matching - -option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTermDbMode :handler-include "theory/quantifiers/options_handlers.h" - which ground terms to consider for instantiation -option registerQuantBodyTerms --register-quant-body-terms bool :default false - consider ground terms within bodies of quantified formulas for matching - -option smartTriggers --smart-triggers bool :default true - enable smart triggers -option relevantTriggers --relevant-triggers bool :default false - prefer triggers that are more relevant based on SInE style analysis -option relationalTriggers --relational-triggers bool :default false - choose relational triggers such as x = f(y), x >= f(y) -option purifyTriggers --purify-triggers bool :default false :read-write - purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1 -option purifyDtTriggers --purify-dt-triggers bool :default false :read-write - purify dt triggers, match all constructors of correct form instead of selectors -option pureThTriggers --pure-th-triggers bool :default false :read-write - use pure theory terms as single triggers -option partialTriggers --partial-triggers bool :default false :read-write - use triggers that do not contain all free variables -option multiTriggerWhenSingle --multi-trigger-when-single bool :default false - select multi triggers when single triggers exist -option multiTriggerPriority --multi-trigger-priority bool :default false - only try multi triggers if single triggers give no instantiations -option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h" - selection mode for triggers -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h" - policy for handling user-provided patterns for quantifier instantiation -option incrementTriggers --increment-triggers bool :default true - generate additional triggers as needed during search - -option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" - when to apply instantiation - -option instMaxLevel --inst-max-level=N int :read-write :default -1 - maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default) -option instLevelInputOnly --inst-level-input-only bool :default true - only input terms are assigned instantiation level zero -option internalReps --quant-internal-reps bool :default true - instantiate with representatives chosen by quantifiers engine - -option eagerInstQuant --eager-inst-quant bool :default false - apply quantifier instantiation eagerly - -option fullSaturateQuant --full-saturate-quant bool :default false :read-write - when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown -option fullSaturateQuantRd --full-saturate-quant-rd bool :default true - whether to use relevant domain first for full saturation instantiation strategy -option fullSaturateInst --fs-inst bool :default false - interleave full saturate instantiation with other techniques - -option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" - choose literal matching mode - -### finite model finding options - -option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write - use finite model finding heuristic for quantifier instantiation - -option quantFunWellDefined --quant-fun-wd bool :default false - assume that function defined by quantifiers are well defined -option fmfFunWellDefined --fmf-fun bool :default false :read-write - find models for recursively defined functions, assumes functions are admissible -option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false - find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant -option fmfEmptySorts --fmf-empty-sorts bool :default false - allow finite model finding to assume sorts that do not occur in ground assertions are empty - -option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" - choose mode for model-based quantifier instantiation -option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false - only add one instantiation per quantifier per round for mbqi -option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false - only add instantiations for one quantifier per round for mbqi - -option fmfInstEngine --fmf-inst-engine bool :default false - use instantiation engine in conjunction with finite model finding -option fmfInstGen --fmf-inst-gen bool :default true - enable Inst-Gen instantiation techniques for finite model finding -option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false - only perform Inst-Gen instantiation techniques on one quantifier per round -option fmfFreshDistConst --fmf-fresh-dc bool :default false - use fresh distinguished representative when applying Inst-Gen techniques -option fmfFmcSimple --fmf-fmc-simple bool :default true - simple models in full model check for finite model finding -option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write - finite model finding on bounded integer quantification -option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write - enforce bounds for bounded integer quantification lazily via use of proxy variables - -### conflict-based instantiation options - -option quantConflictFind --quant-cf bool :read-write :default true - enable conflict find mechanism for quantifiers -option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h" - what effort to apply conflict find mechanism -option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" - when to invoke conflict find mechanism for quantifiers -option qcfTConstraint --qcf-tconstraint bool :read-write :default false - enable entailment checks for t-constraints in qcf algorithm -option qcfAllConflict --qcf-all-conflict bool :read-write :default false - add all available conflicting instances during conflict-based instantiation - -option instNoEntail --inst-no-entail bool :read-write :default true - do not consider instances of quantified formulas that are currently entailed - -### rewrite rules options - -option quantRewriteRules --rewrite-rules bool :default false - use rewrite rules module -option rrOneInstPerRound --rr-one-inst-per-round bool :default false - add one instance of rewrite rule per round - -### induction options - -option quantInduction --quant-ind bool :default false - use all available techniques for inductive reasoning -option dtStcInduction --dt-stc-ind bool :read-write :default false - apply strengthening for existential quantification over datatypes based on structural induction -option intWfInduction --int-wf-ind bool :read-write :default false - apply strengthening for integers based on well-founded induction -option conjectureGen --conjecture-gen bool :read-write :default false - generate candidate conjectures for inductive proofs - -option conjectureGenPerRound --conjecture-gen-per-round=N int :default 1 - number of conjectures to generate per instantiation round -option conjectureNoFilter --conjecture-no-filter bool :default false - do not filter conjectures -option conjectureFilterActiveTerms --conjecture-filter-active-terms bool :read-write :default true - filter based on active terms -option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write :default true - filter based on canonicity -option conjectureFilterModel --conjecture-filter-model bool :read-write :default true - filter based on model -option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 - number of ground terms to generate for model filtering -option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false - more aggressive merging for universal equality engine, introduces terms - -### synthesis options - -option ceGuidedInst --cegqi bool :default false :read-write - counterexample-guided quantifier instantiation -option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" - if and how to apply fairness for cegqi -option cegqiSingleInv --cegqi-si bool :default false :read-write - process single invocation synthesis conjectures -option cegqiSingleInvPartial --cegqi-si-partial bool :default false - combined techniques for synthesis conjectures that are partially single invocation -option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true - reconstruct solutions for single invocation conjectures in original grammar -option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true - include constants when reconstruct solutions for single invocation conjectures in original grammar -option cegqiSingleInvAbort --cegqi-si-abort bool :default false - abort if synthesis conjecture is not single invocation -option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false - abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried - -option sygusNormalForm --sygus-nf bool :default true - only search for sygus builtin terms that are in normal form -option sygusNormalFormArg --sygus-nf-arg bool :default true - account for relationship between arguments of operations in sygus normal form -option sygusNormalFormGlobal --sygus-nf-sym bool :default true - narrow sygus search space based on global state of current candidate program -option sygusNormalFormGlobalGen --sygus-nf-sym-gen bool :default true - generalize lemmas for global search space narrowing -option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true - generalize based on arguments in global search space narrowing -option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true - generalize based on content in global search space narrowing - -option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h" - template mode for sygus invariant synthesis - -# approach applied to general quantified formulas -option cbqiSplx --cbqi-splx bool :read-write :default false - turns on old implementation of counterexample-based quantifier instantiation -option cbqi --cbqi bool :read-write :default false - turns on counterexample-based quantifier instantiation -option recurseCbqi --cbqi-recurse bool :default true - turns on recursive counterexample-based quantifier instantiation -option cbqiSat --cbqi-sat bool :read-write :default true - answer sat when quantifiers are asserted with counterexample-based quantifier instantiation -option cbqiModel --cbqi-model bool :read-write :default true - guide instantiations by model values for counterexample-based quantifier instantiation -option cbqiAll --cbqi-all bool :read-write :default false - apply counterexample-based instantiation to all quantified formulas -option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false - use integer infinity for vts in counterexample-based quantifier instantiation -option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false - use real infinity for vts in counterexample-based quantifier instantiation -option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false - preregister ground instantiations in counterexample-based quantifier instantiation -option cbqiMinBounds --cbqi-min-bounds bool :default false - use minimally constrained lower/upper bound for counterexample-based quantifier instantiation -option cbqiSymLia --cbqi-sym-lia bool :default false - use symbolic integer division in substitutions for counterexample-based quantifier instantiation -option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false - round up integer lower bounds in substitutions for counterexample-based quantifier instantiation -option cbqiMidpoint --cbqi-midpoint bool :default false - choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation -option cbqiNopt --cbqi-nopt bool :default true - non-optimal bounds for counterexample-based quantifier instantiation - -### local theory extensions options - -option localTheoryExt --local-t-ext bool :default false - do instantiation based on local theory extensions -option ltePartialInst --lte-partial-inst bool :default false - partially instantiate local theory quantifiers -option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false - treat arguments of inst closure as restricted terms for instantiation - -### reduction options - -option quantAlphaEquiv --quant-alpha-equiv bool :default true - infer alpha equivalence between quantified formulas -option macrosQuant --macros-quant bool :read-write :default false - perform quantifiers macro expansion -option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMacrosQuantMode :handler-include "theory/quantifiers/options_handlers.h" - mode for quantifiers macro expansion - -### recursive function options - -#option funDefs --fun-defs bool :default false -# enable specialized techniques for recursive function definitions - -### e-unification options - -option quantEqualityEngine --quant-ee bool :default false - maintain congrunce closure over universal equalities - -endmodule diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h deleted file mode 100644 index 02a1a6cf2..000000000 --- a/src/theory/quantifiers/options_handlers.h +++ /dev/null @@ -1,480 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** 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_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H - -#include <string> - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -static const std::string instWhenHelp = "\ -Modes currently supported by the --inst-when option:\n\ -\n\ -full-last-call (default)\n\ -+ Alternate running instantiation rounds at full effort and last\n\ - call. In other words, interleave instantiation and theory combination.\n\ -\n\ -full\n\ -+ Run instantiation round at full effort, before theory combination.\n\ -\n\ -full-delay \n\ -+ Run instantiation round at full effort, before theory combination, after\n\ - all other theories have finished.\n\ -\n\ -full-delay-last-call \n\ -+ Alternate running instantiation rounds at full effort after all other\n\ - theories have finished, and last call. \n\ -\n\ -last-call\n\ -+ Run instantiation at last call effort, after theory combination and\n\ - and theories report sat.\n\ -\n\ -"; - -static const std::string literalMatchHelp = "\ -Literal match modes currently supported by the --literal-match option:\n\ -\n\ -none (default)\n\ -+ Do not use literal matching.\n\ -\n\ -predicate\n\ -+ Consider the phase requirements of predicate literals when applying heuristic\n\ - quantifier instantiation. For example, the trigger P( x ) in the quantified \n\ - formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\ - terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\ - Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\ -\n\ -"; -static const std::string mbqiModeHelp = "\ -Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ -\n\ -default \n\ -+ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\ - Modulo Theories.\n\ -\n\ -none \n\ -+ Disable model-based quantifier instantiation.\n\ -\n\ -gen-ev \n\ -+ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\ - model finding paper based on generalizing evaluations.\n\ -\n\ -fmc-interval \n\ -+ Same as default, but with intervals for models of integer functions.\n\ -\n\ -abs \n\ -+ Use abstract MBQI algorithm (uses disjoint sets). \n\ -\n\ -"; -static const std::string qcfWhenModeHelp = "\ -Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\ -\n\ -default \n\ -+ Default, apply conflict finding at full effort.\n\ -\n\ -last-call \n\ -+ Apply conflict finding at last call, after theory combination and \n\ - and all theories report sat. \n\ -\n\ -std \n\ -+ Apply conflict finding at standard effort.\n\ -\n\ -std-h \n\ -+ Apply conflict finding at standard effort when heuristic says to. \n\ -\n\ -"; -static const std::string qcfModeHelp = "\ -Quantifier conflict find modes currently supported by the --quant-cf option:\n\ -\n\ -prop-eq \n\ -+ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\ -\n\ -conflict \n\ -+ Apply QCF algorithm to find conflicts only.\n\ -\n\ -partial \n\ -+ Apply QCF algorithm to instantiate heuristically as well. \n\ -\n\ -mc \n\ -+ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\ -\n\ -"; -static const std::string userPatModeHelp = "\ -User pattern modes currently supported by the --user-pat option:\n\ -\n\ -trust \n\ -+ When provided, use only user-provided patterns for a quantified formula.\n\ -\n\ -use \n\ -+ Use both user-provided and auto-generated patterns when patterns\n\ - are provided for a quantified formula.\n\ -\n\ -resort \n\ -+ Use user-provided patterns only after auto-generated patterns saturate.\n\ -\n\ -ignore \n\ -+ Ignore user-provided patterns. \n\ -\n\ -interleave \n\ -+ Alternate between use/resort. \n\ -\n\ -"; -static const std::string triggerSelModeHelp = "\ -Trigger selection modes currently supported by the --trigger-sel option:\n\ -\n\ -default \n\ -+ Default, consider all subterms of quantified formulas for trigger selection.\n\ -\n\ -min \n\ -+ Consider only minimal subterms that meet criteria for triggers.\n\ -\n\ -max \n\ -+ Consider only maximal subterms that meet criteria for triggers. \n\ -\n\ -"; -static const std::string prenexQuantModeHelp = "\ -Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ -\n\ -default \n\ -+ Default, prenex all nested quantifiers except those with user patterns.\n\ -\n\ -all \n\ -+ Prenex all nested quantifiers.\n\ -\n\ -none \n\ -+ Do no prenex nested quantifiers. \n\ -\n\ -"; -static const std::string cegqiFairModeHelp = "\ -Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\ -\n\ -uf-dt-size \n\ -+ Enforce fairness using an uninterpreted function for datatypes size.\n\ -\n\ -default | dt-size \n\ -+ Default, enforce fairness using size theory operator.\n\ -\n\ -dt-height-bound \n\ -+ Enforce fairness by height bound predicate.\n\ -\n\ -none \n\ -+ Do not enforce fairness. \n\ -\n\ -"; -static const std::string termDbModeHelp = "\ -Modes for term database, supported by --term-db-mode:\n\ -\n\ -all \n\ -+ Quantifiers module considers all ground terms.\n\ -\n\ -relevant \n\ -+ Quantifiers module considers only ground terms connected to current assertions. \n\ -\n\ -"; -static const std::string iteLiftQuantHelp = "\ -Modes for term database, supported by --ite-lift-quant:\n\ -\n\ -none \n\ -+ Do not lift if-then-else in quantified formulas.\n\ -\n\ -simple \n\ -+ Lift if-then-else in quantified formulas if results in smaller term size.\n\ -\n\ -all \n\ -+ Lift if-then-else in quantified formulas. \n\ -\n\ -"; -static const std::string sygusInvTemplHelp = "\ -Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\ -\n\ -none \n\ -+ Synthesize invariant directly.\n\ -\n\ -pre \n\ -+ Synthesize invariant based on weakening of precondition .\n\ -\n\ -post \n\ -+ Synthesize invariant based on strengthening of postcondition. \n\ -\n\ -"; -static const std::string macrosQuantHelp = "\ -Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\ -\n\ -all \n\ -+ Infer definitions for functions, including those containing quantified formulas.\n\ -\n\ -ground (default) \n\ -+ Only infer ground definitions for functions.\n\ -\n\ -ground-uf \n\ -+ Only infer ground definitions for functions that result in triggers for all free variables.\n\ -\n\ -"; - -inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "pre-full") { - return INST_WHEN_PRE_FULL; - } else if(optarg == "full") { - return INST_WHEN_FULL; - } else if(optarg == "full-delay") { - return INST_WHEN_FULL_DELAY; - } else if(optarg == "full-last-call") { - return INST_WHEN_FULL_LAST_CALL; - } else if(optarg == "full-delay-last-call") { - return INST_WHEN_FULL_DELAY_LAST_CALL; - } else if(optarg == "last-call") { - return INST_WHEN_LAST_CALL; - } else if(optarg == "help") { - puts(instWhenHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --inst-when: `") + - optarg + "'. Try --inst-when help."); - } -} - -inline void checkInstWhenMode(std::string option, InstWhenMode mode, SmtEngine* smt) throw(OptionException) { - if(mode == INST_WHEN_PRE_FULL) { - throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release."); - } -} - -inline LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "none") { - return LITERAL_MATCH_NONE; - } else if(optarg == "predicate") { - return LITERAL_MATCH_PREDICATE; - } else if(optarg == "equality") { - return LITERAL_MATCH_EQUALITY; - } else if(optarg == "help") { - puts(literalMatchHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --literal-matching: `") + - optarg + "'. Try --literal-matching help."); - } -} - -inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, SmtEngine* smt) throw(OptionException) { - if(mode == LITERAL_MATCH_EQUALITY) { - throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release."); - } -} - -inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "gen-ev") { - return MBQI_GEN_EVAL; - } else if(optarg == "none") { - return MBQI_NONE; - } else if(optarg == "default" || optarg == "fmc") { - return MBQI_FMC; - } else if(optarg == "fmc-interval") { - return MBQI_FMC_INTERVAL; - } else if(optarg == "abs") { - return MBQI_ABS; - } else if(optarg == "trust") { - return MBQI_TRUST; - } else if(optarg == "help") { - puts(mbqiModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --mbqi: `") + - optarg + "'. Try --mbqi help."); - } -} - -inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) throw(OptionException) { - -} - -inline QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default") { - return QCF_WHEN_MODE_DEFAULT; - } else if(optarg == "last-call") { - return QCF_WHEN_MODE_LAST_CALL; - } else if(optarg == "std") { - return QCF_WHEN_MODE_STD; - } else if(optarg == "std-h") { - return QCF_WHEN_MODE_STD_H; - } else if(optarg == "help") { - puts(qcfWhenModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --quant-cf-when: `") + - optarg + "'. Try --quant-cf-when help."); - } -} -inline QcfMode stringToQcfMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "conflict") { - return QCF_CONFLICT_ONLY; - } else if(optarg == "default" || optarg == "prop-eq") { - return QCF_PROP_EQ; - } else if(optarg == "partial") { - return QCF_PARTIAL; - } else if(optarg == "mc" ) { - return QCF_MC; - } else if(optarg == "help") { - puts(qcfModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --quant-cf-mode: `") + - optarg + "'. Try --quant-cf-mode help."); - } -} - -inline UserPatMode stringToUserPatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "use") { - return USER_PAT_MODE_USE; - } else if(optarg == "default" || optarg == "trust") { - return USER_PAT_MODE_TRUST; - } else if(optarg == "resort") { - return USER_PAT_MODE_RESORT; - } else if(optarg == "ignore") { - return USER_PAT_MODE_IGNORE; - } else if(optarg == "interleave") { - return USER_PAT_MODE_INTERLEAVE; - } else if(optarg == "help") { - puts(userPatModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --user-pat: `") + - optarg + "'. Try --user-pat help."); - } -} - -inline TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default" || optarg == "all" ) { - return TRIGGER_SEL_DEFAULT; - } else if(optarg == "min") { - return TRIGGER_SEL_MIN; - } else if(optarg == "max") { - return TRIGGER_SEL_MAX; - } else if(optarg == "help") { - puts(triggerSelModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --trigger-sel: `") + - optarg + "'. Try --trigger-sel help."); - } -} - -inline PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default" ) { - return PRENEX_NO_USER_PAT; - } else if(optarg == "all") { - return PRENEX_ALL; - } else if(optarg == "none") { - return PRENEX_NONE; - } else if(optarg == "help") { - puts(prenexQuantModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --prenex-quant: `") + - optarg + "'. Try --prenex-quant help."); - } -} - -inline CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "uf-dt-size" ) { - return CEGQI_FAIR_UF_DT_SIZE; - } else if(optarg == "default" || optarg == "dt-size") { - return CEGQI_FAIR_DT_SIZE; - } else if(optarg == "dt-height-bound" ){ - return CEGQI_FAIR_DT_HEIGHT_PRED; - } else if(optarg == "none") { - return CEGQI_FAIR_NONE; - } else if(optarg == "help") { - puts(cegqiFairModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --cegqi-fair: `") + - optarg + "'. Try --cegqi-fair help."); - } -} - -inline TermDbMode stringToTermDbMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "all" ) { - return TERM_DB_ALL; - } else if(optarg == "relevant") { - return TERM_DB_RELEVANT; - } else if(optarg == "help") { - puts(termDbModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --term-db-mode: `") + - optarg + "'. Try --term-db-mode help."); - } -} - -inline IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "all" ) { - return ITE_LIFT_QUANT_MODE_ALL; - } else if(optarg == "simple") { - return ITE_LIFT_QUANT_MODE_SIMPLE; - } else if(optarg == "none") { - return ITE_LIFT_QUANT_MODE_NONE; - } else if(optarg == "help") { - puts(iteLiftQuantHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --ite-lift-quant: `") + - optarg + "'. Try --ite-lift-quant help."); - } -} - -inline SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "none" ) { - return SYGUS_INV_TEMPL_MODE_NONE; - } else if(optarg == "pre") { - return SYGUS_INV_TEMPL_MODE_PRE; - } else if(optarg == "post") { - return SYGUS_INV_TEMPL_MODE_POST; - } else if(optarg == "help") { - puts(sygusInvTemplHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --sygus-inv-templ: `") + - optarg + "'. Try --sygus-inv-templ help."); - } -} - -inline MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "all" ) { - return MACROS_QUANT_MODE_ALL; - } else if(optarg == "ground") { - return MACROS_QUANT_MODE_GROUND; - } else if(optarg == "ground-uf") { - return MACROS_QUANT_MODE_GROUND_UF; - } else if(optarg == "help") { - puts(macrosQuantHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --macros-quant-mode: `") + - optarg + "'. Try --macros-quant-mode help."); - } -} - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H */ diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index ca5d23cd1..b6256980a 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -13,14 +13,15 @@ ** **/ +#include "theory/quantifiers/quant_conflict_find.h" + #include <vector> -#include "theory/quantifiers/quant_conflict_find.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/quant_util.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index ef5b71f9d..8c6b30124 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -13,7 +13,8 @@ **/ #include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/options.h" + +#include "options/quantifiers_options.h" #include "theory/quantifiers/term_database.h" using namespace std; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 1e2ac21a0..0afc8b1bb 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -13,9 +13,10 @@ **/ #include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" + +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" using namespace std; diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index a70d36ac0..4c8050239 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -15,13 +15,14 @@ **/ #include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/quant_util.h" + +#include "options/quantifiers_options.h" #include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/options.h" #include "theory/quantifiers/inst_match_generator.h" -#include "theory/theory_engine.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database.h" +#include "theory/theory_engine.h" using namespace CVC4; using namespace std; diff --git a/src/theory/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp index 12b16ef06..4c8e24d08 100644 --- a/src/theory/quantifiers/symmetry_breaking.cpp +++ b/src/theory/quantifiers/symmetry_breaking.cpp @@ -13,15 +13,16 @@ ** **/ +#include "theory/quantifiers/symmetry_breaking.h" + #include <vector> -#include "theory/quantifiers/symmetry_breaking.h" -#include "theory/rewriter.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" +#include "theory/sort_inference.h" #include "theory/theory_engine.h" -#include "util/sort_inference.h" -#include "theory/uf/theory_uf_strong_solver.h" #include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_strong_solver.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index c3ba92214..43e5ec765 100644 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -17,20 +17,19 @@ #ifndef __CVC4__QUANT_SYMMETRY_BREAKING_H #define __CVC4__QUANT_SYMMETRY_BREAKING_H -#include "theory/theory.h" - #include <iostream> +#include <map> #include <string> #include <vector> -#include <map> -#include "expr/node.h" -#include "expr/type_node.h" -#include "util/sort_inference.h" +#include "context/cdchunk_list.h" +#include "context/cdhashmap.h" #include "context/context.h" #include "context/context_mm.h" -#include "context/cdhashmap.h" -#include "context/cdchunk_list.h" +#include "expr/node.h" +#include "expr/type_node.h" +#include "theory/sort_inference.h" +#include "theory/theory.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 724f16947..f3bbc65cc 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -13,22 +13,23 @@ **/ #include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/trigger.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/theory_quantifiers.h" -#include "util/datatype.h" + +#include "expr/datatype.h" +#include "options/quantifiers_options.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fun_def_engine.h" +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" //for sygus +#include "smt/smt_engine_scope.h" #include "theory/bv/theory_bv_utils.h" #include "util/bitvector.h" -#include "smt/smt_engine_scope.h" using namespace std; using namespace CVC4; @@ -2807,4 +2808,3 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node > out << n; } } - diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 48891732b..e9ff60137 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -14,17 +14,18 @@ ** Implementation of the theory of quantifiers. **/ - #include "theory/quantifiers/theory_quantifiers.h" -#include "theory/valuation.h" -#include "theory/quantifiers_engine.h" + + +#include "base/cvc4_assert.h" +#include "expr/kind.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/model_engine.h" -#include "expr/kind.h" -#include "util/cvc4_assert.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" +#include "theory/valuation.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 0f16f0e80..98f486145 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -19,15 +19,15 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#include "context/cdhashmap.h" -#include "theory/theory.h" -#include "util/hash.h" -#include "util/statistics_registry.h" - #include <ext/hash_set> #include <iostream> #include <map> +#include "context/cdhashmap.h" +#include "expr/statistics_registry.h" +#include "theory/theory.h" +#include "util/hash.h" + namespace CVC4 { class TheoryEngine; diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 3ce0250fe..1fb8ddaf9 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -19,7 +19,7 @@ #ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H #define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H -#include "util/matcher.h" +#include "expr/matcher.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index fdfa77b02..9aee18317 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -13,13 +13,14 @@ **/ #include "theory/quantifiers/trigger.h" -#include "theory/theory_engine.h" -#include "theory/quantifiers_engine.h" + +#include "options/quantifiers_options.h" #include "theory/quantifiers/candidate_generator.h" -#include "theory/uf/equality_engine.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/inst_match_generator.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory_engine.h" +#include "theory/uf/equality_engine.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2c4c58900..e46c59dc0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -13,34 +13,35 @@ **/ #include "theory/quantifiers_engine.h" -#include "theory/theory_engine.h" -#include "theory/uf/theory_uf_strong_solver.h" -#include "theory/uf/equality_engine.h" + +#include "options/quantifiers_options.h" +#include "options/uf_options.h" #include "theory/arrays/theory_arrays.h" #include "theory/datatypes/theory_datatypes.h" -#include "theory/quantifiers/quantifiers_rewriter.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/instantiation_engine.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/alpha_equivalence.h" +#include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/bounded_integers.h" -#include "theory/quantifiers/rewrite_engine.h" -#include "theory/quantifiers/quant_conflict_find.h" -#include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/local_theory_ext.h" -#include "theory/quantifiers/relevant_domain.h" -#include "theory/quantifiers/alpha_equivalence.h" -#include "theory/uf/options.h" -#include "theory/uf/theory_uf.h" +#include "theory/quantifiers/conjecture_generator.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/fun_def_engine.h" -#include "theory/quantifiers/quant_equality_engine.h" -#include "theory/quantifiers/inst_strategy_e_matching.h" #include "theory/quantifiers/inst_strategy_cbqi.h" +#include "theory/quantifiers/inst_strategy_e_matching.h" +#include "theory/quantifiers/instantiation_engine.h" +#include "theory/quantifiers/local_theory_ext.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/quant_conflict_find.h" +#include "theory/quantifiers/quant_equality_engine.h" +#include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/rewrite_engine.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" +#include "theory/theory_engine.h" +#include "theory/uf/equality_engine.h" +#include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_strong_solver.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index bbf3fad61..ba41b2ca3 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -17,20 +17,19 @@ #ifndef __CVC4__THEORY__QUANTIFIERS_ENGINE_H #define __CVC4__THEORY__QUANTIFIERS_ENGINE_H -#include "theory/theory.h" -#include "util/hash.h" -#include "theory/quantifiers/inst_match.h" -#include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/modes.h" -#include "expr/attribute.h" - -#include "util/statistics_registry.h" - #include <ext/hash_set> #include <iostream> #include <map> + #include "context/cdchunk_list.h" #include "context/cdhashset.h" +#include "expr/attribute.h" +#include "expr/statistics_registry.h" +#include "options/quantifiers_modes.h" +#include "theory/quantifiers/inst_match.h" +#include "theory/quantifiers/quant_util.h" +#include "theory/theory.h" +#include "util/hash.h" namespace CVC4 { diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 842df69c5..758f4a913 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -15,11 +15,12 @@ ** \todo document this file **/ -#include "theory/theory.h" #include "theory/rewriter.h" + +#include "expr/resource_manager.h" +#include "theory/theory.h" #include "theory/rewriter_tables.h" #include "smt/smt_engine_scope.h" -#include "util/resource_manager.h" using namespace std; diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 44035e7d9..5ad6adca8 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -21,8 +21,6 @@ #include "expr/node.h" #include "util/unsafe_interrupt_exception.h" -//#include "expr/attribute.h" - namespace CVC4 { namespace theory { diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h index 86f12082a..f293d0714 100644 --- a/src/theory/sets/expr_patterns.h +++ b/src/theory/sets/expr_patterns.h @@ -18,6 +18,8 @@ #pragma once +#include "expr/node.h" + namespace CVC4 { namespace expr { namespace pattern { diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 39e7883c6..a43902b1b 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -18,7 +18,7 @@ properties check propagate constant EMPTYSET \ ::CVC4::EmptySet \ ::CVC4::EmptySetHashFunction \ - "util/emptyset.h" \ + "expr/emptyset.h" \ "the empty set constant; payload is an instance of the CVC4::EmptySet class" # the type diff --git a/src/theory/sets/options b/src/theory/sets/options deleted file mode 100644 index 6f4b5129d..000000000 --- a/src/theory/sets/options +++ /dev/null @@ -1,20 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module SETS "theory/sets/options.h" Sets - -option setsPropagate --sets-propagate bool :default true - determines whether to propagate learnt facts to Theory Engine / SAT solver - -option setsEagerLemmas --sets-eager-lemmas bool :default true - add lemmas even at regular effort - -expert-option setsCare1 --sets-care1 bool :default false - generate one lemma at a time for care graph - -option setsPropFull --sets-prop-full bool :default true - additional propagation at full effort - -endmodule diff --git a/src/theory/sets/options_handlers.h b/src/theory/sets/options_handlers.h deleted file mode 100644 index f0af6e7a3..000000000 --- a/src/theory/sets/options_handlers.h +++ /dev/null @@ -1,31 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Kshitij Bansal - ** 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_private.h" - -#ifndef __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H - -namespace CVC4 { -namespace theory { -namespace sets { - -}/* CVC4::theory::sets namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 4054f3e21..f200397bc 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -14,18 +14,17 @@ ** Sets theory implementation. **/ +#include "theory/sets/theory_sets_private.h" + #include <boost/foreach.hpp> -#include "theory/theory_model.h" +#include "expr/emptyset.h" +#include "expr/result.h" +#include "options/sets_options.h" +#include "theory/sets/expr_patterns.h" // ONLY included here #include "theory/sets/scrutinize.h" #include "theory/sets/theory_sets.h" -#include "theory/sets/theory_sets_private.h" - -#include "theory/sets/options.h" -#include "theory/sets/expr_patterns.h" // ONLY included here - -#include "util/emptyset.h" -#include "util/result.h" +#include "theory/theory_model.h" using namespace std; using namespace CVC4::expr::pattern; diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index e01a407e1..fd45cca15 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -17,11 +17,11 @@ #pragma once +#include "context/cdhashset.h" #include "expr/node.h" +#include "expr/statistics_registry.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" -#include "util/statistics_registry.h" -#include "context/cdhashset.h" namespace CVC4 { diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp new file mode 100644 index 000000000..a26c0e9d7 --- /dev/null +++ b/src/theory/sort_inference.cpp @@ -0,0 +1,759 @@ +/********************* */ +/*! \file sort_inference.cpp + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): Kshitij Bansal + ** 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 Sort inference module + ** + ** This class implements sort inference, based on a simple algorithm: + ** First, we assume all functions and predicates have distinct uninterpreted types. + ** One pass is made through the input assertions, while a union-find data structure + ** maintains necessary information regarding constraints on these types. + **/ + +#include "theory/sort_inference.h" + +#include <vector> + +#include "options/quantifiers_options.h" +#include "options/smt_options.h" +#include "options/uf_options.h" +#include "proof/proof_manager.h" +#include "theory/rewriter.h" + +using namespace std; + +namespace CVC4 { + +void SortInference::UnionFind::print(const char * c){ + for( std::map< int, int >::iterator it = d_eqc.begin(); it != d_eqc.end(); ++it ){ + Trace(c) << "s_" << it->first << " = s_" << it->second << ", "; + } + for( unsigned i=0; i<d_deq.size(); i++ ){ + Trace(c) << "s_" << d_deq[i].first << " != s_" << d_deq[i].second << ", "; + } + Trace(c) << std::endl; +} + +void SortInference::UnionFind::set( UnionFind& c ) { + clear(); + for( std::map< int, int >::iterator it = c.d_eqc.begin(); it != c.d_eqc.end(); ++it ){ + d_eqc[ it->first ] = it->second; + } + d_deq.insert( d_deq.end(), c.d_deq.begin(), c.d_deq.end() ); +} + +int SortInference::UnionFind::getRepresentative( int t ){ + std::map< int, int >::iterator it = d_eqc.find( t ); + if( it==d_eqc.end() || it->second==t ){ + return t; + }else{ + int rt = getRepresentative( it->second ); + d_eqc[t] = rt; + return rt; + } +} + +void SortInference::UnionFind::setEqual( int t1, int t2 ){ + if( t1!=t2 ){ + int rt1 = getRepresentative( t1 ); + int rt2 = getRepresentative( t2 ); + if( rt1>rt2 ){ + d_eqc[rt1] = rt2; + }else{ + d_eqc[rt2] = rt1; + } + } +} + +bool SortInference::UnionFind::isValid() { + for( unsigned i=0; i<d_deq.size(); i++ ){ + if( areEqual( d_deq[i].first, d_deq[i].second ) ){ + return false; + } + } + return true; +} + + +void SortInference::recordSubsort( TypeNode tn, int s ){ + s = d_type_union_find.getRepresentative( s ); + if( std::find( d_sub_sorts.begin(), d_sub_sorts.end(), s )==d_sub_sorts.end() ){ + d_sub_sorts.push_back( s ); + d_type_sub_sorts[tn].push_back( s ); + } +} + +void SortInference::printSort( const char* c, int t ){ + int rt = d_type_union_find.getRepresentative( t ); + if( d_type_types.find( rt )!=d_type_types.end() ){ + Trace(c) << d_type_types[rt]; + }else{ + Trace(c) << "s_" << rt; + } +} + +void SortInference::reset() { + d_sub_sorts.clear(); + d_non_monotonic_sorts.clear(); + d_type_sub_sorts.clear(); + //reset info + sortCount = 1; + d_type_union_find.clear(); + d_type_types.clear(); + d_id_for_types.clear(); + d_op_return_types.clear(); + d_op_arg_types.clear(); + d_var_types.clear(); + //for rewriting + d_symbol_map.clear(); + d_const_map.clear(); +} + +bool SortInference::simplify( std::vector< Node >& assertions ){ + Trace("sort-inference") << "Calculating sort inference..." << std::endl; + //process all assertions + for( unsigned i=0; i<assertions.size(); i++ ){ + Trace("sort-inference-debug") << "Process " << assertions[i] << std::endl; + std::map< Node, Node > var_bound; + process( assertions[i], var_bound ); + } + for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ + Trace("sort-inference") << it->first << " : "; + TypeNode retTn = it->first.getType(); + if( !d_op_arg_types[ it->first ].empty() ){ + Trace("sort-inference") << "( "; + for( size_t i=0; i<d_op_arg_types[ it->first ].size(); i++ ){ + recordSubsort( retTn[i], d_op_arg_types[ it->first ][i] ); + printSort( "sort-inference", d_op_arg_types[ it->first ][i] ); + Trace("sort-inference") << " "; + } + Trace("sort-inference") << ") -> "; + retTn = retTn[(int)retTn.getNumChildren()-1]; + } + recordSubsort( retTn, it->second ); + printSort( "sort-inference", it->second ); + Trace("sort-inference") << std::endl; + } + for( std::map< Node, std::map< Node, int > >::iterator it = d_var_types.begin(); it != d_var_types.end(); ++it ){ + Trace("sort-inference") << "Quantified formula : " << it->first << " : " << std::endl; + for( unsigned i=0; i<it->first[0].getNumChildren(); i++ ){ + recordSubsort( it->first[0][i].getType(), it->second[it->first[0][i]] ); + printSort( "sort-inference", it->second[it->first[0][i]] ); + Trace("sort-inference") << std::endl; + } + Trace("sort-inference") << std::endl; + } + + if( !options::ufssSymBreak() ){ + bool rewritten = false; + //determine monotonicity of sorts + for( unsigned i=0; i<assertions.size(); i++ ){ + Trace("sort-inference-debug") << "Process monotonicity for " << assertions[i] << std::endl; + std::map< Node, Node > var_bound; + processMonotonic( assertions[i], true, true, var_bound ); + } + + Trace("sort-inference") << "We have " << d_sub_sorts.size() << " sub-sorts : " << std::endl; + for( unsigned i=0; i<d_sub_sorts.size(); i++ ){ + printSort( "sort-inference", d_sub_sorts[i] ); + if( d_type_types.find( d_sub_sorts[i] )!=d_type_types.end() ){ + Trace("sort-inference") << " is interpreted." << std::endl; + }else if( d_non_monotonic_sorts.find( d_sub_sorts[i] )==d_non_monotonic_sorts.end() ){ + Trace("sort-inference") << " is monotonic." << std::endl; + }else{ + Trace("sort-inference") << " is not monotonic." << std::endl; + } + } + + //simplify all assertions by introducing new symbols wherever necessary + for( unsigned i=0; i<assertions.size(); i++ ){ + Node prev = assertions[i]; + std::map< Node, Node > var_bound; + Trace("sort-inference-debug") << "Rewrite " << assertions[i] << std::endl; + Node curr = simplify( assertions[i], var_bound ); + Trace("sort-inference-debug") << "Done." << std::endl; + if( curr!=assertions[i] ){ + curr = theory::Rewriter::rewrite( curr ); + rewritten = true; + Trace("sort-inference-rewrite") << assertions << std::endl; + Trace("sort-inference-rewrite") << " --> " << curr << std::endl; + PROOF( ProofManager::currentPM()->addDependence(curr, assertions[i]); ); + assertions[i] = curr; + } + } + //now, ensure constants are distinct + for( std::map< TypeNode, std::map< Node, Node > >::iterator it = d_const_map.begin(); it != d_const_map.end(); ++it ){ + std::vector< Node > consts; + for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + consts.push_back( it2->second ); + } + //TODO: add lemma enforcing introduced constants to be distinct + } + + //enforce constraints based on monotonicity + for( std::map< TypeNode, std::vector< int > >::iterator it = d_type_sub_sorts.begin(); it != d_type_sub_sorts.end(); ++it ){ + int nmonSort = -1; + for( unsigned i=0; i<it->second.size(); i++ ){ + if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ + nmonSort = it->second[i]; + break; + } + } + if( nmonSort!=-1 ){ + std::vector< Node > injections; + TypeNode base_tn = getOrCreateTypeForId( nmonSort, it->first ); + for( unsigned i=0; i<it->second.size(); i++ ){ + if( it->second[i]!=nmonSort ){ + TypeNode new_tn = getOrCreateTypeForId( it->second[i], it->first ); + //make injection to nmonSort + Node a1 = mkInjection( new_tn, base_tn ); + injections.push_back( a1 ); + if( d_non_monotonic_sorts.find( it->second[i] )!=d_non_monotonic_sorts.end() ){ + //also must make injection from nmonSort to this + Node a2 = mkInjection( base_tn, new_tn ); + injections.push_back( a2 ); + } + } + } + Trace("sort-inference-rewrite") << "Add the following injections for " << it->first << " to ensure consistency wrt non-monotonic sorts : " << std::endl; + for( unsigned j=0; j<injections.size(); j++ ){ + Trace("sort-inference-rewrite") << " " << injections[j] << std::endl; + } + assertions.insert( assertions.end(), injections.begin(), injections.end() ); + if( !injections.empty() ){ + rewritten = true; + } + } + } + //no sub-sort information is stored + reset(); + return rewritten; + } + /* + else if( !options::ufssSymBreak() ){ + //just add the unit lemmas between constants + std::map< TypeNode, std::map< int, Node > > constants; + for( std::map< Node, int >::iterator it = d_op_return_types.begin(); it != d_op_return_types.end(); ++it ){ + int rt = d_type_union_find.getRepresentative( it->second ); + if( d_op_arg_types[ it->first ].empty() ){ + TypeNode tn = it->first.getType(); + if( constants[ tn ].find( rt )==constants[ tn ].end() ){ + constants[ tn ][ rt ] = it->first; + } + } + } + //add unit lemmas for each constant + for( std::map< TypeNode, std::map< int, Node > >::iterator it = constants.begin(); it != constants.end(); ++it ){ + Node first_const; + for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + if( first_const.isNull() ){ + first_const = it2->second; + }else{ + Node eq = first_const.eqNode( it2->second ); + //eq = Rewriter::rewrite( eq ); + Trace("sort-inference-lemma") << "Sort inference lemma : " << eq << std::endl; + assertions.push_back( eq ); + } + } + } + } + */ + initialSortCount = sortCount; + return false; +} + +void SortInference::setEqual( int t1, int t2 ){ + if( t1!=t2 ){ + int rt1 = d_type_union_find.getRepresentative( t1 ); + int rt2 = d_type_union_find.getRepresentative( t2 ); + if( rt1!=rt2 ){ + Trace("sort-inference-debug") << "Set equal : "; + printSort( "sort-inference-debug", rt1 ); + Trace("sort-inference-debug") << " "; + printSort( "sort-inference-debug", rt2 ); + Trace("sort-inference-debug") << std::endl; + /* + d_type_eq_class[rt1].insert( d_type_eq_class[rt1].end(), d_type_eq_class[rt2].begin(), d_type_eq_class[rt2].end() ); + d_type_eq_class[rt2].clear(); + Trace("sort-inference-debug") << "EqClass : { "; + for( int i=0; i<(int)d_type_eq_class[rt1].size(); i++ ){ + Trace("sort-inference-debug") << d_type_eq_class[rt1][i] << ", "; + } + Trace("sort-inference-debug") << "}" << std::endl; + */ + if( rt2>rt1 ){ + //swap + int swap = rt1; + rt1 = rt2; + rt2 = swap; + } + std::map< int, TypeNode >::iterator it1 = d_type_types.find( rt1 ); + if( it1!=d_type_types.end() ){ + if( d_type_types.find( rt2 )==d_type_types.end() ){ + d_type_types[rt2] = it1->second; + d_type_types.erase( rt1 ); + }else{ + Trace("sort-inference-debug") << "...fail : associated with types " << d_type_types[rt1] << " and " << d_type_types[rt2] << std::endl; + return; + } + } + d_type_union_find.d_eqc[rt1] = rt2; + } + } +} + +int SortInference::getIdForType( TypeNode tn ){ + //register the return type + std::map< TypeNode, int >::iterator it = d_id_for_types.find( tn ); + if( it==d_id_for_types.end() ){ + int sc = sortCount; + d_type_types[ sortCount ] = tn; + d_id_for_types[ tn ] = sortCount; + sortCount++; + return sc; + }else{ + return it->second; + } +} + +int SortInference::process( Node n, std::map< Node, Node >& var_bound ){ + //add to variable bindings + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + if( d_var_types.find( n )!=d_var_types.end() ){ + return getIdForType( n.getType() ); + }else{ + for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + //apply sort inference to quantified variables + d_var_types[n][ n[0][i] ] = sortCount; + sortCount++; + + //type of the quantified variable must be the same + var_bound[ n[0][i] ] = n; + } + } + } + + //process children + std::vector< Node > children; + std::vector< int > child_types; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + bool processChild = true; + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1; + } + if( processChild ){ + children.push_back( n[i] ); + child_types.push_back( process( n[i], var_bound ) ); + } + } + + //remove from variable bindings + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + //erase from variable bound + for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + var_bound.erase( n[0][i] ); + } + } + Trace("sort-inference-debug") << "...Process " << n << std::endl; + + int retType; + if( n.getKind()==kind::EQUAL ){ + Trace("sort-inference-debug") << "For equality " << n << ", set equal types from : " << n[0].getType() << " " << n[1].getType() << std::endl; + //if original types are mixed (e.g. Int/Real), don't commit type equality in either direction + if( n[0].getType()!=n[1].getType() ){ + //for now, assume the original types + for( unsigned i=0; i<2; i++ ){ + int ct = getIdForType( n[i].getType() ); + setEqual( child_types[i], ct ); + } + }else{ + //we only require that the left and right hand side must be equal + setEqual( child_types[0], child_types[1] ); + } + //int eqType = getIdForType( n[0].getType() ); + //setEqual( child_types[0], eqType ); + //setEqual( child_types[1], eqType ); + retType = getIdForType( n.getType() ); + }else if( n.getKind()==kind::APPLY_UF ){ + Node op = n.getOperator(); + TypeNode tn_op = op.getType(); + if( d_op_return_types.find( op )==d_op_return_types.end() ){ + if( n.getType().isBoolean() ){ + //use booleans + d_op_return_types[op] = getIdForType( n.getType() ); + }else{ + //assign arbitrary sort for return type + d_op_return_types[op] = sortCount; + sortCount++; + } + //d_type_eq_class[sortCount].push_back( op ); + //assign arbitrary sort for argument types + for( size_t i=0; i<n.getNumChildren(); i++ ){ + d_op_arg_types[op].push_back( sortCount ); + sortCount++; + } + } + for( size_t i=0; i<n.getNumChildren(); i++ ){ + //the argument of the operator must match the return type of the subterm + if( n[i].getType()!=tn_op[i] ){ + //if type mismatch, assume original types + Trace("sort-inference-debug") << "Argument " << i << " of " << op << " " << n[i] << " has type " << n[i].getType(); + Trace("sort-inference-debug") << ", while operator arg has type " << tn_op[i] << std::endl; + int ct1 = getIdForType( n[i].getType() ); + setEqual( child_types[i], ct1 ); + int ct2 = getIdForType( tn_op[i] ); + setEqual( d_op_arg_types[op][i], ct2 ); + }else{ + setEqual( child_types[i], d_op_arg_types[op][i] ); + } + } + //return type is the return type + retType = d_op_return_types[op]; + }else{ + std::map< Node, Node >::iterator it = var_bound.find( n ); + if( it!=var_bound.end() ){ + Trace("sort-inference-debug") << n << " is a bound variable." << std::endl; + //the return type was specified while binding + retType = d_var_types[it->second][n]; + }else if( n.getKind() == kind::VARIABLE || n.getKind()==kind::SKOLEM ){ + Trace("sort-inference-debug") << n << " is a variable." << std::endl; + if( d_op_return_types.find( n )==d_op_return_types.end() ){ + //assign arbitrary sort + d_op_return_types[n] = sortCount; + sortCount++; + //d_type_eq_class[sortCount].push_back( n ); + } + retType = d_op_return_types[n]; + //}else if( n.isConst() ){ + // Trace("sort-inference-debug") << n << " is a constant." << std::endl; + //can be any type we want + // retType = sortCount; + // sortCount++; + }else{ + Trace("sort-inference-debug") << n << " is a interpreted symbol." << std::endl; + //it is an interpretted term + for( size_t i=0; i<children.size(); i++ ){ + Trace("sort-inference-debug") << children[i] << " forced to have " << children[i].getType() << std::endl; + //must enforce the actual type of the operator on the children + int ct = getIdForType( children[i].getType() ); + setEqual( child_types[i], ct ); + } + //return type must be the actual return type + retType = getIdForType( n.getType() ); + } + } + Trace("sort-inference-debug") << "...Type( " << n << " ) = "; + printSort("sort-inference-debug", retType ); + Trace("sort-inference-debug") << std::endl; + return retType; +} + +void SortInference::processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ) { + Trace("sort-inference-debug") << "...Process monotonic " << pol << " " << hasPol << " " << n << std::endl; + if( n.getKind()==kind::FORALL ){ + for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ + var_bound[n[0][i]] = n; + } + processMonotonic( n[1], pol, hasPol, var_bound ); + for( unsigned i=0; i<n[0].getNumChildren(); i++ ){ + var_bound.erase( n[0][i] ); + } + }else if( n.getKind()==kind::EQUAL ){ + if( !hasPol || pol ){ + for( unsigned i=0; i<2; i++ ){ + if( var_bound.find( n[i] )!=var_bound.end() ){ + int sid = getSortId( var_bound[n[i]], n[i] ); + d_non_monotonic_sorts[sid] = true; + break; + } + } + } + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + bool npol = pol; + bool nhasPol = hasPol; + if( n.getKind()==kind::NOT || ( n.getKind()==kind::IMPLIES && i==0 ) ){ + npol = !npol; + } + if( ( n.getKind()==kind::ITE && i==0 ) || n.getKind()==kind::XOR || n.getKind()==kind::IFF ){ + nhasPol = false; + } + processMonotonic( n[i], npol, nhasPol, var_bound ); + } +} + + +TypeNode SortInference::getOrCreateTypeForId( int t, TypeNode pref ){ + int rt = d_type_union_find.getRepresentative( t ); + if( d_type_types.find( rt )!=d_type_types.end() ){ + return d_type_types[rt]; + }else{ + TypeNode retType; + //see if we can assign pref + if( !pref.isNull() && d_id_for_types.find( pref )==d_id_for_types.end() ){ + retType = pref; + }else{ + //must create new type + std::stringstream ss; + ss << "it_" << t << "_" << pref; + retType = NodeManager::currentNM()->mkSort( ss.str() ); + } + Trace("sort-inference") << "-> Make type " << retType << " to correspond to "; + printSort("sort-inference", t ); + Trace("sort-inference") << std::endl; + d_id_for_types[ retType ] = rt; + d_type_types[ rt ] = retType; + return retType; + } +} + +TypeNode SortInference::getTypeForId( int t ){ + int rt = d_type_union_find.getRepresentative( t ); + if( d_type_types.find( rt )!=d_type_types.end() ){ + return d_type_types[rt]; + }else{ + return TypeNode::null(); + } +} + +Node SortInference::getNewSymbol( Node old, TypeNode tn ){ + if( tn==old.getType() ){ + return old; + }else if( old.isConst() ){ + //must make constant of type tn + if( d_const_map[tn].find( old )==d_const_map[tn].end() ){ + std::stringstream ss; + ss << "ic_" << tn << "_" << old; + d_const_map[tn][ old ] = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "constant created during sort inference" ); //use mkConst??? + } + return d_const_map[tn][ old ]; + }else if( old.getKind()==kind::BOUND_VARIABLE ){ + std::stringstream ss; + ss << "b_" << old; + return NodeManager::currentNM()->mkBoundVar( ss.str(), tn ); + }else{ + std::stringstream ss; + ss << "i_" << old; + return NodeManager::currentNM()->mkSkolem( ss.str(), tn, "created during sort inference" ); + } +} + +Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ + Trace("sort-inference-debug2") << "Simplify " << n << std::endl; + std::vector< Node > children; + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + //recreate based on types of variables + std::vector< Node > new_children; + for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + TypeNode tn = getOrCreateTypeForId( d_var_types[n][ n[0][i] ], n[0][i].getType() ); + Node v = getNewSymbol( n[0][i], tn ); + Trace("sort-inference-debug2") << "Map variable " << n[0][i] << " to " << v << std::endl; + new_children.push_back( v ); + var_bound[ n[0][i] ] = v; + } + children.push_back( NodeManager::currentNM()->mkNode( n[0].getKind(), new_children ) ); + } + + //process children + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + bool childChanged = false; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + bool processChild = true; + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1; + } + if( processChild ){ + Node nc = simplify( n[i], var_bound ); + Trace("sort-inference-debug2") << "Simplify " << i << " " << n[i] << " returned " << nc << std::endl; + children.push_back( nc ); + childChanged = childChanged || nc!=n[i]; + } + } + + //remove from variable bindings + if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ + //erase from variable bound + for( size_t i=0; i<n[0].getNumChildren(); i++ ){ + Trace("sort-inference-debug2") << "Remove bound for " << n[0][i] << std::endl; + var_bound.erase( n[0][i] ); + } + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else if( n.getKind()==kind::EQUAL ){ + TypeNode tn1 = children[0].getType(); + TypeNode tn2 = children[1].getType(); + if( !tn1.isSubtypeOf( tn2 ) && !tn2.isSubtypeOf( tn1 ) ){ + if( children[0].isConst() ){ + children[0] = getNewSymbol( children[0], children[1].getType() ); + }else if( children[1].isConst() ){ + children[1] = getNewSymbol( children[1], children[0].getType() ); + }else{ + Trace("sort-inference-warn") << "Sort inference created bad equality: " << children[0] << " = " << children[1] << std::endl; + Trace("sort-inference-warn") << " Types : " << children[0].getType() << " " << children[1].getType() << std::endl; + Assert( false ); + } + } + return NodeManager::currentNM()->mkNode( kind::EQUAL, children ); + }else if( n.getKind()==kind::APPLY_UF ){ + Node op = n.getOperator(); + if( d_symbol_map.find( op )==d_symbol_map.end() ){ + //make the new operator if necessary + bool opChanged = false; + std::vector< TypeNode > argTypes; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + TypeNode tn = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() ); + argTypes.push_back( tn ); + if( tn!=n[i].getType() ){ + opChanged = true; + } + } + TypeNode retType = getOrCreateTypeForId( d_op_return_types[op], n.getType() ); + if( retType!=n.getType() ){ + opChanged = true; + } + if( opChanged ){ + std::stringstream ss; + ss << "io_" << op; + TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType ); + d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); + Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl; + d_model_replace_f[op] = d_symbol_map[op]; + }else{ + d_symbol_map[op] = op; + } + } + children[0] = d_symbol_map[op]; + //make sure all children have been taken care of + for( size_t i=0; i<n.getNumChildren(); i++ ){ + TypeNode tn = children[i+1].getType(); + TypeNode tna = getTypeForId( d_op_arg_types[op][i] ); + if( tn!=tna ){ + if( n[i].isConst() ){ + children[i+1] = getNewSymbol( n[i], tna ); + }else{ + Trace("sort-inference-warn") << "Sort inference created bad child: " << n << " " << n[i] << " " << tn << " " << tna << std::endl; + Assert( false ); + } + } + } + return NodeManager::currentNM()->mkNode( kind::APPLY_UF, children ); + }else{ + std::map< Node, Node >::iterator it = var_bound.find( n ); + if( it!=var_bound.end() ){ + return it->second; + }else if( n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM ){ + if( d_symbol_map.find( n )==d_symbol_map.end() ){ + TypeNode tn = getOrCreateTypeForId( d_op_return_types[n], n.getType() ); + d_symbol_map[n] = getNewSymbol( n, tn ); + } + return d_symbol_map[n]; + }else if( n.isConst() ){ + //just return n, we will fix at higher scope + return n; + }else{ + if( childChanged ){ + return NodeManager::currentNM()->mkNode( n.getKind(), children ); + }else{ + return n; + } + } + } + +} + +Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) { + std::vector< TypeNode > tns; + tns.push_back( tn1 ); + TypeNode typ = NodeManager::currentNM()->mkFunctionType( tns, tn2 ); + Node f = NodeManager::currentNM()->mkSkolem( "inj", typ, "injection for monotonicity constraint" ); + Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl; + Node v1 = NodeManager::currentNM()->mkBoundVar( "?x", tn1 ); + Node v2 = NodeManager::currentNM()->mkBoundVar( "?y", tn1 ); + Node ret = NodeManager::currentNM()->mkNode( kind::FORALL, + NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, v1, v2 ), + NodeManager::currentNM()->mkNode( kind::OR, + NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v1 ).eqNode( NodeManager::currentNM()->mkNode( kind::APPLY_UF, f, v2 ) ).negate(), + v1.eqNode( v2 ) ) ); + ret = theory::Rewriter::rewrite( ret ); + return ret; +} + +int SortInference::getSortId( Node n ) { + Node op = n.getKind()==kind::APPLY_UF ? n.getOperator() : n; + if( d_op_return_types.find( op )!=d_op_return_types.end() ){ + return d_type_union_find.getRepresentative( d_op_return_types[op] ); + }else{ + return 0; + } +} + +int SortInference::getSortId( Node f, Node v ) { + if( d_var_types.find( f )!=d_var_types.end() ){ + return d_type_union_find.getRepresentative( d_var_types[f][v] ); + }else{ + return 0; + } +} + +void SortInference::setSkolemVar( Node f, Node v, Node sk ){ + Trace("sort-inference-temp") << "Set skolem var for " << f << ", variable " << v << std::endl; + if( isWellSortedFormula( f ) && d_var_types.find( f )==d_var_types.end() ){ + //calculate the sort for variables if not done so already + std::map< Node, Node > var_bound; + process( f, var_bound ); + } + d_op_return_types[sk] = getSortId( f, v ); + Trace("sort-inference-temp") << "Set skolem sort id for " << sk << " to " << d_op_return_types[sk] << std::endl; +} + +bool SortInference::isWellSortedFormula( Node n ) { + if( n.getType().isBoolean() && n.getKind()!=kind::APPLY_UF ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( !isWellSortedFormula( n[i] ) ){ + return false; + } + } + return true; + }else{ + return isWellSorted( n ); + } +} + +bool SortInference::isWellSorted( Node n ) { + if( getSortId( n )==0 ){ + return false; + }else{ + if( n.getKind()==kind::APPLY_UF ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + int s1 = getSortId( n[i] ); + int s2 = d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ); + if( s1!=s2 ){ + return false; + } + if( !isWellSorted( n[i] ) ){ + return false; + } + } + } + return true; + } +} + +void SortInference::getSortConstraints( Node n, UnionFind& uf ) { + if( n.getKind()==kind::APPLY_UF ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + getSortConstraints( n[i], uf ); + uf.setEqual( getSortId( n[i] ), d_type_union_find.getRepresentative( d_op_arg_types[ n.getOperator() ][i] ) ); + } + } +} + +}/* CVC4 namespace */ diff --git a/src/theory/sort_inference.h b/src/theory/sort_inference.h new file mode 100644 index 000000000..4bb1a072e --- /dev/null +++ b/src/theory/sort_inference.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \file sort_inference.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: Morgan Deters + ** 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 Pre-process step for performing sort inference + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SORT_INFERENCE_H +#define __CVC4__SORT_INFERENCE_H + +#include <iostream> +#include <string> +#include <vector> +#include <map> +#include "expr/node.h" +#include "expr/type_node.h" + +namespace CVC4 { + +class SortInference { +private: + //all subsorts + std::vector< int > d_sub_sorts; + std::map< int, bool > d_non_monotonic_sorts; + std::map< TypeNode, std::vector< int > > d_type_sub_sorts; + void recordSubsort( TypeNode tn, int s ); +public: + class UnionFind { + public: + UnionFind(){} + UnionFind( UnionFind& c ){ + set( c ); + } + std::map< int, int > d_eqc; + //pairs that must be disequal + std::vector< std::pair< int, int > > d_deq; + void print(const char * c); + void clear() { d_eqc.clear(); d_deq.clear(); } + void set( UnionFind& c ); + int getRepresentative( int t ); + void setEqual( int t1, int t2 ); + void setDisequal( int t1, int t2 ){ d_deq.push_back( std::pair< int, int >( t1, t2 ) ); } + bool areEqual( int t1, int t2 ) { return getRepresentative( t1 )==getRepresentative( t2 ); } + bool isValid(); + }; +private: + int sortCount; + int initialSortCount; + UnionFind d_type_union_find; + std::map< int, TypeNode > d_type_types; + std::map< TypeNode, int > d_id_for_types; + //for apply uf operators + std::map< Node, int > d_op_return_types; + std::map< Node, std::vector< int > > d_op_arg_types; + //for bound variables + std::map< Node, std::map< Node, int > > d_var_types; + //get representative + void setEqual( int t1, int t2 ); + int getIdForType( TypeNode tn ); + void printSort( const char* c, int t ); + //process + int process( Node n, std::map< Node, Node >& var_bound ); +//for monotonicity inference +private: + void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ); + +//for rewriting +private: + //mapping from old symbols to new symbols + std::map< Node, Node > d_symbol_map; + //mapping from constants to new symbols + std::map< TypeNode, std::map< Node, Node > > d_const_map; + //helper functions for simplify + TypeNode getOrCreateTypeForId( int t, TypeNode pref ); + TypeNode getTypeForId( int t ); + Node getNewSymbol( Node old, TypeNode tn ); + //simplify + Node simplify( Node n, std::map< Node, Node >& var_bound ); + //make injection + Node mkInjection( TypeNode tn1, TypeNode tn2 ); + //reset + void reset(); +public: + SortInference() : sortCount( 1 ){} + ~SortInference(){} + + bool simplify( std::vector< Node >& assertions ); + //get sort id for term n + int getSortId( Node n ); + //get sort id for variable of quantified formula f + int getSortId( Node f, Node v ); + //set that sk is the skolem variable of v for quantifier f + void setSkolemVar( Node f, Node v, Node sk ); +public: + //is well sorted + bool isWellSortedFormula( Node n ); + bool isWellSorted( Node n ); + //get constraints for being well-typed according to computed sub-types + void getSortConstraints( Node n, SortInference::UnionFind& uf ); +public: + //list of all functions and the uninterpreted symbols they were replaced with + std::map< Node, Node > d_model_replace_f; +}; + +} + +#endif diff --git a/src/theory/strings/options b/src/theory/strings/options deleted file mode 100644 index 59a95e5ec..000000000 --- a/src/theory/strings/options +++ /dev/null @@ -1,56 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module STRINGS "theory/strings/options.h" Strings theory - -option stringExp strings-exp --strings-exp bool :default false :read-write - experimental features in the theory of strings - -option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h" - the strategy of LB rule application: 0-lazy, 1-eager, 2-no - -option stdASCII strings-std-ascii --strings-std-ascii bool :default true :predicate options::less_equal(2) :predicate-include "smt/smt_engine.h" - the alphabet contains only characters from the standard ASCII or the extended one - -option stringFMF strings-fmf --strings-fmf bool :default false :read-write - the finite model finding used by the theory of strings - -option stringEager strings-eager --strings-eager bool :default false - strings eager check - -option stringEIT strings-eit --strings-eit bool :default false - the eager intersection used by the theory of strings - -option stringOpt1 strings-opt1 --strings-opt1 bool :default true - internal option1 for strings: normal form - -option stringOpt2 strings-opt2 --strings-opt2 bool :default false - internal option2 for strings: constant regexp splitting - -option stringIgnNegMembership strings-inm --strings-inm bool :default false - internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now) - -#expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 128 :read-write -# the cardinality of the characters used by the theory of strings, default 128 (for standard ASCII) or 256 (for extended ASCII) - -option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true - perform string preprocessing lazily upon assertion -option stringLazyPreproc2 strings-lazy-pp2 --strings-lazy-pp2 bool :default true - perform string preprocessing lazily upon failure to reduce - -option stringLenGeqZ strings-len-geqz --strings-len-geqz bool :default false - strings length greater than zero lemmas - -option stringLenNorm strings-len-norm --strings-len-norm bool :default true - strings length normalization lemma -option stringSplitEmp strings-sp-emp --strings-sp-emp bool :default true - strings split on empty string -option stringInferSym strings-infer-sym --strings-infer-sym bool :default true - strings split on empty string -option stringEagerLen strings-eager-len --strings-eager-len bool :default true - strings eager length lemmas - - -endmodule diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index ac4bddd73..98f03327a 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -15,8 +15,9 @@ **/ #include "theory/strings/regexp_operation.h" + #include "expr/kind.h" -#include "theory/strings/options.h" +#include "options/strings_options.h" namespace CVC4 { namespace theory { diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index d4a3cf9c5..dfd3c4803 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -14,18 +14,19 @@ ** Implementation of the theory of strings. **/ - #include "theory/strings/theory_strings.h" -#include "theory/valuation.h" + +#include <cmath> + #include "expr/kind.h" -#include "theory/rewriter.h" -#include "expr/command.h" -#include "theory/theory_model.h" +#include "options/strings_options.h" #include "smt/logic_exception.h" -#include "theory/strings/options.h" -#include "theory/strings/type_enumerator.h" +#include "smt_util/command.h" +#include "theory/rewriter.h" #include "theory/strings/theory_strings_rewriter.h" -#include <cmath> +#include "theory/strings/type_enumerator.h" +#include "theory/theory_model.h" +#include "theory/valuation.h" using namespace std; using namespace CVC4::context; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 80eb89cc3..a1c93a369 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -15,11 +15,14 @@ **/ #include "theory/strings/theory_strings_preprocess.h" -#include "expr/kind.h" -#include "theory/strings/options.h" -#include "smt/logic_exception.h" + #include <stdint.h> + +#include "expr/kind.h" +#include "options/strings_options.h" #include "proof/proof_manager.h" +#include "smt/logic_exception.h" + namespace CVC4 { namespace theory { diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index e0e295d40..733471288 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -13,11 +13,14 @@ ** ** Implementation of the theory of strings. **/ + #include "theory/strings/theory_strings_rewriter.h" -#include "theory/strings/options.h" -#include "smt/logic_exception.h" + #include <stdint.h> +#include "options/strings_options.h" +#include "smt/logic_exception.h" + using namespace std; using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index 13f3b3b73..aff033338 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -15,7 +15,7 @@ **/ #include "cvc4_private.h" -#include "theory/strings/options.h" +#include "options/strings_options.h" #ifndef __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H #define __CVC4__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 7ece4594d..2aa00a177 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -14,8 +14,9 @@ **/ #include "theory/term_registration_visitor.h" + +#include "options/quantifiers_options.h" #include "theory/theory_engine.h" -#include "theory/quantifiers/options.h" using namespace std; using namespace CVC4; diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 62f2a5ec2..05795ca8f 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -15,12 +15,14 @@ **/ #include "theory/theory.h" -#include "util/cvc4_assert.h" -#include "theory/quantifiers_engine.h" -#include "theory/substitutions.h" #include <vector> +#include "base/cvc4_assert.h" +#include "theory/substitutions.h" +#include "theory/quantifiers_engine.h" + + using namespace std; namespace CVC4 { diff --git a/src/theory/theory.h b/src/theory/theory.h index 2dab434d1..5f4c80cf2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -19,28 +19,26 @@ #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H -#include "expr/node.h" -//#include "expr/attribute.h" -#include "expr/command.h" -#include "smt/logic_request.h" -#include "theory/valuation.h" -#include "theory/output_channel.h" -#include "theory/logic_info.h" -#include "theory/options.h" -#include "theory/theoryof_mode.h" -#include "context/context.h" +#include <ext/hash_set> +#include <iostream> +#include <string> +#include <strings.h> + #include "context/cdlist.h" #include "context/cdo.h" -#include "options/options.h" -#include "util/statistics_registry.h" -#include "util/dump.h" +#include "context/context.h" +#include "expr/node.h" +#include "expr/statistics_registry.h" #include "lib/ffs.h" - -#include <string> -#include <iostream> - -#include <strings.h> -#include <ext/hash_set> +#include "options/options.h" +#include "options/theory_options.h" +#include "options/theoryof_mode.h" +#include "smt/logic_request.h" +#include "smt_util/command.h" +#include "smt_util/dump.h" +#include "theory/logic_info.h" +#include "theory/output_channel.h" +#include "theory/valuation.h" namespace CVC4 { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b5a2a1390..52922e2ca 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -14,51 +14,38 @@ ** The theory engine. **/ -#include <vector> -#include <list> +#include "theory/theory_engine.h" -#include "theory/arith/arith_ite_utils.h" +#include <list> +#include <vector> #include "decision/decision_engine.h" - #include "expr/attribute.h" #include "expr/node.h" #include "expr/node_builder.h" +#include "expr/resource_manager.h" +#include "options/bv_options.h" #include "options/options.h" -#include "util/lemma_output_channel.h" -#include "util/resource_manager.h" - -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "theory/rewriter.h" -#include "theory/theory_traits.h" - -#include "smt/logic_exception.h" - +#include "options/quantifiers_options.h" #include "proof/proof_manager.h" - -#include "util/node_visitor.h" -#include "util/ite_removal.h" - -//#include "theory/ite_simplifier.h" -//#include "theory/ite_compressor.h" +#include "proof/proof_manager.h" +#include "smt/logic_exception.h" +#include "smt_util/ite_removal.h" +#include "smt_util/lemma_output_channel.h" +#include "smt_util/node_visitor.h" +#include "theory/arith/arith_ite_utils.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/ite_utilities.h" -#include "theory/unconstrained_simplifier.h" - -#include "theory/theory_model.h" - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/theory_quantifiers.h" -#include "theory/quantifiers/options.h" -#include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/first_order_model.h" - +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/theory_quantifiers.h" +#include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" +#include "theory/theory.h" +#include "theory/theory_model.h" +#include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" -//#include "theory/rewriterules/efficient_e_matching.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/bv/options.h" - -#include "proof/proof_manager.h" +#include "theory/unconstrained_simplifier.h" using namespace std; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b28a73b9d..0355256a3 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -23,32 +23,32 @@ #include <vector> #include <utility> +#include "base/cvc4_assert.h" +#include "context/cdhashset.h" #include "expr/node.h" -#include "expr/command.h" +#include "expr/statistics_registry.h" +#include "options/options.h" +#include "options/smt_options.h" #include "prop/prop_engine.h" -#include "context/cdhashset.h" -#include "theory/theory.h" +#include "smt_util/command.h" +#include "theory/atom_requests.h" +#include "theory/bv/bv_to_bool.h" +#include "theory/interrupted.h" +#include "theory/quantifiers/quant_conflict_find.h" #include "theory/rewriter.h" -#include "theory/substitutions.h" #include "theory/shared_terms_database.h" +#include "theory/sort_inference.h" +#include "theory/substitutions.h" #include "theory/term_registration_visitor.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" #include "theory/valuation.h" -#include "theory/interrupted.h" -#include "options/options.h" -#include "smt/options.h" -#include "util/statistics_registry.h" -#include "util/cvc4_assert.h" -#include "util/sort_inference.h" #include "util/unsafe_interrupt_exception.h" -#include "theory/quantifiers/quant_conflict_find.h" -#include "theory/uf/equality_engine.h" -#include "theory/bv/bv_to_bool.h" -#include "theory/atom_requests.h" namespace CVC4 { class ResourceManager; - + /** * A pair of a theory and a node. This is used to mark the flow of * propagations between theories. diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 44e4193eb..a39d74bb0 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -11,15 +11,15 @@ ** ** \brief Implementation of model class **/ - #include "theory/theory_model.h" + +#include "options/smt_options.h" +#include "options/uf_options.h" +#include "smt/smt_engine.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" #include "theory/type_enumerator.h" -#include "smt/options.h" -#include "smt/smt_engine.h" #include "theory/uf/theory_uf_model.h" -#include "theory/uf/options.h" using namespace std; using namespace CVC4; diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index e023edadd..fb2c3cd01 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -17,7 +17,7 @@ #ifndef __CVC4__THEORY__THEORY_MODEL_H #define __CVC4__THEORY__THEORY_MODEL_H -#include "util/model.h" +#include "smt_util/model.h" #include "theory/uf/equality_engine.h" #include "theory/rep_set.h" #include "theory/substitutions.h" diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 6fe92eb6e..f493e253e 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -19,16 +19,16 @@ #ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H #define __CVC4__THEORY__THEORY_TEST_UTILS_H -#include "util/cvc4_assert.h" +#include <iostream> +#include <utility> +#include <vector> + +#include "base/cvc4_assert.h" #include "expr/node.h" -#include "theory/output_channel.h" #include "theory/interrupted.h" +#include "theory/output_channel.h" #include "util/unsafe_interrupt_exception.h" -#include <vector> -#include <utility> -#include <iostream> - namespace CVC4 { namespace theory { diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index b052fb58f..b0e7010b7 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -21,8 +21,8 @@ #pragma once +#include "options/theory_options.h" #include "theory/theory.h" -#include "theory/options.h" ${theory_includes} diff --git a/src/theory/theoryof_mode.h b/src/theory/theoryof_mode.h deleted file mode 100644 index c39120216..000000000 --- a/src/theory/theoryof_mode.h +++ /dev/null @@ -1,46 +0,0 @@ -/********************* */ -/*! \file theoryof_mode.h - ** \verbatim - ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters - ** 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 Option selection for theoryOf() operation - ** - ** Option selection for theoryOf() operation. - **/ - -#include "cvc4_public.h" - -#pragma once - -namespace CVC4 { -namespace theory { - -/** How do we associate theories with the terms */ -enum TheoryOfMode { - /** Equality, variables and constants are associated with the types */ - THEORY_OF_TYPE_BASED, - /** Variables are uninterpreted, constants are with the type, equalities prefer parametric */ - THEORY_OF_TERM_BASED -};/* enum TheoryOfMode */ - -inline std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() CVC4_PUBLIC; - -inline std::ostream& operator<<(std::ostream& out, TheoryOfMode m) throw() { - switch(m) { - case THEORY_OF_TYPE_BASED: return out << "THEORY_OF_TYPE_BASED"; - case THEORY_OF_TERM_BASED: return out << "THEORY_OF_TERM_BASED"; - default: return out << "TheoryOfMode!UNKNOWN"; - } - - Unreachable(); -} - -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index d8006a5a4..015cbb288 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -19,10 +19,10 @@ #ifndef __CVC4__THEORY__TYPE_ENUMERATOR_H #define __CVC4__THEORY__TYPE_ENUMERATOR_H -#include "util/exception.h" +#include "base/exception.h" +#include "base/cvc4_assert.h" #include "expr/node.h" #include "expr/type_node.h" -#include "util/cvc4_assert.h" namespace CVC4 { namespace theory { diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index ca2413f90..f0eafed18 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -16,10 +16,10 @@ #include <sstream> +#include "base/cvc4_assert.h" +#include "expr/kind.h" #include "theory/type_enumerator.h" -#include "expr/kind.h" -#include "util/cvc4_assert.h" ${type_enumerator_includes} #line 26 "${template}" diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index a26947ed1..f7f7f9ddd 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -19,20 +19,19 @@ #pragma once -#include <queue> #include <deque> -#include <vector> #include <ext/hash_map> +#include <queue> +#include <vector> -#include "expr/node.h" -#include "expr/kind_map.h" -#include "context/cdo.h" +#include "base/output.h" #include "context/cdhashmap.h" -#include "util/output.h" -#include "util/statistics_registry.h" +#include "context/cdo.h" +#include "expr/kind_map.h" +#include "expr/node.h" +#include "expr/statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory.h" - #include "theory/uf/equality_engine_types.h" namespace CVC4 { diff --git a/src/theory/uf/options b/src/theory/uf/options deleted file mode 100644 index cb6ddc0fa..000000000 --- a/src/theory/uf/options +++ /dev/null @@ -1,42 +0,0 @@ -# -# Option specification file for CVC4 -# See src/options/base_options for a description of this file format -# - -module UF "theory/uf/options.h" Uninterpreted functions theory - -option ufSymmetryBreaker uf-symmetry-breaker --symmetry-breaker bool :read-write :default true - use UF symmetry breaker (Deharbe et al., CADE 2011) - -option condenseFunctionValues condense-function-values --condense-function-values bool :default true - condense models for functions rather than explicitly representing them - -option ufssRegions /--disable-uf-ss-regions bool :default true - disable region-based method for discovering cliques and splits in uf strong solver -option ufssEagerSplits --uf-ss-eager-split bool :default false - add splits eagerly for uf strong solver -option ufssTotality --uf-ss-totality bool :default false - always use totality axioms for enforcing cardinality constraints -option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1 - apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default) -option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false - apply symmetry breaking for totality axioms -option ufssAbortCardinality --uf-ss-abort-card=N int :default -1 - tells the uf strong solver a cardinality to abort at (-1 == no limit, default) -option ufssExplainedCliques --uf-ss-explained-cliques bool :default false - use explained clique lemmas for uf strong solver -option ufssSimpleCliques --uf-ss-simple-cliques bool :default true - always use simple clique lemmas for uf strong solver -option ufssDiseqPropagation --uf-ss-deq-prop bool :default false - eagerly propagate disequalities for uf strong solver -option ufssMode --uf-ss=MODE CVC4::theory::uf::UfssMode :default CVC4::theory::uf::UF_SS_FULL :include "theory/uf/options_handlers.h" :handler CVC4::theory::uf::stringToUfssMode :handler-include "theory/uf/options_handlers.h" - mode of operation for uf strong solver. -option ufssCliqueSplits --uf-ss-clique-splits bool :default false - use cliques instead of splitting on demand to shrink model - -option ufssSymBreak --uf-ss-sym-break bool :default false - finite model finding symmetry breaking techniques -option ufssFairness --uf-ss-fair bool :default true - use fair strategy for finite model finding multiple sorts - -endmodule diff --git a/src/theory/uf/options_handlers.h b/src/theory/uf/options_handlers.h deleted file mode 100644 index 8c072e232..000000000 --- a/src/theory/uf/options_handlers.h +++ /dev/null @@ -1,70 +0,0 @@ -/********************* */ -/*! \file options_handlers.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** 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 Custom handlers and predicates for TheoryUF options - ** - ** Custom handlers and predicates for TheoryUF options. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__OPTIONS_HANDLERS_H -#define __CVC4__THEORY__UF__OPTIONS_HANDLERS_H - -namespace CVC4 { -namespace theory { -namespace uf { - -typedef enum { - /** default, use uf strong solver to find minimal models for uninterpreted sorts */ - UF_SS_FULL, - /** use uf strong solver to shrink model sizes, but do no enforce minimality */ - UF_SS_NO_MINIMAL, - /** do not use uf strong solver */ - UF_SS_NONE, -} UfssMode; - -static const std::string ufssModeHelp = "\ -UF strong solver options currently supported by the --uf-ss option:\n\ -\n\ -full \n\ -+ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\ -\n\ -no-minimal \n\ -+ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\ -\n\ -none \n\ -+ Do not use uf strong solver to shrink model sizes. \n\ -\n\ -"; - -inline UfssMode stringToUfssMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { - if(optarg == "default" || optarg == "full" ) { - return UF_SS_FULL; - } else if(optarg == "no-minimal") { - return UF_SS_NO_MINIMAL; - } else if(optarg == "none") { - return UF_SS_NONE; - } else if(optarg == "help") { - puts(ufssModeHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --uf-ss: `") + - optarg + "'. Try --uf-ss help."); - } -} - -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__UF__OPTIONS_HANDLERS_H */ - diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index d07ef64e0..e49b4652a 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -48,11 +48,11 @@ #include <list> #include <vector> +#include "context/cdlist.h" +#include "context/context.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "context/context.h" -#include "context/cdlist.h" -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 6679b5dc2..31bee316a 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -16,12 +16,13 @@ **/ #include "theory/uf/theory_uf.h" -#include "theory/uf/options.h" -#include "smt/options.h" -#include "theory/quantifiers/options.h" -#include "theory/uf/theory_uf_strong_solver.h" + +#include "options/quantifiers_options.h" +#include "options/smt_options.h" +#include "options/uf_options.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" +#include "theory/uf/theory_uf_strong_solver.h" using namespace std; using namespace CVC4; diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 64f06ceb7..6d0123a19 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -12,16 +12,18 @@ ** \brief Implementation of Theory UF Model **/ +#include "theory/uf/theory_uf_model.h" + +#include <stack> +#include <vector> + #include "expr/attribute.h" +#include "options/quantifiers_options.h" +#include "theory/quantifiers/term_database.h" #include "theory/theory_engine.h" -#include "theory/uf/theory_uf_model.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/options.h" -#include <vector> -#include <stack> #define RECONSIDER_FUNC_DEFAULT_VALUE #define USE_PARTIAL_DEFAULT_VALUES diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 29e726da7..d617207cf 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -13,12 +13,13 @@ **/ #include "theory/uf/theory_uf_strong_solver.h" + +#include "options/uf_options.h" #include "theory/uf/theory_uf.h" #include "theory/uf/equality_engine.h" #include "theory/theory_engine.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" -#include "theory/uf/options.h" #include "theory/theory_model.h" #include "theory/quantifiers/symmetry_breaking.h" diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 3e612ff1f..dd32154d9 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -17,14 +17,12 @@ #ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H #define __CVC4__THEORY_UF_STRONG_SOLVER_H -#include "theory/theory.h" - +#include "context/cdchunk_list.h" +#include "context/cdhashmap.h" #include "context/context.h" #include "context/context_mm.h" -#include "context/cdhashmap.h" -#include "context/cdchunk_list.h" - -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" +#include "theory/theory.h" namespace CVC4 { diff --git a/src/theory/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h index e23c4853d..6c04d66e7 100644 --- a/src/theory/unconstrained_simplifier.h +++ b/src/theory/unconstrained_simplifier.h @@ -24,8 +24,8 @@ #include <utility> #include "expr/node.h" +#include "expr/statistics_registry.h" #include "theory/substitutions.h" -#include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 540ebd8fc..c9bff14a4 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -22,7 +22,7 @@ #define __CVC4__THEORY__VALUATION_H #include "expr/node.h" -#include "theory/theoryof_mode.h" +#include "options/theoryof_mode.h" namespace CVC4 { |