Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.

4 files changed, 162 insertions, 116 deletions

diff --git a/src/prop/minisat/CVC4-README b/src/prop/minisat/CVC4-README
index cd3b638d6..2fcf2ed49 100644
--- a/src/prop/minisat/CVC4-README
+++ b/src/prop/minisat/CVC4-README
@@ -1,6 +1,6 @@
 ================ CHANGES TO THE ORIGINAL CODE ==================================
 
-The only CVC4 connections passed to minisat are the proxy (defined in sat.h) and
+The only cvc5 connections passed to minisat are the proxy (defined in sat.h) and
 the context. The context is obtained from the SmtEngine, and the proxy is an 
 intermediary class that has all-access to the SatSolver so as to simplify the 
 interface to (possible) other sat solvers. These two are passed to minisat at 
@@ -35,7 +35,7 @@ Backtracking in minisat is performed through the cancelUntil() method, which is
 now modified to pop the context the appropriate number of times.
 
 Minisat pushes the scope in the newDecisionLevel() method where we appropriately 
-also push the CVC4 context.
+also push the cvc5 context.
 
 * Phase caching
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 8f59ec13b..981e51e31 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -2123,7 +2123,7 @@ void Solver::push()
   trail_ok.push(ok);
   assigns_lim.push(assigns.size());
 
-  d_context->push();  // SAT context for CVC4
+  d_context->push();  // SAT context for cvc5
 
   Debug("minisat") << "MINISAT PUSH assertionLevel is " << assertionLevel << ", trail.size is " << trail.size() << std::endl;
 }
@@ -2162,7 +2162,7 @@ void Solver::pop()
   removeClausesAboveLevel(clauses_removable, assertionLevel);
   Debug("minisat") << cvc5::pop;
   // Pop the SAT context to notify everyone
-  d_context->pop();  // SAT context for CVC4
+  d_context->pop();  // SAT context for cvc5
 
   Debug("minisat") << "MINISAT POP assertionLevel is " << assertionLevel
                    << ", trail.size is " << trail.size() << "\n";
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index fd682639b..f85dc0d24 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -54,8 +54,7 @@ namespace Minisat {
 // Solver -- the main class:
 
 class Solver {
-
-  /** The only two CVC4 entry points to the private solver data */
+  /** The only two cvc5 entry points to the private solver data */
   friend class cvc5::prop::PropEngine;
   friend class cvc5::prop::TheoryProxy;
   friend class cvc5::prop::SatProofManager;
@@ -198,117 +197,164 @@ public:
    }
  };
 
-    // CVC4 context push/pop
-    void          push                     ();
-    void          pop                      ();
-
-    /*
-     * Reset the decisions in the DPLL(T) SAT solver at the current assertion
-     * level.
-     */
-    void resetTrail();
-    // addClause returns the ClauseId corresponding to the clause added in the
-    // reference parameter id.
-    bool    addClause (const vec<Lit>& ps, bool removable, ClauseId& id);  // Add a clause to the solver.
-    bool    addEmptyClause(bool removable);                                // Add the empty clause, making the solver contradictory.
-    bool    addClause (Lit p, bool removable, ClauseId& id);               // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable, ClauseId& id);        // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
-    bool    addClause_(      vec<Lit>& ps, bool removable, 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
-
-    void toDimacs();
-    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    freezePolarity (Var v, bool b); // Declare which polarity the decision heuristic MUST ALWAYS 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;
-    bool    isDecision (Var x) const;       // is the given var a decision?
-
-    // Debugging SMT explanations
-    //
-    bool    properExplanation(Lit l, Lit expl) const; // returns true if expl can be used to explain l---i.e., both assigned and trail_index(expl) < trail_index(l)
-
-    // 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.
+ // cvc5 context push/pop
+ void push();
+ void pop();
+
+ /*
+  * Reset the decisions in the DPLL(T) SAT solver at the current assertion
+  * level.
+  */
+ void resetTrail();
+ // addClause returns the ClauseId corresponding to the clause added in the
+ // reference parameter id.
+ bool addClause(const vec<Lit>& ps,
+                bool removable,
+                ClauseId& id);  // Add a clause to the solver.
+ bool addEmptyClause(
+     bool removable);  // Add the empty clause, making the solver contradictory.
+ bool addClause(Lit p,
+                bool removable,
+                ClauseId& id);  // Add a unit clause to the solver.
+ bool addClause(Lit p,
+                Lit q,
+                bool removable,
+                ClauseId& id);  // Add a binary clause to the solver.
+ bool addClause(Lit p,
+                Lit q,
+                Lit r,
+                bool removable,
+                ClauseId& id);  // Add a ternary clause to the solver.
+ bool addClause_(
+     vec<Lit>& ps,
+     bool removable,
+     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
+
+ void toDimacs();
+ 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 freezePolarity(
+     Var v,
+     bool b);  // Declare which polarity the decision heuristic MUST ALWAYS 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;
+ bool isDecision(Var x) const;  // is the given var a decision?
+
+ // Debugging SMT explanations
+ //
+ bool properExplanation(Lit l, Lit expl)
+     const;  // returns true if expl can be used to explain l---i.e., both
+             // assigned and trail_index(expl) < trail_index(l)
 
-    // Memory managment:
-    //
-    virtual void garbageCollect();
-    void    checkGarbage(double gf);
-    void    checkGarbage();
+ // 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> d_conflict;          // If problem is unsatisfiable (possibly under
-                          // assumptions), this vector represent the final
-                          // conflict clause expressed in the assumptions.
+ // Extra results: (read-only member variable)
+ //
+ vec<lbool> model;  // If problem is satisfiable, this vector contains the model
+                    // (if any).
+ vec<Lit> d_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, resources_consumed;
-    uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
+ // 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,
+     resources_consumed;
+ uint64_t dec_vars, clauses_literals, learnts_literals, max_literals,
+     tot_literals;
 
 protected:
 
@@ -389,7 +435,7 @@ protected:
 
     ClauseAllocator     ca;
 
-    // CVC4 Stuff
+    // cvc5 Stuff
     /**
      * A vector determining whether each variable represents a theory atom.
      * More generally, this value is true for any literal that the theory proxy
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 55209b248..813292a21 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -129,7 +129,7 @@ void MinisatSatSolver::initialize(context::Context* context,
 // Like initialize() above, but called just before each search when in
 // incremental mode
 void MinisatSatSolver::setupOptions() {
-  // Copy options from CVC4 options structure into minisat, as appropriate
+  // Copy options from cvc5 options structure into minisat, as appropriate
 
   // Set up the verbosity
   d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1;