Help has moved to the Planio platform. All logins and passwords remained the same. All users will be able to login and use Redmine just as before. *Read more...*

Feature #154551


add resource limit command

Added by Cesare Tinelli over 9 years ago. Updated almost 9 years ago.

Start date:
Due date:
% Done:


Estimated time:


Add a command to set some generic resource limit (for each of the next check-sat commands, until changed by a new occurrence of the command).

See suggestion below by Martin Brain.

Resource limits
The need is for a repeatable, deterministic way of limiting the
run-time of a solver. This is needed for performing automatic
regression testing on sets of programs that include some conditions that
will cause the solver to 'time out'. Thus all that is needed is some
way of setting a limit / counter that is monotonic with respect to the
time taken by the solver. Rough consistency between formulae would be
nice but there is no need for it to be consistent between solvers,
solver versions, etc. Simple options include using the number of
conflicts learnt, inference steps performed, etc.

Actions #1

Updated by Clark Barrett over 9 years ago

  • Subject changed from add esource limit command to add resource limit command
Actions #2

Updated by Clark Barrett about 9 years ago

see also email conversation with Cesare,Pascal Jul 28-29, 2013

Actions #3

Updated by Cesare Tinelli almost 9 years ago

  • Priority changed from Normal to High

Also available in: Atom PDF