diff options
Diffstat (limited to 'src/theory/arith/nl')
73 files changed, 182 insertions, 182 deletions
diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index 7fd22fb76..c9f3ce3da 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -29,12 +29,12 @@ namespace std { template <typename T> std::ostream& operator<<(std::ostream& os, const std::vector<T>& v) { - CVC5::container_to_stream(os, v); + cvc5::container_to_stream(os, v); return os; } } // namespace std -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -545,6 +545,6 @@ void CDCAC::pruneRedundantIntervals(std::vector<CACInterval>& intervals) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 2b607ae78..338f54da2 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -31,7 +31,7 @@ #include "theory/arith/nl/cad/proof_generator.h" #include "theory/arith/nl/cad/variable_ordering.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -210,7 +210,7 @@ class CDCAC } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp index f40d528ff..999e491f6 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.cpp +++ b/src/theory/arith/nl/cad/cdcac_utils.cpp @@ -20,7 +20,7 @@ #include "theory/arith/nl/cad/projections.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -370,6 +370,6 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h index 3b3a3638b..607a2226f 100644 --- a/src/theory/arith/nl/cad/cdcac_utils.h +++ b/src/theory/arith/nl/cad/cdcac_utils.h @@ -28,7 +28,7 @@ #include "expr/node.h" #include "theory/arith/nl/cad/projections.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -105,7 +105,7 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp index 1ea172d11..75d1cb723 100644 --- a/src/theory/arith/nl/cad/constraints.cpp +++ b/src/theory/arith/nl/cad/constraints.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/poly_conversion.h" #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -79,6 +79,6 @@ void Constraints::sortConstraints() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h index 70c52e85c..e9e59c40b 100644 --- a/src/theory/arith/nl/cad/constraints.h +++ b/src/theory/arith/nl/cad/constraints.h @@ -28,7 +28,7 @@ #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -87,7 +87,7 @@ class Constraints } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp index b9e17f844..1bac0c160 100644 --- a/src/theory/arith/nl/cad/projections.cpp +++ b/src/theory/arith/nl/cad/projections.cpp @@ -20,7 +20,7 @@ #include "base/check.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -106,6 +106,6 @@ PolyVector projection_mccallum(const std::vector<Polynomial>& polys) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h index 3b8eb412f..94bdfc3ef 100644 --- a/src/theory/arith/nl/cad/projections.h +++ b/src/theory/arith/nl/cad/projections.h @@ -25,7 +25,7 @@ #include <vector> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -76,7 +76,7 @@ PolyVector projectionMcCallum(const std::vector<poly::Polynomial>& polys); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp index f1ab2d6a9..3cd8fe98e 100644 --- a/src/theory/arith/nl/cad/proof_checker.cpp +++ b/src/theory/arith/nl/cad/proof_checker.cpp @@ -17,9 +17,9 @@ #include "expr/sequence.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -58,4 +58,4 @@ Node CADProofRuleChecker::checkInternal(PfRule id, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h index 26bbcc3a9..9100762b7 100644 --- a/src/theory/arith/nl/cad/proof_checker.h +++ b/src/theory/arith/nl/cad/proof_checker.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "expr/proof_checker.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -53,6 +53,6 @@ class CADProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index fe3734dce..73e19aa28 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -19,7 +19,7 @@ #include "theory/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -230,6 +230,6 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h index c1bb4be1e..76a72f9c5 100644 --- a/src/theory/arith/nl/cad/proof_generator.h +++ b/src/theory/arith/nl/cad/proof_generator.h @@ -28,7 +28,7 @@ #include "theory/arith/nl/cad/cdcac_utils.h" #include "theory/lazy_tree_proof_generator.h" -namespace CVC5 { +namespace cvc5 { class ProofGenerator; @@ -144,7 +144,7 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif #endif diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp index 63db35553..7ebbc90dd 100644 --- a/src/theory/arith/nl/cad/variable_ordering.cpp +++ b/src/theory/arith/nl/cad/variable_ordering.cpp @@ -20,7 +20,7 @@ #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -132,6 +132,6 @@ std::vector<poly::Variable> VariableOrdering::operator()( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h index 7fda3faa4..0ab585197 100644 --- a/src/theory/arith/nl/cad/variable_ordering.h +++ b/src/theory/arith/nl/cad/variable_ordering.h @@ -26,7 +26,7 @@ #include "theory/arith/nl/cad/constraints.h" #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -65,7 +65,7 @@ std::vector<poly_utils::VariableInformation> collectInformation( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index dc18fbdf5..1cf9cbc54 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -20,7 +20,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -212,4 +212,4 @@ bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index de97c48cc..620679735 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -22,7 +22,7 @@ #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/cad/proof_checker.h" -namespace CVC5 { +namespace cvc5 { class ProofNodeManager; @@ -110,6 +110,6 @@ class CadSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__CAD_SOLVER_H */ diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp index 41331d041..688bab86d 100644 --- a/src/theory/arith/nl/ext/constraint.cpp +++ b/src/theory/arith/nl/ext/constraint.cpp @@ -18,9 +18,9 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/nl/ext/monomial.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -123,4 +123,4 @@ bool ConstraintDb::isMaximal(Node atom, Node x) const } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h index 9e6451c99..a96949a1e 100644 --- a/src/theory/arith/nl/ext/constraint.h +++ b/src/theory/arith/nl/ext/constraint.h @@ -21,7 +21,7 @@ #include "expr/kind.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -84,6 +84,6 @@ class ConstraintDb } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL_SOLVER_H */ diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index fc806199e..e20224207 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nl_lemma_utils.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -109,4 +109,4 @@ CDProof* ExtState::getProof() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 1d8e7ea0a..2d20e1557 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -21,7 +21,7 @@ #include "expr/proof_set.h" #include "theory/arith/nl/ext/monomial.h" -namespace CVC5 { +namespace cvc5 { class CDProof; @@ -91,6 +91,6 @@ struct ExtState } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 675368843..09e1d4f10 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -207,4 +207,4 @@ Node FactoringCheck::getFactorSkolem(Node n, CDProof* proof) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h index 89c5fce30..08154cb98 100644 --- a/src/theory/arith/nl/ext/factoring_check.h +++ b/src/theory/arith/nl/ext/factoring_check.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { class CDProof; @@ -69,6 +69,6 @@ class FactoringCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp index 86abed70c..784c07691 100644 --- a/src/theory/arith/nl/ext/monomial.cpp +++ b/src/theory/arith/nl/ext/monomial.cpp @@ -18,9 +18,9 @@ #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -333,4 +333,4 @@ Node MonomialDb::mkMonomialRemFactor(Node n, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h index 98083b996..6646e4a73 100644 --- a/src/theory/arith/nl/ext/monomial.h +++ b/src/theory/arith/nl/ext/monomial.h @@ -20,7 +20,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -144,6 +144,6 @@ class MonomialDb } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL_MONOMIAL_H */ diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index c8194bbd0..344218148 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -24,7 +24,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -520,4 +520,4 @@ void MonomialBoundsCheck::checkResBounds() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h index e63dd454a..a19c61e64 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.h +++ b/src/theory/arith/nl/ext/monomial_bounds_check.h @@ -18,7 +18,7 @@ #include "expr/node.h" #include "theory/arith/nl/ext/constraint.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -86,6 +86,6 @@ class MonomialBoundsCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 9fc2ba10a..a30d4aff9 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -22,7 +22,7 @@ #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/ext/ext_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -757,4 +757,4 @@ void MonomialCheck::setMonomialFactor(Node a, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index 948368542..f242182b4 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -19,7 +19,7 @@ #include "theory/arith/nl/ext/monomial.h" #include "theory/theory_inference.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -194,6 +194,6 @@ class MonomialCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index 26db3c9e0..b6c4572f5 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -18,9 +18,9 @@ #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -158,4 +158,4 @@ Node ExtProofRuleChecker::checkInternal(PfRule id, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h index 7bd4b7e38..90518fc08 100644 --- a/src/theory/arith/nl/ext/proof_checker.h +++ b/src/theory/arith/nl/ext/proof_checker.h @@ -21,7 +21,7 @@ #include "expr/proof_checker.h" #include "expr/proof_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -51,6 +51,6 @@ class ExtProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 543b6a0bd..7392d45f4 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -22,7 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -57,4 +57,4 @@ void SplitZeroCheck::check() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index 316e304ff..04148bd19 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -18,7 +18,7 @@ #include "expr/node.h" #include "context/cdhashset.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -50,6 +50,6 @@ class SplitZeroCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index bdeca7a29..711bc9816 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -22,7 +22,7 @@ #include "theory/arith/nl/ext/ext_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -164,4 +164,4 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h index 7d48d249b..b5159e721 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.h +++ b/src/theory/arith/nl/ext/tangent_plane_check.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -67,6 +67,6 @@ class TangentPlaneCheck } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index 125fbb05a..72848ac89 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -17,9 +17,9 @@ #include "theory/arith/arith_utilities.h" #include "theory/uf/equality_engine.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -129,4 +129,4 @@ bool NlExtTheoryCallback::isExtfReduced(int effort, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h index c747eef69..0e0e1411b 100644 --- a/src/theory/arith/nl/ext_theory_callback.h +++ b/src/theory/arith/nl/ext_theory_callback.h @@ -18,7 +18,7 @@ #include "expr/node.h" #include "theory/ext_theory.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace eq { class EqualityEngine; @@ -84,6 +84,6 @@ class NlExtTheoryCallback : public ExtTheoryCallback } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */ diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 01f4c6e15..0e339857b 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -25,9 +25,9 @@ #include "theory/rewriter.h" #include "util/iand.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -298,4 +298,4 @@ Node IAndSolver::bitwiseLemma(Node i) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 95d9632aa..2b7f90e9b 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -22,7 +22,7 @@ #include "expr/node.h" #include "theory/arith/nl/iand_utils.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -132,6 +132,6 @@ class IAndSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__IAND_SOLVER_H */ diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index cd96021b0..e08068b7e 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -21,7 +21,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -276,4 +276,4 @@ Node IAndUtils::twoToKMinusOne(unsigned k) const } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h index da5f8f04f..60c3cbe13 100644 --- a/src/theory/arith/nl/iand_utils.h +++ b/src/theory/arith/nl/iand_utils.h @@ -20,7 +20,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -169,6 +169,6 @@ class IAndUtils } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */ diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp index 87d823018..31b7b085b 100644 --- a/src/theory/arith/nl/icp/candidate.cpp +++ b/src/theory/arith/nl/icp/candidate.cpp @@ -23,7 +23,7 @@ #include "theory/arith/nl/icp/intersection.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -115,6 +115,6 @@ std::ostream& operator<<(std::ostream& os, const Candidate& c) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h index d4ad11fcf..4bcbf3e85 100644 --- a/src/theory/arith/nl/icp/candidate.h +++ b/src/theory/arith/nl/icp/candidate.h @@ -23,7 +23,7 @@ #include "expr/node.h" #include "theory/arith/nl/icp/intersection.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -78,7 +78,7 @@ std::ostream& operator<<(std::ostream& os, const Candidate& c); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp index c0b0cb768..acf499a21 100644 --- a/src/theory/arith/nl/icp/contraction_origins.cpp +++ b/src/theory/arith/nl/icp/contraction_origins.cpp @@ -14,7 +14,7 @@ #include "theory/arith/nl/icp/contraction_origins.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -117,4 +117,4 @@ inline std::ostream& operator<<(std::ostream& os, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h index 0f22b5463..dfddbce78 100644 --- a/src/theory/arith/nl/icp/contraction_origins.h +++ b/src/theory/arith/nl/icp/contraction_origins.h @@ -20,7 +20,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -99,6 +99,6 @@ std::ostream& operator<<(std::ostream& os, const ContractionOriginManager& com); } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index e09264a25..2f6cdf220 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -26,7 +26,7 @@ #include "theory/rewriter.h" #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -384,4 +384,4 @@ void ICPSolver::check() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index 56ec03706..11fd9ac1b 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -28,7 +28,7 @@ #include "theory/arith/nl/icp/intersection.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -153,6 +153,6 @@ class ICPSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index 6cdba297c..e0e93e1dd 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -24,7 +24,7 @@ #include "base/output.h" #include "theory/arith/nl/poly_conversion.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -221,6 +221,6 @@ PropagationResult intersect_interval_with(poly::Interval& cur, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index c453f8314..dd4afadfc 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -25,7 +25,7 @@ namespace poly { class Interval; } -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -77,7 +77,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h index 8acbfec05..981355e4a 100644 --- a/src/theory/arith/nl/icp/interval.h +++ b/src/theory/arith/nl/icp/interval.h @@ -22,7 +22,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -58,7 +58,7 @@ inline std::ostream& operator<<(std::ostream& os, const Interval& i) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index f3c2d70c8..9740e1b46 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -17,7 +17,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/nonlinear_extension.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -78,4 +78,4 @@ Node ArgTrie::add(Node d, const std::vector<Node>& args) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index 71d86b08a..32fe763b4 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -21,7 +21,7 @@ #include "expr/node.h" #include "theory/theory_inference.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -144,6 +144,6 @@ class ArgTrie } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H */ diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index f7edefff7..882cd12a4 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -24,9 +24,9 @@ #include "theory/theory_model.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -1342,4 +1342,4 @@ void NlModel::getModelValueRepair( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index b2c435098..9da8738b6 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -22,7 +22,7 @@ #include "expr/kind.h" #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace context { class Context; @@ -329,6 +329,6 @@ class NlModel } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 3c46e1652..03563006b 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -27,9 +27,9 @@ #include "theory/rewriter.h" #include "theory/theory_model.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -622,4 +622,4 @@ void NonlinearExtension::runStrategy(Theory::Effort effort, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index b6fb53651..722741d7d 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -41,7 +41,7 @@ #include "theory/theory.h" #include "util/result.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace eq { class EqualityEngine; @@ -296,6 +296,6 @@ class NonlinearExtension } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */ diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 5738dccfc..c7b549655 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -23,12 +23,12 @@ #include "theory/arith/bound_inference.h" #include "util/poly_util.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { -poly::Variable VariableMapper::operator()(const CVC5::Node& n) +poly::Variable VariableMapper::operator()(const cvc5::Node& n) { auto it = mVarCVCpoly.find(n); if (it == mVarCVCpoly.end()) @@ -54,7 +54,7 @@ poly::Variable VariableMapper::operator()(const CVC5::Node& n) return it->second; } -CVC5::Node VariableMapper::operator()(const poly::Variable& n) +cvc5::Node VariableMapper::operator()(const poly::Variable& n) { auto it = mVarpolyCVC.find(n); Assert(it != mVarpolyCVC.end()) @@ -62,7 +62,7 @@ CVC5::Node VariableMapper::operator()(const poly::Variable& n) return it->second; } -CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC5::Node& var) +cvc5::Node as_cvc_upolynomial(const poly::UPolynomial& p, const cvc5::Node& var) { Trace("poly::conversion") << "Converting " << p << " over " << var << std::endl; @@ -87,9 +87,9 @@ CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC5::Node& var) return res; } -poly::UPolynomial as_poly_upolynomial_impl(const CVC5::Node& n, +poly::UPolynomial as_poly_upolynomial_impl(const cvc5::Node& n, poly::Integer& denominator, - const CVC5::Node& var) + const cvc5::Node& var) { denominator = poly::Integer(1); if (n.isVar()) @@ -140,14 +140,14 @@ poly::UPolynomial as_poly_upolynomial_impl(const CVC5::Node& n, return poly::UPolynomial(); } -poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n, - const CVC5::Node& var) +poly::UPolynomial as_poly_upolynomial(const cvc5::Node& n, + const cvc5::Node& var) { poly::Integer denom; return as_poly_upolynomial_impl(n, denom, var); } -poly::Polynomial as_poly_polynomial_impl(const CVC5::Node& n, +poly::Polynomial as_poly_polynomial_impl(const cvc5::Node& n, poly::Integer& denominator, VariableMapper& vm) { @@ -195,12 +195,12 @@ poly::Polynomial as_poly_polynomial_impl(const CVC5::Node& n, } return poly::Polynomial(); } -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, VariableMapper& vm) +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm) { poly::Integer denom; return as_poly_polynomial_impl(n, denom, vm); } -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm, poly::Rational& denominator) { @@ -257,7 +257,7 @@ void collect_monomials(const lp_polynomial_context_t* ctx, } } // namespace -CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm) +cvc5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm) { CollectMonomialData cmd(vm); // Do the actual conversion @@ -274,7 +274,7 @@ CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm) return cmd.d_nm->mkNode(Kind::PLUS, cmd.d_terms); } -poly::SignCondition normalize_kind(CVC5::Kind kind, +poly::SignCondition normalize_kind(cvc5::Kind kind, bool negated, poly::Polynomial& lhs) { @@ -803,6 +803,6 @@ poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 9adc9a996..9aef0db18 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -30,7 +30,7 @@ #include "expr/node.h" #include "util/real_algebraic_number.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -42,23 +42,23 @@ namespace nl { struct VariableMapper { /** A mapping from CVC4 variables to poly variables. */ - std::map<CVC5::Node, poly::Variable> mVarCVCpoly; + std::map<cvc5::Node, poly::Variable> mVarCVCpoly; /** A mapping from poly variables to CVC4 variables. */ - std::map<poly::Variable, CVC5::Node> mVarpolyCVC; + std::map<poly::Variable, cvc5::Node> mVarpolyCVC; /** Retrieves the according poly variable. */ - poly::Variable operator()(const CVC5::Node& n); + poly::Variable operator()(const cvc5::Node& n); /** Retrieves the according CVC4 variable. */ - CVC5::Node operator()(const poly::Variable& n); + cvc5::Node operator()(const poly::Variable& n); }; -/** Convert a poly univariate polynomial to a CVC5::Node. */ -CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p, - const CVC5::Node& var); +/** Convert a poly univariate polynomial to a cvc5::Node. */ +cvc5::Node as_cvc_upolynomial(const poly::UPolynomial& p, + const cvc5::Node& var); -/** Convert a CVC5::Node to a poly univariate polynomial. */ -poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n, - const CVC5::Node& var); +/** Convert a cvc5::Node to a poly univariate polynomial. */ +poly::UPolynomial as_poly_upolynomial(const cvc5::Node& n, + const cvc5::Node& var); /** * Constructs a polynomial from the given node. @@ -73,8 +73,8 @@ poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n, * in the context of ICP) the second overload provides the denominator in the * third argument. */ -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, VariableMapper& vm); -poly::Polynomial as_poly_polynomial(const CVC5::Node& n, +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm); +poly::Polynomial as_poly_polynomial(const cvc5::Node& n, VariableMapper& vm, poly::Rational& denominator); @@ -87,7 +87,7 @@ poly::Polynomial as_poly_polynomial(const CVC5::Node& n, * multiplications with one or use NONLINEAR_MULT where regular MULT may be * sufficient), so it may be sensible to rewrite it afterwards. */ -CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm); +cvc5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm); /** * Constructs a constraints (a polynomial and a sign condition) from the given @@ -164,7 +164,7 @@ poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp index 92cebc8fc..33a73ddd7 100644 --- a/src/theory/arith/nl/stats.cpp +++ b/src/theory/arith/nl/stats.cpp @@ -16,7 +16,7 @@ #include "smt/smt_statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -38,4 +38,4 @@ NlStats::~NlStats() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index 66157d0a3..66f41375b 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -19,7 +19,7 @@ #include "util/statistics_registry.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -44,6 +44,6 @@ class NlStats } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL__STATS_H */ diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index af23f67f9..4df53b103 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -19,7 +19,7 @@ #include "base/check.h" #include "options/arith_options.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -173,4 +173,4 @@ StepGenerator Strategy::getStrategy() } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index 9caf6322b..139db7459 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -18,7 +18,7 @@ #include <iosfwd> #include <vector> -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -173,6 +173,6 @@ class Strategy } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL__STRATEGY_H */ diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 05849a579..5e2358b68 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -28,7 +28,7 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -276,4 +276,4 @@ std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index 8bd00c456..c5eb45728 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -19,7 +19,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -108,6 +108,6 @@ class ExponentialSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index fe071c36a..4fc85666a 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -19,9 +19,9 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -402,4 +402,4 @@ Node TranscendentalProofRuleChecker::checkInternal( } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h index 2a6837590..a4c8b55cb 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.h +++ b/src/theory/arith/nl/transcendental/proof_checker.h @@ -21,7 +21,7 @@ #include "expr/proof_checker.h" #include "expr/proof_node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -53,6 +53,6 @@ class TranscendentalProofRuleChecker : public ProofRuleChecker } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 052b6c056..c8c375096 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -28,7 +28,7 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -484,4 +484,4 @@ std::pair<Node, Node> SineSolver::getSecantBounds(TNode e, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index c20c50f6d..b85d0dc48 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -20,7 +20,7 @@ #include "expr/node.h" #include "theory/arith/nl/transcendental/transcendental_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -175,6 +175,6 @@ class SineSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index f2817344a..5a9e87b7f 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -18,7 +18,7 @@ #include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -243,4 +243,4 @@ std::pair<Node, Node> TaylorGenerator::getTfModelBounds(Node tf, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index b13be57f0..8b7f5340d 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -17,7 +17,7 @@ #include "expr/node.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -118,6 +118,6 @@ class TaylorGenerator } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index bedfe4d3b..ed5ab4255 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -27,9 +27,9 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" -using namespace CVC5::kind; +using namespace cvc5::kind; -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -438,4 +438,4 @@ int TranscendentalSolver::regionToConcavity(Kind k, int region) } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index e22bf3e64..c3d098e03 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -22,7 +22,7 @@ #include "theory/arith/nl/transcendental/sine_solver.h" #include "theory/arith/nl/transcendental/transcendental_state.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { @@ -200,6 +200,6 @@ class TranscendentalSolver } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */ diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 6ab136d39..e662c017e 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -21,7 +21,7 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" -namespace CVC5 { +namespace cvc5 { namespace theory { namespace arith { namespace nl { @@ -437,4 +437,4 @@ void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds, } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 21a60e038..a55071ef1 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -21,7 +21,7 @@ #include "theory/arith/nl/transcendental/proof_checker.h" #include "theory/arith/nl/transcendental/taylor_generator.h" -namespace CVC5 { +namespace cvc5 { class CDProof; namespace theory { namespace arith { @@ -278,6 +278,6 @@ struct TranscendentalState } // namespace nl } // namespace arith } // namespace theory -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */ |