Infrastructure for approximations in model output (#1884)

1 files changed, 26 insertions, 0 deletions

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 );