Infrastructure for approximations in model output (#1884)

6 files changed, 86 insertions, 1 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 36076ec3c..27feea60e 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -443,6 +443,7 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::ARCCOSECANT:
   case kind::ARCSECANT:
   case kind::ARCCOTANGENT:
+  case kind::PI:
   case kind::SQRT:
   case kind::MINUS:
   case kind::UMINUS:
@@ -926,6 +927,7 @@ static string smtKindString(Kind k, Variant v)
   case kind::ARCCOSECANT: return "arccsc";
   case kind::ARCSECANT: return "arcsec";
   case kind::ARCCOTANGENT: return "arccot";
+  case kind::PI: return "real.pi";
   case kind::SQRT: return "sqrt";
   case kind::MINUS: return "-";
   case kind::UMINUS: return "-";
@@ -1309,6 +1311,15 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const
   }
   //print the model
   out << "(model" << endl;
+  // print approximations
+  if (m.hasApproximations())
+  {
+    std::vector<std::pair<Expr, Expr> > approx = m.getApproximations();
+    for (unsigned i = 0, size = approx.size(); i < size; i++)
+    {
+      out << "(approximation " << approx[i].second << ")" << std::endl;
+    }
+  }
   this->Printer::toStream(out, m);
   out << ")" << endl;
   //print the heap model, if it exists
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);
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index edea22fbf..11da42e07 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -645,7 +645,9 @@ void TheoryEngine::check(Theory::Effort effort) {
         {
           // if we are incomplete, there is no guarantee on the model.
           // thus, we do not check the model here. (related to #1693)
-          if (!d_incomplete)
+          // we also don't debug-check the model if the checkModels()
+          // is not enabled.
+          if (!d_incomplete && options::checkModels())
           {
             d_curr_model_builder->debugCheckModel(d_curr_model);
           }
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 739925f4f..4b603d02a 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -64,6 +64,8 @@ void TheoryModel::reset(){
   d_comment_str.clear();
   d_sep_heap = Node::null();
   d_sep_nil_eq = Node::null();
+  d_approximations.clear();
+  d_approx_list.clear();
   d_reps.clear();
   d_rep_set.clear();
   d_uf_terms.clear();
@@ -93,6 +95,19 @@ bool TheoryModel::getHeapModel( Expr& h, Expr& neq ) const {
   }
 }
 
+bool TheoryModel::hasApproximations() const { return !d_approx_list.empty(); }
+
+std::vector<std::pair<Expr, Expr> > TheoryModel::getApproximations() const
+{
+  std::vector<std::pair<Expr, Expr> > approx;
+  for (const std::pair<Node, Node>& ap : d_approx_list)
+  {
+    approx.push_back(
+        std::pair<Expr, Expr>(ap.first.toExpr(), ap.second.toExpr()));
+  }
+  return approx;
+}
+
 Node TheoryModel::getValue(TNode n, bool useDontCares) const {
   //apply substitutions
   Node nn = d_substitutions.apply(n);
@@ -449,6 +464,17 @@ void TheoryModel::assertSkeleton(TNode n)
   d_reps[ n ] = n;
 }
 
+void TheoryModel::recordApproximation(TNode n, TNode pred)
+{
+  Trace("model-builder-debug")
+      << "Record approximation : " << n << " satisfies the predicate " << pred
+      << std::endl;
+  Assert(d_approximations.find(n) == d_approximations.end());
+  Assert(pred.getType().isBoolean());
+  d_approximations[n] = pred;
+  d_approx_list.push_back(std::pair<Node, Node>(n, pred));
+}
+
 bool TheoryModel::hasTerm(TNode a)
 {
   return d_equalityEngine->hasTerm( a );
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index 1f9fd92d4..b6d1288ae 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -139,6 +139,28 @@ public:
    * during Theory's collectModelInfo( ... ) functions.
    */
   void assertSkeleton(TNode n);
+  /** record approximation
+   *
+   * This notifies this model that the value of n was approximated in this
+   * model such that the predicate pred (involving n) holds. For example,
+   * for transcendental functions, we may determine an error bound on the
+   * value of a transcendental function, say c-e <= y <= c+e where
+   * c and e are constants. We call this function with n set to sin( x ) and
+   * pred set to c-e <= sin( x ) <= c+e.
+   *
+   * If recordApproximation is called at least once during the model
+   * construction process, then check-model is not guaranteed to succeed.
+   * However, there are cases where we can establish the input is satisfiable
+   * without constructing an exact model. For example, if x=.77, sin(x)=.7, and
+   * say we have computed c=.7 and e=.01 as an approximation in the above
+   * example, then we may reason that the set of assertions { sin(x)>.6 } is
+   * satisfiable, albiet without establishing an exact (irrational) value for
+   * sin(x).
+   *
+   * This function is simply for bookkeeping, it does not affect the model
+   * construction process.
+   */
+  void recordApproximation(TNode n, TNode pred);
   //---------------------------- end building the model
 
   // ------------------- general equality queries
@@ -171,6 +193,10 @@ public:
   bool getHeapModel(Expr& h, Expr& neq) const override;
   //---------------------------- end separation logic
 
+  /** is the list of approximations non-empty? */
+  bool hasApproximations() const override;
+  /** get approximations */
+  std::vector<std::pair<Expr, Expr> > getApproximations() const override;
   /** get the representative set object */
   const RepSet* getRepSet() const { return &d_rep_set; }
   /** get the representative set object (FIXME: remove this, see #1199) */
@@ -215,6 +241,10 @@ public:
   context::Context* d_eeContext;
   /** equality engine containing all known equalities/disequalities */
   eq::EqualityEngine* d_equalityEngine;
+  /** approximations (see recordApproximation) */
+  std::map<Node, Node> d_approximations;
+  /** list of all approximations */
+  std::vector<std::pair<Node, Node> > d_approx_list;
   /** map of representatives of equality engine to used representatives in
    * representative set */
   std::map<Node, Node> d_reps;