summaryrefslogtreecommitdiff
path: root/src/prop/minisat
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/minisat')
-rw-r--r--src/prop/minisat/core/Dimacs.h4
-rw-r--r--src/prop/minisat/core/Solver.cc38
-rw-r--r--src/prop/minisat/core/Solver.h34
-rw-r--r--src/prop/minisat/core/SolverTypes.h14
-rw-r--r--src/prop/minisat/minisat.cpp14
-rw-r--r--src/prop/minisat/minisat.h6
-rw-r--r--src/prop/minisat/mtl/Alg.h4
-rw-r--r--src/prop/minisat/mtl/Alloc.h4
-rw-r--r--src/prop/minisat/mtl/Heap.h4
-rw-r--r--src/prop/minisat/mtl/Map.h4
-rw-r--r--src/prop/minisat/mtl/Queue.h4
-rw-r--r--src/prop/minisat/mtl/Sort.h4
-rw-r--r--src/prop/minisat/mtl/Vec.h4
-rw-r--r--src/prop/minisat/mtl/XAlloc.h4
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc10
-rw-r--r--src/prop/minisat/simp/SimpSolver.h14
-rw-r--r--src/prop/minisat/utils/Options.h4
-rw-r--r--src/prop/minisat/utils/ParseUtils.h4
18 files changed, 87 insertions, 87 deletions
diff --git a/src/prop/minisat/core/Dimacs.h b/src/prop/minisat/core/Dimacs.h
index b48044457..02182fde3 100644
--- a/src/prop/minisat/core/Dimacs.h
+++ b/src/prop/minisat/core/Dimacs.h
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/utils/ParseUtils.h"
#include "prop/minisat/core/SolverTypes.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -86,6 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 9dbcada15..cd3ae5edf 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -39,9 +39,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/mtl/Sort.h"
#include "prop/theory_proxy.h"
-using namespace CVC5::prop;
+using namespace cvc5::prop;
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
namespace {
@@ -83,7 +83,7 @@ static inline void dtviewPropagationHeaderHelper(size_t level)
// Writes to Trace macro for propagation tracing
static inline void dtviewBoolPropagationHelper(size_t level,
Lit& l,
- CVC5::prop::TheoryProxy* proxy)
+ cvc5::prop::TheoryProxy* proxy)
{
Trace("dtview::prop") << std::string(
level + 1 - (options::incrementalSolving() ? 1 : 0), ' ')
@@ -95,7 +95,7 @@ static inline void dtviewBoolPropagationHelper(size_t level,
// Writes to Trace macro for conflict tracing
static inline void dtviewPropConflictHelper(size_t level,
Clause& confl,
- CVC5::prop::TheoryProxy* proxy)
+ cvc5::prop::TheoryProxy* proxy)
{
Trace("dtview::conflict")
<< std::string(level + 1 - (options::incrementalSolving() ? 1 : 0), ' ')
@@ -148,9 +148,9 @@ class ScopedBool
//=================================================================================================
// Constructor/Destructor:
-Solver::Solver(CVC5::prop::TheoryProxy* proxy,
- CVC5::context::Context* context,
- CVC5::context::UserContext* userContext,
+Solver::Solver(cvc5::prop::TheoryProxy* proxy,
+ cvc5::context::Context* context,
+ cvc5::context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental)
: d_proxy(proxy),
@@ -548,7 +548,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
ProofManager::getCnfProof()->registerConvertedClause(id);
}
ProofManager::getSatProof()->finalizeProof(
- CVC5::Minisat::CRef_Lazy);
+ cvc5::Minisat::CRef_Lazy);
}
if (isProofEnabled())
{
@@ -648,7 +648,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
id = ProofManager::getSatProof()->storeUnitConflict(
ca[confl][0], LEARNT);
ProofManager::getSatProof()->finalizeProof(
- CVC5::Minisat::CRef_Lazy);
+ cvc5::Minisat::CRef_Lazy);
}
else
{
@@ -1030,7 +1030,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
Trace("pf::sat") << "\n";
}
- Trace("pf::sat") << CVC5::push;
+ Trace("pf::sat") << cvc5::push;
for (int j = (p == lit_Undef) ? 0 : 1, size = ca[confl].size();
j < size;
j++)
@@ -1073,7 +1073,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
}
}
}
- Trace("pf::sat") << CVC5::pop;
+ Trace("pf::sat") << cvc5::pop;
// Select next clause to look at:
while (!seen[var(trail[index--])]);
@@ -1326,7 +1326,7 @@ CRef Solver::propagate(TheoryCheckType type)
// theory propagation
if (type == CHECK_FINAL) {
// Do the theory check
- theoryCheck(CVC5::theory::Theory::EFFORT_FULL);
+ theoryCheck(cvc5::theory::Theory::EFFORT_FULL);
// Pick up the theory propagated literals (there could be some,
// if new lemmas are added)
propagateTheory();
@@ -1350,9 +1350,9 @@ CRef Solver::propagate(TheoryCheckType type)
if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) {
// Do the theory check
if (type == CHECK_FINAL_FAKE) {
- theoryCheck(CVC5::theory::Theory::EFFORT_FULL);
+ theoryCheck(cvc5::theory::Theory::EFFORT_FULL);
} else {
- theoryCheck(CVC5::theory::Theory::EFFORT_STANDARD);
+ theoryCheck(cvc5::theory::Theory::EFFORT_STANDARD);
}
// Pick up the theory propagated literals
propagateTheory();
@@ -1439,7 +1439,7 @@ void Solver::propagateTheory() {
|
| Note: the propagation queue might be NOT empty
|________________________________________________________________________________________________@*/
-void Solver::theoryCheck(CVC5::theory::Theory::Effort effort)
+void Solver::theoryCheck(cvc5::theory::Theory::Effort effort)
{
d_proxy->theoryCheck(effort);
}
@@ -2145,7 +2145,7 @@ void Solver::pop()
--assertionLevel;
Debug("minisat") << "in user pop, decreasing assertion level to "
<< assertionLevel << "\n"
- << CVC5::push;
+ << cvc5::push;
while (true) {
Debug("minisat") << "== unassigning " << trail.last() << std::endl;
Var x = var(trail.last());
@@ -2167,7 +2167,7 @@ void Solver::pop()
// Remove the clauses
removeClausesAboveLevel(clauses_persistent, assertionLevel);
removeClausesAboveLevel(clauses_removable, assertionLevel);
- Debug("minisat") << CVC5::pop;
+ Debug("minisat") << cvc5::pop;
// Pop the SAT context to notify everyone
d_context->pop(); // SAT context for CVC4
@@ -2347,7 +2347,7 @@ CRef Solver::updateLemmas() {
void ClauseAllocator::reloc(CRef& cr,
ClauseAllocator& to,
- CVC5::TSatProof<Solver>* proof)
+ cvc5::TSatProof<Solver>* proof)
{
Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
// FIXME what is this CRef_lazy
@@ -2398,4 +2398,4 @@ std::shared_ptr<ProofNode> Solver::getProof()
bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
} // namespace Minisat
-} // namespace CVC5
+} // namespace cvc5
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 53f7a828c..9da0e2f89 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -38,16 +38,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "theory/theory.h"
#include "util/resource_manager.h"
-namespace CVC5 {
+namespace cvc5 {
template <class Solver> class TSatProof;
namespace prop {
class PropEngine;
class TheoryProxy;
} // namespace prop
-} // namespace CVC5
+} // namespace cvc5
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -56,10 +56,10 @@ namespace Minisat {
class Solver {
/** The only two CVC4 entry points to the private solver data */
- friend class CVC5::prop::PropEngine;
- friend class CVC5::prop::TheoryProxy;
- friend class CVC5::prop::SatProofManager;
- friend class CVC5::TSatProof<Minisat::Solver>;
+ friend class cvc5::prop::PropEngine;
+ friend class cvc5::prop::TheoryProxy;
+ friend class cvc5::prop::SatProofManager;
+ friend class cvc5::TSatProof<Minisat::Solver>;
public:
static CRef TCRef_Undef;
@@ -73,10 +73,10 @@ class Solver {
protected:
/** The pointer to the proxy that provides interfaces to the SMT engine */
- CVC5::prop::TheoryProxy* d_proxy;
+ cvc5::prop::TheoryProxy* d_proxy;
/** The context from the SMT solver */
- CVC5::context::Context* d_context;
+ cvc5::context::Context* d_context;
/** The current assertion level (user) */
int assertionLevel;
@@ -88,7 +88,7 @@ class Solver {
Var varFalse;
/** The resolution proof manager */
- std::unique_ptr<CVC5::prop::SatProofManager> d_pfManager;
+ std::unique_ptr<cvc5::prop::SatProofManager> d_pfManager;
public:
/** Returns the current user assertion level */
@@ -105,7 +105,7 @@ class Solver {
vec<bool> lemmas_removable;
/** Nodes being converted to CNF */
- std::vector<CVC5::Node> lemmas_cnf_assertion;
+ std::vector<cvc5::Node> lemmas_cnf_assertion;
/** Do a another check if FULL_EFFORT was the last one */
bool recheck;
@@ -134,9 +134,9 @@ public:
// Constructor/Destructor:
//
- Solver(CVC5::prop::TheoryProxy* proxy,
- CVC5::context::Context* context,
- CVC5::context::UserContext* userContext,
+ Solver(cvc5::prop::TheoryProxy* proxy,
+ cvc5::context::Context* context,
+ cvc5::context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental = false);
virtual ~Solver();
@@ -153,7 +153,7 @@ public:
Var falseVar() const { return varFalse; }
/** Retrive the SAT proof manager */
- CVC5::prop::SatProofManager* getProofManager();
+ cvc5::prop::SatProofManager* getProofManager();
/** Retrive the refutation proof */
std::shared_ptr<ProofNode> getProof();
@@ -438,7 +438,7 @@ protected:
CRef propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause.
void propagateTheory (); // Perform Theory propagation.
void theoryCheck(
- CVC5::theory::Theory::Effort
+ cvc5::theory::Theory::Effort
effort); // Perform a theory satisfiability check. Adds lemmas.
CRef updateLemmas (); // Add the lemmas, backtraking if necessary and return a conflict if there is one
void cancelUntil (int level); // Backtrack until a certain level.
@@ -666,6 +666,6 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ ve
//=================================================================================================
} // namespace Minisat
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 4d9dd682d..c3f4279cb 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -31,15 +31,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/mtl/Map.h"
#include "prop/minisat/mtl/Vec.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
class Solver;
}
template <class Solver>
class TSatProof;
-} // namespace CVC5
+} // namespace cvc5
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -183,9 +183,9 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
}
} // namespace Minisat
-} // namespace CVC5
+} // namespace cvc5
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat{
//=================================================================================================
@@ -322,7 +322,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
void reloc(CRef& cr,
ClauseAllocator& to,
- CVC5::TSatProof<Solver>* proof = NULL);
+ cvc5::TSatProof<Solver>* proof = NULL);
// Implementation moved to Solver.cc.
};
@@ -500,6 +500,6 @@ inline void Clause::strengthen(Lit p)
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index e95677d57..07b345eda 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -25,7 +25,7 @@
#include "proof/sat_proof.h"
#include "util/statistics_registry.h"
-namespace CVC5 {
+namespace cvc5 {
namespace prop {
//// DPllMinisatSatSolver
@@ -301,20 +301,20 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
}
} // namespace prop
-} // namespace CVC5
+} // namespace cvc5
-namespace CVC5 {
+namespace cvc5 {
template <>
-prop::SatLiteral toSatLiteral<CVC5::Minisat::Solver>(Minisat::Solver::TLit lit)
+prop::SatLiteral toSatLiteral<cvc5::Minisat::Solver>(Minisat::Solver::TLit lit)
{
return prop::MinisatSatSolver::toSatLiteral(lit);
}
template <>
-void toSatClause<CVC5::Minisat::Solver>(
- const CVC5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
+void toSatClause<cvc5::Minisat::Solver>(
+ const cvc5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
{
prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
}
-} // namespace CVC5
+} // namespace cvc5
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 7dfeb6aa2..0a36b6297 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -20,7 +20,7 @@
#include "prop/minisat/simp/SimpSolver.h"
#include "util/statistics_registry.h"
-namespace CVC5 {
+namespace cvc5 {
namespace prop {
class MinisatSatSolver : public CDCLTSatSolverInterface
@@ -40,7 +40,7 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause);
void initialize(context::Context* context,
TheoryProxy* theoryProxy,
- CVC5::context::UserContext* userContext,
+ cvc5::context::UserContext* userContext,
ProofNodeManager* pnm) override;
ClauseId addClause(SatClause& clause, bool removable) override;
@@ -119,4 +119,4 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
}; /* class MinisatSatSolver */
} // namespace prop
-} // namespace CVC5
+} // namespace cvc5
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index 37bc4b7b6..69b782da9 100644
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "base/check.h"
#include "prop/minisat/mtl/Vec.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -82,6 +82,6 @@ static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true);
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
index 850aaeb73..f6e6d64b2 100644
--- a/src/prop/minisat/mtl/Alloc.h
+++ b/src/prop/minisat/mtl/Alloc.h
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/mtl/Vec.h"
#include "prop/minisat/mtl/XAlloc.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -149,6 +149,6 @@ RegionAllocator<T>::alloc(int size)
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index e2ad1513f..7a88c874d 100644
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "base/check.h"
#include "prop/minisat/mtl/Vec.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -156,6 +156,6 @@ class Heap {
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index 2efed4433..1c48f3962 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/mtl/IntTypes.h"
#include "prop/minisat/mtl/Vec.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -191,6 +191,6 @@ class Map {
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index ef30591bf..cdbc22600 100644
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "base/check.h"
#include "prop/minisat/mtl/Vec.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -86,6 +86,6 @@ public:
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index 7cf393847..2b9550d48 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
//=================================================================================================
// Some sorting algorithms for vec's
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
template<class T>
@@ -94,6 +94,6 @@ template <class T> void sort(vec<T>& v) {
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index e17e320d2..5410981f9 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/mtl/IntTypes.h"
#include "prop/minisat/mtl/XAlloc.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -147,6 +147,6 @@ void vec<T>::clear(bool dealloc) {
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h
index 6bd8c02e8..300dbb16b 100644
--- a/src/prop/minisat/mtl/XAlloc.h
+++ b/src/prop/minisat/mtl/XAlloc.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <errno.h>
#include <stdlib.h>
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -42,6 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size)
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 52162776b..e29c1032a 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -27,8 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/mtl/Sort.h"
#include "prop/minisat/utils/System.h"
-using namespace CVC5;
-using namespace CVC5::Minisat;
+using namespace cvc5;
+using namespace cvc5::Minisat;
//=================================================================================================
// Options:
@@ -48,9 +48,9 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
//=================================================================================================
// Constructor/Destructor:
-SimpSolver::SimpSolver(CVC5::prop::TheoryProxy* proxy,
- CVC5::context::Context* context,
- CVC5::context::UserContext* userContext,
+SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy,
+ cvc5::context::Context* context,
+ cvc5::context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental)
: Solver(proxy, context, userContext, pnm, enableIncremental),
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 6c8a87d5e..63a5a93fd 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -27,13 +27,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/core/Solver.h"
#include "prop/minisat/mtl/Queue.h"
-namespace CVC5 {
+namespace cvc5 {
namespace prop {
class TheoryProxy;
}
-} // namespace CVC5
+} // namespace cvc5
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//=================================================================================================
@@ -42,9 +42,9 @@ class SimpSolver : public Solver {
public:
// Constructor/Destructor:
//
- SimpSolver(CVC5::prop::TheoryProxy* proxy,
- CVC5::context::Context* context,
- CVC5::context::UserContext* userContext,
+ SimpSolver(cvc5::prop::TheoryProxy* proxy,
+ cvc5::context::Context* context,
+ cvc5::context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental = false);
~SimpSolver();
@@ -271,6 +271,6 @@ inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool t
//=================================================================================================
} // namespace Minisat
- } // namespace CVC5
+ } // namespace cvc5
#endif
diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h
index f37b6305e..22e4cd6ee 100644
--- a/src/prop/minisat/utils/Options.h
+++ b/src/prop/minisat/utils/Options.h
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "prop/minisat/mtl/Vec.h"
#include "prop/minisat/utils/ParseUtils.h"
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//==================================================================================================
@@ -432,6 +432,6 @@ class BoolOption : public Option
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
diff --git a/src/prop/minisat/utils/ParseUtils.h b/src/prop/minisat/utils/ParseUtils.h
index 27e454d00..ae8783e96 100644
--- a/src/prop/minisat/utils/ParseUtils.h
+++ b/src/prop/minisat/utils/ParseUtils.h
@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
//#include <zlib.h>
#include <unistd.h>
-namespace CVC5 {
+namespace cvc5 {
namespace Minisat {
//-------------------------------------------------------------------------------------------------
@@ -120,6 +120,6 @@ static bool eagerMatch(B& in, const char* str) {
//=================================================================================================
}
-} // namespace CVC5
+} // namespace cvc5
#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback