Print response to get-model using the API (#7084)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Sep 2021 18:05:48 +0000 (13:05 -0500)
committerGitHub <noreply@github.com>
Wed, 1 Sep 2021 18:05:48 +0000 (18:05 +0000)
commit7a3aa7033719b14b34c0334d6956834b850fa9eb
tree53c2f3543a6314eaabd76eff9e38c2752a5c4afa
parent24c4e9d5612fd7549a8ff7acaf76ce95acaca0d9
Print response to get-model using the API (#7084)

This changes our implementation of GetModelCommand so that we use the API to print the model.

It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.

It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.

This eliminates the last call to getSmtEngine() from the command layer.
23 files changed:
src/api/cpp/cvc5.cpp
src/api/cpp/cvc5.h
src/main/command_executor.h
src/printer/ast/ast_printer.cpp
src/printer/ast/ast_printer.h
src/printer/cvc/cvc_printer.cpp
src/printer/cvc/cvc_printer.h
src/printer/printer.cpp
src/printer/printer.h
src/printer/smt2/smt2_printer.cpp
src/printer/smt2/smt2_printer.h
src/printer/tptp/tptp_printer.cpp
src/printer/tptp/tptp_printer.h
src/smt/check_models.cpp
src/smt/check_models.h
src/smt/command.cpp
src/smt/command.h
src/smt/model.cpp
src/smt/model.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
test/regress/regress0/cvc-rerror-print.cvc
test/unit/api/solver_black.cpp