}
void NonlinearExtension::sendLemmas(const std::vector<Node>& out,
- bool preprocess)
+ bool preprocess,
+ std::map<Node, NlLemmaSideEffect>& lemSE)
{
+ std::map<Node, NlLemmaSideEffect>::iterator its;
for (const Node& lem : out)
{
Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
d_containing.getOutputChannel().lemma(lem, false, preprocess);
+ // process the side effect
+ its = lemSE.find(lem);
+ if (its != lemSE.end())
+ {
+ processSideEffect(its->second);
+ }
// add to cache if not preprocess
if (!preprocess)
{
}
}
+void NonlinearExtension::processSideEffect(const NlLemmaSideEffect& se)
+{
+ for (const std::tuple<Node, unsigned, Node>& sp : se.d_secantPoint)
+ {
+ Node tf = std::get<0>(sp);
+ unsigned d = std::get<1>(sp);
+ Node c = std::get<2>(sp);
+ d_secant_points[tf][d].push_back(c);
+ }
+}
+
unsigned NonlinearExtension::filterLemma(Node lem, std::vector<Node>& out)
{
Trace("nl-ext-lemma-debug")
const std::vector<Node>& xts,
std::vector<Node>& lems,
std::vector<Node>& lemsPp,
- std::vector<Node>& wlems)
+ std::vector<Node>& wlems,
+ std::map<Node, NlLemmaSideEffect>& lemSE)
{
d_ms_vars.clear();
d_ms_proc.clear();
}
if (options::nlExtTfTangentPlanes())
{
- lemmas = checkTranscendentalTangentPlanes();
+ lemmas = checkTranscendentalTangentPlanes(lemSE);
filterLemmas(lemmas, wlems);
}
Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas."
// If we computed lemmas during collectModelInfo, send them now.
if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty())
{
- sendLemmas(d_cmiLemmas);
- sendLemmas(d_cmiLemmasPp, true);
+ sendLemmas(d_cmiLemmas, false, d_cmiLemmasSE);
+ sendLemmas(d_cmiLemmasPp, true, d_cmiLemmasSE);
return;
}
// Otherwise, we will answer SAT. The values that we approximated are
}
}
-bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems,
- std::vector<Node>& mlemsPp)
+bool NonlinearExtension::modelBasedRefinement(
+ std::vector<Node>& mlems,
+ std::vector<Node>& mlemsPp,
+ std::map<Node, NlLemmaSideEffect>& lemSE)
{
// get the assertions
std::vector<Node> assertions;
if (!false_asserts.empty() || num_shared_wrong_value > 0)
{
complete_status = num_shared_wrong_value > 0 ? -1 : 0;
- checkLastCall(assertions, false_asserts, xts, mlems, mlemsPp, wlems);
+ checkLastCall(
+ assertions, false_asserts, xts, mlems, mlemsPp, wlems, lemSE);
if (!mlems.empty() || !mlemsPp.empty())
{
return true;
// run a last call effort check
d_cmiLemmas.clear();
d_cmiLemmasPp.clear();
+ d_cmiLemmasSE.clear();
if (!d_builtModel.get())
{
Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
- modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp);
+ modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp, d_cmiLemmasSE);
}
if (d_builtModel.get())
{
return lemmas;
}
-std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes()
+std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes(
+ std::map<Node, NlLemmaSideEffect>& lemSE)
{
std::vector<Node> lemmas;
Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..."
{
Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
unsigned prev = lemmas.size();
- if (!checkTfTangentPlanesFun(tf, d, lemmas))
+ if (!checkTfTangentPlanesFun(tf, d, lemmas, lemSE))
{
Trace("nl-ext-tftp")
<< "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl;
return lemmas;
}
-bool NonlinearExtension::checkTfTangentPlanesFun(Node tf,
- unsigned d,
- std::vector<Node>& lemmas)
+bool NonlinearExtension::checkTfTangentPlanesFun(
+ Node tf,
+ unsigned d,
+ std::vector<Node>& lemmas,
+ std::map<Node, NlLemmaSideEffect>& lemSE)
{
Assert(d_model.isRefineableTfFun(tf));
Assert(std::find(
d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), c)
== d_secant_points[tf][d].end());
- // insert into the vector
- d_secant_points[tf][d].push_back(c);
+ // Insert into the (temporary) vector. We do not update this vector
+ // until we are sure this secant plane lemma has been processed. We do
+ // this by mapping the lemma to a side effect below.
+ std::vector<Node> spoints = d_secant_points[tf][d];
+ spoints.push_back(c);
+
// sort
SortNlModel smv;
smv.d_nlm = &d_model;
smv.d_isConcrete = true;
- std::sort(
- d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), smv);
+ std::sort(spoints.begin(), spoints.end(), smv);
// get the resulting index of c
unsigned index =
- std::find(
- d_secant_points[tf][d].begin(), d_secant_points[tf][d].end(), c)
- - d_secant_points[tf][d].begin();
+ std::find(spoints.begin(), spoints.end(), c) - spoints.begin();
// bounds are the next closest upper/lower bound values
if (index > 0)
{
- bounds[0] = d_secant_points[tf][d][index - 1];
+ bounds[0] = spoints[index - 1];
}
else
{
bounds[0] = Rewriter::rewrite(nm->mkNode(MINUS, c, d_one));
}
}
- if (index < d_secant_points[tf][d].size() - 1)
+ if (index < spoints.size() - 1)
{
- bounds[1] = d_secant_points[tf][d][index + 1];
+ bounds[1] = spoints[index + 1];
}
else
{
Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds[0]
<< " ... " << bounds[1] << std::endl;
+ // the secant plane may be conjunction of 1-2 guarded inequalities
+ std::vector<Node> lemmaConj;
for (unsigned s = 0; s < 2; s++)
{
// compute secant plane
lem = Rewriter::rewrite(lem);
Trace("nl-ext-tftp-lemma") << "*** Secant plane lemma : " << lem
<< std::endl;
- // Figure 3 : line 22
- lemmas.push_back(lem);
+ lemmaConj.push_back(lem);
Assert(d_model.computeAbstractModelValue(lem) == d_false);
}
}
+ // Figure 3 : line 22
+ Assert(!lemmaConj.empty());
+ Node lem =
+ lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj);
+ lemmas.push_back(lem);
+ // The side effect says that if lem is added, then we should add the
+ // secant point c for (tf,d).
+ lemSE[lem].d_secantPoint.push_back(std::make_tuple(tf, d, c));
}
return false;
}
#include "context/context.h"
#include "expr/kind.h"
#include "expr/node.h"
+#include "theory/arith/nl_lemma_utils.h"
#include "theory/arith/nl_model.h"
#include "theory/arith/theory_arith.h"
#include "theory/uf/equality_engine.h"
* Otherwise, it returns false. In the latter case, the model object d_model
* may have information regarding how to construct a model, in the case that
* we determined the problem is satisfiable.
+ *
+ * The argument lemSE is the "side effect" of the lemmas in mlems and mlemsPp
+ * (for details, see checkLastCall).
*/
bool modelBasedRefinement(std::vector<Node>& mlems,
- std::vector<Node>& mlemsPp);
+ std::vector<Node>& mlemsPp,
+ std::map<Node, NlLemmaSideEffect>& lemSE);
/** returns true if the multiset containing the
* factors of monomial a is a subset of the multiset
* containing the factors of monomial b.
* output channel as a last resort. In other words, only if we are not
* able to establish SAT via a call to checkModel(...) should wlems be
* considered. This set typically contains tangent plane lemmas.
+ *
+ * The argument lemSE is the "side effect" of the lemmas from the previous
+ * three calls. If a lemma is mapping to a side effect, it should be
+ * processed via a call to processSideEffect(...) immediately after the
+ * lemma is sent (if it is indeed sent on this call to check).
*/
int checkLastCall(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
const std::vector<Node>& xts,
std::vector<Node>& lems,
std::vector<Node>& lemsPp,
- std::vector<Node>& wlems);
+ std::vector<Node>& wlems,
+ std::map<Node, NlLemmaSideEffect>& lemSE);
//---------------------------------------term utilities
static bool isArithKind(Kind k);
static Node mkLit(Node a, Node b, int status, bool isAbsolute = false);
/**
* Send lemmas in out on the output channel of theory of arithmetic.
*/
- void sendLemmas(const std::vector<Node>& out, bool preprocess = false);
+ void sendLemmas(const std::vector<Node>& out,
+ bool preprocess,
+ std::map<Node, NlLemmaSideEffect>& lemSE);
+ /** Process side effect se */
+ void processSideEffect(const NlLemmaSideEffect& se);
// Returns the NodeMultiset for an existing monomial.
const NodeMultiset& getMonomialExponentMap(Node monomial) const;
*/
std::vector<Node> d_cmiLemmas;
std::vector<Node> d_cmiLemmasPp;
+ /** the side effects of the above lemmas */
+ std::map<Node, NlLemmaSideEffect> d_cmiLemmasSE;
/**
* The approximations computed during collectModelInfo. For details, see
* NlModel::getModelValueRepair.
std::vector<Node> checkTranscendentalMonotonic();
/** check transcendental tangent planes
- *
- * Returns a set of valid theory lemmas, based on
- * computing an "incremental linearization" of
- * transcendental functions based on the model values
- * of transcendental functions and their arguments.
- * It is based on Figure 3 of "Satisfiability
- * Modulo Transcendental Functions via Incremental
- * Linearization" by Cimatti et al., CADE 2017.
- * This schema is not terminating in general.
- * It is not enabled by default, and can
- * be enabled by --nl-ext-tf-tplanes.
- *
- * Example:
- *
- * Assume we have a term sin(y) where M( y ) = 1 where M is the current model.
- * Note that:
- * sin(1) ~= .841471
- *
- * The Taylor series and remainder of sin(y) of degree 7 is
- * P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5
- * R_{7,sin(0),b}( x ) = (-1/5040)*x^7
- *
- * This gives us lower and upper bounds :
- * P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x )
- * ...where note P_u( 1 ) = 4243/5040 ~= .841865
- * P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x )
- * ...where note P_l( 1 ) = 4241/5040 ~= .841468
- *
- * Assume that M( sin(y) ) > P_u( 1 ).
- * Since the concavity of sine in the region 0 < x < PI/2 is -1,
- * we add a tangent plane refinement.
- * The tangent plane at the point 1 in P_u is
- * given by the formula:
- * T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 )
- * We add the lemma:
- * ( 0 < y < PI/2 ) => sin( y ) <= T( y )
- * which is:
- * ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506)
- *
- * Assume that M( sin(y) ) < P_u( 1 ).
- * Since the concavity of sine in the region 0 < x < PI/2 is -1,
- * we add a secant plane refinement for some constants ( l, u )
- * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose
- * l = 0 and u = M( PI/2 ) = 150517/47912.
- * The secant planes at point 1 for P_l
- * are given by the formulas:
- * S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l )
- * S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u )
- * We add the lemmas:
- * ( 0 < y < 1 ) => sin( y ) >= S_l( y )
- * ( 1 < y < PI/2 ) => sin( y ) >= S_u( y )
- * which are:
- * ( 0 < y < 1 ) => (sin y) >= 4251/5040*y
- * ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2)
- * where c1, c2 are rationals (for brevity, omitted here)
- * such that c1 ~= .277 and c2 ~= 2.032.
- */
- std::vector<Node> checkTranscendentalTangentPlanes();
+ *
+ * Returns a set of valid theory lemmas, based on
+ * computing an "incremental linearization" of
+ * transcendental functions based on the model values
+ * of transcendental functions and their arguments.
+ * It is based on Figure 3 of "Satisfiability
+ * Modulo Transcendental Functions via Incremental
+ * Linearization" by Cimatti et al., CADE 2017.
+ * This schema is not terminating in general.
+ * It is not enabled by default, and can
+ * be enabled by --nl-ext-tf-tplanes.
+ *
+ * Example:
+ *
+ * Assume we have a term sin(y) where M( y ) = 1 where M is the current model.
+ * Note that:
+ * sin(1) ~= .841471
+ *
+ * The Taylor series and remainder of sin(y) of degree 7 is
+ * P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5
+ * R_{7,sin(0),b}( x ) = (-1/5040)*x^7
+ *
+ * This gives us lower and upper bounds :
+ * P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x )
+ * ...where note P_u( 1 ) = 4243/5040 ~= .841865
+ * P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x )
+ * ...where note P_l( 1 ) = 4241/5040 ~= .841468
+ *
+ * Assume that M( sin(y) ) > P_u( 1 ).
+ * Since the concavity of sine in the region 0 < x < PI/2 is -1,
+ * we add a tangent plane refinement.
+ * The tangent plane at the point 1 in P_u is
+ * given by the formula:
+ * T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 )
+ * We add the lemma:
+ * ( 0 < y < PI/2 ) => sin( y ) <= T( y )
+ * which is:
+ * ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506)
+ *
+ * Assume that M( sin(y) ) < P_u( 1 ).
+ * Since the concavity of sine in the region 0 < x < PI/2 is -1,
+ * we add a secant plane refinement for some constants ( l, u )
+ * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose
+ * l = 0 and u = M( PI/2 ) = 150517/47912.
+ * The secant planes at point 1 for P_l
+ * are given by the formulas:
+ * S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l )
+ * S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u )
+ * We add the lemmas:
+ * ( 0 < y < 1 ) => sin( y ) >= S_l( y )
+ * ( 1 < y < PI/2 ) => sin( y ) >= S_u( y )
+ * which are:
+ * ( 0 < y < 1 ) => (sin y) >= 4251/5040*y
+ * ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2)
+ * where c1, c2 are rationals (for brevity, omitted here)
+ * such that c1 ~= .277 and c2 ~= 2.032.
+ *
+ * The argument lemSE is the "side effect" of the lemmas in the return
+ * value of this function (for details, see checkLastCall).
+ */
+ std::vector<Node> checkTranscendentalTangentPlanes(
+ std::map<Node, NlLemmaSideEffect>& lemSE);
/** check transcendental function refinement for tf
*
* This method is called by the above method for each refineable
*
* This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental
* function application tf for Taylor degree d. It may add a secant or
- * tangent plane lemma to lems.
+ * tangent plane lemma to lems and its side effect (if one exists)
+ * to lemSE.
*/
- bool checkTfTangentPlanesFun(Node tf, unsigned d, std::vector<Node>& lems);
+ bool checkTfTangentPlanesFun(Node tf,
+ unsigned d,
+ std::vector<Node>& lems,
+ std::map<Node, NlLemmaSideEffect>& lemSE);
//-------------------------------------------- end lemma schemas
}; /* class NonlinearExtension */
projects / cvc5.git / commitdiff