Eliminate eager model building (#7038)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 20 Aug 2021 01:51:33 +0000 (20:51 -0500)
committerGitHub <noreply@github.com>
Fri, 20 Aug 2021 01:51:33 +0000 (01:51 +0000)
commit6c47289737ca3c9a1345d4bf5666eaed4011edcc
treeb8a926cf8115495943cbc9768f0d48f82e3684b2
parent48904b48eff10b6db84053584511d779fe2bc5fe
Eliminate eager model building (#7038)

Previously, we had a special case to support users who directly accessed the model object pointer in the old API.

The special case ensure that the information in the model was eagerly updated after each "sat" response, in the case that the user did not re-request a pointer to the model.

Since users no longer can access the internal model pointer (apart from GetModelCommand), this special case is no longer necessary.

This PR should make us slightly faster for incremental benchmarks where the user asks for the model on some but not all "sat" responses.
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h