From cfaa03f3db71dc2805b695f98b073431d0430e43 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 8 May 2018 16:28:22 -0500 Subject: [PATCH] Infrastructure for approximations in model output (#1884) --- src/printer/smt2/smt2_printer.cpp | 11 +++++++++++ src/smt/model.h | 8 ++++++++ src/smt/smt_engine.cpp | 8 ++++++++ src/theory/theory_engine.cpp | 4 +++- src/theory/theory_model.cpp | 26 ++++++++++++++++++++++++++ src/theory/theory_model.h | 30 ++++++++++++++++++++++++++++++ 6 files changed, 86 insertions(+), 1 deletion(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 36076ec3c..27feea60e 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -443,6 +443,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::ARCCOSECANT: case kind::ARCSECANT: case kind::ARCCOTANGENT: + case kind::PI: case kind::SQRT: case kind::MINUS: case kind::UMINUS: @@ -926,6 +927,7 @@ static string smtKindString(Kind k, Variant v) case kind::ARCCOSECANT: return "arccsc"; case kind::ARCSECANT: return "arcsec"; case kind::ARCCOTANGENT: return "arccot"; + case kind::PI: return "real.pi"; case kind::SQRT: return "sqrt"; case kind::MINUS: return "-"; case kind::UMINUS: return "-"; @@ -1309,6 +1311,15 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m) const } //print the model out << "(model" << endl; + // print approximations + if (m.hasApproximations()) + { + std::vector > approx = m.getApproximations(); + for (unsigned i = 0, size = approx.size(); i < size; i++) + { + out << "(approximation " << approx[i].second << ")" << std::endl; + } + } this->Printer::toStream(out, m); out << ")" << endl; //print the heap model, if it exists 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 > 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); 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 > TheoryModel::getApproximations() const +{ + std::vector > approx; + for (const std::pair& ap : d_approx_list) + { + approx.push_back( + std::pair(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(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 > 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 d_approximations; + /** list of all approximations */ + std::vector > d_approx_list; /** map of representatives of equality engine to used representatives in * representative set */ std::map d_reps; -- 2.30.2