Ho model (#1120)

* Update model construction for higher order. If HO_APPLY terms are present for a function, we use a curried (tree) model construction to avoid exponential size model representations for function definitions.

* Update comments.

* Change terminology in comment.

* Improve comments.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 41c68a117..2b7ba7ac9 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -275,7 +275,8 @@ bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
     it->second.update( fm );
     Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
     //construct function values
-    fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
+    Node f_def = it->second.getFunctionValue( "$x" );
+    fm->assignFunctionDefinition( it->first, f_def );
   }
   Assert( d_addedLemmas==0 );
   return TheoryEngineModelBuilder::processBuildModel( m );