diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-06-15 18:00:08 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-15 18:00:08 -0300 |
| commit | 545bdeebf38e7212dc161567ec16ddc6bd36d708 (patch) | |
| tree | f35c4ffdca509abf3a1f8581fcc9a08d330fb367 /src/theory/theory_model.cpp | |
| parent | 3cb6e28c13a2c3ff42d68d5b5025e4b56cb2054b (diff) | |
Support AND/OR definitions in lambda to array rewriting (#4615)
This makes the conversion between lambdas and arrays, done in the theory builtin rewriter and used in higher-order model construction, robust to function definitions in terms of AND/OR.
This also improves tracing and makes a few parts of the code adhere to code guidelines.
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 567b5c4e4..6c8687623 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -681,7 +681,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { f_def = Rewriter::rewrite( f_def ); Trace("model-builder-debug") << "Model value (post-rewrite) : " << f_def << std::endl; - Assert(f_def.isConst()); + Assert(f_def.isConst()) << "Non-constant f_def: " << f_def; } // d_uf_models only stores models for variables |