diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-19 09:44:04 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-19 09:44:04 -0500 |
| commit | 7988675ce9666b6f2214b583d42b9fa8be52ae60 (patch) | |
| tree | 12cda1e352a6d80819f00d131f969d7728bf28ec /src/theory/uf | |
| parent | cfe4f59c0a10d49a35b9f59bb2fd6ab7d224e53d (diff) | |
Support context-(in)dependent decision strategies. (#3281)
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 94e5f67c1..87696ef5f 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -504,6 +504,8 @@ void SortModel::initialize( OutputChannel* out ){ if (d_c_dec_strat.get() != nullptr && !d_initialized) { d_initialized = true; + // Strategy is user-context-dependent, since it is in sync with + // user-context-dependent flag d_initialized. d_thss->getTheory()->getDecisionManager()->registerStrategy( DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get()); } |