"a", NodeManager::currentNM()->realType());
d_taylor_real_fv_base_rem = NodeManager::currentNM()->mkBoundVar(
"b", NodeManager::currentNM()->realType());
+ d_taylor_degree = options::nlExtTfTaylorDegree();
}
NonlinearExtension::~NonlinearExtension() {}
return sum;
}
-std::set<Node> NonlinearExtension::getFalseInModel(
- const std::vector<Node>& assertions) {
- std::set<Node> false_asserts;
+std::vector<Node> NonlinearExtension::checkModel(
+ const std::vector<Node>& assertions)
+{
+ std::vector<Node> false_asserts;
for (size_t i = 0; i < assertions.size(); ++i) {
Node lit = assertions[i];
Node atom = lit.getKind()==NOT ? lit[0] : lit;
if (litv != d_true) {
Trace("nl-ext-mv") << " [model-false]" << std::endl;
//Assert(litv == d_false);
- false_asserts.insert(lit);
+ false_asserts.push_back(lit);
} else {
Trace("nl-ext-mv") << std::endl;
}
return false_asserts;
}
+bool NonlinearExtension::checkModelTf(const std::vector<Node>& assertions)
+{
+ Trace("nl-ext-tf-check-model") << "check-model : Run" << std::endl;
+ // add bounds for PI
+ d_tf_check_model_bounds[d_pi] =
+ std::pair<Node, Node>(d_pi_bound[0], d_pi_bound[1]);
+ for (const std::pair<const Node, std::pair<Node, Node> >& tfb :
+ d_tf_check_model_bounds)
+ {
+ Node tf = tfb.first;
+ Trace("nl-ext-tf-check-model")
+ << "check-model : satisfied approximate bound : ";
+ Trace("nl-ext-tf-check-model") << tfb.second.first << " <= " << tf
+ << " <= " << tfb.second.second << std::endl;
+ }
+
+ std::vector<Node> check_assertions;
+ for (const Node& a : assertions)
+ {
+ Node av = computeModelValue(a);
+ // simple check
+ if (!simpleCheckModelTfLit(av))
+ {
+ check_assertions.push_back(av);
+ Trace("nl-ext-tf-check-model") << "check-model : assertion : " << av
+ << " (from " << a << ")" << std::endl;
+ }
+ }
+
+ if (check_assertions.empty())
+ {
+ return true;
+ }
+ else
+ {
+ // TODO (#1450) check model for general case
+ return false;
+ }
+}
+
+bool NonlinearExtension::simpleCheckModelTfLit(Node lit)
+{
+ Trace("nl-ext-tf-check-model-simple") << "simple check-model for " << lit
+ << "..." << std::endl;
+ NodeManager* nm = NodeManager::currentNM();
+ bool pol = lit.getKind() != kind::NOT;
+ Node atom = lit.getKind() == kind::NOT ? lit[0] : lit;
+
+ if (atom.getKind() == kind::GEQ)
+ {
+ std::map<Node, Node> msum;
+ if (ArithMSum::getMonomialSumLit(atom, msum))
+ {
+ // map from transcendental functions to whether they were set to lower
+ // bound
+ std::map<Node, bool> set_bound;
+ std::vector<Node> sum_bound;
+ for (std::pair<const Node, Node>& m : msum)
+ {
+ Node v = m.first;
+ if (v.isNull())
+ {
+ sum_bound.push_back(m.second.isNull() ? d_one : m.second);
+ }
+ else
+ {
+ std::map<Node, std::pair<Node, Node> >::iterator bit =
+ d_tf_check_model_bounds.find(v);
+ if (bit != d_tf_check_model_bounds.end())
+ {
+ bool set_lower =
+ (m.second.isNull() || m.second.getConst<Rational>().sgn() == 1)
+ == pol;
+ std::map<Node, bool>::iterator itsb = set_bound.find(v);
+ if (itsb != set_bound.end() && itsb->second != set_lower)
+ {
+ Trace("nl-ext-tf-check-model-simple")
+ << " failed due to conflicting bound for " << v << std::endl;
+ return false;
+ }
+ set_bound[v] = set_lower;
+ // must over/under approximate
+ Node vbound = set_lower ? bit->second.first : bit->second.second;
+ sum_bound.push_back(ArithMSum::mkCoeffTerm(m.second, vbound));
+ }
+ else
+ {
+ Trace("nl-ext-tf-check-model-simple")
+ << " failed due to unknown bound for " << v << std::endl;
+ return false;
+ }
+ }
+ }
+ Node bound;
+ if (sum_bound.size() > 1)
+ {
+ bound = nm->mkNode(kind::PLUS, sum_bound);
+ }
+ else if (sum_bound.size() == 1)
+ {
+ bound = sum_bound[0];
+ }
+ else
+ {
+ bound = d_zero;
+ }
+ Node comp = nm->mkNode(kind::GEQ, bound, d_zero);
+ if (!pol)
+ {
+ comp = comp.negate();
+ }
+ Trace("nl-ext-tf-check-model-simple") << " comparison is : " << comp
+ << std::endl;
+ comp = Rewriter::rewrite(comp);
+ Assert(comp.isConst());
+ Trace("nl-ext-tf-check-model-simple") << " returned : " << comp
+ << std::endl;
+ return comp == d_true;
+ }
+ }
+
+ Trace("nl-ext-tf-check-model-simple") << " failed due to unknown literal."
+ << std::endl;
+ return false;
+}
+
std::vector<Node> NonlinearExtension::checkSplitZero() {
std::vector<Node> lemmas;
for (unsigned i = 0; i < d_ms_vars.size(); i++) {
}
int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
- const std::set<Node>& false_asserts,
- const std::vector<Node>& xts) {
+ const std::vector<Node>& false_asserts,
+ const std::vector<Node>& xts)
+{
d_ms_vars.clear();
d_ms_proc.clear();
d_ms.clear();
d_ci_max.clear();
d_tf_rep_map.clear();
d_tf_region.clear();
+ d_tf_check_model_bounds.clear();
int lemmas_proc = 0;
std::vector<Node> lemmas;
}
}
} else {
- Assert(e == Theory::EFFORT_LAST_CALL);
- Trace("nl-ext-mv") << "Getting model values... check for [model-false]"
- << std::endl;
- // reset cached information
- d_mv[0].clear();
- d_mv[1].clear();
-
- // get the assertions
- std::vector<Node> assertions;
- for (Theory::assertions_iterator it = d_containing.facts_begin();
- it != d_containing.facts_end(); ++it) {
- const Assertion& assertion = *it;
- assertions.push_back(assertion.assertion);
- }
- // get the assertions that are false in the model
- const std::set<Node> false_asserts = getFalseInModel(assertions);
-
- // get the extended terms belonging to this theory
- std::vector<Node> xts;
- d_containing.getExtTheory()->getTerms(xts);
-
- if( Trace.isOn("nl-ext-debug") ){
- Trace("nl-ext-debug") << " processing NonlinearExtension::check : " << std::endl;
- Trace("nl-ext-debug") << " " << false_asserts.size() << " false assertions" << std::endl;
- Trace("nl-ext-debug") << " " << xts.size() << " extended terms: " << std::endl;
- Trace("nl-ext-debug") << " ";
- for( unsigned j=0; j<xts.size(); j++ ){
- Trace("nl-ext-debug") << xts[j] << " ";
- }
- Trace("nl-ext-debug") << std::endl;
- }
-
- // compute whether shared terms have correct values
- unsigned num_shared_wrong_value = 0;
- std::vector< Node > shared_term_value_splits;
- //must ensure that shared terms are equal to their concrete value
- for (context::CDList<TNode>::const_iterator its = d_containing.shared_terms_begin();
- its != d_containing.shared_terms_end(); ++its) {
- TNode shared_term = *its;
- // compute its value in the model, and its evaluation in the model
- Node stv0 = computeModelValue( shared_term, 0 );
- Node stv1 = computeModelValue( shared_term, 1 );
- if( stv0!=stv1 ){
- num_shared_wrong_value++;
- Trace("nl-ext-mv") << "Bad shared term value : " << shared_term << " : " << stv1 << ", actual is " << stv0 << std::endl;
- if( shared_term!=stv0 ){
- //split on the value, this is non-terminating in general, TODO : improve this
- Node eq = shared_term.eqNode(stv0);
- shared_term_value_splits.push_back( eq );
- }else{
- // this can happen for transcendental functions
- // the problem is that we cannot evaluate transcendental functions (they don't have a rewriter that returns constants)
- // thus, the actual value in their model can be themselves, hence we have no reference
- // point to rule out the current model. In this case, we may set incomplete below.
+ bool needsRecheck;
+ do
+ {
+ needsRecheck = false;
+ Assert(e == Theory::EFFORT_LAST_CALL);
+ Trace("nl-ext-mv") << "Getting model values... check for [model-false]"
+ << std::endl;
+ // reset cached information
+ d_mv[0].clear();
+ d_mv[1].clear();
+
+ // get the assertions
+ std::vector<Node> assertions;
+ for (Theory::assertions_iterator it = d_containing.facts_begin();
+ it != d_containing.facts_end();
+ ++it)
+ {
+ const Assertion& assertion = *it;
+ assertions.push_back(assertion.assertion);
+ }
+ // get the assertions that are false in the model
+ const std::vector<Node> false_asserts = checkModel(assertions);
+
+ // get the extended terms belonging to this theory
+ std::vector<Node> xts;
+ d_containing.getExtTheory()->getTerms(xts);
+
+ if (Trace.isOn("nl-ext-debug"))
+ {
+ Trace("nl-ext-debug") << " processing NonlinearExtension::check : "
+ << std::endl;
+ Trace("nl-ext-debug") << " " << false_asserts.size()
+ << " false assertions" << std::endl;
+ Trace("nl-ext-debug") << " " << xts.size()
+ << " extended terms: " << std::endl;
+ Trace("nl-ext-debug") << " ";
+ for (unsigned j = 0; j < xts.size(); j++)
+ {
+ Trace("nl-ext-debug") << xts[j] << " ";
}
+ Trace("nl-ext-debug") << std::endl;
}
- }
- Trace("nl-ext-debug") << " " << num_shared_wrong_value << " shared terms with wrong model value." << std::endl;
-
- // we require a check either if an assertion is false or a shared term has a wrong value
- bool isIncomplete = false;
- int num_added_lemmas = 0;
- if(!false_asserts.empty() || num_shared_wrong_value>0 ){
- isIncomplete = true;
- num_added_lemmas = checkLastCall(assertions, false_asserts, xts);
- }
-
- //if we did not add a lemma during check
- if(num_added_lemmas==0) {
- if(num_shared_wrong_value>0) {
- // resort to splitting on shared terms with their model value
- isIncomplete = true;
- if( !shared_term_value_splits.empty() ){
- std::vector< Node > shared_term_value_lemmas;
- for( unsigned i=0; i<shared_term_value_splits.size(); i++ ){
- Node eq = shared_term_value_splits[i];
- Node literal = d_containing.getValuation().ensureLiteral(eq);
- d_containing.getOutputChannel().requirePhase(literal, true);
- shared_term_value_lemmas.push_back(literal.orNode(literal.negate()));
+
+ // compute whether shared terms have correct values
+ unsigned num_shared_wrong_value = 0;
+ std::vector<Node> shared_term_value_splits;
+ // must ensure that shared terms are equal to their concrete value
+ for (context::CDList<TNode>::const_iterator its =
+ d_containing.shared_terms_begin();
+ its != d_containing.shared_terms_end();
+ ++its)
+ {
+ TNode shared_term = *its;
+ // compute its value in the model, and its evaluation in the model
+ Node stv0 = computeModelValue(shared_term, 0);
+ Node stv1 = computeModelValue(shared_term, 1);
+ if (stv0 != stv1)
+ {
+ num_shared_wrong_value++;
+ Trace("nl-ext-mv") << "Bad shared term value : " << shared_term
+ << " : " << stv1 << ", actual is " << stv0
+ << std::endl;
+ if (shared_term != stv0)
+ {
+ // split on the value, this is non-terminating in general, TODO :
+ // improve this
+ Node eq = shared_term.eqNode(stv0);
+ shared_term_value_splits.push_back(eq);
+ }
+ else
+ {
+ // this can happen for transcendental functions
+ // the problem is that we cannot evaluate transcendental functions
+ // (they don't have a rewriter that returns constants)
+ // thus, the actual value in their model can be themselves, hence we
+ // have no reference
+ // point to rule out the current model. In this case, we may set
+ // incomplete below.
}
- num_added_lemmas = flushLemmas(shared_term_value_lemmas);
- Trace("nl-ext") << "...added " << num_added_lemmas << " shared term value split lemmas." << std::endl;
- }else{
- // this can happen if we are trying to do theory combination with trancendental functions
- // since their model value cannot even be computed exactly
}
}
-
+ Trace("nl-ext-debug") << " " << num_shared_wrong_value
+ << " shared terms with wrong model value."
+ << std::endl;
+
+ // we require a check either if an assertion is false or a shared term has
+ // a wrong value
+ bool isIncomplete = false;
+ int num_added_lemmas = 0;
+ if (!false_asserts.empty() || num_shared_wrong_value > 0)
+ {
+ isIncomplete = true;
+ num_added_lemmas = checkLastCall(assertions, false_asserts, xts);
+ }
+
+ // if we did not add a lemma during check
if(num_added_lemmas==0) {
- if(isIncomplete) {
- Trace("nl-ext") << "...failed to send lemma in NonLinearExtension, set incomplete" << std::endl;
- d_containing.getOutputChannel().setIncomplete();
+ if (num_shared_wrong_value > 0)
+ {
+ // resort to splitting on shared terms with their model value
+ isIncomplete = true;
+ if (!shared_term_value_splits.empty())
+ {
+ std::vector<Node> shared_term_value_lemmas;
+ for (const Node& eq : shared_term_value_splits)
+ {
+ Node literal = d_containing.getValuation().ensureLiteral(eq);
+ d_containing.getOutputChannel().requirePhase(literal, true);
+ shared_term_value_lemmas.push_back(
+ literal.orNode(literal.negate()));
+ }
+ num_added_lemmas = flushLemmas(shared_term_value_lemmas);
+ Trace("nl-ext") << "...added " << num_added_lemmas
+ << " shared term value split lemmas." << std::endl;
+ }
+ else
+ {
+ // this can happen if we are trying to do theory combination with
+ // trancendental functions
+ // since their model value cannot even be computed exactly
+ }
+ }
+ if (num_added_lemmas == 0)
+ {
+ if (isIncomplete)
+ {
+ // check the model using error bounds on the Taylor approximation
+ if (!d_tf_rep_map.empty() && checkModelTf(false_asserts))
+ {
+ isIncomplete = false;
+ }
+ }
+ if (isIncomplete)
+ {
+ if (options::nlExtTfIncPrecision() && !d_tf_rep_map.empty())
+ {
+ d_taylor_degree++;
+ d_secant_points.clear();
+ needsRecheck = true;
+ // increase precision for PI?
+ // Difficult since Taylor series is very slow to converge
+ Trace("nl-ext") << "...increment Taylor degree to "
+ << d_taylor_degree << std::endl;
+ }
+ else
+ {
+ Trace("nl-ext") << "...failed to send lemma in "
+ "NonLinearExtension, set incomplete"
+ << std::endl;
+ d_containing.getOutputChannel().setIncomplete();
+ }
+ }
}
}
- }
+ } while (needsRecheck);
}
}
void NonlinearExtension::getCurrentPiBounds( std::vector< Node >& lemmas ) {
Node pi_lem = NodeManager::currentNM()->mkNode(
AND,
- NodeManager::currentNM()->mkNode(GT, d_pi, d_pi_bound[0]),
- NodeManager::currentNM()->mkNode(LT, d_pi, d_pi_bound[1]));
+ NodeManager::currentNM()->mkNode(GEQ, d_pi, d_pi_bound[0]),
+ NodeManager::currentNM()->mkNode(LEQ, d_pi, d_pi_bound[1]));
lemmas.push_back( pi_lem );
}
Trace("nl-ext") << "...trying " << lemmas.size()
<< " tangent plane lemmas..." << std::endl;
return lemmas;
-}
-
+}
-
-std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node>& nt_lemmas,
- const std::set<Node>& false_asserts ) {
+std::vector<Node> NonlinearExtension::checkMonomialInferBounds(
+ std::vector<Node>& nt_lemmas, const std::vector<Node>& false_asserts)
+{
std::vector< Node > lemmas;
// register constraints
Trace("nl-ext-debug") << "Register bound constraints..." << std::endl;
bool polarity = lit.getKind() != NOT;
Node atom = lit.getKind() == NOT ? lit[0] : lit;
registerConstraint(atom);
- bool is_false_lit = false_asserts.find(lit) != false_asserts.end();
+ bool is_false_lit =
+ std::find(false_asserts.begin(), false_asserts.end(), lit)
+ != false_asserts.end();
// add information about bounds to variables
std::map<Node, std::map<Node, ConstraintInfo> >::iterator itc =
d_c_info.find(atom);
return lemmas;
}
-std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& false_asserts ) {
+std::vector<Node> NonlinearExtension::checkFactoring(
+ const std::vector<Node>& false_asserts)
+{
std::vector< Node > lemmas;
Trace("nl-ext") << "Get factoring lemmas..." << std::endl;
for (context::CDList<Assertion>::const_iterator it =
Node lit = (*it).assertion;
bool polarity = lit.getKind() != NOT;
Node atom = lit.getKind() == NOT ? lit[0] : lit;
- if( false_asserts.find(lit) != false_asserts.end() || d_skolem_atoms.find(atom)!=d_skolem_atoms.end() ){
+ if (std::find(false_asserts.begin(), false_asserts.end(), lit)
+ != false_asserts.end()
+ || d_skolem_atoms.find(atom) != d_skolem_atoms.end())
+ {
std::map<Node, Node> msum;
if (ArithMSum::getMonomialSumLit(atom, msum))
{
std::map<int, Node>
poly_approx_bounds_neg[2]; // the negative case is different for exp
// n is the Taylor degree we are currently considering
- unsigned n = 8;
+ unsigned n = 2 * d_taylor_degree;
// n must be even
std::pair<Node, Node> taylor = getTaylor(tft, n);
Trace("nl-ext-tf-tplanes-debug") << "Taylor for " << k
Trace("nl-ext-tf-tplanes-debug") << "...poly appoximation at c is "
<< poly_approx_c << std::endl;
}
+ else
+ {
+ // store for check model bounds
+ Node atf = computeModelValue(tf);
+ d_tf_check_model_bounds[atf] =
+ std::pair<Node, Node>(model_values[0], model_values[1]);
+ }
if (is_tangent)
{
* TheoryArith.
*/
int checkLastCall(const std::vector<Node>& assertions,
- const std::set<Node>& false_asserts,
+ const std::vector<Node>& false_asserts,
const std::vector<Node>& xts);
//---------------------------------------term utilities
static bool isArithKind(Kind k);
void assignOrderIds(std::vector<Node>& vars, NodeMultiset& d_order,
unsigned orderType);
- /** Returns the subset of assertions whose concrete values are
- * false in the model.
+ /** check model
+ *
+ * Returns the subset of assertions whose concrete values we cannot show are
+ * true in the current model. Notice that we typically cannot compute concrete
+ * values for assertions involving transcendental functions. Any assertion
+ * whose model value cannot be computed is included in the return value of
+ * this function.
+ */
+ std::vector<Node> checkModel(const std::vector<Node>& assertions);
+
+ /** check model for transcendental functions
+ *
+ * Checks the current model using error bounds on the Taylor approximation.
+ *
+ * If this function returns true, then all assertions in the input argument
+ * "assertions" are satisfied for all interpretations of transcendental
+ * functions within their error bounds (as stored in d_tf_check_model_bounds).
+ *
+ * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
+ * "Detecting Satisfiable Formulas".
+ */
+ bool checkModelTf(const std::vector<Node>& assertions);
+
+ /** simple check model for transcendental functions for literal
+ *
+ * This method returns true if literal is true for all interpretations of
+ * transcendental functions within their error bounds (as stored
+ * in d_tf_check_model_bounds). This is determined by a simple under/over
+ * approximation of the value of sum of (linear) monomials. For example,
+ * if we determine that .8 < sin( 1 ) < .9, this function will return
+ * true for literals like:
+ * 2.0*sin( 1 ) > 1.5
+ * -1.0*sin( 1 ) < -0.79
+ * -1.0*sin( 1 ) > -0.91
+ * It will return false for literals like:
+ * sin( 1 ) > 0.85
+ * It will also return false for literals like:
+ * -0.3*sin( 1 )*sin( 2 ) + sin( 2 ) > .7
+ * sin( sin( 1 ) ) > .5
+ * since the bounds on these terms cannot quickly be determined.
*/
- std::set<Node> getFalseInModel(const std::vector<Node>& assertions);
+ bool simpleCheckModelTfLit(Node lit);
/** In the following functions, status states a relationship
* between two arithmetic terms, where:
* where r is the current representative of x
* in the equality engine assoiated with this class.
*/
- std::map< Kind, std::map< Node, Node > > d_tf_rep_map;
-
+ std::map<Kind, std::map<Node, Node> > d_tf_rep_map;
+
+ /** bounds for transcendental functions
+ *
+ * For each transcendental function application t, if this stores the pair
+ * (c_l, c_u) then the model M is such that c_l <= M( t ) <= c_u.
+ */
+ std::map<Node, std::pair<Node, Node> > d_tf_check_model_bounds;
+
// factor skolems
std::map< Node, Node > d_factor_skolem;
Node getFactorSkolem( Node n, std::vector< Node >& lemmas );
std::unordered_map<Node, std::unordered_map<unsigned, Node>, NodeHashFunction>
d_taylor_rem;
+ /** taylor degree
+ *
+ * Indicates that the degree of the polynomials in the Taylor approximation of
+ * all transcendental functions is 2*d_taylor_degree. This value is set
+ * initially to options::nlExtTfTaylorDegree() and may be incremented
+ * if the option options::nlExtTfIncPrecision() is enabled.
+ */
+ unsigned d_taylor_degree;
+
/** concavity region for transcendental functions
*
* This stores an integer that identifies an interval in
* ...where (y > z + w) and x*y are a constraint and term
* that occur in the current context.
*/
- std::vector<Node> checkMonomialInferBounds( std::vector<Node>& nt_lemmas,
- const std::set<Node>& false_asserts );
+ std::vector<Node> checkMonomialInferBounds(
+ std::vector<Node>& nt_lemmas, const std::vector<Node>& false_asserts);
/** check factoring
*
* ...where k is fresh and x*z + y*z > t is a
* constraint that occurs in the current context.
*/
- std::vector<Node> checkFactoring( const std::set<Node>& false_asserts );
+ std::vector<Node> checkFactoring(const std::vector<Node>& false_asserts);
/** check monomial infer resolution bounds
*
projects / cvc5.git / commitdiff