From cec27a6996280820c41a3102e25ba8c87ab9a845 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Sep 2018 21:56:31 -0500 Subject: [PATCH] Improve non-linear check model error handling (#2497) --- src/theory/arith/nonlinear_extension.cpp | 96 +++++++++++++++++------- src/theory/arith/nonlinear_extension.h | 12 ++- 2 files changed, 78 insertions(+), 30 deletions(-) diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 9f6608dc5..4cd7896d3 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -888,17 +888,25 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, Kind k = tfs.first; for (const Node& tf : tfs.second) { + bool success = true; // tf is Figure 3 : tf( x ) Node atf = computeModelValue(tf, 0); if (k == PI) { - addCheckModelBound(atf, d_pi_bound[0], d_pi_bound[1]); + success = addCheckModelBound(atf, d_pi_bound[0], d_pi_bound[1]); } else if (isRefineableTfFun(tf)) { d_used_approx = true; std::pair bounds = getTfModelBounds(tf, d_taylor_degree); - addCheckModelBound(atf, bounds.first, bounds.second); + success = addCheckModelBound(atf, bounds.first, bounds.second); + } + if (!success) + { + Trace("nl-ext-cm-debug") + << "...failed to set bound for transcendental function." + << std::endl; + return false; } if (Trace.isOn("nl-ext-cm")) { @@ -962,7 +970,8 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, << "check-model-bound : exact : " << cur << " = "; printRationalApprox("nl-ext-cm", curv); Trace("nl-ext-cm") << std::endl; - addCheckModelSubstitution(cur, curv); + bool ret = addCheckModelSubstitution(cur, curv); + AlwaysAssert(ret); } } } @@ -1036,15 +1045,31 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, return true; } -void NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s) +bool NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s) { // should not substitute the same variable twice Trace("nl-ext-model") << "* check model substitution : " << v << " -> " << s << std::endl; // should not set exact bound more than once if(std::find(d_check_model_vars.begin(),d_check_model_vars.end(),v)!=d_check_model_vars.end()) { + Trace("nl-ext-model") << "...ERROR: already has value." << std::endl; + // this should never happen since substitutions should be applied eagerly Assert( false ); - return; + return false; + } + // if we previously had an approximate bound, the exact bound should be in its + // range + std::map >::iterator itb = + d_check_model_bounds.find(v); + if (itb != d_check_model_bounds.end()) + { + if (s.getConst() >= itb->second.first.getConst() + || s.getConst() <= itb->second.second.getConst()) + { + Trace("nl-ext-model") + << "...ERROR: already has bound which is out of range." << std::endl; + return false; + } } for (unsigned i = 0, size = d_check_model_subs.size(); i < size; i++) { @@ -1058,23 +1083,32 @@ void NonlinearExtension::addCheckModelSubstitution(TNode v, TNode s) } d_check_model_vars.push_back(v); d_check_model_subs.push_back(s); + return true; } -void NonlinearExtension::addCheckModelBound(TNode v, TNode l, TNode u) +bool NonlinearExtension::addCheckModelBound(TNode v, TNode l, TNode u) { Trace("nl-ext-model") << "* check model bound : " << v << " -> [" << l << " " << u << "]" << std::endl; if( l==u ) { // bound is exact, can add as substitution - addCheckModelSubstitution(v,l); - return; + return addCheckModelSubstitution(v, l); } // should not set a bound for a value that is exact - Assert(std::find(d_check_model_vars.begin(),d_check_model_vars.end(),v)==d_check_model_vars.end()); + if (std::find(d_check_model_vars.begin(), d_check_model_vars.end(), v) + != d_check_model_vars.end()) + { + Trace("nl-ext-model") + << "...ERROR: setting bound for variable that already has exact value." + << std::endl; + Assert(false); + return false; + } Assert(l.isConst()); Assert(u.isConst()); Assert(l.getConst() <= u.getConst()); d_check_model_bounds[v] = std::pair(l, u); + return true; } bool NonlinearExtension::hasCheckModelAssignment(Node v) const @@ -1203,11 +1237,14 @@ bool NonlinearExtension::solveEqualitySimple(Node eq) { Trace("nl-ext-cm") << "check-model-subs : " << uv << " -> " << slv << std::endl; - addCheckModelSubstitution(uv, slv); - Trace("nl-ext-cms") << "...success, model substitution " << uv - << " -> " << slv << std::endl; - d_check_model_solved[eq] = uv; - return true; + bool ret = addCheckModelSubstitution(uv, slv); + if (ret) + { + Trace("nl-ext-cms") << "...success, model substitution " << uv + << " -> " << slv << std::endl; + d_check_model_solved[eq] = uv; + } + return ret; } } } @@ -1223,9 +1260,9 @@ bool NonlinearExtension::solveEqualitySimple(Node eq) Trace("nl-ext-cm") << "check-model-bound : exact : " << uvf << " = "; printRationalApprox("nl-ext-cm", uvfv); Trace("nl-ext-cm") << std::endl; - addCheckModelSubstitution(uvf, uvfv); + bool ret = addCheckModelSubstitution(uvf, uvfv); // recurse - return solveEqualitySimple(eq); + return ret ? solveEqualitySimple(eq) : false; } } Trace("nl-ext-cms") << "...fail due to constrained invalid terms." @@ -1252,10 +1289,13 @@ bool NonlinearExtension::solveEqualitySimple(Node eq) Trace("nl-ext-cm") << "check-model-bound : exact : " << var << " = "; printRationalApprox("nl-ext-cm", val); Trace("nl-ext-cm") << std::endl; - addCheckModelSubstitution(var, val); - Trace("nl-ext-cms") << "...success, solved linear." << std::endl; - d_check_model_solved[eq] = var; - return true; + bool ret = addCheckModelSubstitution(var, val); + if (ret) + { + Trace("nl-ext-cms") << "...success, solved linear." << std::endl; + d_check_model_solved[eq] = var; + } + return ret; } Trace("nl-ext-quad") << "Solve quadratic : " << seq << std::endl; Trace("nl-ext-quad") << " a : " << a << std::endl; @@ -1352,10 +1392,14 @@ bool NonlinearExtension::solveEqualitySimple(Node eq) Trace("nl-ext-cm") << " <= " << var << " <= "; printRationalApprox("nl-ext-cm", bounds[r_use_index][1]); Trace("nl-ext-cm") << std::endl; - addCheckModelBound(var, bounds[r_use_index][0], bounds[r_use_index][1]); - d_check_model_solved[eq] = var; - Trace("nl-ext-cms") << "...success, solved quadratic." << std::endl; - return true; + bool ret = + addCheckModelBound(var, bounds[r_use_index][0], bounds[r_use_index][1]); + if (ret) + { + d_check_model_solved[eq] = var; + Trace("nl-ext-cms") << "...success, solved quadratic." << std::endl; + } + return ret; } bool NonlinearExtension::simpleCheckModelLit(Node lit) @@ -3622,7 +3666,7 @@ std::vector NonlinearExtension::checkFactoring( sum = Rewriter::rewrite( sum ); Trace("nl-ext-factor") << "* Factored sum for " << x << " : " << sum << std::endl; - Node kf = getFactorSkolem( sum, lemmas ); + Node kf = getFactorSkolem(sum, lemmas); std::vector< Node > poly; poly.push_back(NodeManager::currentNM()->mkNode(MULT, x, kf)); std::map >::iterator itfo = @@ -3672,7 +3716,7 @@ Node NonlinearExtension::getFactorSkolem( Node n, std::vector< Node >& lemmas ) return itf->second; } } - + std::vector NonlinearExtension::checkMonomialInferResBounds() { std::vector< Node > lemmas; Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..." << std::endl; diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index c0af312b3..f2cdea334 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -317,8 +317,10 @@ class NonlinearExtension { * Adds the model substitution v -> s. This applies the substitution * { v -> s } to each term in d_check_model_subs and adds v,s to * d_check_model_vars and d_check_model_subs respectively. + * If this method returns false, then the substitution v -> s is inconsistent + * with the current substitution and bounds. */ - void addCheckModelSubstitution(TNode v, TNode s); + bool addCheckModelSubstitution(TNode v, TNode s); /** lower and upper bounds for check model * * For each term t in the domain of this map, if this stores the pair @@ -335,9 +337,11 @@ class NonlinearExtension { /** add check model bound * * Adds the bound x -> < l, u > to the map above, and records the - * approximation ( x, l <= x <= u ) in the model. + * approximation ( x, l <= x <= u ) in the model. This method returns false + * if the bound is inconsistent with the current model substitution or + * bounds. */ - void addCheckModelBound(TNode v, TNode l, TNode u); + bool addCheckModelBound(TNode v, TNode l, TNode u); /** * The map from literals that our model construction solved, to the variable * that was solved for. Examples of such literals are: @@ -586,7 +590,7 @@ class NonlinearExtension { // factor skolems std::map< Node, Node > d_factor_skolem; Node getFactorSkolem( Node n, std::vector< Node >& lemmas ); - + // tangent plane bounds std::map< Node, std::map< Node, Node > > d_tangent_val_bound[4]; -- 2.30.2