From: Andrew Reynolds Date: Thu, 5 Dec 2019 20:23:16 +0000 (-0600) Subject: Make nonlinear solver intercept model assignments from the linear arithmetic solver... X-Git-Tag: cvc5-1.0.0~3794 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=643e4d5369734923267694c55363ec0456f18263;p=cvc5.git Make nonlinear solver intercept model assignments from the linear arithmetic solver (#3525) --- diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 762e8b141..fe756e5f7 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl_model.h" #include "expr/node_algorithm.h" +#include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" @@ -36,11 +37,18 @@ NlModel::NlModel(context::Context* c) : d_used_approx(false) NlModel::~NlModel() {} -void NlModel::reset(TheoryModel* m) +void NlModel::reset(TheoryModel* m, std::map& arithModel) { d_model = m; d_mv[0].clear(); d_mv[1].clear(); + d_arithVal.clear(); + // process arithModel + std::map::iterator it; + for (const std::pair& m : arithModel) + { + d_arithVal[m.first] = m.second; + } } void NlModel::resetCheck() @@ -127,21 +135,42 @@ Node NlModel::computeModelValue(Node n, bool isConcrete) return ret; } -Node NlModel::getValueInternal(Node n) const -{ - return d_model->getValue(n); -} - bool NlModel::hasTerm(Node n) const { - return d_model->hasTerm(n); + return d_arithVal.find(n) != d_arithVal.end(); } Node NlModel::getRepresentative(Node n) const { + if (n.isConst()) + { + return n; + } + std::map::const_iterator it = d_arithVal.find(n); + if (it != d_arithVal.end()) + { + AlwaysAssert(it->second.isConst()); + return it->second; + } return d_model->getRepresentative(n); } +Node NlModel::getValueInternal(Node n) const +{ + if (n.isConst()) + { + return n; + } + std::map::const_iterator it = d_arithVal.find(n); + if (it != d_arithVal.end()) + { + AlwaysAssert(it->second.isConst()); + return it->second; + } + // It is unconstrained in the model, return 0. + return d_zero; +} + int NlModel::compare(Node i, Node j, bool isConcrete, bool isAbsolute) { Node ci = computeModelValue(i, isConcrete); diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h index ed13327cc..66c5d89c1 100644 --- a/src/theory/arith/nl_model.h +++ b/src/theory/arith/nl_model.h @@ -52,7 +52,7 @@ class NlModel * where m is the model of the theory of arithmetic. This method resets the * cache of computed model values. */ - void reset(TheoryModel* m); + void reset(TheoryModel* m, std::map& arithModel); /** reset check * * This method is called when the non-linear arithmetic solver restarts @@ -265,6 +265,12 @@ class NlModel Node d_true; Node d_false; 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. + */ + std::map d_arithVal; /** cache of model values * * Stores the the concrete/abstract model values. This is a cache of the diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 287acbc36..6e8e7623d 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -185,7 +185,6 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee) : d_lemmas(containing.getUserContext()), d_zero_split(containing.getUserContext()), - d_skolem_atoms(containing.getUserContext()), d_containing(containing), d_ee(ee), d_needsLastCall(false), @@ -735,16 +734,16 @@ std::vector NonlinearExtension::checkModelEval( for (size_t i = 0; i < assertions.size(); ++i) { Node lit = assertions[i]; Node atom = lit.getKind()==NOT ? lit[0] : lit; - if( d_skolem_atoms.find( atom )==d_skolem_atoms.end() ){ - Node litv = d_model.computeConcreteModelValue(lit); - Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv; - if (litv != d_true) { - Trace("nl-ext-mv-assert") << " [model-false]" << std::endl; - //Assert(litv == d_false); - false_asserts.push_back(lit); - } else { - Trace("nl-ext-mv-assert") << std::endl; - } + Node litv = d_model.computeConcreteModelValue(lit); + Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv; + if (litv != d_true) + { + Trace("nl-ext-mv-assert") << " [model-false]" << std::endl; + false_asserts.push_back(lit); + } + else + { + Trace("nl-ext-mv-assert") << std::endl; } } return false_asserts; @@ -1271,32 +1270,17 @@ void NonlinearExtension::check(Theory::Effort e) { } else { - std::map approximations; - std::map arithModel; - TheoryModel* tm = d_containing.getValuation().getModel(); - if (!d_builtModel.get()) + // If we computed lemmas during collectModelInfo, send them now. + if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty()) { - // run a last call effort check - std::vector mlems; - std::vector mlemsPp; - if (modelBasedRefinement(mlems, mlemsPp)) - { - sendLemmas(mlems); - sendLemmas(mlemsPp, true); - return; - } + sendLemmas(d_cmiLemmas); + sendLemmas(d_cmiLemmasPp, true); + return; } - // get the values that should be replaced in the model - d_model.getModelValueRepair(arithModel, approximations); - // those that are exact are written as exact approximations to the model - for (std::pair& r : arithModel) - { - Node eq = r.first.eqNode(r.second); - eq = Rewriter::rewrite(eq); - tm->recordApproximation(r.first, eq); - } - // those that are approximate are recorded as approximations - for (std::pair& a : approximations) + // Otherwise, we will answer SAT. The values that we approximated are + // recorded as approximations here. + TheoryModel* tm = d_containing.getValuation().getModel(); + for (std::pair& a : d_approximations) { tm->recordApproximation(a.first, a.second); } @@ -1306,8 +1290,6 @@ void NonlinearExtension::check(Theory::Effort e) { bool NonlinearExtension::modelBasedRefinement(std::vector& mlems, std::vector& mlemsPp) { - // reset the model object - d_model.reset(d_containing.getValuation().getModel()); // get the assertions std::vector assertions; getAssertions(assertions); @@ -1497,6 +1479,29 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems, return false; } +void NonlinearExtension::interceptModel(std::map& arithModel) +{ + if (!needsCheckLastEffort()) + { + // no non-linear constraints, we are done + return; + } + d_model.reset(d_containing.getValuation().getModel(), arithModel); + // run a last call effort check + d_cmiLemmas.clear(); + d_cmiLemmasPp.clear(); + if (!d_builtModel.get()) + { + modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp); + } + if (d_builtModel.get()) + { + d_approximations.clear(); + // modify the model values + d_model.getModelValueRepair(arithModel, d_approximations); + } +} + void NonlinearExtension::presolve() { Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl; @@ -2453,17 +2458,9 @@ std::vector NonlinearExtension::checkFactoring( Node atom = lit.getKind() == NOT ? lit[0] : lit; Node litv = d_model.computeConcreteModelValue(lit); bool considerLit = false; - if( d_skolem_atoms.find(atom) != d_skolem_atoms.end() ) - { - //always consider skolem literals - considerLit = true; - } - else - { - // Only consider literals that are in false_asserts. - considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit) - != false_asserts.end(); - } + // Only consider literals that are in false_asserts. + considerLit = std::find(false_asserts.begin(), false_asserts.end(), lit) + != false_asserts.end(); if (considerLit) { @@ -2538,7 +2535,6 @@ std::vector NonlinearExtension::checkFactoring( Trace("nl-ext-factor") << "...factored polynomial : " << polyn << std::endl; Node conc_lit = NodeManager::currentNM()->mkNode( atom.getKind(), polyn, d_zero ); conc_lit = Rewriter::rewrite( conc_lit ); - d_skolem_atoms.insert( conc_lit ); if( !polarity ){ conc_lit = conc_lit.negate(); } @@ -2562,7 +2558,6 @@ Node NonlinearExtension::getFactorSkolem( Node n, std::vector< Node >& lemmas ) if( itf==d_factor_skolem.end() ){ Node k = NodeManager::currentNM()->mkSkolem( "kf", n.getType() ); Node k_eq = Rewriter::rewrite( k.eqNode( n ) ); - d_skolem_atoms.insert( k_eq ); lemmas.push_back( k_eq ); d_factor_skolem[n] = k; return k; diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 20357b722..ddca284a4 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -116,8 +116,44 @@ class NonlinearExtension { * * This call may result in (possibly multiple) calls to d_out->lemma(...) * where d_out is the output channel of TheoryArith. + * + * If e is FULL, then we add lemmas based on context-depedent + * simplification (see Reynolds et al FroCoS 2017). + * + * If e is LAST_CALL, we add lemmas based on model-based refinement + * (see additionally Cimatti et al., TACAS 2017). The lemmas added at this + * effort may be computed during a call to interceptModel as described below. */ void check(Theory::Effort e); + /** intercept model + * + * This method is called during TheoryArith::collectModelInfo, which is + * invoked after the linear arithmetic solver passes a full effort check + * with no lemmas. + * + * The argument arithModel is a map of the form { v1 -> c1, ..., vn -> cn } + * which represents the linear arithmetic theory solver's contribution to the + * current candidate model. That is, its collectModelInfo method is requesting + * that equalities v1 = c1, ..., vn = cn be added to the current model, where + * v1, ..., vn are arithmetic variables and c1, ..., cn are constants. Notice + * arithmetic variables may be real-valued terms belonging to other theories, + * or abstractions of applications of multiplication (kind NONLINEAR_MULT). + * + * This method requests that the non-linear solver inspect this model and + * do any number of the following: + * (1) Construct lemmas based on a model-based refinement procedure inspired + * by Cimatti et al., TACAS 2017., + * (2) In the case that the nonlinear solver finds that the current + * constraints are satisfiable, it may "repair" the values in the argument + * arithModel so that it satisfies certain nonlinear constraints. This may + * involve e.g. solving for variables in nonlinear equations. + * + * Notice that in the former case, the lemmas it constructs are not sent out + * immediately. Instead, they are put in temporary vectors d_cmiLemmas + * and d_cmiLemmasPp, which are then sent out (if necessary) when a last call + * effort check is issued to this class. + */ + void interceptModel(std::map& arithModel); /** Does this class need a call to check(...) at last call effort? */ bool needsCheckLastEffort() const { return d_needsLastCall; } /** presolve @@ -390,12 +426,6 @@ class NonlinearExtension { NodeSet d_lemmas; /** cache of terms t for which we have added the lemma ( t = 0 V t != 0 ). */ NodeSet d_zero_split; - - /** - * The set of atoms with Skolems that this solver introduced. We do not - * require that models satisfy literals over Skolem atoms. - */ - NodeSet d_skolem_atoms; /** commonly used terms */ Node d_zero; @@ -443,6 +473,15 @@ class NonlinearExtension { * and for establishing when we are able to answer "SAT". */ NlModel d_model; + /** + * The lemmas we computed during collectModelInfo. We store two vectors of + * lemmas to be sent out on the output channel of TheoryArith. The first + * is not preprocessed, the second is. + */ + std::vector d_cmiLemmas; + std::vector d_cmiLemmasPp; + /** The approximations computed during collectModelInfo. */ + std::map d_approximations; /** have we successfully built the model in this SAT context? */ context::CDO d_builtModel; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index bc4d7db02..58636a10b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3550,7 +3550,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ if(effortLevel == Theory::EFFORT_LAST_CALL){ if( options::nlExt() ){ - d_nonlinearExtension->check( effortLevel ); + d_nonlinearExtension->check(effortLevel); } return; } @@ -4321,6 +4321,8 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) // TODO: // This is not very good for user push/pop.... // Revisit when implementing push/pop + // Map of terms to values, constructed when non-linear arithmetic is active. + std::map arithModel; for(var_iterator vi = var_begin(), vend = var_end(); vi != vend; ++vi){ ArithVar v = *vi; @@ -4335,10 +4337,18 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) Node qNode = mkRationalNode(qmodel); Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl; - - if (!m->assertEquality(term, qNode, true)) + if (options::nlExt()) { - return false; + // Let non-linear extension inspect the values before they are sent + // to the theory model. + arithModel[term] = qNode; + } + else + { + if (!m->assertEquality(term, qNode, true)) + { + return false; + } } }else{ Debug("arith::collectModelInfo") << "Skipping m->assertEquality(" << term << ", true)" << endl; @@ -4346,6 +4356,20 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) } } } + if (options::nlExt()) + { + // Non-linear may repair values to satisfy non-linear constraints (see + // documentation for NonlinearExtension::interceptModel). + d_nonlinearExtension->interceptModel(arithModel); + // We are now ready to assert the model. + for (std::pair& p : arithModel) + { + if (!m->assertEquality(p.first, p.second, true)) + { + return false; + } + } + } // Iterate over equivalence classes in LinearEqualityModule // const eq::EqualityEngine& ee = d_congruenceManager.getEqualityEngine(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 90038872f..0bcaa049a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -537,7 +537,9 @@ set(regress_0_tests regress0/model-core.smt2 regress0/nl/coeff-sat.smt2 regress0/nl/ext-rew-aggr-test.smt2 + regress0/nl/issue3003.smt2 regress0/nl/issue3407.smt2 + regress0/nl/issue3411.smt2 regress0/nl/issue3475.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 @@ -554,6 +556,7 @@ set(regress_0_tests regress0/nl/nta/tan-rewrite.smt2 regress0/nl/real-as-int.smt2 regress0/nl/real-div-ufnra.smt2 + regress0/nl/sin-cos-346-b-chunk-0169.smt2 regress0/nl/sqrt.smt2 regress0/nl/sqrt2-value.smt2 regress0/nl/subs0-unsat-confirm.smt2 @@ -1261,6 +1264,7 @@ set(regress_1_tests regress1/nl/exp1-lb.smt2 regress1/nl/exp_monotone.smt2 regress1/nl/factor_agg_s.smt2 + regress1/nl/issue3441.smt2 regress1/nl/metitarski-1025.smt2 regress1/nl/metitarski-3-4.smt2 regress1/nl/metitarski_3_4_2e.smt2 diff --git a/test/regress/regress0/nl/issue3003.smt2 b/test/regress/regress0/nl/issue3003.smt2 new file mode 100644 index 000000000..52bb25963 --- /dev/null +++ b/test/regress/regress0/nl/issue3003.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun _substvar_15_ () Real) +(declare-fun _substvar_17_ () Real) +(assert (let ((?v_1 (<= 0.0 _substvar_15_))) (and ?v_1 (and ?v_1 (and ?v_1 (= (* _substvar_15_ _substvar_15_) (+ 1 (* _substvar_17_ (* _substvar_17_ (- 1)))))))))) +(check-sat) diff --git a/test/regress/regress0/nl/issue3411.smt2 b/test/regress/regress0/nl/issue3411.smt2 new file mode 100644 index 000000000..daf69834b --- /dev/null +++ b/test/regress/regress0/nl/issue3411.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-logic NRA) +(set-info :status sat) +(declare-fun a () Real) +(declare-fun b () Real) +(assert (= (/ 0 (+ 1 (* a a b))) 0)) +(check-sat) diff --git a/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 new file mode 100644 index 000000000..65e705fa3 --- /dev/null +++ b/test/regress/regress0/nl/sin-cos-346-b-chunk-0169.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --no-check-models +; EXPECT: sat +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :category "industrial") +(set-info :status sat) +(declare-fun skoX () Real) +(declare-fun skoSQ3 () Real) +(declare-fun pi () Real) +(assert (let ((?v_0 (* skoSQ3 skoSQ3))) (and (not (<= (* skoX (* skoX (* skoX (* skoX (+ (/ 1 24) (* skoX (* skoX (+ (/ (- 1) 720) (* skoX (* skoX (/ 1 40320))))))))))) (+ (- 3) ?v_0))) (and (= ?v_0 3) (and (not (<= (+ (/ (- 1) 10000000) (* pi (/ 1 2))) skoX)) (and (not (<= pi (/ 15707963 5000000))) (and (not (<= (/ 31415927 10000000) pi)) (and (not (<= skoX 0)) (not (<= skoSQ3 0)))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/issue3441.smt2 b/test/regress/regress1/nl/issue3441.smt2 new file mode 100644 index 000000000..19fe98bc5 --- /dev/null +++ b/test/regress/regress1/nl/issue3441.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_NIA) +(set-info :status sat) +(declare-fun a () Int) +(declare-fun b () Int) +(declare-fun c () Int) +(declare-fun d () Int) +(assert (and (>= (+ (* b c (- (- 4) d)) (- 1)) 0 (div a b)))) +(check-sat)