Infrastructure for approximations in model output (#1884)

3 files changed, 59 insertions, 1 deletions

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;