docs: Remove references to checkEntailed(). (#8789)

diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst
index f9d5b338b84e00c4096edd5db15dc5847aa489c8..baa0844d2ff7a394f302fe09fc4aa6a885ddb547 100644 (file)
--- a/docs/resource-limits.rst
+++ b/docs/resource-limits.rst
@@ -7,7 +7,7 @@ cvc5 supports limiting the time or *resources* it uses during solving via the op
 All these options take a single non-negative number as an argument where giving zero explicitly disables the respective limit. For time limits the number is interpreted as the number of milliseconds, and for resource limits it indicates the amount of *resources*.
 
 The limits configured using :ref:`tlimit <lbl-option-tlimit>` and :ref:`rlimit <lbl-option-rlimit>` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver <cvc5::Solver>` object, respectively.
-In contrast to that, :ref:`tlimit-per <lbl-option-tlimit-per>` and :ref:`rlimit-per <lbl-option-rlimit-per>` apply to every check individually (:cpp:func:`checkSat <cvc5::Solver::checkSat>`, :cpp:func:`checkSatAssuming <cvc5::Solver::checkSatAssuming>`, :cpp:func:`checkEntailed <cvc5::Solver::checkEntailed>`, etc).
+In contrast to that, :ref:`tlimit-per <lbl-option-tlimit-per>` and :ref:`rlimit-per <lbl-option-rlimit-per>` apply to every check individually (:cpp:func:`checkSat <cvc5::Solver::checkSat>`, :cpp:func:`checkSatAssuming <cvc5::Solver::checkSatAssuming>`, etc).
 
 Except for the overall time limit (see below), the limits are checked by cvc5 itself. This means that the solver remains in a safe state after a limit has been reached.
 Due to the way cvc5 checks these limits (see below), cvc5 may not precisely honor per-call time limits: if a subroutine requires a long time to finish without spending resources itself, cvc5 only realizes afterwards that the timeout has (long) passed.

diff --git a/src/smt/assertions.h b/src/smt/assertions.h
index 366b0f231f7f3179659b4024cab7b9508e5dd34c..05a23a41eef8fa738a615b5a0cc58697d4aafe86 100644 (file)
--- a/src/smt/assertions.h
+++ b/src/smt/assertions.h
@@ -174,9 +174,6 @@ class Assertions : protected EnvObj
   context::CDO<size_t> d_globalDefineFunLemmasIndex;
   /**
    * The list of assumptions from the previous call to checkSatisfiability.
-   * Note that if the last call to checkSatisfiability was an entailment check,
-   * i.e., a call to checkEntailed(a1, ..., an), then d_assumptions contains
-   * one single assumption ~(a1 AND ... AND an).
    */
   std::vector<Node> d_assumptions;
   /** Whether we did a global negation of the formula. */

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 8b19e664e0aad0f4d872d56c8d21a8e903d31edd..3b509bf468bb836ad81759b8bba9625ba96e03ae 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -787,7 +787,7 @@ class CVC5_EXPORT SolverEngine
    *
    * Note that the per-call timer only ticks away when one of the
    * SolverEngine's workhorse functions (things like assertFormula(),
-   * checkEntailed(), checkSat(), and simplify()) are running.
+   * checkSat(), and simplify()) are running.
    * Between calls, the timer is still.
    *
    * When an SolverEngine is first created, it has no time or resource

diff --git a/src/smt/solver_engine_state.h b/src/smt/solver_engine_state.h
index cc6eded72e2f2db3c114a4592f015c5e0f55e2fc..e6de541fc316aa625b541fc460bf53d3d68f95e6 100644 (file)
--- a/src/smt/solver_engine_state.h
+++ b/src/smt/solver_engine_state.h
@@ -220,7 +220,7 @@ class SolverEngineState : protected EnvObj
 
   /**
    * Whether or not a notifyCheckSat call has been made, which corresponds to
-   * when a checkEntailed() or checkSatisfiability() has already been
+   * when a checkSatisfiability() has already been
    * made through the SolverEngine.  If true, and incrementalSolving is false,
    * then attempting an additional checks for satisfiability will fail with
    * a ModalException during notifyCheckSat.
@@ -235,7 +235,7 @@ class SolverEngineState : protected EnvObj
   bool d_needPostsolve;
 
   /**
-   * Most recent result of last checkSatisfiability/checkEntailed in the
+   * Most recent result of last checkSatisfiability in the
    * SolverEngine.
    */
   Result d_status;