Rename namespace CVC4 to CVC5. (#6249)

21 files changed, 315 insertions, 267 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index e58060191..fb764631f 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -20,7 +20,7 @@
 #include "proof/clause_id.h"
 #include "util/statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
@@ -297,5 +297,5 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
   d_statEliminatedVars.set(minisat->eliminated_vars);
 }
 
-} /* namespace CVC4::prop */
-} /* namespace CVC4 */
+}  // namespace prop
+} // namespace CVC5
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index f91ed4d1d..2a099ad21 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -28,7 +28,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class BVMinisatSatSolver : public BVSatSolverInterface,
@@ -147,5 +147,5 @@ public:
   Statistics d_statistics;
 };
 
-} /* CVC4::prop namespace */
-} /* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC5
diff --git a/src/prop/bvminisat/core/Dimacs.h b/src/prop/bvminisat/core/Dimacs.h
index c94f473a9..be82fb557 100644
--- a/src/prop/bvminisat/core/Dimacs.h
+++ b/src/prop/bvminisat/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/bvminisat/core/SolverTypes.h"
 #include "prop/bvminisat/utils/ParseUtils.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -85,7 +85,7 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
     parse_DIMACS_main(in, S); }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 3b2b814cd..d7dc3f6d4 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -34,7 +34,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "theory/interrupted.h"
 #include "util/utility.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "
@@ -82,7 +82,7 @@ CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here
 //=================================================================================================
 // Constructor/Destructor:
 
-Solver::Solver(CVC4::context::Context* context)
+Solver::Solver(CVC5::context::Context* context)
     :
 
       // Parameters (user settable):
@@ -976,7 +976,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
         return l_False;
       }
 
-      if (!CVC4::options::bvEagerExplanations())
+      if (!CVC5::options::bvEagerExplanations())
       {
         // check if uip leads to a conflict
         if (backtrack_level < assumptions.size())
@@ -1028,7 +1028,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
         isWithinBudget =
             withinBudget(ResourceManager::Resource::BvSatConflictsStep);
       }
-      catch (const CVC4::theory::Interrupted& e)
+      catch (const CVC5::theory::Interrupted& e)
       {
         // do some clean-up and rethrow
         cancelUntil(assumptions.size());
@@ -1417,5 +1417,5 @@ bool Solver::withinBudget(ResourceManager::Resource r) const
           propagations < (uint64_t)propagation_budget);
 }
 
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 03c46985b..6386c33fa 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -33,7 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/utils/Options.h"
 #include "util/resource_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace BVMinisat {
 class Solver;
@@ -80,7 +80,7 @@ private:
     Notify* d_notify;
 
     /** Cvc4 context */
-    CVC4::context::Context* c;
+    CVC5::context::Context* c;
 
     /** True constant */
     Var varTrue;
@@ -92,138 +92,175 @@ public:
 
     // Constructor/Destructor:
     //
