summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-07-06 13:33:55 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-07-06 13:33:55 -0500
commit673bb476c2a1b51abbc95acb0afaf4e3b8a9feb7 (patch)
treeff5b597fe15afaeb83eae9e32d732f6bf27bff67 /src/smt
parentcbc5adb5d4f131ea6bf9a40b0c27fecf67353b4d (diff)
Add comment field for model, resolves hack for printing sep logic models.
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/model.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/model.h b/src/smt/model.h
index 768cb3e6a..eadeb1c4b 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -58,7 +58,6 @@ public:
const SmtEngine* getSmtEngine() const { return &d_smt; }
/** get the input name (file name, etc.) this model is associated to */
std::string getInputName() const { return d_inputName; }
-
public:
/** Check whether this expr is a don't-care in the model */
virtual bool isDontCare(Expr expr) const { return false; }
@@ -66,6 +65,8 @@ public:
virtual Expr getValue(Expr expr) const = 0;
/** get cardinality for sort */
virtual Cardinality getCardinality(Type t) const = 0;
+ /** print comments */
+ virtual void getComments(std::ostream& out) const {}
};/* class Model */
class ModelBuilder {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback