diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-23 15:44:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-23 15:44:50 -0500 |
commit | a96fbfe33c05bea0b94d5387dda65c2ae343f66b (patch) | |
tree | a3b1e28dc45f05ef218331217ed072e842d6dfd3 /src/theory/theory_model_builder.cpp | |
parent | 4c2138a14c4abba2431bc8ba51359d3a565baf05 (diff) |
Add notions of evaluated kinds in TheoryModel (#1947)
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
-rw-r--r-- | src/theory/theory_model_builder.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index e88d1e3be..f91a413e3 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -930,7 +930,10 @@ bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m) bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m) { - assignFunctions(m); + if (m->areFunctionValuesEnabled()) + { + assignFunctions(m); + } return true; } @@ -1098,6 +1101,10 @@ struct sortTypeSize void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) { + if (!options::assignFunctionValues()) + { + return; + } Trace("model-builder") << "Assigning function values..." << std::endl; std::vector<Node> funcs_to_assign = m->getFunctionsToAssign(); |