From eb812afac2884131b21948aee3da9d8c1e92ba98 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 28 Oct 2020 15:17:05 -0500 Subject: [PATCH] Fixes for unconstrained variables in nonlinear model (#5351) This ensures that we explicitly mark x -> 0 as part of the arithmetic model coming from nonlinear for unconstrained variables x that nonlinear extension assumes to be 0. This fixes #5348. --- src/theory/arith/nl/nl_model.cpp | 38 +++++++-------------- src/theory/arith/nl/nl_model.h | 11 +++--- src/theory/arith/nl/nonlinear_extension.cpp | 20 +++++------ src/theory/arith/nl/nonlinear_extension.h | 7 +--- test/regress/CMakeLists.txt | 4 ++- test/regress/regress0/nl/iand-no-init.smt2 | 5 +++ 6 files changed, 36 insertions(+), 49 deletions(-) create mode 100644 test/regress/regress0/nl/iand-no-init.smt2 diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index b27654b2c..79f2a2350 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -159,7 +159,7 @@ Node NlModel::getRepresentative(Node n) const return d_model->getRepresentative(n); } -Node NlModel::getValueInternal(Node n) const +Node NlModel::getValueInternal(Node n) { if (n.isConst()) { @@ -171,7 +171,11 @@ Node NlModel::getValueInternal(Node n) const AlwaysAssert(it->second.isConst()); return it->second; } - // It is unconstrained in the model, return 0. + // It is unconstrained in the model, return 0. We additionally add it + // to mapping from the linear solver. This ensures that if the nonlinear + // solver assumes that n = 0, then this assumption is recorded in the overall + // model. + d_arithVal[n] = d_zero; return d_zero; } @@ -215,8 +219,7 @@ int NlModel::compareValue(Node i, Node j, bool isAbsolute) const bool NlModel::checkModel(const std::vector& assertions, unsigned d, - std::vector& lemmas, - std::vector& gs) + std::vector& lemmas) { Trace("nl-ext-cm-debug") << " solve for equalities..." << std::endl; for (const Node& atom : assertions) @@ -312,26 +315,6 @@ bool NlModel::checkModel(const std::vector& assertions, return false; } Trace("nl-ext-cm") << "...simple check succeeded!" << std::endl; - - // must assert and re-check if produce models is true - if (options::produceModels()) - { - NodeManager* nm = NodeManager::currentNM(); - // model guard whose semantics is "the model we constructed holds" - Node mg = nm->mkSkolem("model", nm->booleanType()); - gs.push_back(mg); - // assert the constructed model as assertions - for (const std::pair> cb : - d_check_model_bounds) - { - Node l = cb.second.first; - Node u = cb.second.second; - Node v = cb.first; - Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); - pred = nm->mkNode(OR, mg.negate(), pred); - lemmas.emplace_back(pred); - } - } return true; } @@ -1280,7 +1263,12 @@ void NlModel::getModelValueRepair( std::map& witnesses) { Trace("nl-model") << "NlModel::getModelValueRepair:" << std::endl; - + // If we extended the model with entries x -> 0 for unconstrained values, + // we first update the map to the extended one. + if (d_arithVal.size() > arithModel.size()) + { + arithModel = d_arithVal; + } // Record the approximations we used. This code calls the // recordApproximation method of the model, which overrides the model // values for variables that we solved for, using techniques specific to diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 7831d78ef..cd2d15563 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -154,8 +154,7 @@ class NlModel */ bool checkModel(const std::vector& assertions, unsigned d, - std::vector& lemmas, - std::vector& gs); + std::vector& lemmas); /** * Set that we have used an approximation during this check. This flag is * reset on a call to resetCheck. It is set when we use reasoning that @@ -195,7 +194,7 @@ class NlModel /** The current model */ TheoryModel* d_model; /** Get the model value of n from the model object above */ - Node getValueInternal(Node n) const; + Node getValueInternal(Node n); /** Does the equality engine of the model have term n? */ bool hasTerm(Node n) const; /** Get the representative of n in the model */ @@ -263,8 +262,10 @@ class NlModel Node d_null; /** * The values that the arithmetic theory solver assigned in the model. This - * corresponds to exactly the set of equalities that TheoryArith is currently - * sending to TheoryModel during collectModelInfo. + * corresponds to the set of equalities that linear solver (via TheoryArith) + * is currently sending to TheoryModel during collectModelValues, plus + * additional entries x -> 0 for variables that were unassigned by the linear + * solver. */ std::map d_arithVal; /** diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index a5ac8e3fe..76f37213a 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -338,8 +338,7 @@ std::vector NonlinearExtension::checkModelEval( return false_asserts; } -bool NonlinearExtension::checkModel(const std::vector& assertions, - std::vector& gs) +bool NonlinearExtension::checkModel(const std::vector& assertions) { Trace("nl-ext-cm") << "--- check-model ---" << std::endl; @@ -366,7 +365,7 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, Trace("nl-ext-cm") << "-----" << std::endl; unsigned tdegree = d_trSlv.getTaylorDegree(); std::vector lemmas; - bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs); + bool ret = d_model.checkModel(passertions, tdegree, lemmas); for (const auto& al: lemmas) { d_im.addPendingArithLemma(al); @@ -539,18 +538,10 @@ bool NonlinearExtension::modelBasedRefinement() << std::endl; // check the model based on simple solving of equalities and using // error bounds on the Taylor approximation of transcendental functions. - std::vector gs; - if (checkModel(assertions, gs)) + if (checkModel(assertions)) { complete_status = 1; } - for (const Node& mg : gs) - { - Node mgr = Rewriter::rewrite(mg); - mgr = d_containing.getValuation().ensureLiteral(mgr); - d_containing.getOutputChannel().requirePhase(mgr, true); - d_builtModel = true; - } if (d_im.hasUsed()) { d_im.clearWaitingLemmas(); @@ -622,6 +613,11 @@ bool NonlinearExtension::modelBasedRefinement() d_containing.getOutputChannel().setIncomplete(); } } + else + { + // we have built a model + d_builtModel = true; + } d_im.clearWaitingLemmas(); } while (needsRecheck); diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index cd26a027f..2f4586d78 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -185,13 +185,8 @@ class NonlinearExtension * * For details, see Section 3 of Cimatti et al CADE 2017 under the heading * "Detecting Satisfiable Formulas". - * - * The arguments lemmas and gs store the lemmas and guard literals to be sent - * out on the output channel of TheoryArith as lemmas and calls to - * ensureLiteral respectively. */ - bool checkModel(const std::vector& assertions, - std::vector& gs); + bool checkModel(const std::vector& assertions); //---------------------------end check model /** compute relevant assertions */ void computeRelevantAssertions(const std::vector& assertions, diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a6bf46cad..cd99823f1 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -608,6 +608,7 @@ set(regress_0_tests regress0/model-core.smt2 regress0/nl/coeff-sat.smt2 regress0/nl/ext-rew-aggr-test.smt2 + regress0/nl/iand-no-init.smt2 regress0/nl/issue3003.smt2 regress0/nl/issue3407.smt2 regress0/nl/issue3411.smt2 @@ -1643,7 +1644,6 @@ set(regress_1_tests regress1/quantifiers/quant-wf-int-ind.smt2 regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 regress1/quantifiers/recfact.cvc - regress1/quantifiers/rel-trigger-unusable.smt2 regress1/quantifiers/repair-const-nterm.smt2 regress1/quantifiers/rew-to-0211-dd.smt2 regress1/quantifiers/ricart-agrawala6.smt2 @@ -2534,6 +2534,8 @@ set(regression_disabled_tests regress1/quantifiers/macro-subtype-param.smt2 # times out with competition build: regress1/quantifiers/model_6_1_bv.smt2 + # timeout after changes to nonlinear on PR #5351 + regress1/quantifiers/rel-trigger-unusable.smt2 # ajreynol: different error messages on production and debug: regress1/quantifiers/subtype-param-unk.smt2 regress1/quantifiers/subtype-param.smt2 diff --git a/test/regress/regress0/nl/iand-no-init.smt2 b/test/regress/regress0/nl/iand-no-init.smt2 new file mode 100644 index 000000000..f73703693 --- /dev/null +++ b/test/regress/regress0/nl/iand-no-init.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status sat) +(declare-fun y () Int) +(assert (= 0 ((_ iand 5) y 1))) +(check-sat) -- 2.30.2