-    Solver(CVC4::context::Context* c);
-    virtual ~Solver();
-
-    void setNotify(Notify* toNotify);
-
-    // Problem specification:
-    //
-    Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
-    Var     trueVar() const { return varTrue; }
-    Var     falseVar() const { return varFalse; }
-
-    bool addClause(const vec<Lit>& ps,
-                   ClauseId& id);  // Add a clause to the solver.
-    bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
-    bool addClause(Lit p, ClauseId& id);  // Add a unit clause to the solver.
-    bool addClause(Lit p,
-                   Lit q,
-                   ClauseId& id);  // Add a binary clause to the solver.
-    bool addClause(Lit p,
-                   Lit q,
-                   Lit r,
-                   ClauseId& id);  // Add a ternary clause to the solver.
-    bool    addClause_(      vec<Lit>& ps, ClauseId& id);                     // Add a clause to the solver without making superflous internal copy. Will
-                                                                // change the passed vector 'ps'.
-
-    // Solving:
-    //
-    bool    simplify     ();                        // Removes already satisfied clauses.
-    lbool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
-    lbool   solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
-    lbool    solve        ();                        // Search without assumptions.
-    lbool    solve        (Lit p);                   // Search for a model that respects a single assumption.
-    lbool    solve        (Lit p, Lit q);            // Search for a model that respects two assumptions.
-    lbool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
-    bool    okay         () const;                  // FALSE means solver is in a conflicting state
-    lbool   assertAssumption(Lit p, bool propagate);  // Assert a new assumption, start BCP if propagate = true
-    lbool   propagateAssumptions();                   // Do BCP over asserted assumptions
-    void    popAssumption();                          // Pop an assumption
-
-    void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
-    void    toDimacs     (const char *file, const vec<Lit>& assumps);
-    void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);
-
-    // Convenience versions of 'toDimacs()':
-    void    toDimacs     (const char* file);
-    void    toDimacs     (const char* file, Lit p);
-    void    toDimacs     (const char* file, Lit p, Lit q);
-    void    toDimacs     (const char* file, Lit p, Lit q, Lit r);
-
-    // Variable mode:
-    //
-    void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
-    void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
-
-    // Read state:
-    //
-    lbool   value      (Var x) const;       // The current value of a variable.
-    lbool   value      (Lit p) const;       // The current value of a literal.
-    lbool   modelValue (Var x) const;       // The value of a variable in the last model. The last call to solve must have been satisfiable.
-    lbool   modelValue (Lit p) const;       // The value of a literal in the last model. The last call to solve must have been satisfiable.
-    int     nAssigns   ()      const;       // The current number of assigned literals.
-    int     nClauses   ()      const;       // The current number of original clauses.
-    int     nLearnts   ()      const;       // The current number of learnt clauses.
-    int     nVars      ()      const;       // The current number of variables.
-    int     nFreeVars  ()      const;
-
-    // Resource contraints:
-    //
-    void    setConfBudget(int64_t x);
-    void    setPropBudget(int64_t x);
-    void    budgetOff();
-    void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
-    void    clearInterrupt();     // Clear interrupt indicator flag.
-
-    // Memory managment:
-    //
-    virtual void garbageCollect();
-    void    checkGarbage(double gf);
-    void    checkGarbage();
-
-    // Extra results: (read-only member variable)
-    //
-    vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
-    vec<Lit>   conflict;          // If problem is unsatisfiable (possibly under assumptions),
-                                  // this vector represent the final conflict clause expressed in the assumptions.
-
-    // Mode of operation:
-    //
-    int       verbosity;
-    double    var_decay;
-    double    clause_decay;
-    double    random_var_freq;
-    double    random_seed;
-    bool      luby_restart;
-    int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
-    int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).
-    bool      rnd_pol;            // Use random polarities for branching heuristics.
-    bool      rnd_init_act;       // Initialize variable activities with a small random value.
-    double    garbage_frac;       // The fraction of wasted memory allowed before a garbage collection is triggered.
-
-    int       restart_first;      // The initial restart limit.                                                                (default 100)
-    double    restart_inc;        // The factor with which the restart limit is multiplied in each restart.                    (default 1.5)
-    double    learntsize_factor;  // The intitial limit for learnt clauses is a factor of the original clauses.                (default 1 / 3)
-    double    learntsize_inc;     // The limit for learnt clauses is multiplied with this factor each restart.                 (default 1.1)
-
-    int       learntsize_adjust_start_confl;
-    double    learntsize_adjust_inc;
-
-    // Statistics: (read-only member variable)
-    //
-    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
-    uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
-
-    // Bitvector Propagations
-    //
-
-    void addMarkerLiteral(Var var);
-
-    bool need_to_propagate;  // true if we added new clauses, set to true in
-                             // propagation
-    bool only_bcp;                      // solving mode in which only boolean constraint propagation is done
-    void setOnlyBCP (bool val) { only_bcp = val;}
-    void explain(Lit l, std::vector<Lit>& explanation);
-
-   protected:
-
-    // has a clause been added
-    bool                clause_added;
-
-    // Helper structures:
-    //
-    struct VarData { CRef reason; int level; };
+ Solver(CVC5::context::Context* c);
+ virtual ~Solver();
+
+ void setNotify(Notify* toNotify);
+
+ // Problem specification:
+ //
+ Var newVar(bool polarity = true,
+            bool dvar = true);  // Add a new variable with parameters specifying
+                                // variable mode.
+ Var trueVar() const { return varTrue; }
+ Var falseVar() const { return varFalse; }
+
+ bool addClause(const vec<Lit>& ps,
+                ClauseId& id);  // Add a clause to the solver.
+ bool addEmptyClause();         // Add the empty clause, making the solver
+                                // contradictory.
+ bool addClause(Lit p, ClauseId& id);  // Add a unit clause to the solver.
+ bool addClause(Lit p,
+                Lit q,
+                ClauseId& id);  // Add a binary clause to the solver.
+ bool addClause(Lit p,
+                Lit q,
+                Lit r,
+                ClauseId& id);  // Add a ternary clause to the solver.
+ bool addClause_(
+     vec<Lit>& ps,
+     ClauseId& id);  // Add a clause to the solver without making superflous
+                     // internal copy. Will change the passed vector 'ps'.
+
+ // Solving:
+ //
+ bool simplify();                       // Removes already satisfied clauses.
+ lbool solve(const vec<Lit>& assumps);  // Search for a model that respects a
+                                        // given set of assumptions.
+ lbool solveLimited(
+     const vec<Lit>& assumps);  // Search for a model that respects a given set
+                                // of assumptions (With resource constraints).
+ lbool solve();                 // Search without assumptions.
+ lbool solve(Lit p);  // Search for a model that respects a single assumption.
+ lbool solve(Lit p,
+             Lit q);  // Search for a model that respects two assumptions.
+ lbool solve(Lit p,
+             Lit q,
+             Lit r);  // Search for a model that respects three assumptions.
+ bool okay() const;   // FALSE means solver is in a conflicting state
+ lbool assertAssumption(
+     Lit p,
+     bool propagate);  // Assert a new assumption, start BCP if propagate = true
+ lbool propagateAssumptions();  // Do BCP over asserted assumptions
+ void popAssumption();          // Pop an assumption
+
+ void toDimacs(FILE* f,
+               const vec<Lit>& assumps);  // Write CNF to file in DIMACS-format.
+ void toDimacs(const char* file, const vec<Lit>& assumps);
+ void toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max);
+
+ // Convenience versions of 'toDimacs()':
+ void toDimacs(const char* file);
+ void toDimacs(const char* file, Lit p);
+ void toDimacs(const char* file, Lit p, Lit q);
+ void toDimacs(const char* file, Lit p, Lit q, Lit r);
+
+ // Variable mode:
+ //
+ void setPolarity(
+     Var v, bool b);  // Declare which polarity the decision heuristic should
+                      // use for a variable. Requires mode 'polarity_user'.
+ void setDecisionVar(Var v,
+                     bool b);  // Declare if a variable should be eligible for
+                               // selection in the decision heuristic.
+
+ // Read state:
+ //
+ lbool value(Var x) const;  // The current value of a variable.
+ lbool value(Lit p) const;  // The current value of a literal.
+ lbool modelValue(
+     Var x) const;  // The value of a variable in the last model. The last call
+                    // to solve must have been satisfiable.
+ lbool modelValue(
+     Lit p) const;  // The value of a literal in the last model. The last call
+                    // to solve must have been satisfiable.
+ int nAssigns() const;  // The current number of assigned literals.
+ int nClauses() const;  // The current number of original clauses.
+ int nLearnts() const;  // The current number of learnt clauses.
+ int nVars() const;     // The current number of variables.
+ int nFreeVars() const;
+
+ // Resource contraints:
+ //
+ void setConfBudget(int64_t x);
+ void setPropBudget(int64_t x);
+ void budgetOff();
+ void interrupt();  // Trigger a (potentially asynchronous) interruption of the
+                    // solver.
+ void clearInterrupt();  // Clear interrupt indicator flag.
+
+ // Memory managment:
+ //
+ virtual void garbageCollect();
+ void checkGarbage(double gf);
+ void checkGarbage();
+
+ // Extra results: (read-only member variable)
+ //
+ vec<lbool> model;  // If problem is satisfiable, this vector contains the model
+                    // (if any).
+ vec<Lit> conflict;  // If problem is unsatisfiable (possibly under
+                     // assumptions), this vector represent the final conflict
+                     // clause expressed in the assumptions.
+
+ // Mode of operation:
+ //
+ int verbosity;
+ double var_decay;
+ double clause_decay;
+ double random_var_freq;
+ double random_seed;
+ bool luby_restart;
+ int ccmin_mode;    // Controls conflict clause minimization (0=none, 1=basic,
+                    // 2=deep).
+ int phase_saving;  // Controls the level of phase saving (0=none, 1=limited,
+                    // 2=full).
+ bool rnd_pol;      // Use random polarities for branching heuristics.
+ bool
+     rnd_init_act;  // Initialize variable activities with a small random value.
+ double garbage_frac;  // The fraction of wasted memory allowed before a garbage
+                       // collection is triggered.
+
+ int restart_first;   // The initial restart limit. (default 100)
+ double restart_inc;  // The factor with which the restart limit is multiplied
+                      // in each restart.                    (default 1.5)
+ double
+     learntsize_factor;  // The intitial limit for learnt clauses is a factor of
+                         // the original clauses.                (default 1 / 3)
+ double learntsize_inc;  // The limit for learnt clauses is multiplied with this
+                         // factor each restart.                 (default 1.1)
+
+ int learntsize_adjust_start_confl;
+ double learntsize_adjust_inc;
+
+ // Statistics: (read-only member variable)
+ //
+ uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
+ uint64_t dec_vars, clauses_literals, learnts_literals, max_literals,
+     tot_literals;
+
+ // Bitvector Propagations
+ //
+
+ void addMarkerLiteral(Var var);
+
+ bool need_to_propagate;  // true if we added new clauses, set to true in
+                          // propagation
+ bool only_bcp;  // solving mode in which only boolean constraint propagation is
+                 // done
+ void setOnlyBCP(bool val) { only_bcp = val; }
+ void explain(Lit l, std::vector<Lit>& explanation);
+
+protected:
+ // has a clause been added
+ bool clause_added;
+
+ // Helper structures:
+ //
+ struct VarData
+ {
+   CRef reason;
+   int level; };
     static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
 
     struct Watcher {
@@ -496,8 +533,7 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
-
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index 776052848..96022efbf 100644
--- a/src/prop/bvminisat/core/SolverTypes.h
+++ b/src/prop/bvminisat/core/SolverTypes.h
@@ -28,15 +28,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Map.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 class Solver;
 }
 template <class Solver>
 class TSatProof;
