From 60978d75345cc4e939cf12f57ead93cbb08823ab Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 7 Apr 2017 11:22:44 -0500 Subject: [PATCH] Change option names for nl. --- src/options/arith_options | 18 +- src/smt/smt_engine.cpp | 6 +- src/theory/arith/nonlinear_extension.cpp | 292 +++++++++--------- src/theory/arith/theory_arith.cpp | 2 +- src/theory/arith/theory_arith_private.cpp | 16 +- test/regress/regress0/nl/bug698.smt2 | 2 +- test/regress/regress0/nl/coeff-sat.smt2 | 2 +- .../regress/regress0/nl/coeff-unsat-base.smt2 | 2 +- test/regress/regress0/nl/coeff-unsat.smt2 | 2 +- test/regress/regress0/nl/combine.smt2 | 2 +- test/regress/regress0/nl/disj-eval.smt2 | 2 +- test/regress/regress0/nl/dist-big.smt2 | 2 +- .../regress0/nl/magnitude-wrong-1020-m.smt2 | 2 +- test/regress/regress0/nl/metitarski-1025.smt2 | 2 +- test/regress/regress0/nl/metitarski-3-4.smt2 | 2 +- .../regress0/nl/metitarski_3_4_2e.smt2 | 2 +- test/regress/regress0/nl/mult-po.smt2 | 2 +- test/regress/regress0/nl/nia-wrong-tl.smt2 | 2 +- .../regress0/nl/nl-help-unsat-quant.smt2 | 2 +- test/regress/regress0/nl/nl-unk-quant.smt2 | 2 +- test/regress/regress0/nl/nt-lemmas-bad.smt2 | 2 +- test/regress/regress0/nl/ones.smt2 | 2 +- test/regress/regress0/nl/poly-1025.smt2 | 2 +- test/regress/regress0/nl/quant-nl.smt2 | 2 +- test/regress/regress0/nl/red-exp.smt2 | 2 +- test/regress/regress0/nl/rewriting-sums.smt2 | 2 +- .../regress0/nl/simple-mono-unsat.smt2 | 2 +- test/regress/regress0/nl/simple-mono.smt2 | 2 +- .../regress0/nl/subs0-unsat-confirm.smt2 | 2 +- test/regress/regress0/nl/very-easy-sat.smt2 | 2 +- .../regress0/nl/very-simple-unsat.smt2 | 2 +- test/regress/regress0/nl/zero-subset.smt2 | 2 +- 32 files changed, 194 insertions(+), 194 deletions(-) diff --git a/src/options/arith_options b/src/options/arith_options index c84f4cf36..d90cdfa7b 100644 --- a/src/options/arith_options +++ b/src/options/arith_options @@ -165,28 +165,28 @@ option pbRewriteThreshold --pb-rewrite-threshold int :default 256 option sNormInferEq --snorm-infer-eq bool :default false infer equalities based on Shostak normalization -option nlAlg --nl-alg bool :default false - algebraic approach to non-linear +option nlExt --nl-ext bool :default false + extended approach to non-linear -option nlAlgResBound --nl-alg-rbound bool :default false +option nlExtResBound --nl-ext-rbound bool :default false use resolution-style inference for inferring new bounds -option nlAlgTangentPlanes --nl-alg-tplanes bool :default false +option nlExtTangentPlanes --nl-ext-tplanes bool :default false use non-terminating tangent plane strategy for non-linear -option nlAlgEntailConflicts --nl-alg-ent-conf bool :default false +option nlExtEntailConflicts --nl-ext-ent-conf bool :default false check for entailed conflicts in non-linear solver -option nlAlgRewrites --nl-alg-rewrite bool :default true +option nlExtRewrites --nl-ext-rewrite bool :default true do rewrites in non-linear solver -option nlAlgSolveSubs --nl-alg-solve-subs bool :default false +option nlExtSolveSubs --nl-ext-solve-subs bool :default false do solving for determining constant substitutions -option nlAlgPurify --nl-alg-purify bool :default false +option nlExtPurify --nl-ext-purify bool :default false purify non-linear terms at preprocess -option nlAlgSplitZero --nl-alg-split-zero bool :default false +option nlExtSplitZero --nl-ext-split-zero bool :default false intial splits on zero for all variables endmodule diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5ef77f9d8..8ae432162 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1979,8 +1979,8 @@ void SmtEngine::setDefaults() { options::arraysLazyRIntro1.set(false); } - // Non-linear arithmetic does not support models unless nlAlg is enabled - if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() && !options::nlAlg() ) { + // Non-linear arithmetic does not support models unless nlExt is enabled + if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() && !options::nlExt() ) { if (options::produceModels()) { if(options::produceModels.wasSetByUser()) { throw OptionException("produce-model not supported with nonlinear arith"); @@ -3998,7 +3998,7 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertions : " << d_assertions.size() << endl; - if( options::nlAlgPurify() ){ + if( options::nlExtPurify() ){ hash_map cache; hash_map bcache; std::vector< Node > var_eq; diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index d0b1748c4..5ff70e09f 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -277,7 +277,7 @@ void NonlinearExtension::registerMonomialSubset(Node a, Node b) { Node nlmult_term = safeConstructNary(kind::NONLINEAR_MULT, diff_children); d_m_contain_mult[a][b] = mult_term; d_m_contain_umult[a][b] = nlmult_term; - Trace("nl-alg-mindex") << "..." << a << " is a subset of " << b + Trace("nl-ext-mindex") << "..." << a << " is a subset of " << b << ", difference is " << mult_term << std::endl; } @@ -646,7 +646,7 @@ bool NonlinearExtension::getCurrentSubstitution( } } - if (options::nlAlgSolveSubs()) { + if (options::nlExtSolveSubs()) { NonLinearExtentionSubstitutionSolver substitution_solver(d_ee); if (substitution_solver.solve(vars, &subs, &exp, &rep_to_subs_index)) { retVal = true; @@ -665,12 +665,12 @@ std::pair NonlinearExtension::isExtfReduced( return std::make_pair(n.getKind() != kind::NONLINEAR_MULT, Node::null()); } Assert(n == d_zero); - Trace("nl-alg-zero-exp") << "Infer zero : " << on << " == " << n << std::endl; + Trace("nl-ext-zero-exp") << "Infer zero : " << on << " == " << n << std::endl; // minimize explanation const std::set vars(on.begin(), on.end()); for (unsigned i = 0; i < exp.size(); i++) { - Trace("nl-alg-zero-exp") << " exp[" << i << "] = " << exp[i] << std::endl; + Trace("nl-ext-zero-exp") << " exp[" << i << "] = " << exp[i] << std::endl; std::vector eqs; if (exp[i].getKind() == kind::EQUAL) { eqs.push_back(exp[i]); @@ -685,7 +685,7 @@ std::pair NonlinearExtension::isExtfReduced( for (unsigned j = 0; j < eqs.size(); j++) { for (unsigned r = 0; r < 2; r++) { if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end()) { - Trace("nl-alg-zero-exp") << "...single exp : " << eqs[j] << std::endl; + Trace("nl-ext-zero-exp") << "...single exp : " << eqs[j] << std::endl; return std::make_pair(true, eqs[j]); } } @@ -699,7 +699,7 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) { if (it != d_mv[index].end()) { return it->second; } else { - Trace("nl-alg-debug") << "computeModelValue " << n << std::endl; + Trace("nl-ext-debug") << "computeModelValue " << n << std::endl; Node ret; if (n.isConst()) { ret = n; @@ -728,19 +728,19 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) { ret = Rewriter::rewrite( NodeManager::currentNM()->mkNode(n.getKind(), children)); if (!ret.isConst()) { - Trace("nl-alg-debug") << "...got non-constant : " << ret << " for " + Trace("nl-ext-debug") << "...got non-constant : " << ret << " for " << n << ", ask model directly." << std::endl; ret = d_containing.getValuation().getModel()->getValue(ret); } } } if (ret.getType().isReal() && !isArithKind(n.getKind())) { - // Trace("nl-alg-mv-debug") << ( index==0 ? "M" : "M_A" ) << "[ " << n + // Trace("nl-ext-mv-debug") << ( index==0 ? "M" : "M_A" ) << "[ " << n // << " ] -> " << ret << std::endl; Assert(ret.isConst()); } } - Trace("nl-alg-debug") << "computed " << (index == 0 ? "M" : "M_A") << "[" + Trace("nl-ext-debug") << "computed " << (index == 0 ? "M" : "M_A") << "[" << n << "] = " << ret << std::endl; d_mv[index][n] = ret; return ret; @@ -750,7 +750,7 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) { void NonlinearExtension::registerMonomial(Node n) { if (!IsInVector(d_monomials, n)) { d_monomials.push_back(n); - Trace("nl-alg-debug") << "Register monomial : " << n << std::endl; + Trace("nl-ext-debug") << "Register monomial : " << n << std::endl; if (n.getKind() == kind::NONLINEAR_MULT) { // get exponent count for (unsigned k = 0; k < n.getNumChildren(); k++) { @@ -772,7 +772,7 @@ void NonlinearExtension::registerMonomial(Node n) { } // TODO: sort necessary here? std::sort(d_m_vlist[n].begin(), d_m_vlist[n].end()); - Trace("nl-alg-mindex") << "Add monomial to index : " << n << std::endl; + Trace("nl-ext-mindex") << "Add monomial to index : " << n << std::endl; d_m_index.addTerm(n, d_m_vlist[n], this); } } @@ -782,7 +782,7 @@ void NonlinearExtension::setMonomialFactor(Node a, Node b, // Could not tell if this was being inserted intentionally or not. std::map& mono_diff_a = d_mono_diff[a]; if (!Contains(mono_diff_a, b)) { - Trace("nl-alg-mono-factor") + Trace("nl-ext-mono-factor") << "Set monomial factor for " << a << "/" << b << std::endl; mono_diff_a[b] = mkMonomialRemFactor(a, common); } @@ -791,12 +791,12 @@ void NonlinearExtension::setMonomialFactor(Node a, Node b, void NonlinearExtension::registerConstraint(Node atom) { if (!IsInVector(d_constraints, atom)) { d_constraints.push_back(atom); - Trace("nl-alg-debug") << "Register constraint : " << atom << std::endl; + Trace("nl-ext-debug") << "Register constraint : " << atom << std::endl; std::map msum; if (QuantArith::getMonomialSumLit(atom, msum)) { - Trace("nl-alg-debug") << "got monomial sum: " << std::endl; - if (Trace.isOn("nl-alg-debug")) { - QuantArith::debugPrintMonomialSum(msum, "nl-alg-debug"); + Trace("nl-ext-debug") << "got monomial sum: " << std::endl; + if (Trace.isOn("nl-ext-debug")) { + QuantArith::debugPrintMonomialSum(msum, "nl-ext-debug"); } unsigned max_degree = 0; std::vector all_m; @@ -806,7 +806,7 @@ void NonlinearExtension::registerConstraint(Node atom) { if (!itm->first.isNull()) { all_m.push_back(itm->first); registerMonomial(itm->first); - Trace("nl-alg-debug2") + Trace("nl-ext-debug2") << "...process monomial " << itm->first << std::endl; Assert(d_m_degree.find(itm->first) != d_m_degree.end()); unsigned d = d_m_degree[itm->first]; @@ -829,11 +829,11 @@ void NonlinearExtension::registerConstraint(Node atom) { if (res == -1) { type = reverseRelationKind(type); } - Trace("nl-alg-constraint") << "Constraint : " << atom << " <=> "; + Trace("nl-ext-constraint") << "Constraint : " << atom << " <=> "; if (!coeff.isNull()) { - Trace("nl-alg-constraint") << coeff << " * "; + Trace("nl-ext-constraint") << coeff << " * "; } - Trace("nl-alg-constraint") + Trace("nl-ext-constraint") << m << " " << type << " " << rhs << std::endl; d_c_info[atom][m].d_rhs = rhs; d_c_info[atom][m].d_coeff = coeff; @@ -845,7 +845,7 @@ void NonlinearExtension::registerConstraint(Node atom) { d_c_info_maxm[atom][m] = true; } } else { - Trace("nl-alg-debug") << "...failed to get monomial sum." << std::endl; + Trace("nl-ext-debug") << "...failed to get monomial sum." << std::endl; } } } @@ -964,52 +964,52 @@ Node NonlinearExtension::mkMonomialRemFactor( itme2 != exponent_map.end(); ++itme2) { Node v = itme2->first; unsigned inc = itme2->second; - Trace("nl-alg-mono-factor") + Trace("nl-ext-mono-factor") << "..." << inc << " factors of " << v << std::endl; unsigned count_in_n_exp_rem = getCountWithDefault(n_exp_rem, v, 0); Assert(count_in_n_exp_rem <= inc); inc -= count_in_n_exp_rem; - Trace("nl-alg-mono-factor") + Trace("nl-ext-mono-factor") << "......rem, now " << inc << " factors of " << v << std::endl; children.insert(children.end(), inc, v); } Node ret = safeConstructNary(kind::MULT, children); ret = Rewriter::rewrite(ret); - Trace("nl-alg-mono-factor") << "...return : " << ret << std::endl; + Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl; return ret; } int NonlinearExtension::flushLemma(Node lem) { - Trace("nl-alg-lemma-debug") + Trace("nl-ext-lemma-debug") << "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl; lem = Rewriter::rewrite(lem); if (Contains(d_lemmas, lem)) { - Trace("nl-alg-lemma-debug") + Trace("nl-ext-lemma-debug") << "NonlinearExtension::Lemma duplicate : " << lem << std::endl; // should not generate duplicates // Assert( false ); return 0; } d_lemmas.insert(lem); - Trace("nl-alg-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl; + Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl; d_containing.getOutputChannel().lemma(lem); return 1; } int NonlinearExtension::flushLemmas(std::vector& lemmas) { - if (options::nlAlgEntailConflicts()) { + if (options::nlExtEntailConflicts()) { // check if any are entailed to be false for (unsigned i = 0; i < lemmas.size(); i++) { Node ch_lemma = lemmas[i].negate(); ch_lemma = Rewriter::rewrite(ch_lemma); - Trace("nl-alg-et-debug") + Trace("nl-ext-et-debug") << "Check entailment of " << ch_lemma << "..." << std::endl; std::pair et = d_containing.getValuation().entailmentCheck( THEORY_OF_TYPE_BASED, ch_lemma); - Trace("nl-alg-et-debug") << "entailment test result : " << et.first << " " + Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " " << et.second << std::endl; if (et.first) { - Trace("nl-alg-et") << "*** Lemma entailed to be in conflict : " + Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " << lemmas[i] << std::endl; // return just this lemma if (flushLemma(lemmas[i])) { @@ -1034,13 +1034,13 @@ std::set NonlinearExtension::getFalseInModel( for (size_t i = 0; i < assertions.size(); ++i) { Node lit = assertions[i]; Node litv = computeModelValue(lit); - Trace("nl-alg-mv") << "M[[ " << lit << " ]] -> " << litv; + Trace("nl-ext-mv") << "M[[ " << lit << " ]] -> " << litv; if (litv != d_true) { - Trace("nl-alg-mv") << " [model-false]" << std::endl; + Trace("nl-ext-mv") << " [model-false]" << std::endl; Assert(litv == d_false); false_asserts.insert(lit); } else { - Trace("nl-alg-mv") << std::endl; + Trace("nl-ext-mv") << std::endl; } } return false_asserts; @@ -1049,7 +1049,7 @@ std::set NonlinearExtension::getFalseInModel( std::vector NonlinearExtension::splitOnZeros( const std::vector& ms_vars) { std::vector lemmas; - if (!options::nlAlgSplitZero()) { + if (!options::nlExtSplitZero()) { return lemmas; } for (unsigned i = 0; i < ms_vars.size(); i++) { @@ -1078,7 +1078,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, std::vector ms_vars; // register monomials - Trace("nl-alg-mv") << "Monomials : " << std::endl; + Trace("nl-ext-mv") << "Monomials : " << std::endl; for (unsigned j = 0; j < ms.size(); j++) { Node a = ms[j]; registerMonomial(a); @@ -1086,7 +1086,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, computeModelValue(a, 1); Assert(d_mv[1][a].isConst()); Assert(d_mv[0][a].isConst()); - Trace("nl-alg-mv") << " " << a << " -> " << d_mv[1][a] << " [" + Trace("nl-ext-mv") << " " << a << " -> " << d_mv[1][a] << " [" << d_mv[0][a] << "]" << std::endl; std::map >::iterator itvl = d_m_vlist.find(a); @@ -1104,7 +1104,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, itme->second.end(); ++itme2 ){ Node v = itme->first; Assert( d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if( mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true; - Trace("nl-alg-mv") + Trace("nl-ext-mv") << "...mark " << a << " reduced since has 1 factor." << std::endl; break; } @@ -1124,44 +1124,44 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, std::vector lemmas; // register variables - Trace("nl-alg-mv") << "Variables : " << std::endl; - Trace("nl-alg") << "Get zero split lemmas..." << std::endl; + Trace("nl-ext-mv") << "Variables : " << std::endl; + Trace("nl-ext") << "Get zero split lemmas..." << std::endl; for (unsigned i = 0; i < ms_vars.size(); i++) { Node v = ms_vars[i]; registerMonomial(v); computeModelValue(v, 0); computeModelValue(v, 1); - Trace("nl-alg-mv") << " " << v << " -> " << d_mv[0][v] << std::endl; + Trace("nl-ext-mv") << " " << v << " -> " << d_mv[0][v] << std::endl; } // possibly split on zero? lemmas = splitOnZeros(ms_vars); lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { - Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return; } //-----------------------------------lemmas based on sign (comparison to zero) std::map signs; - Trace("nl-alg") << "Get sign lemmas..." << std::endl; + Trace("nl-ext") << "Get sign lemmas..." << std::endl; for (unsigned j = 0; j < ms.size(); j++) { Node a = ms[j]; if (ms_proc.find(a) == ms_proc.end()) { std::vector exp; - Trace("nl-alg-debug") << " process " << a << "..." << std::endl; + Trace("nl-ext-debug") << " process " << a << "..." << std::endl; signs[a] = compareSign(a, a, 0, 1, exp, lemmas); if (signs[a] == 0) { ms_proc[a] = true; - Trace("nl-alg-mv") << "...mark " << a + Trace("nl-ext-mv") << "...mark " << a << " reduced since its value is 0." << std::endl; } } } lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { - Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return; } @@ -1182,7 +1182,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L // in lemmas std::map > > cmp_infers; - Trace("nl-alg") << "Get comparison lemmas (order=" << r + Trace("nl-ext") << "Get comparison lemmas (order=" << r << ", compare=" << c << ")..." << std::endl; for (unsigned j = 0; j < ms.size(); j++) { Node a = ms[j]; @@ -1239,7 +1239,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, : itmea2->second; a_exp_proc[itmea2->first] = min_exp; b_exp_proc[itmea2->first] = min_exp; - Trace("nl-alg-comp") + Trace("nl-ext-comp") << "Common exponent : " << itmea2->first << " : " << min_exp << std::endl; } @@ -1266,7 +1266,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, } // remove redundant lemmas, e.g. if a > b, b > c, a > c were // inferred, discard lemma with conclusion a > c - Trace("nl-alg-comp") << "Compute redundancies for " << lemmas.size() + Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size() << " lemmas." << std::endl; // naive std::vector r_lemmas; @@ -1286,7 +1286,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, if (cmp_holds(itc3->first, itc2->first, itb->second, exp, visited)) { r_lemmas.push_back(itc2->second); - Trace("nl-alg-comp") + Trace("nl-ext-comp") << "...inference of " << itc->first << " > " << itc2->first << " was redundant." << std::endl; break; @@ -1305,11 +1305,11 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, } // TODO: only take maximal lower/minimial lower bounds? - Trace("nl-alg-comp") << nr_lemmas.size() << " / " << lemmas.size() + Trace("nl-ext-comp") << nr_lemmas.size() << " / " << lemmas.size() << " were non-redundant." << std::endl; lemmas_proc = flushLemmas(nr_lemmas); if (lemmas_proc > 0) { - Trace("nl-alg") << " ...finished with " << lemmas_proc + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas (out of possible " << lemmas.size() << ")." << std::endl; return; @@ -1340,7 +1340,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, std::map > tplane_refine_dir; // register constraints - Trace("nl-alg-debug") << "Register bound constraints..." << std::endl; + Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; for (context::CDList::const_iterator it = d_containing.facts_begin(); it != d_containing.facts_end(); ++it) { @@ -1385,9 +1385,9 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, } // add to status if maximal degree ci_max[x][coeff][rhs] = itcm->second.find(x) != itcm->second.end(); - if (Trace.isOn("nl-alg-bound-debug2")) { + if (Trace.isOn("nl-ext-bound-debug2")) { Node t = QuantArith::mkCoeffTerm(coeff, x); - Trace("nl-alg-bound-debug2") + Trace("nl-ext-bound-debug2") << "Add Bound: " << t << " " << type << " " << rhs << " by " << exp << std::endl; } @@ -1397,7 +1397,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, ci[x][coeff][rhs] = type; ci_exp[x][coeff][rhs] = exp; } else if (type != its->second) { - Trace("nl-alg-bound-debug2") + Trace("nl-ext-bound-debug2") << "Joining kinds : " << type << " " << its->second << std::endl; Kind jk = joinKinds(type, its->second); if (jk == kind::UNDEFINED_KIND) { @@ -1415,20 +1415,20 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, updated = false; } } - if (Trace.isOn("nl-alg-bound")) { + if (Trace.isOn("nl-ext-bound")) { if (updated) { - Trace("nl-alg-bound") << "Bound: "; - debugPrintBound("nl-alg-bound", coeff, x, ci[x][coeff][rhs], rhs); - Trace("nl-alg-bound") << " by " << ci_exp[x][coeff][rhs]; + Trace("nl-ext-bound") << "Bound: "; + debugPrintBound("nl-ext-bound", coeff, x, ci[x][coeff][rhs], rhs); + Trace("nl-ext-bound") << " by " << ci_exp[x][coeff][rhs]; if (ci_max[x][coeff][rhs]) { - Trace("nl-alg-bound") << ", is max degree"; + Trace("nl-ext-bound") << ", is max degree"; } - Trace("nl-alg-bound") << std::endl; + Trace("nl-ext-bound") << std::endl; } } // compute if bound is not satisfied, and store what is required // for a possible refinement - if (options::nlAlgTangentPlanes()) { + if (options::nlExtTangentPlanes()) { if (is_false_lit) { Node rhs_v = computeModelValue(rhs, 0); Node x_v = computeModelValue(x, 0); @@ -1453,20 +1453,20 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, refineDir = true; } } - Trace("nl-alg-tplanes-cons-debug") + Trace("nl-ext-tplanes-cons-debug") << "...compute if bound corresponds to a required " "refinement" << std::endl; - Trace("nl-alg-tplanes-cons-debug") + Trace("nl-ext-tplanes-cons-debug") << "...M[" << x << "] = " << x_v << ", M[" << rhs << "] = " << rhs_v << std::endl; - Trace("nl-alg-tplanes-cons-debug") << "...refine = " << needsRefine + Trace("nl-ext-tplanes-cons-debug") << "...refine = " << needsRefine << "/" << refineDir << std::endl; if (needsRefine) { - Trace("nl-alg-tplanes-cons") + Trace("nl-ext-tplanes-cons") << "---> By " << lit << " and since M[" << x << "] = " << x_v << ", M[" << rhs << "] = " << rhs_v << ", "; - Trace("nl-alg-tplanes-cons") + Trace("nl-ext-tplanes-cons") << "monomial " << x << " should be " << (refineDir ? "larger" : "smaller") << std::endl; tplane_refine_dir[x][refineDir] = true; @@ -1487,17 +1487,17 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, //-----------------------------------------------------------------------------------------inferred // bounds lemmas, e.g. x >= t => y*x >= y*t - Trace("nl-alg") << "Get inferred bound lemmas..." << std::endl; + Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl; std::vector nt_lemmas; for (unsigned k = 0; k < terms.size(); k++) { Node x = terms[k]; - Trace("nl-alg-bound-debug") + Trace("nl-ext-bound-debug") << "Process bounds for " << x << " : " << std::endl; std::map >::iterator itm = d_m_contain_parent.find(x); if (itm != d_m_contain_parent.end()) { - Trace("nl-alg-bound-debug") << "...has " << itm->second.size() + Trace("nl-ext-bound-debug") << "...has " << itm->second.size() << " parent monomials." << std::endl; // check derived bounds std::map > >::iterator itc = @@ -1522,14 +1522,14 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, // x t => m*x t where y = m*x // get the sign of mult Node mmv = computeModelValue(mult); - Trace("nl-alg-bound-debug2") + Trace("nl-ext-bound-debug2") << "Model value of " << mult << " is " << mmv << std::endl; Assert(mmv.isConst()); int mmv_sign = mmv.getConst().sgn(); - Trace("nl-alg-bound-debug2") + Trace("nl-ext-bound-debug2") << " sign of " << mmv << " is " << mmv_sign << std::endl; if (mmv_sign != 0) { - Trace("nl-alg-bound-debug") + Trace("nl-ext-bound-debug") << " from " << x << " * " << mult << " = " << y << " and " << t << " " << type << " " << rhs << ", infer : " << std::endl; @@ -1541,13 +1541,13 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs); Node infer = NodeManager::currentNM()->mkNode( infer_type, infer_lhs, infer_rhs); - Trace("nl-alg-bound-debug") << " " << infer << std::endl; + Trace("nl-ext-bound-debug") << " " << infer << std::endl; infer = Rewriter::rewrite(infer); - Trace("nl-alg-bound-debug2") + Trace("nl-ext-bound-debug2") << " ...rewritten : " << infer << std::endl; // check whether it is false in model for abstraction Node infer_mv = computeModelValue(infer, 1); - Trace("nl-alg-bound-debug") + Trace("nl-ext-bound-debug") << " ...infer model value is " << infer_mv << std::endl; if (infer_mv == d_false) { @@ -1561,10 +1561,10 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, Node pr_iblem = iblem; iblem = Rewriter::rewrite(iblem); bool introNewTerms = hasNewMonomials(iblem, ms); - Trace("nl-alg-bound-lemma") + Trace("nl-ext-bound-lemma") << "*** Bound inference lemma : " << iblem << " (pre-rewrite : " << pr_iblem << ")" << std::endl; - // Trace("nl-alg-bound-lemma") << " intro new + // Trace("nl-ext-bound-lemma") << " intro new // monomials = " << introNewTerms << std::endl; if (!introNewTerms) { lemmas.push_back(iblem); @@ -1573,7 +1573,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, } } } else { - Trace("nl-alg-bound-debug") << " ...coefficient " << mult + Trace("nl-ext-bound-debug") << " ...coefficient " << mult << " is zero." << std::endl; } } @@ -1582,15 +1582,15 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, } } } else { - Trace("nl-alg-bound-debug") << "...has no parent monomials." << std::endl; + Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl; } } - // Trace("nl-alg") << "Bound lemmas : " << lemmas.size() << ", " << + // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << // nt_lemmas.size() << std::endl; prioritize lemmas that do not // introduce new monomials lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { - Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return; } @@ -1598,8 +1598,8 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, //------------------------------------resolution bound inferences, e.g. //( // y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t - if (options::nlAlgResBound()) { - Trace("nl-alg") << "Get resolution inferred bound lemmas..." << std::endl; + if (options::nlExtResBound()) { + Trace("nl-ext") << "Get resolution inferred bound lemmas..." << std::endl; for (unsigned j = 0; j < terms.size(); j++) { Node a = terms[j]; std::map > >::iterator itca = @@ -1610,7 +1610,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, std::map > >::iterator itcb = ci.find(b); if (itcb != ci.end()) { - Trace("nl-alg-rbound-debug") << "resolution inferences : compare " + Trace("nl-ext-rbound-debug") << "resolution inferences : compare " << a << " and " << b << std::endl; // if they have common factors std::map::iterator ita = d_mono_diff[a].find(b); @@ -1625,12 +1625,12 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, Assert(mv_b.isConst()); int mv_b_sgn = mv_b.getConst().sgn(); Assert(mv_b_sgn != 0); - Trace("nl-alg-rbound") << "Get resolution inferences for [a] " + Trace("nl-ext-rbound") << "Get resolution inferences for [a] " << a << " vs [b] " << b << std::endl; - Trace("nl-alg-rbound") + Trace("nl-ext-rbound") << " [a] factor is " << ita->second << ", sign in model = " << mv_a_sgn << std::endl; - Trace("nl-alg-rbound") + Trace("nl-ext-rbound") << " [b] factor is " << itb->second << ", sign in model = " << mv_b_sgn << std::endl; @@ -1669,15 +1669,15 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, if (!hasNewMonomials(rhs_b_res, ms)) { Kind type_b = itcbr->second; exp.push_back(ci_exp[b][coeff_b][rhs_b]); - if (Trace.isOn("nl-alg-rbound")) { - Trace("nl-alg-rbound") << "* try bounds : "; - debugPrintBound("nl-alg-rbound", coeff_a, a, type_a, + if (Trace.isOn("nl-ext-rbound")) { + Trace("nl-ext-rbound") << "* try bounds : "; + debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, rhs_a); - Trace("nl-alg-rbound") << std::endl; - Trace("nl-alg-rbound") << " "; - debugPrintBound("nl-alg-rbound", coeff_b, b, type_b, + Trace("nl-ext-rbound") << std::endl; + Trace("nl-ext-rbound") << " "; + debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, rhs_b); - Trace("nl-alg-rbound") << std::endl; + Trace("nl-ext-rbound") << std::endl; } Kind types[2]; for (unsigned r = 0; r < 2; r++) { @@ -1698,7 +1698,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, } } Kind jk = transKinds(types[0], types[1]); - Trace("nl-alg-rbound-debug") + Trace("nl-ext-rbound-debug") << "trans kind : " << types[0] << " + " << types[1] << " = " << jk << std::endl; if (jk != kind::UNDEFINED_KIND) { @@ -1711,13 +1711,13 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, NodeManager::currentNM()->mkNode(kind::AND, exp), conc); - Trace("nl-alg-rbound-lemma-debug") + Trace("nl-ext-rbound-lemma-debug") << "Resolution bound lemma " "(pre-rewrite) " ": " << rblem << std::endl; rblem = Rewriter::rewrite(rblem); - Trace("nl-alg-rbound-lemma") + Trace("nl-ext-rbound-lemma") << "Resolution bound lemma : " << rblem << std::endl; lemmas.push_back(rblem); @@ -1740,7 +1740,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, } lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { - Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return; } @@ -1749,19 +1749,19 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, // from inferred bound inferences lemmas_proc = flushLemmas(nt_lemmas); if (lemmas_proc > 0) { - Trace("nl-alg") << " ...finished with " << lemmas_proc + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new (monomial-introducing) lemmas." << std::endl; return; } - if (options::nlAlgTangentPlanes()) { - Trace("nl-alg") << "Get tangent plane lemmas..." << std::endl; + if (options::nlExtTangentPlanes()) { + Trace("nl-ext") << "Get tangent plane lemmas..." << std::endl; unsigned kstart = ms_vars.size(); for (unsigned k = kstart; k < terms.size(); k++) { Node t = terms[k]; // if this term requires a refinement if (tplane_refine_dir.find(t) != tplane_refine_dir.end()) { - Trace("nl-alg-tplanes") + Trace("nl-ext-tplanes") << "Look at monomial requiring refinement : " << t << std::endl; // get a decomposition std::map >::iterator it = @@ -1777,7 +1777,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, Node b = tc < tc_diff ? tc_diff : tc; if (dproc[a].find(b) == dproc[a].end()) { dproc[a][b] = true; - Trace("nl-alg-tplanes") + Trace("nl-ext-tplanes") << " decomposable into : " << a << " * " << b << std::endl; Node a_v = computeModelValue(a, 1); Node b_v = computeModelValue(b, 1); @@ -1798,7 +1798,7 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, d <= 1 ? kind::LEQ : kind::GEQ, t, tplane); Node tlem = NodeManager::currentNM()->mkNode( kind::OR, aa.negate(), ab.negate(), conc); - Trace("nl-alg-tplanes") + Trace("nl-ext-tplanes") << "Tangent plane lemma : " << tlem << std::endl; lemmas.push_back(tlem); } @@ -1808,41 +1808,41 @@ void NonlinearExtension::checkLastCall(const std::vector& assertions, } } } - Trace("nl-alg") << "...trying " << lemmas.size() + Trace("nl-ext") << "...trying " << lemmas.size() << " tangent plane lemmas..." << std::endl; lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { - Trace("nl-alg") << " ...finished with " << lemmas_proc << " new lemmas." + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return; } } - Trace("nl-alg") << "...set incomplete" << std::endl; + Trace("nl-ext") << "...set incomplete" << std::endl; d_containing.getOutputChannel().setIncomplete(); } void NonlinearExtension::check(Theory::Effort e) { - Trace("nl-alg") << std::endl; - Trace("nl-alg") << "NonlinearExtension::check, effort = " << e << std::endl; + Trace("nl-ext") << std::endl; + Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl; if (e == Theory::EFFORT_FULL) { d_containing.getExtTheory()->clearCache(); d_needsLastCall = true; - if (options::nlAlgRewrites()) { + if (options::nlExtRewrites()) { std::vector nred; if (!d_containing.getExtTheory()->doInferences(0, nred)) { - Trace("nl-alg") << "...sent no lemmas, # extf to reduce = " + Trace("nl-ext") << "...sent no lemmas, # extf to reduce = " << nred.size() << std::endl; if (nred.empty()) { d_needsLastCall = false; } } else { - Trace("nl-alg") << "...sent lemmas." << std::endl; + Trace("nl-ext") << "...sent lemmas." << std::endl; } } } else { Assert(e == Theory::EFFORT_LAST_CALL); - Trace("nl-alg-mv") << "Getting model values... check for [model-false]" + Trace("nl-ext-mv") << "Getting model values... check for [model-false]" << std::endl; d_mv[0].clear(); d_mv[1].clear(); @@ -1866,7 +1866,7 @@ void NonlinearExtension::check(Theory::Effort e) { Node stv1 = computeModelValue( shared_term, 1 ); if( stv0!=stv1 ){ - Trace("nl-alg-mv") << "Bad shared term value : " << shared_term << " : " << stv1 << ", actual is " << stv0 << std::endl; + Trace("nl-ext-mv") << "Bad shared term value : " << shared_term << " : " << stv1 << ", actual is " << stv0 << std::endl; //split on the value, FIXME : this is non-terminating in general, improve this Node lem = shared_term.eqNode(stv0); lem = Rewriter::rewrite(lem); @@ -1878,7 +1878,7 @@ void NonlinearExtension::check(Theory::Effort e) { } if( !lemmas.empty() ){ int lemmas_proc = flushLemmas(lemmas); - Trace("nl-alg-mv") << "...added " << lemmas_proc << " shared term split lemmas." << std::endl; + Trace("nl-ext-mv") << "...added " << lemmas_proc << " shared term split lemmas." << std::endl; Assert( lemmas_proc>0 ); } } @@ -1902,7 +1902,7 @@ void NonlinearExtension::assignOrderIds(std::vector& vars, for (unsigned j = 0; j < vars.size(); j++) { Node x = vars[j]; Node v = get_compare_value(x, orderType); - Trace("nl-alg-mvo") << " order " << x << " : " << v << std::endl; + Trace("nl-ext-mvo") << " order " << x << " : " << v << std::endl; if (v != prev) { // builtin points bool success; @@ -1912,7 +1912,7 @@ void NonlinearExtension::assignOrderIds(std::vector& vars, Node vv = get_compare_value(d_order_points[order_index], orderType); if (compare_value(v, vv, orderType) <= 0) { counter++; - Trace("nl-alg-mvo") + Trace("nl-ext-mvo") << "O_" << orderType << "[" << d_order_points[order_index] << "] = " << counter << std::endl; order[d_order_points[order_index]] = counter; @@ -1926,14 +1926,14 @@ void NonlinearExtension::assignOrderIds(std::vector& vars, if (prev.isNull() || compare_value(v, prev, orderType) != 0) { counter++; } - Trace("nl-alg-mvo") << "O_" << orderType << "[" << x << "] = " << counter + Trace("nl-ext-mvo") << "O_" << orderType << "[" << x << "] = " << counter << std::endl; order[x] = counter; prev = v; } while (order_index < d_order_points.size()) { counter++; - Trace("nl-alg-mvo") << "O_" << orderType << "[" + Trace("nl-ext-mvo") << "O_" << orderType << "[" << d_order_points[order_index] << "] = " << counter << std::endl; order[d_order_points[order_index]] = counter; @@ -1959,7 +1959,7 @@ int NonlinearExtension::compare(Node i, Node j, unsigned orderType) const { int NonlinearExtension::compare_value(Node i, Node j, unsigned orderType) const { Assert(orderType >= 0 && orderType <= 3); - Trace("nl-alg-debug") << "compare_value " << i << " " << j + Trace("nl-ext-debug") << "compare_value " << i << " " << j << ", o = " << orderType << std::endl; int ret; if (i == j) { @@ -1967,9 +1967,9 @@ int NonlinearExtension::compare_value(Node i, Node j, } else if (orderType == 0 || orderType == 2) { ret = i.getConst() < j.getConst() ? 1 : -1; } else { - Trace("nl-alg-debug") << "vals : " << i.getConst() << " " + Trace("nl-ext-debug") << "vals : " << i.getConst() << " " << j.getConst() << std::endl; - Trace("nl-alg-debug") << i.getConst().abs() << " " + Trace("nl-ext-debug") << i.getConst().abs() << " " << j.getConst().abs() << std::endl; ret = (i.getConst().abs() == j.getConst().abs() ? 0 @@ -1977,12 +1977,12 @@ int NonlinearExtension::compare_value(Node i, Node j, ? 1 : -1)); } - Trace("nl-alg-debug") << "...return " << ret << std::endl; + Trace("nl-ext-debug") << "...return " << ret << std::endl; return ret; } Node NonlinearExtension::get_compare_value(Node i, unsigned orderType) const { - Trace("nl-alg-debug") << "Compare variable " << i << " " << orderType + Trace("nl-ext-debug") << "Compare variable " << i << " " << orderType << std::endl; Assert(orderType >= 0 && orderType <= 3); unsigned mindex = orderType <= 1 ? 0 : 1; @@ -1996,7 +1996,7 @@ Node NonlinearExtension::get_compare_value(Node i, unsigned orderType) const { int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index, int status, std::vector& exp, std::vector& lem) { - Trace("nl-alg-debug") << "Process " << a << " at index " << a_index + Trace("nl-ext-debug") << "Process " << a << " at index " << a_index << ", status is " << status << std::endl; Assert(d_mv[1].find(oa) != d_mv[1].end()); if (a_index == d_m_vlist[a].size()) { @@ -2013,7 +2013,7 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index, // take current sign in model Assert(d_mv[0].find(av) != d_mv[0].end()); int sgn = d_mv[0][av].getConst().sgn(); - Trace("nl-alg-debug") << "Process var " << av << "^" << aexp + Trace("nl-ext-debug") << "Process var " << av << "^" << aexp << ", model sign = " << sgn << std::endl; if (sgn == 0) { if (d_mv[1][oa].getConst().sgn() != 0) { @@ -2038,7 +2038,7 @@ bool NonlinearExtension::compareMonomial( Node oa, Node a, NodeMultiset& a_exp_proc, Node ob, Node b, NodeMultiset& b_exp_proc, std::vector& exp, std::vector& lem, std::map > >& cmp_infers) { - Trace("nl-alg-comp-debug") + Trace("nl-ext-comp-debug") << "Check |" << a << "| >= |" << b << "|" << std::endl; unsigned pexp_size = exp.size(); if (compareMonomial(oa, a, 0, a_exp_proc, ob, b, 0, b_exp_proc, 0, exp, lem, @@ -2046,7 +2046,7 @@ bool NonlinearExtension::compareMonomial( return true; } else { exp.resize(pexp_size); - Trace("nl-alg-comp-debug") + Trace("nl-ext-comp-debug") << "Check |" << b << "| >= |" << a << "|" << std::endl; if (compareMonomial(ob, b, 0, b_exp_proc, oa, a, 0, a_exp_proc, 0, exp, lem, cmp_infers)) { @@ -2086,18 +2086,18 @@ bool NonlinearExtension::compareMonomial( Node b, unsigned b_index, NodeMultiset& b_exp_proc, int status, std::vector& exp, std::vector& lem, std::map > >& cmp_infers) { - Trace("nl-alg-comp-debug") + Trace("nl-ext-comp-debug") << "compareMonomial " << oa << " and " << ob << ", indices = " << a_index << " " << b_index << std::endl; Assert(status == 0 || status == 2); if (a_index == d_m_vlist[a].size() && b_index == d_m_vlist[b].size()) { // finished, compare abstract values int modelStatus = compare(oa, ob, 3) * -2; - Trace("nl-alg-comp") << "...finished comparison with " << oa << " <" + Trace("nl-ext-comp") << "...finished comparison with " << oa << " <" << status << "> " << ob << ", model status = " << modelStatus << std::endl; if (status != modelStatus) { - Trace("nl-alg-comp-infer") + Trace("nl-ext-comp-infer") << "infer : " << oa << " <" << status << "> " << ob << std::endl; if (status == 2) { // must state that all variables are non-zero @@ -2108,7 +2108,7 @@ bool NonlinearExtension::compareMonomial( Node clem = NodeManager::currentNM()->mkNode( kind::IMPLIES, safeConstructNary(kind::AND, exp), mkLit(oa, ob, status, 1)); - Trace("nl-alg-comp-lemma") << "comparison lemma : " << clem << std::endl; + Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl; lem.push_back(clem); cmp_infers[status][oa][ob] = clem; } @@ -2146,33 +2146,33 @@ bool NonlinearExtension::compareMonomial( // get "one" information Assert(d_order_vars[1].find(d_one) != d_order_vars[1].end()); unsigned ovo = d_order_vars[1][d_one]; - Trace("nl-alg-comp-debug") << "....vars : " << av << "^" << aexp << " " + Trace("nl-ext-comp-debug") << "....vars : " << av << "^" << aexp << " " << bv << "^" << bexp << std::endl; //--- cases if (av.isNull()) { if (bvo <= ovo) { - Trace("nl-alg-comp-debug") << "...take leading " << bv << std::endl; + Trace("nl-ext-comp-debug") << "...take leading " << bv << std::endl; // can multiply b by <=1 exp.push_back(mkLit(d_one, bv, bvo == ovo ? 0 : 2, 1)); return compareMonomial(oa, a, a_index, a_exp_proc, ob, b, b_index + 1, b_exp_proc, bvo == ovo ? status : 2, exp, lem, cmp_infers); } else { - Trace("nl-alg-comp-debug") + Trace("nl-ext-comp-debug") << "...failure, unmatched |b|>1 component." << std::endl; return false; } } else if (bv.isNull()) { if (avo >= ovo) { - Trace("nl-alg-comp-debug") << "...take leading " << av << std::endl; + Trace("nl-ext-comp-debug") << "...take leading " << av << std::endl; // can multiply a by >=1 exp.push_back(mkLit(av, d_one, avo == ovo ? 0 : 2, 1)); return compareMonomial(oa, a, a_index + 1, a_exp_proc, ob, b, b_index, b_exp_proc, avo == ovo ? status : 2, exp, lem, cmp_infers); } else { - Trace("nl-alg-comp-debug") + Trace("nl-ext-comp-debug") << "...failure, unmatched |a|<1 component." << std::endl; return false; } @@ -2180,7 +2180,7 @@ bool NonlinearExtension::compareMonomial( Assert(!av.isNull() && !bv.isNull()); if (avo >= bvo) { if (bvo < ovo && avo >= ovo) { - Trace("nl-alg-comp-debug") << "...take leading " << av << std::endl; + Trace("nl-ext-comp-debug") << "...take leading " << av << std::endl; // do avo>=1 instead exp.push_back(mkLit(av, d_one, avo == ovo ? 0 : 2, 1)); return compareMonomial(oa, a, a_index + 1, a_exp_proc, ob, b, b_index, @@ -2190,7 +2190,7 @@ bool NonlinearExtension::compareMonomial( unsigned min_exp = aexp > bexp ? bexp : aexp; a_exp_proc[av] += min_exp; b_exp_proc[bv] += min_exp; - Trace("nl-alg-comp-debug") + Trace("nl-ext-comp-debug") << "...take leading " << min_exp << " from " << av << " and " << bv << std::endl; exp.push_back(mkLit(av, bv, avo == bvo ? 0 : 2, 1)); @@ -2203,14 +2203,14 @@ bool NonlinearExtension::compareMonomial( } } else { if (bvo <= ovo) { - Trace("nl-alg-comp-debug") << "...take leading " << bv << std::endl; + Trace("nl-ext-comp-debug") << "...take leading " << bv << std::endl; // try multiply b <= 1 exp.push_back(mkLit(d_one, bv, bvo == ovo ? 0 : 2, 1)); return compareMonomial(oa, a, a_index, a_exp_proc, ob, b, b_index + 1, b_exp_proc, bvo == ovo ? status : 2, exp, lem, cmp_infers); } else { - Trace("nl-alg-comp-debug") + Trace("nl-ext-comp-debug") << "...failure, leading |b|>|a|>1 component." << std::endl; return false; } @@ -2253,14 +2253,14 @@ void NonlinearExtension::MonomialIndex::addTerm(Node n, if (m != n) { // we are superset if we are equal and haven't traversed all variables int cstatus = status == 0 ? (argIndex == reps.size() ? 0 : -1) : status; - Trace("nl-alg-mindex-debug") << " compare " << n << " and " << m + Trace("nl-ext-mindex-debug") << " compare " << n << " and " << m << ", status = " << cstatus << std::endl; if (cstatus <= 0 && nla->isMonomialSubset(m, n)) { nla->registerMonomialSubset(m, n); - Trace("nl-alg-mindex-debug") << "...success" << std::endl; + Trace("nl-ext-mindex-debug") << "...success" << std::endl; } else if (cstatus >= 0 && nla->isMonomialSubset(n, m)) { nla->registerMonomialSubset(n, m); - Trace("nl-alg-mindex-debug") << "...success (rev)" << std::endl; + Trace("nl-ext-mindex-debug") << "...success (rev)" << std::endl; } } } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 45dcd5d51..f390503a3 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -37,7 +37,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, , d_ppRewriteTimer("theory::arith::ppRewriteTimer") { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); - if (options::nlAlg()) { + if (options::nlExt()) { setupExtTheory(); getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT); } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index acb44bd43..34529007d 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -162,7 +162,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context { srand(79); - if( options::nlAlg() ){ + if( options::nlExt() ){ d_nonlinearExtension = new NonlinearExtension( containing, d_congruenceManager.getEqualityEngine()); } @@ -1574,7 +1574,7 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic."); } - if( !options::nlAlg() ){ + if( !options::nlExt() ){ setIncomplete(); d_nlIncomplete = true; } @@ -1820,7 +1820,7 @@ void TheoryArithPrivate::setupAtom(TNode atom) { void TheoryArithPrivate::preRegisterTerm(TNode n) { Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl; - if( options::nlAlg() ){ + if( options::nlExt() ){ d_containing.getExtTheory()->registerTermRec( n ); } @@ -3647,7 +3647,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ } if(effortLevel == Theory::EFFORT_LAST_CALL){ - if( options::nlAlg() ){ + if( options::nlExt() ){ d_nonlinearExtension->check( effortLevel ); } return; @@ -3967,7 +3967,7 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel() if(!emmittedConflictOrSplit && effortLevel>=Theory::EFFORT_FULL){ - if( options::nlAlg() ){ + if( options::nlExt() ){ d_nonlinearExtension->check( effortLevel ); } } @@ -4148,7 +4148,7 @@ void TheoryArithPrivate::debugPrintModel(std::ostream& out) const{ } bool TheoryArithPrivate::needsCheckLastEffort() { - if( options::nlAlg() ){ + if( options::nlExt() ){ return d_nonlinearExtension->needsCheckLastEffort(); }else{ return false; @@ -4185,7 +4185,7 @@ 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::nlAlg() ){ + if( options::nlExt() ){ return d_nonlinearExtension->getCurrentSubstitution( effort, vars, subs, exp ); }else{ return false; @@ -4194,7 +4194,7 @@ bool TheoryArithPrivate::getCurrentSubstitution( int effort, std::vector< Node > bool TheoryArithPrivate::isExtfReduced(int effort, Node n, Node on, std::vector& exp) { - if (options::nlAlg()) { + if (options::nlExt()) { std::pair reduced = d_nonlinearExtension->isExtfReduced(effort, n, on, exp); if (!reduced.second.isNull()) { diff --git a/test/regress/regress0/nl/bug698.smt2 b/test/regress/regress0/nl/bug698.smt2 index ba7610145..ffb1eead2 100644 --- a/test/regress/regress0/nl/bug698.smt2 +++ b/test/regress/regress0/nl/bug698.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --incremental --nl-alg --fmf-fun-rlv --no-check-models +; COMMAND-LINE: --incremental --nl-ext --fmf-fun-rlv --no-check-models (set-logic UFNIA) (set-info :smt-lib-version 2.5) diff --git a/test/regress/regress0/nl/coeff-sat.smt2 b/test/regress/regress0/nl/coeff-sat.smt2 index 08d189af1..84502bb63 100644 --- a/test/regress/regress0/nl/coeff-sat.smt2 +++ b/test/regress/regress0/nl/coeff-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/nl/coeff-unsat-base.smt2 b/test/regress/regress0/nl/coeff-unsat-base.smt2 index e91cae09e..d56421bf9 100644 --- a/test/regress/regress0/nl/coeff-unsat-base.smt2 +++ b/test/regress/regress0/nl/coeff-unsat-base.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/coeff-unsat.smt2 b/test/regress/regress0/nl/coeff-unsat.smt2 index 91e4506da..f86d08fe7 100644 --- a/test/regress/regress0/nl/coeff-unsat.smt2 +++ b/test/regress/regress0/nl/coeff-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/combine.smt2 b/test/regress/regress0/nl/combine.smt2 index 9c9d839d4..9f7e7a548 100644 --- a/test/regress/regress0/nl/combine.smt2 +++ b/test/regress/regress0/nl/combine.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/disj-eval.smt2 b/test/regress/regress0/nl/disj-eval.smt2 index 717f7a28f..ac8cfc937 100644 --- a/test/regress/regress0/nl/disj-eval.smt2 +++ b/test/regress/regress0/nl/disj-eval.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NIA) (set-info :status sat) diff --git a/test/regress/regress0/nl/dist-big.smt2 b/test/regress/regress0/nl/dist-big.smt2 index cbd87b085..53c9c3f1d 100644 --- a/test/regress/regress0/nl/dist-big.smt2 +++ b/test/regress/regress0/nl/dist-big.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 index d0c038d73..9411224e5 100644 --- a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 +++ b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/metitarski-1025.smt2 b/test/regress/regress0/nl/metitarski-1025.smt2 index af922a466..5a95364f3 100644 --- a/test/regress/regress0/nl/metitarski-1025.smt2 +++ b/test/regress/regress0/nl/metitarski-1025.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/metitarski-3-4.smt2 b/test/regress/regress0/nl/metitarski-3-4.smt2 index 2cd913379..835d60732 100644 --- a/test/regress/regress0/nl/metitarski-3-4.smt2 +++ b/test/regress/regress0/nl/metitarski-3-4.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/metitarski_3_4_2e.smt2 b/test/regress/regress0/nl/metitarski_3_4_2e.smt2 index d08aef410..3f12ec34b 100644 --- a/test/regress/regress0/nl/metitarski_3_4_2e.smt2 +++ b/test/regress/regress0/nl/metitarski_3_4_2e.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/nl/mult-po.smt2 b/test/regress/regress0/nl/mult-po.smt2 index 3f38a7236..65498338a 100644 --- a/test/regress/regress0/nl/mult-po.smt2 +++ b/test/regress/regress0/nl/mult-po.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :status sat) diff --git a/test/regress/regress0/nl/nia-wrong-tl.smt2 b/test/regress/regress0/nl/nia-wrong-tl.smt2 index 25cae599b..40ac92b43 100644 --- a/test/regress/regress0/nl/nia-wrong-tl.smt2 +++ b/test/regress/regress0/nl/nia-wrong-tl.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NIA) (set-info :status sat) diff --git a/test/regress/regress0/nl/nl-help-unsat-quant.smt2 b/test/regress/regress0/nl/nl-help-unsat-quant.smt2 index 45a504de3..f2f7667c8 100644 --- a/test/regress/regress0/nl/nl-help-unsat-quant.smt2 +++ b/test/regress/regress0/nl/nl-help-unsat-quant.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic UFNIA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/nl-unk-quant.smt2 b/test/regress/regress0/nl/nl-unk-quant.smt2 index 4ab034c7c..bb5cd43df 100644 --- a/test/regress/regress0/nl/nl-unk-quant.smt2 +++ b/test/regress/regress0/nl/nl-unk-quant.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic UFNIA) (set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011. Translated to SMT2 by Andrew Reynolds and Morgan Deters.|) diff --git a/test/regress/regress0/nl/nt-lemmas-bad.smt2 b/test/regress/regress0/nl/nt-lemmas-bad.smt2 index c137214f6..cea877c23 100644 --- a/test/regress/regress0/nl/nt-lemmas-bad.smt2 +++ b/test/regress/regress0/nl/nt-lemmas-bad.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg --nl-alg-tplanes +; COMMAND-LINE: --nl-ext --nl-ext-tplanes ; EXPECT: unsat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/ones.smt2 b/test/regress/regress0/nl/ones.smt2 index 88e73c56e..be06912d0 100644 --- a/test/regress/regress0/nl/ones.smt2 +++ b/test/regress/regress0/nl/ones.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/poly-1025.smt2 b/test/regress/regress0/nl/poly-1025.smt2 index 0a6e9dcf3..482696532 100644 --- a/test/regress/regress0/nl/poly-1025.smt2 +++ b/test/regress/regress0/nl/poly-1025.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/quant-nl.smt2 b/test/regress/regress0/nl/quant-nl.smt2 index 2544a5f2e..7d251ab7d 100644 --- a/test/regress/regress0/nl/quant-nl.smt2 +++ b/test/regress/regress0/nl/quant-nl.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic UFNIA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/red-exp.smt2 b/test/regress/regress0/nl/red-exp.smt2 index 9a413902d..5dc5258e2 100644 --- a/test/regress/regress0/nl/red-exp.smt2 +++ b/test/regress/regress0/nl/red-exp.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/rewriting-sums.smt2 b/test/regress/regress0/nl/rewriting-sums.smt2 index 9d0f33e9f..ca2edf024 100644 --- a/test/regress/regress0/nl/rewriting-sums.smt2 +++ b/test/regress/regress0/nl/rewriting-sums.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NIA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/simple-mono-unsat.smt2 b/test/regress/regress0/nl/simple-mono-unsat.smt2 index e640c943b..b82b7ad7c 100644 --- a/test/regress/regress0/nl/simple-mono-unsat.smt2 +++ b/test/regress/regress0/nl/simple-mono-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/simple-mono.smt2 b/test/regress/regress0/nl/simple-mono.smt2 index a9761fa5a..3d4adad28 100644 --- a/test/regress/regress0/nl/simple-mono.smt2 +++ b/test/regress/regress0/nl/simple-mono.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/subs0-unsat-confirm.smt2 b/test/regress/regress0/nl/subs0-unsat-confirm.smt2 index 044f7654c..a1df91b17 100644 --- a/test/regress/regress0/nl/subs0-unsat-confirm.smt2 +++ b/test/regress/regress0/nl/subs0-unsat-confirm.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) diff --git a/test/regress/regress0/nl/very-easy-sat.smt2 b/test/regress/regress0/nl/very-easy-sat.smt2 index b9aecac7a..06efa5806 100644 --- a/test/regress/regress0/nl/very-easy-sat.smt2 +++ b/test/regress/regress0/nl/very-easy-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: sat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/very-simple-unsat.smt2 b/test/regress/regress0/nl/very-simple-unsat.smt2 index bcfdaad40..e23d2d542 100644 --- a/test/regress/regress0/nl/very-simple-unsat.smt2 +++ b/test/regress/regress0/nl/very-simple-unsat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :source | diff --git a/test/regress/regress0/nl/zero-subset.smt2 b/test/regress/regress0/nl/zero-subset.smt2 index 6087551c1..a8ce65b02 100644 --- a/test/regress/regress0/nl/zero-subset.smt2 +++ b/test/regress/regress0/nl/zero-subset.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-alg +; COMMAND-LINE: --nl-ext ; EXPECT: unsat (set-logic QF_NRA) (set-info :status unsat) -- 2.30.2