diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-23 19:12:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-23 19:12:32 -0600 |
| commit | 854ab7e1adce90ebd822cc29ffabf5546d13f5cc (patch) | |
| tree | 96bcb318ada0448c73d293c0b99db7b98eb1e4c4 /src/theory/theory_model_builder.cpp | |
| parent | 4c0dbb8ec7871ff114a9e66233cd8c8dd853f0b4 (diff) | |
Add interface to TheoryState for sort inference and facts (#5967)
This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.
This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 53b8f25a4..9604dc72b 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -16,8 +16,8 @@ #include "expr/dtype.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "options/theory_options.h" #include "options/uf_options.h" -#include "theory/theory_engine.h" #include "theory/uf/theory_uf_model.h" using namespace std; @@ -60,9 +60,7 @@ Node TheoryEngineModelBuilder::Assigner::getNextAssignment() return n; } -TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te) -{ -} +TheoryEngineModelBuilder::TheoryEngineModelBuilder() {} Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r) { |