-}
+}  // namespace CVC5
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace BVMinisat {
 
@@ -429,7 +429,7 @@ inline void Clause::strengthen(Lit p)
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Alg.h b/src/prop/bvminisat/mtl/Alg.h
index 5918b2f4c..0b173eb08 100644
--- a/src/prop/bvminisat/mtl/Alg.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -81,7 +81,7 @@ template<class T>
 static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Alloc.h b/src/prop/bvminisat/mtl/Alloc.h
index 8a03caa69..582db74f1 100644
--- a/src/prop/bvminisat/mtl/Alloc.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/mtl/XAlloc.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -148,7 +148,7 @@ RegionAllocator<T>::alloc(int size)
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Heap.h b/src/prop/bvminisat/mtl/Heap.h
index 38b47bc7f..7b04a5091 100644
--- a/src/prop/bvminisat/mtl/Heap.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -155,8 +155,7 @@ class Heap {
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
-
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h
index 919149fa9..fd64fc751 100644
--- a/src/prop/bvminisat/mtl/Map.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/IntTypes.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -190,7 +190,7 @@ class Map {
 };
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Queue.h b/src/prop/bvminisat/mtl/Queue.h
index 1120188f8..a72660337 100644
--- a/src/prop/bvminisat/mtl/Queue.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -85,7 +85,7 @@ public:
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Sort.h b/src/prop/bvminisat/mtl/Sort.h
index f4a10aabb..1cfa220ab 100644
--- a/src/prop/bvminisat/mtl/Sort.h
+++ b/src/prop/bvminisat/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 BVMinisat {
 
 template<class T>
@@ -94,7 +93,7 @@ template <class T> void sort(vec<T>& v) {
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Vec.h b/src/prop/bvminisat/mtl/Vec.h
index a6e3bca4b..c918fc4a0 100644
--- a/src/prop/bvminisat/mtl/Vec.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/IntTypes.h"
 #include "prop/bvminisat/mtl/XAlloc.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -146,7 +146,7 @@ void vec<T>::clear(bool dealloc) {
         if (dealloc) free(data), data = NULL, cap = 0; } }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/XAlloc.h b/src/prop/bvminisat/mtl/XAlloc.h
index 9e469a6fb..1500114a2 100644
--- a/src/prop/bvminisat/mtl/XAlloc.h
+++ b/src/prop/bvminisat/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 BVMinisat {
 
 //=================================================================================================
@@ -41,8 +41,7 @@ static inline void* xrealloc(void *ptr, size_t size)
 }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
-
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 10f0aa03e..b4f9bd354 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Sort.h"
 #include "prop/bvminisat/utils/System.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -48,7 +48,7 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 //=================================================================================================
 // Constructor/Destructor:
 
-SimpSolver::SimpSolver(CVC4::context::Context* context)
+SimpSolver::SimpSolver(CVC5::context::Context* context)
     : Solver(context),
       grow(opt_grow),
       clause_lim(opt_clause_lim),
@@ -57,9 +57,9 @@ SimpSolver::SimpSolver(CVC4::context::Context* context)
       use_asymm(opt_use_asymm),
       use_rcheck(opt_use_rcheck),
       use_elim(opt_use_elim
-               && CVC4::options::bitblastMode()
-                      == CVC4::options::BitblastMode::EAGER
-               && !CVC4::options::produceModels()),
+               && CVC5::options::bitblastMode()
+                      == CVC5::options::BitblastMode::EAGER
+               && !CVC5::options::produceModels()),
       merges(0),
       asymm_lits(0),
       eliminated_vars(0),
@@ -94,7 +94,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* context)
 
 SimpSolver::~SimpSolver()
 {
-  //  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time);
+  //  CVC5::StatisticsRegistry::unregisterStat(&total_eliminate_time);
 }
 
 
