diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-01 13:05:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-01 18:05:48 +0000 |
| commit | 7a3aa7033719b14b34c0334d6956834b850fa9eb (patch) | |
| tree | 53c2f3543a6314eaabd76eff9e38c2752a5c4afa /src/printer/cvc/cvc_printer.h | |
| parent | 24c4e9d5612fd7549a8ff7acaf76ce95acaca0d9 (diff) | |
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.
Diffstat (limited to 'src/printer/cvc/cvc_printer.h')
| -rw-r--r-- | src/printer/cvc/cvc_printer.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 555237177..4851868d3 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -175,19 +175,19 @@ class CvcPrinter : public cvc5::Printer LetBinding* lbind) const; /** * To stream model sort. This prints the appropriate output for type - * tn declared via declare-sort or declare-datatype. + * tn declared via declare-sort. */ void toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const override; + TypeNode tn, + const std::vector<Node>& elements) const override; /** * To stream model term. This prints the appropriate output for term * n declared via declare-fun. */ void toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const override; + const Node& n, + const Node& value) const override; /** * To stream with let binding. This prints n, possibly in the scope * of letification generated by this method based on lbind. |