From: Andrew Reynolds Date: Thu, 25 Jun 2020 12:15:06 +0000 (-0500) Subject: Update option --nl-ext to enable/disable incremental linearization solver only (... X-Git-Tag: cvc5-1.0.0~3175 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1af865f3429c0dd5910b5a8d1e12d690c3623dfa;p=cvc5.git Update option --nl-ext to enable/disable incremental linearization solver only (#4649) Previously, this option disabled/enabled the entire non-linear solver. This is in preparation for new CAD techniques. I am intentionally not renaming "--nl-ext" to e.g. "--nl-inc-lin" for the sake of not breaking user configurations. It makes some minor changes to clean the interface in a few places and to not enable the non-linear solver in linear logics. --- diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 0bfc26338..ce747b62d 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -435,7 +435,7 @@ header = "options/arith_options.h" type = "bool" default = "true" read_only = true - help = "extended approach to non-linear" + help = "incremental linearization approach to non-linear" [[option]] name = "nlExtResBound" @@ -444,7 +444,7 @@ header = "options/arith_options.h" type = "bool" default = "false" read_only = true - help = "use resolution-style inference for inferring new bounds" + help = "use resolution-style inference for inferring new bounds in non-linear incremental linearization solver" [[option]] name = "nlExtFactor" @@ -453,7 +453,7 @@ header = "options/arith_options.h" type = "bool" default = "true" read_only = true - help = "use factoring inference in non-linear solver" + help = "use factoring inference in non-linear incremental linearization solver" [[option]] name = "nlExtTangentPlanes" @@ -462,7 +462,7 @@ header = "options/arith_options.h" type = "bool" default = "false" read_only = true - help = "use non-terminating tangent plane strategy for non-linear" + help = "use non-terminating tangent plane strategy for non-linear incremental linearization solver" [[option]] name = "nlExtTangentPlanesInterleave" @@ -470,7 +470,7 @@ header = "options/arith_options.h" long = "nl-ext-tplanes-interleave" type = "bool" default = "false" - help = "interleave tangent plane strategy for non-linear" + help = "interleave tangent plane strategy for non-linear incremental linearization solver" [[option]] name = "nlExtTfTangentPlanes" @@ -479,7 +479,7 @@ header = "options/arith_options.h" type = "bool" default = "true" read_only = true - help = "use non-terminating tangent plane strategy for transcendental functions for non-linear" + help = "use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver" [[option]] name = "nlExtEntailConflicts" @@ -497,7 +497,7 @@ header = "options/arith_options.h" type = "bool" default = "true" read_only = true - help = "do rewrites in non-linear solver" + help = "do context-dependent simplification based on rewrites in non-linear solver" [[option]] name = "nlExtPurify" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index afc8eb7bb..d663352f7 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1442,12 +1442,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) disableModels = true; sOptNoModel = "minisat-elimination"; } - else if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() - && !options::nlExt()) - { - disableModels = true; - sOptNoModel = "nonlinear arithmetic without nl-ext"; - } else if (options::globalNegate()) { disableModels = true; diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index bf27ecbb3..d471bf0f6 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -211,13 +211,12 @@ int NlModel::compareValue(Node i, Node j, bool isAbsolute) const } bool NlModel::checkModel(const std::vector& assertions, - const std::vector& false_asserts, unsigned d, std::vector& lemmas, std::vector& gs) { Trace("nl-ext-cm-debug") << " solve for equalities..." << std::endl; - for (const Node& atom : false_asserts) + for (const Node& atom : assertions) { // see if it corresponds to a univariate polynomial equation of degree two if (atom.getKind() == EQUAL) @@ -489,6 +488,7 @@ bool NlModel::solveEqualitySimple(Node eq, { if (seq.getConst()) { + // already true d_check_model_solved[eq] = Node::null(); return true; } diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 86bac88a9..fdce446fc 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -151,7 +151,6 @@ class NlModel * d is a degree indicating how precise our computations are. */ bool checkModel(const std::vector& assertions, - const std::vector& false_asserts, unsigned d, std::vector& lemmas, std::vector& gs); diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 087d7681a..5ded7d3d0 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -380,17 +380,18 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, // get the presubstitution Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; std::vector passertions = assertions; - - // preprocess the assertions with the trancendental solver - if (!d_trSlv.preprocessAssertionsCheckModel(passertions)) + if (options::nlExt()) { - return false; + // preprocess the assertions with the trancendental solver + if (!d_trSlv.preprocessAssertionsCheckModel(passertions)) + { + return false; + } } Trace("nl-ext-cm") << "-----" << std::endl; unsigned tdegree = d_trSlv.getTaylorDegree(); - bool ret = - d_model.checkModel(passertions, false_asserts, tdegree, lemmas, gs); + bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs); return ret; } @@ -400,14 +401,16 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, std::vector& lems, std::vector& wlems) { - // initialize the non-linear solver - d_nlSlv.initLastCall(assertions, false_asserts, xts); - // initialize the trancendental function solver std::vector lemmas; - d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas); - - // process lemmas that may have been generated by the transcendental solver - filterLemmas(lemmas, lems); + if (options::nlExt()) + { + // initialize the non-linear solver + d_nlSlv.initLastCall(assertions, false_asserts, xts); + // initialize the trancendental function solver + d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas); + // process lemmas that may have been generated by the transcendental solver + filterLemmas(lemmas, lems); + } if (!lems.empty()) { Trace("nl-ext") << " ...finished with " << lems.size() @@ -416,7 +419,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } //----------------------------------- possibly split on zero - if (options::nlExtSplitZero()) + if (options::nlExt() && options::nlExtSplitZero()) { Trace("nl-ext") << "Get zero split lemmas..." << std::endl; lemmas = d_nlSlv.checkSplitZero(); @@ -430,90 +433,34 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } //-----------------------------------initial lemmas for transcendental - //functions - lemmas = d_trSlv.checkTranscendentalInitialRefine(); - filterLemmas(lemmas, lems); - if (!lems.empty()) - { - Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." - << std::endl; - return lems.size(); - } - - //-----------------------------------lemmas based on sign (comparison to zero) - lemmas = d_nlSlv.checkMonomialSign(); - filterLemmas(lemmas, lems); - if (!lems.empty()) - { - Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." - << std::endl; - return lems.size(); - } - - //-----------------------------------monotonicity of transdental functions - lemmas = d_trSlv.checkTranscendentalMonotonic(); - filterLemmas(lemmas, lems); - if (!lems.empty()) - { - Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." - << std::endl; - return lems.size(); - } - - //-----------------------------------lemmas based on magnitude of non-zero - //monomials - for (unsigned c = 0; c < 3; c++) + if (options::nlExt()) { - // c is effort level - lemmas = d_nlSlv.checkMonomialMagnitude(c); - unsigned nlem = lemmas.size(); + // functions + lemmas = d_trSlv.checkTranscendentalInitialRefine(); filterLemmas(lemmas, lems); if (!lems.empty()) { - Trace("nl-ext") << " ...finished with " << lems.size() - << " new lemmas (out of possible " << nlem << ")." + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." << std::endl; return lems.size(); } } - //-----------------------------------inferred bounds lemmas - // e.g. x >= t => y*x >= y*t - std::vector nt_lemmas; - lemmas = - d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts); - // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << - // nt_lemmas.size() << std::endl; prioritize lemmas that do not - // introduce new monomials - filterLemmas(lemmas, lems); - - if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave()) + // main calls to nlExt + if (options::nlExt()) { - lemmas = d_nlSlv.checkTangentPlanes(); + //---------------------------------lemmas based on sign (comparison to zero) + lemmas = d_nlSlv.checkMonomialSign(); filterLemmas(lemmas, lems); - } - - if (!lems.empty()) - { - Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." - << std::endl; - return lems.size(); - } - - // from inferred bound inferences : now do ones that introduce new terms - filterLemmas(nt_lemmas, lems); - if (!lems.empty()) - { - Trace("nl-ext") << " ...finished with " << lems.size() - << " new (monomial-introducing) lemmas." << std::endl; - return lems.size(); - } + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + << std::endl; + return lems.size(); + } - //------------------------------------factoring lemmas - // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t - if (options::nlExtFactor()) - { - lemmas = d_nlSlv.checkFactoring(assertions, false_asserts); + //-----------------------------------monotonicity of transdental functions + lemmas = d_trSlv.checkTranscendentalMonotonic(); filterLemmas(lemmas, lems); if (!lems.empty()) { @@ -521,33 +468,98 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, << std::endl; return lems.size(); } - } - //------------------------------------resolution bound inferences - // e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t - if (options::nlExtResBound()) - { - lemmas = d_nlSlv.checkMonomialInferResBounds(); + //------------------------lemmas based on magnitude of non-zero monomials + for (unsigned c = 0; c < 3; c++) + { + // c is effort level + lemmas = d_nlSlv.checkMonomialMagnitude(c); + unsigned nlem = lemmas.size(); + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() + << " new lemmas (out of possible " << nlem << ")." + << std::endl; + return lems.size(); + } + } + + //-----------------------------------inferred bounds lemmas + // e.g. x >= t => y*x >= y*t + std::vector nt_lemmas; + lemmas = + d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts); + // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << + // nt_lemmas.size() << std::endl; prioritize lemmas that do not + // introduce new monomials filterLemmas(lemmas, lems); + + if (options::nlExtTangentPlanes() + && options::nlExtTangentPlanesInterleave()) + { + lemmas = d_nlSlv.checkTangentPlanes(); + filterLemmas(lemmas, lems); + } + if (!lems.empty()) { Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." << std::endl; return lems.size(); } - } - //------------------------------------tangent planes - if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave()) - { - lemmas = d_nlSlv.checkTangentPlanes(); - filterLemmas(lemmas, wlems); - } - if (options::nlExtTfTangentPlanes()) - { - lemmas = d_trSlv.checkTranscendentalTangentPlanes(); - filterLemmas(lemmas, wlems); + // from inferred bound inferences : now do ones that introduce new terms + filterLemmas(nt_lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() + << " new (monomial-introducing) lemmas." << std::endl; + return lems.size(); + } + + //------------------------------------factoring lemmas + // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t + if (options::nlExtFactor()) + { + lemmas = d_nlSlv.checkFactoring(assertions, false_asserts); + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() + << " new lemmas." << std::endl; + return lems.size(); + } + } + + //------------------------------------resolution bound inferences + // e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t + if (options::nlExtResBound()) + { + lemmas = d_nlSlv.checkMonomialInferResBounds(); + filterLemmas(lemmas, lems); + if (!lems.empty()) + { + Trace("nl-ext") << " ...finished with " << lems.size() + << " new lemmas." << std::endl; + return lems.size(); + } + } + + //------------------------------------tangent planes + if (options::nlExtTangentPlanes() + && !options::nlExtTangentPlanesInterleave()) + { + lemmas = d_nlSlv.checkTangentPlanes(); + filterLemmas(lemmas, wlems); + } + if (options::nlExtTfTangentPlanes()) + { + lemmas = d_trSlv.checkTranscendentalTangentPlanes(); + filterLemmas(lemmas, wlems); + } } + Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas." << std::endl; @@ -774,7 +786,8 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) } // we are incomplete - if (options::nlExtIncPrecision() && d_model.usedApproximate()) + if (options::nlExt() && options::nlExtIncPrecision() + && d_model.usedApproximate()) { d_trSlv.incrementTaylorDegree(); needsRecheck = true; diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 7310233f1..cb436bda7 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -300,7 +300,7 @@ class NonlinearExtension /** The nonlinear extension object * * This is the subsolver responsible for running the procedure for - * constraints involving nonlinear mulitplication. + * constraints involving nonlinear mulitplication, Cimatti et al., TACAS 2017. */ NlSolver d_nlSlv; /** diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c25090f38..30b8ed01d 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -40,7 +40,9 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, , d_proofRecorder(nullptr) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); - if (options::nlExt()) { + // if logic is non-linear + if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) + { setupExtTheory(); getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT); getExtTheory()->addFunctionKind(kind::EXPONENTIAL); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 7b7f5a411..d0da29e7a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -158,7 +158,9 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_statistics(), d_opElim(logicInfo) { - if( options::nlExt() ){ + // only need to create if non-linear logic + if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) + { d_nonlinearExtension = new nl::NonlinearExtension( containing, d_congruenceManager.getEqualityEngine()); } @@ -1263,7 +1265,8 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic."); } - if( !options::nlExt() ){ + if (d_nonlinearExtension == nullptr) + { d_nlIncomplete = true; } @@ -1274,7 +1277,8 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ markSetup(vlNode); }else{ - if( !options::nlExt() ){ + if (d_nonlinearExtension == nullptr) + { if( vlNode.getKind()==kind::EXPONENTIAL || vlNode.getKind()==kind::SINE || vlNode.getKind()==kind::COSINE || vlNode.getKind()==kind::TANGENT ){ d_nlIncomplete = true; @@ -1440,8 +1444,9 @@ void TheoryArithPrivate::setupAtom(TNode atom) { void TheoryArithPrivate::preRegisterTerm(TNode n) { Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; - - if( options::nlExt() ){ + + if (d_nonlinearExtension != nullptr) + { d_containing.getExtTheory()->registerTermRec( n ); } @@ -3322,7 +3327,8 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ } if(effortLevel == Theory::EFFORT_LAST_CALL){ - if( options::nlExt() ){ + if (d_nonlinearExtension != nullptr) + { d_nonlinearExtension->check(effortLevel); } return; @@ -3646,7 +3652,8 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel() if(!emmittedConflictOrSplit && effortLevel>=Theory::EFFORT_FULL){ - if( options::nlExt() ){ + if (d_nonlinearExtension != nullptr) + { d_nonlinearExtension->check( effortLevel ); } } @@ -3849,7 +3856,8 @@ void TheoryArithPrivate::debugPrintModel(std::ostream& out) const{ } bool TheoryArithPrivate::needsCheckLastEffort() { - if( options::nlExt() ){ + if (d_nonlinearExtension != nullptr) + { return d_nonlinearExtension->needsCheckLastEffort(); }else{ return false; @@ -3886,7 +3894,8 @@ Node TheoryArithPrivate::explain(TNode n) } bool TheoryArithPrivate::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) { - if( options::nlExt() ){ + if (d_nonlinearExtension != nullptr) + { return d_nonlinearExtension->getCurrentSubstitution( effort, vars, subs, exp ); }else{ return false; @@ -3895,7 +3904,8 @@ bool TheoryArithPrivate::getCurrentSubstitution( int effort, std::vector< Node > bool TheoryArithPrivate::isExtfReduced(int effort, Node n, Node on, std::vector& exp) { - if (options::nlExt()) { + if (d_nonlinearExtension != nullptr) + { std::pair reduced = d_nonlinearExtension->isExtfReduced(effort, n, on, exp); if (!reduced.second.isNull()) { @@ -4143,7 +4153,7 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) Node qNode = mkRationalNode(qmodel); Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl; - if (options::nlExt()) + if (d_nonlinearExtension != nullptr) { // Let non-linear extension inspect the values before they are sent // to the theory model. @@ -4162,7 +4172,7 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m) } } } - if (options::nlExt()) + if (d_nonlinearExtension != nullptr) { // Non-linear may repair values to satisfy non-linear constraints (see // documentation for NonlinearExtension::interceptModel). @@ -4312,7 +4322,7 @@ void TheoryArithPrivate::presolve(){ outputLemma(lem); } - if (options::nlExt()) + if (d_nonlinearExtension != nullptr) { d_nonlinearExtension->presolve(); }