From 6f5e85af48265e6fc478cb695bb40ab9ce6661d5 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 17 May 2022 11:43:52 -0700 Subject: [PATCH] docs: Remove references to checkEntailed(). (#8789) --- docs/resource-limits.rst | 2 +- src/smt/assertions.h | 3 --- src/smt/solver_engine.h | 2 +- src/smt/solver_engine_state.h | 4 ++-- 4 files changed, 4 insertions(+), 7 deletions(-) diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst index f9d5b338b..baa0844d2 100644 --- 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 ` and :ref:`rlimit ` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver ` object, respectively. -In contrast to that, :ref:`tlimit-per ` and :ref:`rlimit-per ` apply to every check individually (:cpp:func:`checkSat `, :cpp:func:`checkSatAssuming `, :cpp:func:`checkEntailed `, etc). +In contrast to that, :ref:`tlimit-per ` and :ref:`rlimit-per ` apply to every check individually (:cpp:func:`checkSat `, :cpp:func:`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 366b0f231..05a23a41e 100644 --- a/src/smt/assertions.h +++ b/src/smt/assertions.h @@ -174,9 +174,6 @@ class Assertions : protected EnvObj context::CDO 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 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 8b19e664e..3b509bf46 100644 --- 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 cc6eded72..e6de541fc 100644 --- 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; -- 2.30.2