diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-27 10:36:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-27 15:36:27 +0000 |
| commit | e8d3e68b892225aba597dc65da2ca2074e520889 (patch) | |
| tree | cb6275c60dc92a7609a247a494dfa4a286afbe52 /src/theory/theory_model.h | |
| parent | 1639655ca7b8f0f18145fdbb515253810b119d08 (diff) | |
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.
Diffstat (limited to 'src/theory/theory_model.h')
| -rw-r--r-- | src/theory/theory_model.h | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 4034e43bd..6841a11d8 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -296,8 +296,6 @@ class TheoryModel * has called buildModel(...) on this model. */ Node getValue(TNode n) const; - /** get comments */ - void getComments(std::ostream& out) const; //---------------------------- separation logic /** set the heap and value sep.nil is equal to */ @@ -318,6 +316,8 @@ class TheoryModel RepSet* getRepSetPtr() { return &d_rep_set; } //---------------------------- model cores + /** True if a model core has been computed for this model. */ + bool isUsingModelCore() const; /** set using model core */ void setUsingModelCore(); /** record model core symbol */ @@ -394,8 +394,6 @@ class TheoryModel /** true/false nodes */ Node d_true; Node d_false; - /** comment stream to include in printing */ - std::stringstream d_comment_str; /** are we using model cores? */ bool d_using_model_core; /** symbols that are in the model core */ |