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/smt | |
parent | f5e3739358b98d9a6ebc16fbc5aed9edee1483dc (diff) |
Infrastructure for approximations in model output (#1884)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/model.h | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 8 |
2 files changed, 16 insertions, 0 deletions
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); |