diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/prop | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/prop')
69 files changed, 482 insertions, 434 deletions
diff --git a/src/prop/README.minisat b/src/prop/README.minisat index 2f1d8bb47..081e79191 100644 --- a/src/prop/README.minisat +++ b/src/prop/README.minisat @@ -4,7 +4,7 @@ This is MiniSAT 2.2.0, downloaded from here: on 11 July 2010. -The code has been modified to put everything in the CVC4::MiniSat +The code has been modified to put everything in the CVC5::MiniSat namespace. The build process has been modified. Other parts have been modified to serve CVC4's purposes. diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h index 9a303a514..1645a096a 100644 --- a/src/prop/bv_sat_solver_notify.h +++ b/src/prop/bv_sat_solver_notify.h @@ -21,7 +21,7 @@ #include "prop/sat_solver_types.h" #include "util/resource_manager.h" -namespace CVC4 { +namespace CVC5 { namespace prop { class BVSatSolverNotify { @@ -45,6 +45,6 @@ public: };/* class BVSatSolverInterface::Notify */ } -} +} // namespace CVC5 #endif 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 diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp index 6020efad1..9bad7072a 100644 --- a/src/prop/cadical.cpp +++ b/src/prop/cadical.cpp @@ -20,7 +20,7 @@ #include "base/check.h" -namespace CVC4 { +namespace CVC5 { namespace prop { using CadicalLit = int; @@ -200,6 +200,6 @@ CadicalSolver::Statistics::~Statistics() { } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif // CVC4_USE_CADICAL diff --git a/src/prop/cadical.h b/src/prop/cadical.h index dfd761e2e..c49aa8d03 100644 --- a/src/prop/cadical.h +++ b/src/prop/cadical.h @@ -26,7 +26,7 @@ #include <cadical.hpp> -namespace CVC4 { +namespace CVC5 { namespace prop { class CadicalSolver : public SatSolver @@ -103,7 +103,7 @@ class CadicalSolver : public SatSolver }; } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif // CVC4_USE_CADICAL #endif // CVC4__PROP__CADICAL_H diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 8cd4da505..bd23bad94 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -37,7 +37,7 @@ #include "theory/theory.h" #include "theory/theory_engine.h" -namespace CVC4 { +namespace CVC5 { namespace prop { CnfStream::CnfStream(SatSolver* satSolver, @@ -787,5 +787,5 @@ void CnfStream::convertAndAssert(TNode node, bool negated) } } -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ +} // namespace prop +} // namespace CVC5 diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 1a900a524..af86da746 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -34,7 +34,7 @@ #include "prop/registrar.h" #include "prop/sat_solver_types.h" -namespace CVC4 { +namespace CVC5 { class OutputManager; @@ -318,6 +318,6 @@ class CnfStream { }; /* class CnfStream */ } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__PROP__CNF_STREAM_H */ diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index d81429d44..91fc12c6c 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -22,7 +22,7 @@ #include <cryptominisat5/cryptominisat.h> -namespace CVC4 { +namespace CVC5 { namespace prop { using CMSatVar = unsigned; @@ -244,5 +244,5 @@ CryptoMinisatSolver::Statistics::~Statistics() { } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index 3bb443cfc..fb118619c 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -33,7 +33,7 @@ namespace CMSat { class SATSolver; } -namespace CVC4 { +namespace CVC5 { namespace prop { class CryptoMinisatSolver : public SatSolver @@ -106,7 +106,7 @@ class CryptoMinisatSolver : public SatSolver }; } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif // CVC4_USE_CRYPTOMINISAT #endif // CVC4__PROP__CRYPTOMINISAT_H diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp index 7ff6d76ee..ccca3a3b4 100644 --- a/src/prop/kissat.cpp +++ b/src/prop/kissat.cpp @@ -20,7 +20,7 @@ #include "base/check.h" -namespace CVC4 { +namespace CVC5 { namespace prop { using KissatLit = int32_t; @@ -173,6 +173,6 @@ KissatSolver::Statistics::~Statistics() } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif // CVC4_USE_KISSAT diff --git a/src/prop/kissat.h b/src/prop/kissat.h index 65088e39e..7bfcbac68 100644 --- a/src/prop/kissat.h +++ b/src/prop/kissat.h @@ -28,7 +28,7 @@ extern "C" { #include <kissat/kissat.h> } -namespace CVC4 { +namespace CVC5 { namespace prop { class KissatSolver : public SatSolver @@ -97,7 +97,7 @@ class KissatSolver : public SatSolver }; } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif // CVC4_USE_KISSAT #endif // CVC4__PROP__KISSAT_H 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 diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 014063f30..ab5c59dd1 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -18,7 +18,7 @@ #include "prop/minisat/minisat.h" #include "theory/builtin/proof_checker.h" -namespace CVC4 { +namespace CVC5 { namespace prop { ProofCnfStream::ProofCnfStream(context::UserContext* u, @@ -1012,4 +1012,4 @@ SatLiteral ProofCnfStream::handleIte(TNode node) } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 6f9261278..7c97a2e8e 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -27,7 +27,7 @@ #include "theory/eager_proof_generator.h" #include "theory/theory_proof_step_buffer.h" -namespace CVC4 { +namespace CVC5 { namespace prop { class SatProofManager; @@ -170,6 +170,6 @@ class ProofCnfStream : public ProofGenerator }; } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp index 44a30ccc6..7f075ab37 100644 --- a/src/prop/proof_post_processor.cpp +++ b/src/prop/proof_post_processor.cpp @@ -17,7 +17,7 @@ #include "theory/builtin/proof_checker.h" -namespace CVC4 { +namespace CVC5 { namespace prop { ProofPostprocessCallback::ProofPostprocessCallback( @@ -105,4 +105,4 @@ void ProofPostproccess::process(std::shared_ptr<ProofNode> pf) } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h index 9a8894eef..c74cb540f 100644 --- a/src/prop/proof_post_processor.h +++ b/src/prop/proof_post_processor.h @@ -23,7 +23,7 @@ #include "expr/proof_node_updater.h" #include "prop/proof_cnf_stream.h" -namespace CVC4 { +namespace CVC5 { namespace prop { @@ -107,6 +107,6 @@ class ProofPostproccess }; } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 3f53433ae..9032dbb75 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -42,7 +42,7 @@ #include "util/resource_manager.h" #include "util/result.h" -namespace CVC4 { +namespace CVC5 { namespace prop { /** Keeps a boolean flag scoped */ @@ -616,4 +616,4 @@ std::shared_ptr<ProofNode> PropEngine::getProof() bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index fe5d94122..1145961a1 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -27,7 +27,7 @@ #include "theory/trust_node.h" #include "util/result.h" -namespace CVC4 { +namespace CVC5 { class ResourceManager; class DecisionEngine; @@ -381,6 +381,6 @@ class PropEngine }; } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__PROP_ENGINE_H */ diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp index 399f8fd03..cb380f92d 100644 --- a/src/prop/prop_proof_manager.cpp +++ b/src/prop/prop_proof_manager.cpp @@ -19,7 +19,7 @@ #include "prop/prop_proof_manager.h" #include "prop/sat_solver.h" -namespace CVC4 { +namespace CVC5 { namespace prop { PropPfManager::PropPfManager(context::UserContext* userContext, @@ -109,4 +109,4 @@ std::shared_ptr<ProofNode> PropPfManager::getProof() } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h index c429936ec..d8732c11a 100644 --- a/src/prop/prop_proof_manager.h +++ b/src/prop/prop_proof_manager.h @@ -23,7 +23,7 @@ #include "prop/proof_post_processor.h" #include "prop/sat_proof_manager.h" -namespace CVC4 { +namespace CVC5 { namespace prop { @@ -92,6 +92,6 @@ class PropPfManager }; /* class PropPfManager */ } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__PROP__PROOF_MANAGER_H */ diff --git a/src/prop/registrar.h b/src/prop/registrar.h index e54a5314b..d0fc0fe25 100644 --- a/src/prop/registrar.h +++ b/src/prop/registrar.h @@ -23,7 +23,7 @@ #ifndef CVC4__PROP__REGISTRAR_H #define CVC4__PROP__REGISTRAR_H -namespace CVC4 { +namespace CVC5 { namespace prop { class Registrar { @@ -39,7 +39,7 @@ public: };/* class NullRegistrar */ -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ +} // namespace prop +} // namespace CVC5 #endif /* CVC4__PROP__REGISTRAR_H */ diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 6f6209a76..a11eeaa8a 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -20,7 +20,7 @@ #include "prop/minisat/minisat.h" #include "theory/theory_proof_step_buffer.h" -namespace CVC4 { +namespace CVC5 { namespace prop { SatProofManager::SatProofManager(Minisat::Solver* solver, @@ -753,4 +753,4 @@ void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps) } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index c71e7e8a3..514f0153b 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -28,7 +28,7 @@ namespace Minisat { class Solver; } -namespace CVC4 { +namespace CVC5 { class ProofNodeManager; @@ -587,6 +587,6 @@ class SatProofManager }; /* class SatProofManager */ } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__SAT_PROOF_MANAGER_H */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index 0cc20d2d2..f06171775 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -30,7 +30,7 @@ #include "prop/sat_solver_types.h" #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { namespace prop { @@ -150,7 +150,7 @@ class CDCLTSatSolverInterface : public SatSolver virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy, - CVC4::context::UserContext* userContext, + CVC5::context::UserContext* userContext, ProofNodeManager* pnm) = 0; virtual void push() = 0; @@ -208,7 +208,7 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) { return out; } -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ +} // namespace prop +} // namespace CVC5 #endif /* CVC4__PROP__SAT_MODULE_H */ diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp index 9fbbfb60f..1d933dce8 100644 --- a/src/prop/sat_solver_factory.cpp +++ b/src/prop/sat_solver_factory.cpp @@ -22,7 +22,7 @@ #include "prop/kissat.h" #include "prop/minisat/minisat.h" -namespace CVC4 { +namespace CVC5 { namespace prop { BVSatSolverInterface* SatSolverFactory::createMinisat( @@ -76,4 +76,4 @@ SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry, } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h index ca9e1ad81..97b018e09 100644 --- a/src/prop/sat_solver_factory.h +++ b/src/prop/sat_solver_factory.h @@ -27,7 +27,7 @@ #include "prop/sat_solver.h" #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { namespace prop { class SatSolverFactory @@ -50,6 +50,6 @@ class SatSolverFactory }; /* class SatSolverFactory */ } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif // CVC4__PROP__SAT_SOLVER_FACTORY_H diff --git a/src/prop/sat_solver_types.cpp b/src/prop/sat_solver_types.cpp index 3a303852a..3380329c3 100644 --- a/src/prop/sat_solver_types.cpp +++ b/src/prop/sat_solver_types.cpp @@ -18,11 +18,11 @@ #include <algorithm> -namespace CVC4 { +namespace CVC5 { namespace prop { bool SatClauseLessThan::operator()(const SatClause& l, const SatClause& r) const { return std::lexicographical_compare(l.begin(), l.end(), r.begin(), r.end()); } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index a9248fdfb..392dfb2b1 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -29,7 +29,7 @@ #include <unordered_set> #include <vector> -namespace CVC4 { +namespace CVC5 { namespace prop { /** @@ -235,4 +235,4 @@ enum SatSolverLifespan }; } -} +} // namespace CVC5 diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index c2a6a8462..a0819e571 100644 --- a/src/prop/skolem_def_manager.cpp +++ b/src/prop/skolem_def_manager.cpp @@ -16,7 +16,7 @@ #include "expr/attribute.h" -namespace CVC4 { +namespace CVC5 { namespace prop { SkolemDefManager::SkolemDefManager(context::Context* context, @@ -170,4 +170,4 @@ void SkolemDefManager::getSkolems( } } // namespace prop -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h index 9bb118356..6f4ec031f 100644 --- a/src/prop/skolem_def_manager.h +++ b/src/prop/skolem_def_manager.h @@ -26,7 +26,7 @@ #include "context/context.h" #include "expr/node.h" -namespace CVC4 { +namespace CVC5 { namespace prop { /** @@ -86,6 +86,6 @@ class SkolemDefManager }; } // namespace prop -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 66023cd88..ffec0c365 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -28,7 +28,7 @@ #include "theory/theory_engine.h" #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { namespace prop { TheoryProxy::TheoryProxy(PropEngine* propEngine, @@ -105,7 +105,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { theory::TrustNode tte = d_theoryEngine->getExplanation(lNode); Node theoryExplanation = tte.getNode(); - if (CVC4::options::produceProofs()) + if (CVC5::options::produceProofs()) { d_propEngine->getProofCnfStream()->convertPropagation(tte); } @@ -232,5 +232,5 @@ void TheoryProxy::getSkolems(TNode node, void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); } -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ +} // namespace prop +} // namespace CVC5 diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 01d98f1b9..dedd1fa49 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -35,7 +35,7 @@ #include "theory/trust_node.h" #include "util/resource_manager.h" -namespace CVC4 { +namespace CVC5 { class DecisionEngine; class TheoryEngine; @@ -165,8 +165,8 @@ class TheoryProxy : public Registrar std::unique_ptr<SkolemDefManager> d_skdm; }; /* class TheoryProxy */ -}/* CVC4::prop namespace */ +} // namespace prop -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__PROP__SAT_H */ |