summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/nl/nl_constraint.cpp (renamed from src/theory/arith/nl_constraint.cpp)4
-rw-r--r--src/theory/arith/nl/nl_constraint.h (renamed from src/theory/arith/nl_constraint.h)8
-rw-r--r--src/theory/arith/nl/nl_lemma_utils.cpp (renamed from src/theory/arith/nl_lemma_utils.cpp)6
-rw-r--r--src/theory/arith/nl/nl_lemma_utils.h (renamed from src/theory/arith/nl_lemma_utils.h)6
-rw-r--r--src/theory/arith/nl/nl_model.cpp (renamed from src/theory/arith/nl_model.cpp)14
-rw-r--r--src/theory/arith/nl/nl_model.h (renamed from src/theory/arith/nl_model.h)8
-rw-r--r--src/theory/arith/nl/nl_monomial.cpp (renamed from src/theory/arith/nl_monomial.cpp)6
-rw-r--r--src/theory/arith/nl/nl_monomial.h (renamed from src/theory/arith/nl_monomial.h)6
-rw-r--r--src/theory/arith/nl/nl_solver.cpp (renamed from src/theory/arith/nl_solver.cpp)4
-rw-r--r--src/theory/arith/nl/nl_solver.h (renamed from src/theory/arith/nl_solver.h)10
-rw-r--r--src/theory/arith/nl/nonlinear_extension.cpp (renamed from src/theory/arith/nonlinear_extension.cpp)92
-rw-r--r--src/theory/arith/nl/nonlinear_extension.h (renamed from src/theory/arith/nonlinear_extension.h)28
-rw-r--r--src/theory/arith/nl/transcendental_solver.cpp (renamed from src/theory/arith/transcendental_solver.cpp)4
-rw-r--r--src/theory/arith/nl/transcendental_solver.h (renamed from src/theory/arith/transcendental_solver.h)10
-rw-r--r--src/theory/arith/theory_arith_private.cpp4
-rw-r--r--src/theory/arith/theory_arith_private.h4
16 files changed, 136 insertions, 78 deletions
diff --git a/src/theory/arith/nl_constraint.cpp b/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
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 <map>
#include <vector>
#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<Node, std::map<Node, ConstraintInfo> > 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
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<Node>& 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
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 <tuple>
#include <vector>
@@ -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<Node>& 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
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<Node>& assertions,
Node mg = nm->mkSkolem("model", nm->booleanType());
gs.push_back(mg);
// assert the constructed model as assertions
- for (const std::pair<const Node, std::pair<Node, Node> > cb :
+ for (const std::pair<const Node, std::pair<Node, Node>> 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<Node, std::pair<Node, Node> >::iterator itb =
+ std::map<Node, std::pair<Node, Node>>::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<Node, std::pair<Node, Node> >::iterator bit =
+ std::map<Node, std::pair<Node, Node>>::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<Node, Node>& msum, bool pol)
}
Trace("nl-ext-cms-debug") << " ";
}
- std::map<Node, std::pair<Node, Node> >::iterator bit =
+ std::map<Node, std::pair<Node, Node>>::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<const Node, std::pair<Node, Node> >& cb :
+ for (const std::pair<const Node, std::pair<Node, Node>>& 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
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 <map>
#include <unordered_map>
@@ -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<Node, std::pair<Node, Node> > d_check_model_bounds;
+ std::map<Node, std::pair<Node, Node>> 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<Node, NodeHashFunction> 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
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
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 <map>
#include <vector>
@@ -23,6 +23,7 @@
namespace CVC4 {
namespace theory {
namespace arith {
+namespace nl {
class MonomialDb;
class NlModel;
@@ -140,6 +141,7 @@ class MonomialDb
std::map<Node, std::map<Node, Node> > 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
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<Node> 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
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<Node, unsigned> NodeMultiset;
@@ -361,6 +362,7 @@ class NlSolver
Node getFactorSkolem(Node n, std::vector<Node>& 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
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<Node>& vars, std::vector<Node>& subs,
- std::map<Node, std::vector<Node> >& exp) {
+ int effort,
+ const std::vector<Node>& vars,
+ std::vector<Node>& subs,
+ std::map<Node, std::vector<Node>>& exp)
+{
// get the constant equivalence classes
- std::map<Node, std::vector<int> > rep_to_subs_index;
+ std::map<Node, std::vector<int>> 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<bool, Node> NonlinearExtension::isExtfReduced(
- int effort, Node n, Node on, const std::vector<Node>& exp) const {
- if (n != d_zero) {
+ int effort, Node n, Node on, const std::vector<Node>& 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<bool, Node> 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<Node> 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<Node> eqs;
if (exp[i].getKind() == EQUAL)
{
@@ -119,8 +132,8 @@ std::pair<bool, Node> 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<Node> NonlinearExtension::checkModelEval(
const std::vector<Node>& assertions)
{
std::vector<Node> 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<Node>& 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<Node>& 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<Node>& 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<Node>& assertions,
//-----------------------------------inferred bounds lemmas
// e.g. x >= t => y*x >= y*t
- std::vector< Node > nt_lemmas;
+ std::vector<Node> 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<Node>& 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<Node>& 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<Node>& assertions,
return lems.size();
}
}
-
+
//------------------------------------tangent planes
if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave())
{
@@ -535,7 +555,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& 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<Node> 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
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 <stdint.h>
#include <map>
@@ -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<Node, NodeHashFunction> 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<Node>& vars,
+ bool getCurrentSubstitution(int effort,
+ const std::vector<Node>& vars,
std::vector<Node>& subs,
- std::map<Node, std::vector<Node> >& exp);
+ std::map<Node, std::vector<Node>>& 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<bool, Node> isExtfReduced(int effort, Node n, Node on,
+ std::pair<bool, Node> isExtfReduced(int effort,
+ Node n,
+ Node on,
const std::vector<Node>& 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<Node>& mlemsPp,
std::map<Node, NlLemmaSideEffect>& 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<bool> 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
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 <cmath>
#include <set>
@@ -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
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 <map>
#include <unordered_map>
@@ -21,12 +21,13 @@
#include <vector>
#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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback