Ho model (#1120)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 5 Oct 2017 12:12:47 +0000 (07:12 -0500)
committerGitHub <noreply@github.com>
Thu, 5 Oct 2017 12:12:47 +0000 (07:12 -0500)
commitf56f46f5bb5845cff0c329926f51a0377379365b
treeff22d91db4f2265b17634b3797cc724ee079f410
parent3c5c0c2287203b61acc94bb83fac1b91ae290007
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.
src/theory/quantifiers/ambqi_builder.cpp
src/theory/quantifiers/full_model_check.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/theory_model.cpp
src/theory/theory_model.h