diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-31 14:27:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-31 14:27:04 -0500 |
| commit | 63f887783e003546bf8de4501774a79dbcf8d4b0 (patch) | |
| tree | 2932cf5aa5c81746f5747d48c1ea73ea47c0a624 /src/base | |
| parent | 5272f5d02f109b7dbfdb5088a1efbf7d13b64487 (diff) | |
Remove replay and use-theory options and idl (#4186)
Towards disentangling Options / NodeManager / SmtEngine.
This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work.
The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it.
The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging.
It also removes the solver in src/theory/idl, which cannot be enabled after this commit.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/configuration.cpp | 4 | ||||
| -rw-r--r-- | src/base/configuration.h | 2 | ||||
| -rw-r--r-- | src/base/configuration_private.h | 6 |
3 files changed, 0 insertions, 12 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index f907f212f..aed835f3f 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -50,10 +50,6 @@ bool Configuration::isStatisticsBuild() { return IS_STATISTICS_BUILD; } -bool Configuration::isReplayBuild() { - return IS_REPLAY_BUILD; -} - bool Configuration::isTracingBuild() { return IS_TRACING_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 60cdd5a9c..72ccb2301 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -47,8 +47,6 @@ public: static bool isStatisticsBuild(); - static bool isReplayBuild(); - static bool isTracingBuild(); static bool isDumpingBuild(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index f3e76d53b..77db0b51c 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -36,12 +36,6 @@ namespace CVC4 { # define IS_STATISTICS_BUILD false #endif /* CVC4_STATISTICS_ON */ -#ifdef CVC4_REPLAY -# define IS_REPLAY_BUILD true -#else /* CVC4_REPLAY */ -# define IS_REPLAY_BUILD false -#endif /* CVC4_REPLAY */ - #ifdef CVC4_TRACING # define IS_TRACING_BUILD true #else /* CVC4_TRACING */ |