diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-25 07:10:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-25 07:10:38 -0500 |
commit | 16578fca1c50d2ca9fce45c9c262db7ff6e2fd92 (patch) | |
tree | dc827a563e52198b1519c746718b2a976e0c4d16 /src/options/theory_options.toml | |
parent | 5aeb8b78c4a26b274dbfecc882c0e0bb836cb398 (diff) |
Add the combination engine (#4939)
This adds the combination engine, which is the module of TheoryEngine which implements the combineTheories method and owns the various components of theory combination, which includes equality engine manager, model manager, and the "shared solver" (to come later). It will have two variants, CombinationCareGraph and CombinationModelBased, the former is added with this PR.
FYI @barrettcw
The next PR will connect this module to TheoryEngine and remove a few existing methods from TheoryEngine, as they are implemented in the modules of this class.
Diffstat (limited to 'src/options/theory_options.toml')
-rw-r--r-- | src/options/theory_options.toml | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 6ec9d8854..388333124 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -42,3 +42,27 @@ header = "options/theory_options.h" type = "bool" default = "false" help = "enable analysis of relevance of asserted literals with respect to the input formula" + +[[option]] + name = "eeMode" + category = "expert" + long = "ee-mode=MODE" + type = "EqEngineMode" + default = "DISTRIBUTED" + help = "mode for managing equalities across theory solvers" + help_mode = "Defines mode for managing equalities across theory solvers." +[[option.mode.DISTRIBUTED]] + name = "distributed" + help = "Each theory maintains its own equality engine." + +[[option]] + name = "tcMode" + category = "expert" + long = "tc-mode=MODE" + type = "TcMode" + default = "CARE_GRAPH" + help = "mode for theory combination" + help_mode = "Defines mode for theory combination." +[[option.mode.CARE_GRAPH]] + name = "care-graph" + help = "Use care graphs for theory combination." |