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.h | |
parent | f5e3739358b98d9a6ebc16fbc5aed9edee1483dc (diff) |
Infrastructure for approximations in model output (#1884)
Diffstat (limited to 'src/theory/theory_model.h')
-rw-r--r-- | src/theory/theory_model.h | 30 |
1 files changed, 30 insertions, 0 deletions
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; |