@@ -644,64 +644,77 @@ void SimpSolver::extendModel()
 
 bool SimpSolver::eliminate(bool turn_off_elim)
 {
+  //  CVC5::TimerStat::CodeTimer codeTimer(total_eliminate_time);
 
-  //  CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time);
-
-    if (!simplify())
-        return false;
-    else if (!use_simplification)
-        return true;
-
-    // Main simplification loop:
-    //
-    while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
+  if (!simplify())
+    return false;
+  else if (!use_simplification)
+    return true;
 
-        gatherTouchedClauses();
-        // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
-        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
-            && !backwardSubsumptionCheck(true))
-        {
-          ok = false;
-          goto cleanup;
-        }
+  // Main simplification loop:
+  //
+  while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)
+  {
+    gatherTouchedClauses();
+    // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n",
+    // cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
+    if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
+        && !backwardSubsumptionCheck(true))
+    {
+      ok = false;
+      goto cleanup;
+    }
 
-        // Empty elim_heap and return immediately on user-interrupt:
-        if (asynch_interrupt){
-          Assert(bwdsub_assigns == trail.size());
-          Assert(subsumption_queue.size() == 0);
-          Assert(n_touched == 0);
-          elim_heap.clear();
-          goto cleanup;
-        }
+    // Empty elim_heap and return immediately on user-interrupt:
+    if (asynch_interrupt)
+    {
+      Assert(bwdsub_assigns == trail.size());
+      Assert(subsumption_queue.size() == 0);
+      Assert(n_touched == 0);
+      elim_heap.clear();
+      goto cleanup;
+    }
 
