Add missing methods to Solver API for models (#7052)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 27 Aug 2021 15:36:27 +0000 (10:36 -0500)
committerGitHub <noreply@github.com>
Fri, 27 Aug 2021 15:36:27 +0000 (15:36 +0000)
commite8d3e68b892225aba597dc65da2ca2074e520889
treecb6275c60dc92a7609a247a494dfa4a286afbe52
parent1639655ca7b8f0f18145fdbb515253810b119d08
Add missing methods to Solver API for models (#7052)

This adds the last two remaining API methods required for implementing the text output of get-model on the API side.

A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.

This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.
15 files changed:
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h
src/api/python/cvc5.pxd
src/api/python/cvc5.pxi
src/printer/cvc/cvc_printer.cpp
src/printer/smt2/smt2_printer.cpp
src/smt/model_core_builder.cpp
src/smt/preprocessor.cpp
src/smt/preprocessor.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
src/theory/sep/theory_sep.cpp
src/theory/theory_model.cpp
src/theory/theory_model.h
test/unit/api/solver_black.cpp