diff options
| author | Tim King <taking@google.com> | 2015-12-14 18:51:40 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2015-12-14 18:51:40 -0800 |
| commit | 90e3b73fbd1b2eb262a7a7e2e72d701c8f9e3600 (patch) | |
| tree | 77af58f4233d766d31e8e032e16cc0b4833d8de2 /src/theory | |
| parent | 157a2ed349418611302476dce79fced1d95a4ecc (diff) | |
Refactoring Options Handler & Library Cycle Breaking
What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.
The Problem:
The build order of CVC4 used to be [roughly] specified as:
options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.
The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.
The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)
The build order of CVC4 can now be [roughly] specified as
base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.
More details about the directories:
base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.
options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .
util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.
expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.
smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.
What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.
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 { |