-        // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
-        for (int cnt = 0; !elim_heap.empty(); cnt++){
-            Var elim = elim_heap.removeMin();
+    // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(),
+    // elim_heap.size());
+    for (int cnt = 0; !elim_heap.empty(); cnt++)
+    {
+      Var elim = elim_heap.removeMin();
 
-            if (asynch_interrupt) break;
+      if (asynch_interrupt) break;
 
-            if (isEliminated(elim) || value(elim) != l_Undef) continue;
+      if (isEliminated(elim) || value(elim) != l_Undef) continue;
 
-            if (verbosity >= 2 && cnt % 100 == 0)
-                printf("elimination left: %10d\r", elim_heap.size());
+      if (verbosity >= 2 && cnt % 100 == 0)
+        printf("elimination left: %10d\r", elim_heap.size());
 
-            if (use_asymm){
-                // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
-                bool was_frozen = frozen[elim];
-                frozen[elim] = true;
-                if (!asymmVar(elim)){
-                    ok = false; goto cleanup; }
-                frozen[elim] = was_frozen; }
+      if (use_asymm)
+      {
+        // Temporarily freeze variable. Otherwise, it would immediately end up
+        // on the queue again:
+        bool was_frozen = frozen[elim];
+        frozen[elim] = true;
+        if (!asymmVar(elim))
+        {
+          ok = false;
+          goto cleanup;
+        }
+        frozen[elim] = was_frozen;
+      }
 
-            // At this point, the variable may have been set by assymetric branching, so check it
-            // again. Also, don't eliminate frozen variables:
-            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
-                ok = false; goto cleanup; }
+      // At this point, the variable may have been set by assymetric branching,
+      // so check it again. Also, don't eliminate frozen variables:
+      if (use_elim && value(elim) == l_Undef && !frozen[elim]
+          && !eliminateVar(elim))
+      {
+        ok = false;
+        goto cleanup;
+      }
 
-            checkGarbage(simp_garbage_frac);
-        }
+      checkGarbage(simp_garbage_frac);
+    }
 
-        Assert(subsumption_queue.size() == 0);
+    Assert(subsumption_queue.size() == 0);
     }
  cleanup:
 
@@ -795,5 +808,5 @@ void SimpSolver::garbageCollect()
     to.moveTo(ca);
 }
 
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index bf23a7dff..6afdc6ba7 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/core/Solver.h"
 #include "prop/bvminisat/mtl/Queue.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace context {
 class Context;
@@ -41,7 +41,7 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-  SimpSolver(CVC4::context::Context* context);
+  SimpSolver(CVC5::context::Context* context);
   ~SimpSolver();
 
   // Problem specification:
@@ -115,9 +115,9 @@ class SimpSolver : public Solver {
     int     merges;
     int     asymm_lits;
     int     eliminated_vars;
-  //    CVC4::TimerStat total_eliminate_time;
+    //    CVC5::TimerStat total_eliminate_time;
 
- protected:
+   protected:
 
     // Helper structures:
     //
@@ -237,8 +237,7 @@ inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){
     return solve_(do_simp, turn_off_simp); }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
-
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/utils/Options.cc b/src/prop/bvminisat/utils/Options.cc
index ac0964623..44c642441 100644
--- a/src/prop/bvminisat/utils/Options.cc
+++ b/src/prop/bvminisat/utils/Options.cc
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Sort.h"
 #include "prop/bvminisat/utils/ParseUtils.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 void BVMinisat::parseOptions(int& argc, char** argv, bool strict)
@@ -90,6 +90,5 @@ void BVMinisat::printUsageAndExit (int argc, char** argv, bool verbose)
     exit(0);
 }
 
-
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
diff --git a/src/prop/bvminisat/utils/Options.h b/src/prop/bvminisat/utils/Options.h
index 698035b7c..e7b6942bd 100644
--- a/src/prop/bvminisat/utils/Options.h
+++ b/src/prop/bvminisat/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/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/utils/ParseUtils.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //==================================================================================================
@@ -431,7 +431,7 @@ class BoolOption : public Option
 };
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/utils/ParseUtils.h b/src/prop/bvminisat/utils/ParseUtils.h
index 46f404c3e..a748651db 100644
--- a/src/prop/bvminisat/utils/ParseUtils.h
+++ b/src/prop/bvminisat/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 BVMinisat {
 
 //-------------------------------------------------------------------------------------------------
@@ -119,7 +119,7 @@ static bool eagerMatch(B& in, const char* str) {
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/utils/System.cc b/src/prop/bvminisat/utils/System.cc
index aba0a5ac5..9b9f99eb5 100644
--- a/src/prop/bvminisat/utils/System.cc
+++ b/src/prop/bvminisat/utils/System.cc
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdio.h>
 #include <stdlib.h>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
@@ -95,6 +95,5 @@ double BVMinisat::memUsed() {
     return 0; }
 #endif
 
-
-} /* CVC4::BVMinisat namespace */
+} /* CVC5::BVMinisat namespace */
 } /* CVC4 namespace */
diff --git a/src/prop/bvminisat/utils/System.h b/src/prop/bvminisat/utils/System.h
index 6a887bdb0..117fbfa3d 100644
--- a/src/prop/bvminisat/utils/System.h
+++ b/src/prop/bvminisat/utils/System.h
@@ -29,15 +29,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 //-------------------------------------------------------------------------------------------------
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 static inline double cpuTime(void); // CPU-time in seconds.
 extern double memUsed();            // Memory in mega bytes (returns 0 for unsupported architectures).
 extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for unsupported architectures).
 
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 //-------------------------------------------------------------------------------------------------
 // Implementation of inline functions:
@@ -45,17 +45,22 @@ extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for
 #if defined(_MSC_VER) || defined(__MINGW32__)
 #include <time.h>
 
-static inline double CVC4::BVMinisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
+static inline double CVC5::BVMinisat::cpuTime(void)
+{
+  return (double)clock() / CLOCKS_PER_SEC;
+}
 
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
 
-static inline double CVC4::BVMinisat::cpuTime(void) {
-    struct rusage ru;
-    getrusage(RUSAGE_SELF, &ru);
-    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+static inline double CVC5::BVMinisat::cpuTime(void)
+{
+  struct rusage ru;
+  getrusage(RUSAGE_SELF, &ru);
+  return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
+}
 
 #endif