diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-08 16:28:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-08 16:28:22 -0500 |
commit | cfaa03f3db71dc2805b695f98b073431d0430e43 (patch) | |
tree | 29a005932e186354f2966603601982ca8448c89f /src/theory/theory_model.cpp | |
parent | f5e3739358b98d9a6ebc16fbc5aed9edee1483dc (diff) |
Infrastructure for approximations in model output (#1884)
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 26 |
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 ); |