Infrastructure for approximations in model output (#1884)

2 files changed, 16 insertions, 0 deletions

diff --git a/src/smt/model.h b/src/smt/model.h
index f379ae16d..845514a13 100644
--- a/src/smt/model.h
+++ b/src/smt/model.h
@@ -69,6 +69,14 @@ public:
   virtual void getComments(std::ostream& out) const {}
   /** get heap model (for separation logic) */
   virtual bool getHeapModel( Expr& h, Expr& ne ) const { return false; }
+  /** are there any approximations in this model? */
+  virtual bool hasApproximations() const { return false; }
+  /** get the list of approximations
+   *
+   * This is a list of pairs of the form (t,p), where t is a term and p
+   * is a predicate over t that indicates a property that t satisfies.
+   */
+  virtual std::vector<std::pair<Expr, Expr> > getApproximations() const = 0;
 };/* class Model */
 
 class ModelBuilder {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c9733983a..565f99ec5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5191,6 +5191,14 @@ void SmtEngine::checkModel(bool hardFailure) {
   Notice() << "SmtEngine::checkModel(): generating model" << endl;
   TheoryModel* m = d_theoryEngine->getModel();
 
+  // check-model is not guaranteed to succeed if approximate values were used
+  if (m->hasApproximations())
+  {
+    Warning()
+        << "WARNING: running check-model on a model with approximate values..."
+        << endl;
+  }
+
   // Check individual theory assertions
   d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure);