1 /********************* */
2 /*! \file nonlinear_extension.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Gereon Kremer, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/arith/nl/nonlinear_extension.h"
20 #include "options/arith_options.h"
21 #include "options/theory_options.h"
22 #include "theory/arith/arith_state.h"
23 #include "theory/arith/arith_utilities.h"
24 #include "theory/arith/bound_inference.h"
25 #include "theory/arith/theory_arith.h"
26 #include "theory/ext_theory.h"
27 #include "theory/theory_model.h"
29 using namespace CVC4::kind
;
36 NonlinearExtension::NonlinearExtension(TheoryArith
& containing
,
38 eq::EqualityEngine
* ee
,
39 ProofNodeManager
* pnm
)
40 : d_containing(containing
),
41 d_im(containing
.getInferenceManager()),
42 d_needsLastCall(false),
45 d_extTheory(d_extTheoryCb
,
46 containing
.getSatContext(),
47 containing
.getUserContext(),
48 containing
.getOutputChannel()),
49 d_model(containing
.getSatContext()),
50 d_trSlv(d_im
, d_model
, pnm
, containing
.getUserContext()),
51 d_extState(d_im
, d_model
, pnm
, containing
.getUserContext()),
52 d_factoringSlv(&d_extState
),
53 d_monomialBoundsSlv(&d_extState
),
54 d_monomialSlv(&d_extState
),
55 d_splitZeroSlv(&d_extState
),
56 d_tangentPlaneSlv(&d_extState
),
57 d_cadSlv(d_im
, d_model
),
59 d_iandSlv(d_im
, state
, d_model
),
60 d_builtModel(containing
.getSatContext(), false)
62 d_extTheory
.addFunctionKind(kind::NONLINEAR_MULT
);
63 d_extTheory
.addFunctionKind(kind::EXPONENTIAL
);
64 d_extTheory
.addFunctionKind(kind::SINE
);
65 d_extTheory
.addFunctionKind(kind::PI
);
66 d_extTheory
.addFunctionKind(kind::IAND
);
67 d_true
= NodeManager::currentNM()->mkConst(true);
68 d_zero
= NodeManager::currentNM()->mkConst(Rational(0));
69 d_one
= NodeManager::currentNM()->mkConst(Rational(1));
70 d_neg_one
= NodeManager::currentNM()->mkConst(Rational(-1));
72 ProofChecker
* pc
= pnm
!= nullptr ? pnm
->getChecker() : nullptr;
75 d_proofChecker
.registerTo(pc
);
79 NonlinearExtension::~NonlinearExtension() {}
81 void NonlinearExtension::preRegisterTerm(TNode n
)
83 // register terms with extended theory, to find extended terms that can be
84 // eliminated by context-depedendent simplification.
85 d_extTheory
.registerTermRec(n
);
88 void NonlinearExtension::sendLemmas(const std::vector
<NlLemma
>& out
)
90 for (const NlLemma
& nlem
: out
)
92 Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem
.d_inference
93 << " : " << nlem
.d_node
<< std::endl
;
94 d_im
.addPendingArithLemma(nlem
);
95 d_stats
.d_inferences
<< nlem
.d_inference
;
99 void NonlinearExtension::processSideEffect(const NlLemma
& se
)
101 d_trSlv
.processSideEffect(se
);
104 void NonlinearExtension::computeRelevantAssertions(
105 const std::vector
<Node
>& assertions
, std::vector
<Node
>& keep
)
107 Trace("nl-ext-rlv") << "Compute relevant assertions..." << std::endl
;
108 Valuation v
= d_containing
.getValuation();
109 for (const Node
& a
: assertions
)
116 Trace("nl-ext-rlv") << "...keep " << keep
.size() << "/" << assertions
.size()
117 << " assertions" << std::endl
;
120 unsigned NonlinearExtension::filterLemma(NlLemma lem
, std::vector
<NlLemma
>& out
)
122 Trace("nl-ext-lemma-debug")
123 << "NonlinearExtension::Lemma pre-rewrite : " << lem
.d_node
<< std::endl
;
124 lem
.d_node
= Rewriter::rewrite(lem
.d_node
);
126 if (d_im
.hasCachedLemma(lem
.d_node
, lem
.d_property
))
128 Trace("nl-ext-lemma-debug")
129 << "NonlinearExtension::Lemma duplicate : " << lem
.d_node
<< std::endl
;
132 out
.emplace_back(lem
);
136 unsigned NonlinearExtension::filterLemmas(std::vector
<NlLemma
>& lemmas
,
137 std::vector
<NlLemma
>& out
)
139 if (options::nlExtEntailConflicts())
141 // check if any are entailed to be false
142 for (const NlLemma
& lem
: lemmas
)
144 Node ch_lemma
= lem
.d_node
.negate();
145 ch_lemma
= Rewriter::rewrite(ch_lemma
);
146 Trace("nl-ext-et-debug")
147 << "Check entailment of " << ch_lemma
<< "..." << std::endl
;
148 std::pair
<bool, Node
> et
= d_containing
.getValuation().entailmentCheck(
149 options::TheoryOfMode::THEORY_OF_TYPE_BASED
, ch_lemma
);
150 Trace("nl-ext-et-debug") << "entailment test result : " << et
.first
<< " "
151 << et
.second
<< std::endl
;
154 Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : "
155 << lem
.d_node
<< std::endl
;
156 // return just this lemma
157 if (filterLemma(lem
, out
) > 0)
167 for (const NlLemma
& lem
: lemmas
)
169 sum
+= filterLemma(lem
, out
);
170 d_containing
.getOutputChannel().spendResource(
171 ResourceManager::Resource::ArithNlLemmaStep
);
177 void NonlinearExtension::getAssertions(std::vector
<Node
>& assertions
)
179 Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl
;
180 bool useRelevance
= false;
181 if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE
)
183 useRelevance
= (d_checkCounter
% 2);
185 else if (options::nlRlvMode() == options::NlRlvMode::ALWAYS
)
189 Valuation v
= d_containing
.getValuation();
191 BoundInference bounds
;
193 std::unordered_set
<Node
, NodeHashFunction
> init_assertions
;
195 for (Theory::assertions_iterator it
= d_containing
.facts_begin();
196 it
!= d_containing
.facts_end();
199 const Assertion
& assertion
= *it
;
200 Trace("nl-ext-assert-debug")
201 << "Loaded " << assertion
.d_assertion
<< " from theory" << std::endl
;
202 Node lit
= assertion
.d_assertion
;
203 if (useRelevance
&& !v
.isRelevant(lit
))
205 // not relevant, skip
208 if (bounds
.add(lit
, false))
212 init_assertions
.insert(lit
);
215 for (const auto& vb
: bounds
.get())
217 const Bounds
& b
= vb
.second
;
218 if (!b
.lower_bound
.isNull())
220 init_assertions
.insert(b
.lower_bound
);
222 if (!b
.upper_bound
.isNull())
224 init_assertions
.insert(b
.upper_bound
);
228 // Try to be "more deterministic" by adding assertions in the order they were
230 for (auto it
= d_containing
.facts_begin(); it
!= d_containing
.facts_end();
233 Node lit
= (*it
).d_assertion
;
234 auto iait
= init_assertions
.find(lit
);
235 if (iait
!= init_assertions
.end())
237 Trace("nl-ext-assert-debug") << "Adding " << lit
<< std::endl
;
238 assertions
.push_back(lit
);
239 init_assertions
.erase(iait
);
242 // Now add left over assertions that have been newly created within this
243 // function by the code above.
244 for (const Node
& a
: init_assertions
)
246 Trace("nl-ext-assert-debug") << "Adding " << a
<< std::endl
;
247 assertions
.push_back(a
);
249 Trace("nl-ext") << "...keep " << assertions
.size() << " / "
250 << d_containing
.numAssertions() << " assertions."
254 std::vector
<Node
> NonlinearExtension::checkModelEval(
255 const std::vector
<Node
>& assertions
)
257 std::vector
<Node
> false_asserts
;
258 for (size_t i
= 0; i
< assertions
.size(); ++i
)
260 Node lit
= assertions
[i
];
261 Node atom
= lit
.getKind() == NOT
? lit
[0] : lit
;
262 Node litv
= d_model
.computeConcreteModelValue(lit
);
263 Trace("nl-ext-mv-assert") << "M[[ " << lit
<< " ]] -> " << litv
;
266 Trace("nl-ext-mv-assert") << " [model-false]" << std::endl
;
267 false_asserts
.push_back(lit
);
271 Trace("nl-ext-mv-assert") << std::endl
;
274 return false_asserts
;
277 bool NonlinearExtension::checkModel(const std::vector
<Node
>& assertions
)
279 Trace("nl-ext-cm") << "--- check-model ---" << std::endl
;
281 // get the presubstitution
282 Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl
;
283 // Notice that we do not consider relevance here, since assertions were
284 // already filtered based on relevance. It is incorrect to filter based on
285 // relevance here, since we may have discarded literals that are relevant
286 // that are entailed based on the techniques in getAssertions.
287 std::vector
<Node
> passertions
= assertions
;
288 if (options::nlExt())
290 // preprocess the assertions with the trancendental solver
291 if (!d_trSlv
.preprocessAssertionsCheckModel(passertions
))
296 if (options::nlCad())
298 d_cadSlv
.constructModelIfAvailable(passertions
);
301 Trace("nl-ext-cm") << "-----" << std::endl
;
302 unsigned tdegree
= d_trSlv
.getTaylorDegree();
303 std::vector
<NlLemma
> lemmas
;
304 bool ret
= d_model
.checkModel(passertions
, tdegree
, lemmas
);
305 for (const auto& al
: lemmas
)
307 d_im
.addPendingArithLemma(al
);
312 void NonlinearExtension::check(Theory::Effort e
)
314 Trace("nl-ext") << std::endl
;
315 Trace("nl-ext") << "NonlinearExtension::check, effort = " << e
316 << ", built model = " << d_builtModel
.get() << std::endl
;
317 if (e
== Theory::EFFORT_FULL
)
319 d_extTheory
.clearCache();
320 d_needsLastCall
= true;
321 if (options::nlExtRewrites())
323 std::vector
<Node
> nred
;
324 if (!d_extTheory
.doInferences(0, nred
))
326 Trace("nl-ext") << "...sent no lemmas, # extf to reduce = "
327 << nred
.size() << std::endl
;
330 d_needsLastCall
= false;
335 Trace("nl-ext") << "...sent lemmas." << std::endl
;
341 // If we computed lemmas during collectModelInfo, send them now.
342 if (d_im
.hasPendingLemma())
344 d_im
.doPendingFacts();
345 d_im
.doPendingLemmas();
346 d_im
.doPendingPhaseRequirements();
350 // Otherwise, we will answer SAT. The values that we approximated are
351 // recorded as approximations here.
352 TheoryModel
* tm
= d_containing
.getValuation().getModel();
353 for (std::pair
<const Node
, std::pair
<Node
, Node
>>& a
: d_approximations
)
355 if (a
.second
.second
.isNull())
357 tm
->recordApproximation(a
.first
, a
.second
.first
);
361 tm
->recordApproximation(a
.first
, a
.second
.first
, a
.second
.second
);
364 for (const auto& vw
: d_witnesses
)
366 tm
->recordApproximation(vw
.first
, vw
.second
);
371 bool NonlinearExtension::modelBasedRefinement()
373 ++(d_stats
.d_mbrRuns
);
376 // get the assertions
377 std::vector
<Node
> assertions
;
378 getAssertions(assertions
);
380 Trace("nl-ext-mv-assert")
381 << "Getting model values... check for [model-false]" << std::endl
;
382 // get the assertions that are false in the model
383 const std::vector
<Node
> false_asserts
= checkModelEval(assertions
);
384 Trace("nl-ext") << "# false asserts = " << false_asserts
.size() << std::endl
;
386 // get the extended terms belonging to this theory
387 std::vector
<Node
> xts
;
388 d_extTheory
.getTerms(xts
);
390 if (Trace
.isOn("nl-ext-debug"))
392 Trace("nl-ext-debug") << " processing NonlinearExtension::check : "
394 Trace("nl-ext-debug") << " " << false_asserts
.size()
395 << " false assertions" << std::endl
;
396 Trace("nl-ext-debug") << " " << xts
.size()
397 << " extended terms: " << std::endl
;
398 Trace("nl-ext-debug") << " ";
399 for (unsigned j
= 0; j
< xts
.size(); j
++)
401 Trace("nl-ext-debug") << xts
[j
] << " ";
403 Trace("nl-ext-debug") << std::endl
;
406 // compute whether shared terms have correct values
407 unsigned num_shared_wrong_value
= 0;
408 std::vector
<Node
> shared_term_value_splits
;
409 // must ensure that shared terms are equal to their concrete value
410 Trace("nl-ext-mv") << "Shared terms : " << std::endl
;
411 for (context::CDList
<TNode
>::const_iterator its
=
412 d_containing
.shared_terms_begin();
413 its
!= d_containing
.shared_terms_end();
416 TNode shared_term
= *its
;
417 // compute its value in the model, and its evaluation in the model
418 Node stv0
= d_model
.computeConcreteModelValue(shared_term
);
419 Node stv1
= d_model
.computeAbstractModelValue(shared_term
);
420 d_model
.printModelValue("nl-ext-mv", shared_term
);
423 num_shared_wrong_value
++;
424 Trace("nl-ext-mv") << "Bad shared term value : " << shared_term
426 if (shared_term
!= stv0
)
428 // split on the value, this is non-terminating in general, TODO :
430 Node eq
= shared_term
.eqNode(stv0
);
431 shared_term_value_splits
.push_back(eq
);
435 // this can happen for transcendental functions
436 // the problem is that we cannot evaluate transcendental functions
437 // (they don't have a rewriter that returns constants)
438 // thus, the actual value in their model can be themselves, hence we
439 // have no reference point to rule out the current model. In this
440 // case, we may set incomplete below.
444 Trace("nl-ext-debug") << " " << num_shared_wrong_value
445 << " shared terms with wrong model value." << std::endl
;
449 d_model
.resetCheck();
450 needsRecheck
= false;
452 // 1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown
453 int complete_status
= 1;
454 // We require a check either if an assertion is false or a shared term has
456 if (!false_asserts
.empty() || num_shared_wrong_value
> 0)
458 complete_status
= num_shared_wrong_value
> 0 ? -1 : 0;
459 runStrategy(Theory::Effort::EFFORT_FULL
, assertions
, false_asserts
, xts
);
460 if (d_im
.hasSentLemma() || d_im
.hasPendingLemma())
462 d_im
.clearWaitingLemmas();
466 Trace("nl-ext") << "Finished check with status : " << complete_status
469 // if we did not add a lemma during check and there is a chance for SAT
470 if (complete_status
== 0)
473 << "Check model based on bounds for irrational-valued functions..."
475 // check the model based on simple solving of equalities and using
476 // error bounds on the Taylor approximation of transcendental functions.
477 if (checkModel(assertions
))
483 d_im
.clearWaitingLemmas();
488 // if we have not concluded SAT
489 if (complete_status
!= 1)
491 // flush the waiting lemmas
492 if (d_im
.hasWaitingLemma())
494 std::size_t count
= d_im
.numWaitingLemmas();
495 d_im
.flushWaitingLemmas();
496 Trace("nl-ext") << "...added " << count
<< " waiting lemmas."
500 // resort to splitting on shared terms with their model value
501 // if we did not add any lemmas
502 if (num_shared_wrong_value
> 0)
504 complete_status
= -1;
505 if (!shared_term_value_splits
.empty())
507 for (const Node
& eq
: shared_term_value_splits
)
509 Node req
= Rewriter::rewrite(eq
);
510 Node literal
= d_containing
.getValuation().ensureLiteral(req
);
511 d_containing
.getOutputChannel().requirePhase(literal
, true);
512 Trace("nl-ext-debug") << "Split on : " << literal
<< std::endl
;
513 Node split
= literal
.orNode(literal
.negate());
514 NlLemma
nsplit(split
, InferenceId::NL_SHARED_TERM_VALUE_SPLIT
);
515 d_im
.addPendingArithLemma(nsplit
, true);
517 if (d_im
.hasWaitingLemma())
519 d_im
.flushWaitingLemmas();
520 Trace("nl-ext") << "...added " << d_im
.numPendingLemmas()
521 << " shared term value split lemmas." << std::endl
;
527 // this can happen if we are trying to do theory combination with
528 // trancendental functions
529 // since their model value cannot even be computed exactly
534 if (options::nlExt() && options::nlExtIncPrecision()
535 && d_model
.usedApproximate())
537 d_trSlv
.incrementTaylorDegree();
539 // increase precision for PI?
540 // Difficult since Taylor series is very slow to converge
541 Trace("nl-ext") << "...increment Taylor degree to "
542 << d_trSlv
.getTaylorDegree() << std::endl
;
546 Trace("nl-ext") << "...failed to send lemma in "
547 "NonLinearExtension, set incomplete"
549 d_containing
.getOutputChannel().setIncomplete();
554 // we have built a model
557 d_im
.clearWaitingLemmas();
558 } while (needsRecheck
);
560 // did not add lemmas
564 void NonlinearExtension::interceptModel(std::map
<Node
, Node
>& arithModel
)
566 if (!needsCheckLastEffort())
568 // no non-linear constraints, we are done
571 Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl
;
572 d_model
.reset(d_containing
.getValuation().getModel(), arithModel
);
573 // run a last call effort check
574 if (!d_builtModel
.get())
576 Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl
;
577 modelBasedRefinement();
579 if (d_builtModel
.get())
581 Trace("nl-ext") << "interceptModel: do model repair" << std::endl
;
582 d_approximations
.clear();
584 // modify the model values
585 d_model
.getModelValueRepair(arithModel
, d_approximations
, d_witnesses
);
589 void NonlinearExtension::presolve()
591 Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl
;
592 d_builtModel
= false;
595 void NonlinearExtension::runStrategy(Theory::Effort effort
,
596 const std::vector
<Node
>& assertions
,
597 const std::vector
<Node
>& false_asserts
,
598 const std::vector
<Node
>& xts
)
600 ++(d_stats
.d_checkRuns
);
602 if (Trace
.isOn("nl-strategy"))
604 for (const auto& a
: assertions
)
606 Trace("nl-strategy") << "Input assertion: " << a
<< std::endl
;
609 if (!d_strategy
.isStrategyInit())
611 d_strategy
.initializeStrategy();
614 auto steps
= d_strategy
.getStrategy();
616 while (!stop
&& steps
.hasNext())
618 InferStep step
= steps
.next();
619 Trace("nl-strategy") << "Step " << step
<< std::endl
;
622 case InferStep::BREAK
: stop
= d_im
.hasPendingLemma(); break;
623 case InferStep::FLUSH_WAITING_LEMMAS
: d_im
.flushWaitingLemmas(); break;
624 case InferStep::CAD_FULL
: d_cadSlv
.checkFull(); break;
625 case InferStep::CAD_INIT
: d_cadSlv
.initLastCall(assertions
); break;
626 case InferStep::NL_FACTORING
:
627 d_factoringSlv
.check(assertions
, false_asserts
);
629 case InferStep::IAND_INIT
:
630 d_iandSlv
.initLastCall(assertions
, false_asserts
, xts
);
632 case InferStep::IAND_FULL
: d_iandSlv
.checkFullRefine(); break;
633 case InferStep::IAND_INITIAL
: d_iandSlv
.checkInitialRefine(); break;
635 d_icpSlv
.reset(assertions
);
638 case InferStep::NL_INIT
:
639 d_extState
.init(xts
);
640 d_monomialBoundsSlv
.init();
641 d_monomialSlv
.init(xts
);
643 case InferStep::NL_MONOMIAL_INFER_BOUNDS
:
644 d_monomialBoundsSlv
.checkBounds(assertions
, false_asserts
);
646 case InferStep::NL_MONOMIAL_MAGNITUDE0
:
647 d_monomialSlv
.checkMagnitude(0);
649 case InferStep::NL_MONOMIAL_MAGNITUDE1
:
650 d_monomialSlv
.checkMagnitude(1);
652 case InferStep::NL_MONOMIAL_MAGNITUDE2
:
653 d_monomialSlv
.checkMagnitude(2);
655 case InferStep::NL_MONOMIAL_SIGN
: d_monomialSlv
.checkSign(); break;
656 case InferStep::NL_RESOLUTION_BOUNDS
:
657 d_monomialBoundsSlv
.checkResBounds();
659 case InferStep::NL_SPLIT_ZERO
: d_splitZeroSlv
.check(); break;
660 case InferStep::NL_TANGENT_PLANES
: d_tangentPlaneSlv
.check(false); break;
661 case InferStep::NL_TANGENT_PLANES_WAITING
:
662 d_tangentPlaneSlv
.check(true);
664 case InferStep::TRANS_INIT
:
665 d_trSlv
.initLastCall(xts
);
667 case InferStep::TRANS_INITIAL
:
668 d_trSlv
.checkTranscendentalInitialRefine();
670 case InferStep::TRANS_MONOTONIC
:
671 d_trSlv
.checkTranscendentalMonotonic();
673 case InferStep::TRANS_TANGENT_PLANES
:
674 d_trSlv
.checkTranscendentalTangentPlanes();
679 Trace("nl-ext") << "finished strategy" << std::endl
;
680 Trace("nl-ext") << " ...finished with " << d_im
.numWaitingLemmas()
681 << " waiting lemmas." << std::endl
;
682 Trace("nl-ext") << " ...finished with " << d_im
.numPendingLemmas()
683 << " pending lemmas." << std::endl
;
688 } // namespace theory