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.cc40
-rw-r--r--src/prop/minisat/core/Solver.h43
-rw-r--r--src/prop/minisat/core/SolverTypes.h17
-rw-r--r--src/prop/minisat/minisat.cpp23
-rw-r--r--src/prop/minisat/minisat.h8
-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.h5
-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.h16
-rw-r--r--src/prop/minisat/utils/Options.h4
-rw-r--r--src/prop/minisat/utils/ParseUtils.h4
18 files changed, 101 insertions, 101 deletions
diff --git a/src/prop/minisat/core/Dimacs.h b/src/prop/minisat/core/Dimacs.h
index e4728f6b6..b48044457 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -86,6 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 8c27e2bdd..9dbcada15 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 CVC4::prop;
+using namespace CVC5::prop;
-namespace CVC4 {
+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,
- CVC4::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,
- CVC4::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(CVC4::prop::TheoryProxy* proxy,
- CVC4::context::Context* context,
- CVC4::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(
- CVC4::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(
- CVC4::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") << CVC4::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") << CVC4::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(CVC4::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(CVC4::theory::Theory::EFFORT_FULL);
+ theoryCheck(CVC5::theory::Theory::EFFORT_FULL);
} else {
- theoryCheck(CVC4::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(CVC4::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"
- << CVC4::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") << CVC4::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,
- CVC4::TSatProof<Solver>* proof)
+ CVC5::TSatProof<Solver>* proof)
{
Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
// FIXME what is this CRef_lazy
@@ -2397,5 +2397,5 @@ std::shared_ptr<ProofNode> Solver::getProof()
bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
-} /* CVC4::Minisat namespace */
-} /* CVC4 namespace */
+} // namespace Minisat
+} // namespace CVC5
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index df2f9b967..53f7a828c 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -38,17 +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 CVC4 {
+namespace CVC5 {
template <class Solver> class TSatProof;
namespace prop {
class PropEngine;
class TheoryProxy;
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+} // namespace prop
+} // namespace CVC5
-
-namespace CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -57,12 +56,12 @@ namespace Minisat {
class Solver {
/** The only two CVC4 entry points to the private solver data */
- friend class CVC4::prop::PropEngine;
- friend class CVC4::prop::TheoryProxy;
- friend class CVC4::prop::SatProofManager;
- friend class CVC4::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:
+ public:
static CRef TCRef_Undef;
static CRef TCRef_Lazy;
@@ -74,10 +73,10 @@ public:
protected:
/** The pointer to the proxy that provides interfaces to the SMT engine */
- CVC4::prop::TheoryProxy* d_proxy;
+ CVC5::prop::TheoryProxy* d_proxy;
/** The context from the SMT solver */
- CVC4::context::Context* d_context;
+ CVC5::context::Context* d_context;
/** The current assertion level (user) */
int assertionLevel;
@@ -89,7 +88,7 @@ public:
Var varFalse;
/** The resolution proof manager */
- std::unique_ptr<CVC4::prop::SatProofManager> d_pfManager;
+ std::unique_ptr<CVC5::prop::SatProofManager> d_pfManager;
public:
/** Returns the current user assertion level */
@@ -106,7 +105,7 @@ public:
vec<bool> lemmas_removable;
/** Nodes being converted to CNF */
- std::vector<CVC4::Node> lemmas_cnf_assertion;
+ std::vector<CVC5::Node> lemmas_cnf_assertion;
/** Do a another check if FULL_EFFORT was the last one */
bool recheck;
@@ -135,9 +134,9 @@ public:
// Constructor/Destructor:
//
- Solver(CVC4::prop::TheoryProxy* proxy,
- CVC4::context::Context* context,
- CVC4::context::UserContext* userContext,
+ Solver(CVC5::prop::TheoryProxy* proxy,
+ CVC5::context::Context* context,
+ CVC5::context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental = false);
virtual ~Solver();
@@ -154,7 +153,7 @@ public:
Var falseVar() const { return varFalse; }
/** Retrive the SAT proof manager */
- CVC4::prop::SatProofManager* getProofManager();
+ CVC5::prop::SatProofManager* getProofManager();
/** Retrive the refutation proof */
std::shared_ptr<ProofNode> getProof();
@@ -438,7 +437,9 @@ protected:
CRef propagate (TheoryCheckType type); // Perform Boolean and Theory. Returns possibly conflicting clause.
CRef propagateBool (); // Perform Boolean propagation. Returns possibly conflicting clause.
void propagateTheory (); // Perform Theory propagation.
- void theoryCheck (CVC4::theory::Theory::Effort effort); // Perform a theory satisfiability check. Adds lemmas.
+ void theoryCheck(
+ 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.
int analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
@@ -664,7 +665,7 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ ve
//=================================================================================================
-} /* CVC4::Minisat namespace */
-} /* CVC4 namespace */
+} // namespace Minisat
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index f2d2860c8..4d9dd682d 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
class Solver;
}
template <class Solver>
class TSatProof;
-} // namespace CVC4
+} // namespace CVC5
-namespace CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -182,11 +182,10 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
return out;
}
-} /* namespace CVC4::Minisat */
-} /* namespace CVC4 */
+} // namespace Minisat
+} // namespace CVC5
-
-namespace CVC4 {
+namespace CVC5 {
namespace Minisat{
//=================================================================================================
@@ -323,7 +322,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
void reloc(CRef& cr,
ClauseAllocator& to,
- CVC4::TSatProof<Solver>* proof = NULL);
+ CVC5::TSatProof<Solver>* proof = NULL);
// Implementation moved to Solver.cc.
};
@@ -501,6 +500,6 @@ inline void Clause::strengthen(Lit p)
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 694c73e5e..e95677d57 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 CVC4 {
+namespace CVC5 {
namespace prop {
//// DPllMinisatSatSolver
@@ -300,20 +300,21 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
d_statTotLiterals.set(minisat->tot_literals);
}
-} /* namespace CVC4::prop */
-} /* namespace CVC4 */
+} // namespace prop
+} // namespace CVC5
-
-namespace CVC4 {
-template<>
-prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
+namespace CVC5 {
+template <>
+prop::SatLiteral toSatLiteral<CVC5::Minisat::Solver>(Minisat::Solver::TLit lit)
+{
return prop::MinisatSatSolver::toSatLiteral(lit);
}
-template<>
-void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
- prop::SatClause& sat_cl) {
+template <>
+void toSatClause<CVC5::Minisat::Solver>(
+ const CVC5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
+{
prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
}
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 472ded34e..7dfeb6aa2 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 CVC4 {
+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,
- CVC4::context::UserContext* userContext,
+ CVC5::context::UserContext* userContext,
ProofNodeManager* pnm) override;
ClauseId addClause(SatClause& clause, bool removable) override;
@@ -118,5 +118,5 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
}; /* class MinisatSatSolver */
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+} // namespace prop
+} // namespace CVC5
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index 2f8a86c3b..37bc4b7b6 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 CVC4 {
+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
#endif
diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
index 98e59e7bf..850aaeb73 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -149,6 +149,6 @@ RegionAllocator<T>::alloc(int size)
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index 1e64f6ba5..e2ad1513f 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -156,6 +156,6 @@ class Heap {
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index bf299d55d..2efed4433 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -191,6 +191,6 @@ class Map {
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index 242bc9388..ef30591bf 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -86,6 +86,6 @@ public:
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index 2c3454aa3..7cf393847 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -26,8 +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 CVC4 {
+namespace CVC5 {
namespace Minisat {
template<class T>
@@ -95,6 +94,6 @@ template <class T> void sort(vec<T>& v) {
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index 08e40e8bc..e17e320d2 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -147,6 +147,6 @@ void vec<T>::clear(bool dealloc) {
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h
index f1221f94f..6bd8c02e8 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -42,6 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size)
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 7051134eb..52162776b 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 CVC4;
-using namespace CVC4::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(CVC4::prop::TheoryProxy* proxy,
- CVC4::context::Context* context,
- CVC4::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 f553746e6..6c8a87d5e 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 CVC4 {
+namespace CVC5 {
namespace prop {
class TheoryProxy;
}
-}
+} // namespace CVC5
-namespace CVC4 {
+namespace CVC5 {
namespace Minisat {
//=================================================================================================
@@ -42,9 +42,9 @@ class SimpSolver : public Solver {
public:
// Constructor/Destructor:
//
- SimpSolver(CVC4::prop::TheoryProxy* proxy,
- CVC4::context::Context* context,
- CVC4::context::UserContext* userContext,
+ SimpSolver(CVC5::prop::TheoryProxy* proxy,
+ CVC5::context::Context* context,
+ CVC5::context::UserContext* userContext,
ProofNodeManager* pnm,
bool enableIncremental = false);
~SimpSolver();
@@ -270,7 +270,7 @@ inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool t
}
//=================================================================================================
-} /* CVC4::Minisat namespace */
-} /* CVC4 namespace */
+ } // namespace Minisat
+ } // namespace CVC5
#endif
diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h
index 9bddd2b23..f37b6305e 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//==================================================================================================
@@ -432,6 +432,6 @@ class BoolOption : public Option
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
diff --git a/src/prop/minisat/utils/ParseUtils.h b/src/prop/minisat/utils/ParseUtils.h
index 128205967..27e454d00 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 CVC4 {
+namespace CVC5 {
namespace Minisat {
//-------------------------------------------------------------------------------------------------
@@ -120,6 +120,6 @@ static bool eagerMatch(B& in, const char* str) {
//=================================================================================================
}
-}
+} // namespace CVC5
#endif
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback