From 4ac66d3aee2a0571c169e4ce2d6049ea311462ce Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 1 Jun 2020 14:31:48 -0500 Subject: [PATCH] Move non-linear files to src/theory/arith/nl (#4548) Also makes CVC4::theory::arith::nl namespace. This includes some formatting changes. --- src/CMakeLists.txt | 28 +++--- src/theory/arith/{ => nl}/nl_constraint.cpp | 4 +- src/theory/arith/{ => nl}/nl_constraint.h | 8 +- src/theory/arith/{ => nl}/nl_lemma_utils.cpp | 6 +- src/theory/arith/{ => nl}/nl_lemma_utils.h | 6 +- src/theory/arith/{ => nl}/nl_model.cpp | 14 +-- src/theory/arith/{ => nl}/nl_model.h | 8 +- src/theory/arith/{ => nl}/nl_monomial.cpp | 6 +- src/theory/arith/{ => nl}/nl_monomial.h | 6 +- src/theory/arith/{ => nl}/nl_solver.cpp | 4 +- src/theory/arith/{ => nl}/nl_solver.h | 10 +- .../arith/{ => nl}/nonlinear_extension.cpp | 92 ++++++++++++------- .../arith/{ => nl}/nonlinear_extension.h | 28 +++--- .../arith/{ => nl}/transcendental_solver.cpp | 4 +- .../arith/{ => nl}/transcendental_solver.h | 10 +- src/theory/arith/theory_arith_private.cpp | 4 +- src/theory/arith/theory_arith_private.h | 4 +- 17 files changed, 150 insertions(+), 92 deletions(-) rename src/theory/arith/{ => nl}/nl_constraint.cpp (97%) rename src/theory/arith/{ => nl}/nl_constraint.h (92%) rename src/theory/arith/{ => nl}/nl_lemma_utils.cpp (92%) rename src/theory/arith/{ => nl}/nl_lemma_utils.h (95%) rename src/theory/arith/{ => nl}/nl_model.cpp (99%) rename src/theory/arith/{ => nl}/nl_model.h (98%) rename src/theory/arith/{ => nl}/nl_monomial.cpp (98%) rename src/theory/arith/{ => nl}/nl_monomial.h (97%) rename src/theory/arith/{ => nl}/nl_solver.cpp (99%) rename src/theory/arith/{ => nl}/nl_solver.h (98%) rename src/theory/arith/{ => nl}/nonlinear_extension.cpp (95%) rename src/theory/arith/{ => nl}/nonlinear_extension.h (95%) rename src/theory/arith/{ => nl}/transcendental_solver.cpp (99%) rename src/theory/arith/{ => nl}/transcendental_solver.h (98%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e9be4dd3e..20e110b2b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -300,18 +300,20 @@ libcvc4_add_sources( theory/arith/linear_equality.h theory/arith/matrix.cpp theory/arith/matrix.h - theory/arith/nl_constraint.cpp - theory/arith/nl_constraint.h - theory/arith/nl_lemma_utils.cpp - theory/arith/nl_lemma_utils.h - theory/arith/nl_model.cpp - theory/arith/nl_model.h - theory/arith/nl_monomial.cpp - theory/arith/nl_monomial.h - theory/arith/nl_solver.cpp - theory/arith/nl_solver.h - theory/arith/nonlinear_extension.cpp - theory/arith/nonlinear_extension.h + theory/arith/nl/nl_constraint.cpp + theory/arith/nl/nl_constraint.h + theory/arith/nl/nl_lemma_utils.cpp + theory/arith/nl/nl_lemma_utils.h + theory/arith/nl/nl_model.cpp + theory/arith/nl/nl_model.h + theory/arith/nl/nl_monomial.cpp + theory/arith/nl/nl_monomial.h + theory/arith/nl/nl_solver.cpp + theory/arith/nl/nl_solver.h + theory/arith/nl/nonlinear_extension.cpp + theory/arith/nl/nonlinear_extension.h + theory/arith/nl/transcendental_solver.cpp + theory/arith/nl/transcendental_solver.h theory/arith/normal_form.cpp theory/arith/normal_form.h theory/arith/partial_model.cpp @@ -332,8 +334,6 @@ libcvc4_add_sources( theory/arith/theory_arith_private.h theory/arith/theory_arith_private_forward.h theory/arith/theory_arith_type_rules.h - theory/arith/transcendental_solver.cpp - theory/arith/transcendental_solver.h theory/arith/type_enumerator.h theory/arrays/array_info.cpp theory/arrays/array_info.h diff --git a/src/theory/arith/nl_constraint.cpp b/src/theory/arith/nl/nl_constraint.cpp similarity index 97% rename from src/theory/arith/nl_constraint.cpp rename to src/theory/arith/nl/nl_constraint.cpp index 8fb4535ea..c4c4dfbe7 100644 --- a/src/theory/arith/nl_constraint.cpp +++ b/src/theory/arith/nl/nl_constraint.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of utilities for non-linear constraints **/ -#include "theory/arith/nl_constraint.h" +#include "theory/arith/nl/nl_constraint.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" @@ -22,6 +22,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { ConstraintDb::ConstraintDb(MonomialDb& mdb) : d_mdb(mdb) {} @@ -118,6 +119,7 @@ bool ConstraintDb::isMaximal(Node atom, Node x) const return itcm->second.find(x) != itcm->second.end(); } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_constraint.h b/src/theory/arith/nl/nl_constraint.h similarity index 92% rename from src/theory/arith/nl_constraint.h rename to src/theory/arith/nl/nl_constraint.h index faa3cc812..e86ac4b66 100644 --- a/src/theory/arith/nl_constraint.h +++ b/src/theory/arith/nl/nl_constraint.h @@ -12,19 +12,20 @@ ** \brief Utilities for non-linear constraints **/ -#ifndef CVC4__THEORY__ARITH__NL_CONSTRAINT_H -#define CVC4__THEORY__ARITH__NL_CONSTRAINT_H +#ifndef CVC4__THEORY__ARITH__NL__NL_CONSTRAINT_H +#define CVC4__THEORY__ARITH__NL__NL_CONSTRAINT_H #include #include #include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/nl_monomial.h" +#include "theory/arith/nl/nl_monomial.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { /** constraint information * @@ -79,6 +80,7 @@ class ConstraintDb std::map > d_c_info; }; +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp similarity index 92% rename from src/theory/arith/nl_lemma_utils.cpp rename to src/theory/arith/nl/nl_lemma_utils.cpp index e43a77b06..ca34d91a9 100644 --- a/src/theory/arith/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -12,13 +12,14 @@ ** \brief Implementation of utilities for the non-linear solver **/ -#include "theory/arith/nl_lemma_utils.h" +#include "theory/arith/nl/nl_lemma_utils.h" -#include "theory/arith/nl_model.h" +#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { bool SortNlModel::operator()(Node i, Node j) { @@ -58,6 +59,7 @@ Node ArgTrie::add(Node d, const std::vector& args) return at->d_data; } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h similarity index 95% rename from src/theory/arith/nl_lemma_utils.h rename to src/theory/arith/nl/nl_lemma_utils.h index bd729dad9..64a4deb17 100644 --- a/src/theory/arith/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -12,8 +12,8 @@ ** \brief Utilities for processing lemmas from the non-linear solver **/ -#ifndef CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H -#define CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H +#ifndef CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H +#define CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H #include #include @@ -22,6 +22,7 @@ namespace CVC4 { namespace theory { namespace arith { +namespace nl { class NlModel; @@ -98,6 +99,7 @@ class ArgTrie Node add(Node d, const std::vector& args); }; +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp similarity index 99% rename from src/theory/arith/nl_model.cpp rename to src/theory/arith/nl/nl_model.cpp index 0d47c8874..d5df96bd8 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -12,7 +12,7 @@ ** \brief Model object for the non-linear extension class **/ -#include "theory/arith/nl_model.h" +#include "theory/arith/nl/nl_model.h" #include "expr/node_algorithm.h" #include "options/arith_options.h" @@ -25,6 +25,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { NlModel::NlModel(context::Context* c) : d_used_approx(false) { @@ -320,7 +321,7 @@ bool NlModel::checkModel(const std::vector& assertions, Node mg = nm->mkSkolem("model", nm->booleanType()); gs.push_back(mg); // assert the constructed model as assertions - for (const std::pair > cb : + for (const std::pair> cb : d_check_model_bounds) { Node l = cb.second.first; @@ -350,7 +351,7 @@ bool NlModel::addCheckModelSubstitution(TNode v, TNode s) } // if we previously had an approximate bound, the exact bound should be in its // range - std::map >::iterator itb = + std::map>::iterator itb = d_check_model_bounds.find(v); if (itb != d_check_model_bounds.end()) { @@ -852,7 +853,7 @@ bool NlModel::simpleCheckModelLit(Node lit) for (const Node& v : vs) { // is it a valid variable? - std::map >::iterator bit = + std::map>::iterator bit = d_check_model_bounds.find(v); if (!expr::hasSubterm(invalid_vsum, v) && bit != d_check_model_bounds.end()) { @@ -1041,7 +1042,7 @@ bool NlModel::simpleCheckModelMsum(const std::map& msum, bool pol) } Trace("nl-ext-cms-debug") << " "; } - std::map >::iterator bit = + std::map>::iterator bit = d_check_model_bounds.find(vc); // if there is a model bound for this term if (bit != d_check_model_bounds.end()) @@ -1284,7 +1285,7 @@ void NlModel::getModelValueRepair( // values for variables that we solved for, using techniques specific to // this class. NodeManager* nm = NodeManager::currentNM(); - for (const std::pair >& cb : + for (const std::pair>& cb : d_check_model_bounds) { Node l = cb.second.first; @@ -1342,6 +1343,7 @@ void NlModel::getModelValueRepair( } } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl/nl_model.h similarity index 98% rename from src/theory/arith/nl_model.h rename to src/theory/arith/nl/nl_model.h index 5129a7a32..61193fc12 100644 --- a/src/theory/arith/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -12,8 +12,8 @@ ** \brief Model object for the non-linear extension class **/ -#ifndef CVC4__THEORY__ARITH__NL_MODEL_H -#define CVC4__THEORY__ARITH__NL_MODEL_H +#ifndef CVC4__THEORY__ARITH__NL__NL_MODEL_H +#define CVC4__THEORY__ARITH__NL__NL_MODEL_H #include #include @@ -28,6 +28,7 @@ namespace CVC4 { namespace theory { namespace arith { +namespace nl { class NonlinearExtension; @@ -307,7 +308,7 @@ class NlModel * (2) variables we have solved quadratic equations for, whose value * involves approximations of square roots. */ - std::map > d_check_model_bounds; + std::map> d_check_model_bounds; /** * The map from literals that our model construction solved, to the variable * that was solved for. Examples of such literals are: @@ -326,6 +327,7 @@ class NlModel std::unordered_set d_tautology; }; /* class NlModel */ +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_monomial.cpp b/src/theory/arith/nl/nl_monomial.cpp similarity index 98% rename from src/theory/arith/nl_monomial.cpp rename to src/theory/arith/nl/nl_monomial.cpp index be472217d..e8e7aceba 100644 --- a/src/theory/arith/nl_monomial.cpp +++ b/src/theory/arith/nl/nl_monomial.cpp @@ -12,10 +12,10 @@ ** \brief Implementation of utilities for monomials **/ -#include "theory/arith/nl_monomial.h" +#include "theory/arith/nl/nl_monomial.h" #include "theory/arith/arith_utilities.h" -#include "theory/arith/nl_lemma_utils.h" +#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/rewriter.h" using namespace CVC4::kind; @@ -23,6 +23,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { // Returns a[key] if key is in a or value otherwise. unsigned getCountWithDefault(const NodeMultiset& a, Node key, unsigned value) @@ -329,6 +330,7 @@ Node MonomialDb::mkMonomialRemFactor(Node n, return ret; } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_monomial.h b/src/theory/arith/nl/nl_monomial.h similarity index 97% rename from src/theory/arith/nl_monomial.h rename to src/theory/arith/nl/nl_monomial.h index 81665c4d9..b226730ac 100644 --- a/src/theory/arith/nl_monomial.h +++ b/src/theory/arith/nl/nl_monomial.h @@ -12,8 +12,8 @@ ** \brief Utilities for monomials **/ -#ifndef CVC4__THEORY__ARITH__NL_MONOMIAL_H -#define CVC4__THEORY__ARITH__NL_MONOMIAL_H +#ifndef CVC4__THEORY__ARITH__NL__NL_MONOMIAL_H +#define CVC4__THEORY__ARITH__NL__NL_MONOMIAL_H #include #include @@ -23,6 +23,7 @@ namespace CVC4 { namespace theory { namespace arith { +namespace nl { class MonomialDb; class NlModel; @@ -140,6 +141,7 @@ class MonomialDb std::map > d_m_contain_umult; }; +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp similarity index 99% rename from src/theory/arith/nl_solver.cpp rename to src/theory/arith/nl/nl_solver.cpp index 893d3dbd7..12cb02c70 100644 --- a/src/theory/arith/nl_solver.cpp +++ b/src/theory/arith/nl/nl_solver.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of non-linear solver **/ -#include "theory/arith/nl_solver.h" +#include "theory/arith/nl/nl_solver.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" @@ -25,6 +25,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { void debugPrintBound(const char* c, Node coeff, Node x, Kind type, Node rhs) { @@ -1580,6 +1581,7 @@ std::vector NlSolver::checkMonomialInferResBounds() return lemmas; } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nl_solver.h b/src/theory/arith/nl/nl_solver.h similarity index 98% rename from src/theory/arith/nl_solver.h rename to src/theory/arith/nl/nl_solver.h index 73ca97f00..35c51569b 100644 --- a/src/theory/arith/nl_solver.h +++ b/src/theory/arith/nl/nl_solver.h @@ -27,15 +27,16 @@ #include "context/context.h" #include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/nl_constraint.h" -#include "theory/arith/nl_lemma_utils.h" -#include "theory/arith/nl_model.h" -#include "theory/arith/nl_monomial.h" +#include "theory/arith/nl/nl_constraint.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nl_monomial.h" #include "theory/arith/theory_arith.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { typedef std::map NodeMultiset; @@ -361,6 +362,7 @@ class NlSolver Node getFactorSkolem(Node n, std::vector& lemmas); }; /* class NlSolver */ +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp similarity index 95% rename from src/theory/arith/nonlinear_extension.cpp rename to src/theory/arith/nl/nonlinear_extension.cpp index b638d8a59..4b2d2fd37 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -15,7 +15,7 @@ ** \todo document this file **/ -#include "theory/arith/nonlinear_extension.h" +#include "theory/arith/nl/nonlinear_extension.h" #include "options/arith_options.h" #include "theory/arith/arith_utilities.h" @@ -28,6 +28,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { NonlinearExtension::NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee) @@ -49,27 +50,37 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, NonlinearExtension::~NonlinearExtension() {} bool NonlinearExtension::getCurrentSubstitution( - int effort, const std::vector& vars, std::vector& subs, - std::map >& exp) { + int effort, + const std::vector& vars, + std::vector& subs, + std::map>& exp) +{ // get the constant equivalence classes - std::map > rep_to_subs_index; + std::map> rep_to_subs_index; bool retVal = false; - for (unsigned i = 0; i < vars.size(); i++) { + for (unsigned i = 0; i < vars.size(); i++) + { Node n = vars[i]; - if (d_ee->hasTerm(n)) { + if (d_ee->hasTerm(n)) + { Node nr = d_ee->getRepresentative(n); - if (nr.isConst()) { + if (nr.isConst()) + { subs.push_back(nr); Trace("nl-subs") << "Basic substitution : " << n << " -> " << nr << std::endl; exp[n].push_back(n.eqNode(nr)); retVal = true; - } else { + } + else + { rep_to_subs_index[nr].push_back(i); subs.push_back(n); } - } else { + } + else + { subs.push_back(n); } } @@ -79,8 +90,10 @@ bool NonlinearExtension::getCurrentSubstitution( } std::pair NonlinearExtension::isExtfReduced( - int effort, Node n, Node on, const std::vector& exp) const { - if (n != d_zero) { + int effort, Node n, Node on, const std::vector& exp) const +{ + if (n != d_zero) + { Kind k = n.getKind(); return std::make_pair(k != NONLINEAR_MULT && !isTranscendentalKind(k), Node::null()); @@ -88,15 +101,15 @@ std::pair NonlinearExtension::isExtfReduced( Assert(n == d_zero); if (on.getKind() == NONLINEAR_MULT) { - Trace("nl-ext-zero-exp") << "Infer zero : " << on << " == " << n - << std::endl; + Trace("nl-ext-zero-exp") + << "Infer zero : " << on << " == " << n << std::endl; // minimize explanation if a substitution+rewrite results in zero const std::set vars(on.begin(), on.end()); for (unsigned i = 0, size = exp.size(); i < size; i++) { - Trace("nl-ext-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() == EQUAL) { @@ -119,8 +132,8 @@ std::pair NonlinearExtension::isExtfReduced( { if (eqs[j][r] == d_zero && vars.find(eqs[j][1 - r]) != vars.end()) { - Trace("nl-ext-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]); } } @@ -337,9 +350,10 @@ std::vector NonlinearExtension::checkModelEval( const std::vector& assertions) { std::vector false_asserts; - for (size_t i = 0; i < assertions.size(); ++i) { + for (size_t i = 0; i < assertions.size(); ++i) + { Node lit = assertions[i]; - Node atom = lit.getKind()==NOT ? lit[0] : lit; + Node atom = lit.getKind() == NOT ? lit[0] : lit; Node litv = d_model.computeConcreteModelValue(lit); Trace("nl-ext-mv-assert") << "M[[ " << lit << " ]] -> " << litv; if (litv != d_true) @@ -403,7 +417,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } //----------------------------------- possibly split on zero - if (options::nlExtSplitZero()) { + if (options::nlExtSplitZero()) + { Trace("nl-ext") << "Get zero split lemmas..." << std::endl; lemmas = d_nlSlv.checkSplitZero(); filterLemmas(lemmas, lems); @@ -415,7 +430,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } } - //-----------------------------------initial lemmas for transcendental functions + //-----------------------------------initial lemmas for transcendental + //functions lemmas = d_trSlv.checkTranscendentalInitialRefine(); filterLemmas(lemmas, lems); if (!lems.empty()) @@ -445,8 +461,10 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, return lems.size(); } - //-----------------------------------lemmas based on magnitude of non-zero monomials - for (unsigned c = 0; c < 3; c++) { + //-----------------------------------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(); @@ -462,7 +480,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, //-----------------------------------inferred bounds lemmas // e.g. x >= t => y*x >= y*t - std::vector< Node > nt_lemmas; + std::vector nt_lemmas; lemmas = d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts); // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << @@ -494,7 +512,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, //------------------------------------factoring lemmas // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t - if( options::nlExtFactor() ){ + if (options::nlExtFactor()) + { lemmas = d_nlSlv.checkFactoring(assertions, false_asserts); filterLemmas(lemmas, lems); if (!lems.empty()) @@ -507,7 +526,8 @@ int 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::nlExtResBound()) { + if (options::nlExtResBound()) + { lemmas = d_nlSlv.checkMonomialInferResBounds(); filterLemmas(lemmas, lems); if (!lems.empty()) @@ -517,7 +537,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, return lems.size(); } } - + //------------------------------------tangent planes if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave()) { @@ -535,7 +555,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, return 0; } -void NonlinearExtension::check(Theory::Effort e) { +void NonlinearExtension::check(Theory::Effort e) +{ Trace("nl-ext") << std::endl; Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << ", built model = " << d_builtModel.get() << std::endl; @@ -543,15 +564,20 @@ void NonlinearExtension::check(Theory::Effort e) { { d_containing.getExtTheory()->clearCache(); d_needsLastCall = true; - if (options::nlExtRewrites()) { + if (options::nlExtRewrites()) + { std::vector nred; - if (!d_containing.getExtTheory()->doInferences(0, nred)) { + if (!d_containing.getExtTheory()->doInferences(0, nred)) + { Trace("nl-ext") << "...sent no lemmas, # extf to reduce = " << nred.size() << std::endl; - if (nred.empty()) { + if (nred.empty()) + { d_needsLastCall = false; } - } else { + } + else + { Trace("nl-ext") << "...sent lemmas." << std::endl; } } @@ -809,7 +835,7 @@ void NonlinearExtension::presolve() Trace("nl-ext") << "NonlinearExtension::presolve" << std::endl; } - +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h similarity index 95% rename from src/theory/arith/nonlinear_extension.h rename to src/theory/arith/nl/nonlinear_extension.h index 5aa2070a6..855310daa 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -15,8 +15,8 @@ ** multiplication via axiom instantiations. **/ -#ifndef CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H -#define CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H +#ifndef CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H +#define CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H #include #include @@ -25,16 +25,17 @@ #include "context/cdlist.h" #include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/nl_lemma_utils.h" -#include "theory/arith/nl_model.h" -#include "theory/arith/nl_solver.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nl_solver.h" +#include "theory/arith/nl/transcendental_solver.h" #include "theory/arith/theory_arith.h" -#include "theory/arith/transcendental_solver.h" #include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { /** Non-linear extension class * @@ -60,7 +61,8 @@ namespace arith { * for valid arithmetic theory lemmas, based on the current set of assertions, * where d_out is the output channel of TheoryArith. */ -class NonlinearExtension { +class NonlinearExtension +{ typedef context::CDHashSet NodeSet; public: @@ -84,9 +86,10 @@ class NonlinearExtension { * that hold in the current context. We call { vars -> subs } a "derivable * substituion" (see Reynolds et al. FroCoS 2017). */ - bool getCurrentSubstitution(int effort, const std::vector& vars, + bool getCurrentSubstitution(int effort, + const std::vector& vars, std::vector& subs, - std::map >& exp); + std::map>& exp); /** Is the term n in reduced form? * * Used for context-dependent simplification. @@ -103,7 +106,9 @@ class NonlinearExtension { * The second part of the pair is used for constructing * minimal explanations for context-dependent simplifications. */ - std::pair isExtfReduced(int effort, Node n, Node on, + std::pair isExtfReduced(int effort, + Node n, + Node on, const std::vector& exp) const; /** Check at effort level e. * @@ -157,6 +162,7 @@ class NonlinearExtension { * on the output channel of TheoryArith in this function. */ void presolve(); + private: /** Model-based refinement * @@ -179,7 +185,6 @@ class NonlinearExtension { std::vector& mlemsPp, std::map& lemSE); - /** check last call * * Check assertions for consistency in the effort LAST_CALL with a subset of @@ -328,6 +333,7 @@ class NonlinearExtension { context::CDO d_builtModel; }; /* class NonlinearExtension */ +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp similarity index 99% rename from src/theory/arith/transcendental_solver.cpp rename to src/theory/arith/nl/transcendental_solver.cpp index 665accc0a..3e10f6397 100644 --- a/src/theory/arith/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental_solver.cpp @@ -12,7 +12,7 @@ ** \brief Implementation of solver for handling transcendental functions. **/ -#include "theory/arith/transcendental_solver.h" +#include "theory/arith/nl/transcendental_solver.h" #include #include @@ -29,6 +29,7 @@ using namespace CVC4::kind; namespace CVC4 { namespace theory { namespace arith { +namespace nl { TranscendentalSolver::TranscendentalSolver(NlModel& m) : d_model(m) { @@ -1470,6 +1471,7 @@ Node TranscendentalSolver::mkValidPhase(Node a, Node pi) NodeManager::currentNM()->mkNode(MULT, mkRationalNode(-1), pi), a, pi); } +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/transcendental_solver.h b/src/theory/arith/nl/transcendental_solver.h similarity index 98% rename from src/theory/arith/transcendental_solver.h rename to src/theory/arith/nl/transcendental_solver.h index 88de49af3..5cd57d8fa 100644 --- a/src/theory/arith/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental_solver.h @@ -12,8 +12,8 @@ ** \brief Solving for handling transcendental functions. **/ -#ifndef CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H -#define CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H +#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL_SOLVER_H +#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL_SOLVER_H #include #include @@ -21,12 +21,13 @@ #include #include "expr/node.h" -#include "theory/arith/nl_lemma_utils.h" -#include "theory/arith/nl_model.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { /** Transcendental solver class * @@ -421,6 +422,7 @@ class TranscendentalSolver Node d_pi_bound[2]; }; /* class TranscendentalSolver */ +} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 638f5250e..3ff3966cc 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -55,7 +55,7 @@ #include "theory/arith/dio_solver.h" #include "theory/arith/linear_equality.h" #include "theory/arith/matrix.h" -#include "theory/arith/nonlinear_extension.h" +#include "theory/arith/nl/nonlinear_extension.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" #include "theory/arith/simplex.h" @@ -162,7 +162,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_nlin_inverse_skolem(u) { if( options::nlExt() ){ - d_nonlinearExtension = new NonlinearExtension( + d_nonlinearExtension = new nl::NonlinearExtension( containing, d_congruenceManager.getEqualityEngine()); } } diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 8198dbcf1..822b38f69 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -83,7 +83,9 @@ namespace inferbounds { } class InferBoundsResult; +namespace nl { class NonlinearExtension; +} /** * Implementation of QF_LRA. @@ -372,7 +374,7 @@ private: AttemptSolutionSDP d_attemptSolSimplex; /** non-linear algebraic approach */ - NonlinearExtension * d_nonlinearExtension; + nl::NonlinearExtension* d_nonlinearExtension; bool solveRealRelaxation(Theory::Effort effortLevel); -- 2.30.2