Induction improvements #525
Conversation
…when resolving and its usefulness is also questionable
…ng over induction terms in index
…ome may sneak in under ep=RSTC, until it's fixed)
… the other argument as a bound
…ve survived so wrong for so long?), fix BottomUpTermTransformer to be compatible with specialTerms, stop being silly about many overloads of transform
|
This also contains two new induction schedules: |
mezpusz
force-pushed
the
rule-induction-sorting
branch
from
79cb14e
to
7565a92
Compare
Shell/Options.cpp
Outdated
| @@ -95,7 +95,7 @@ void Options::init() | |||
| _simulatedInstructionLimit = UnsignedOptionValue("simulated_instruction_limit","sil",0); | |||
| _simulatedInstructionLimit.description= | |||
| "Instruction limit (in millions) of executed instructions for the purpose of reachability estimations of the LRS saturation algorithm (if 0, the actual instruction limit is used)"; | |||
| _simulatedInstructionLimit.onlyUsefulWith(_saturationAlgorithm.is(equal(SaturationAlgorithm::LRS))); | |||
| // _simulatedInstructionLimit.onlyUsefulWith(Or(_saturationAlgorithm.is(equal(SaturationAlgorithm::LRS)),_splittingAvatimer.is(notEqual(1.0f)))); | |||
There was a problem hiding this comment.
Well spotted! But yes, this should be the same commit as
be8e2f5
which is already in master. The reason is the same. (In my use case, it pays off to set sil unconditionally and the warning becomes very annoying.)
CASC/Schedules.cpp
Outdated
There was a problem hiding this comment.
Seems the new configurations have time limit 0. What is happening here?
There was a problem hiding this comment.
Correct me if I'm wrong @quickbeam123, I think the instruction limit i= is used, or it is converted to an approximate time value if this is not supported by the system.
There was a problem hiding this comment.
What happens on my machine is:
% Running in auto input_syntax mode. Trying SMTLIB2
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% ott+10_1:4_av=off:drc=off:ind=struct:indgen=on:newcnf=on:nui=on:uwa=ground:i=10:si=on:rtra=on_0 on 0 for (1ds/10Mi)
perf_event_open failed (instruction limiting will be disabled): Permission denied
% Time limit reached!
% ------------------------------
% Version: Vampire 4.8 (commit c2fca0bff on 2024-03-01 15:15:02 +0100)
% Linked with Z3 4.12.2.0 e417f7d78509b2d0c9ebc911fee7632e6ef546b6 z3-4.8.4-7517-ge417f7d78
% Termination reason: Time limit
% Termination phase: Saturation
% Memory used [KB]: 1908
% Time elapsed: 0.200 s
% ------------------------------
% ------------------------------
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
% dis+10_1:1_aac=none:alpa=true:drc=off:ind=both:indoct=on:newcnf=on:sac=on:taea=off:to=lpo:i=5:si=on:rtra=on_0 on 0 for (1ds/5Mi)
perf_event_open failed (instruction limiting will be disabled): Permission denied
% Time limit reached!
% ------------------------------
% Version: Vampire 4.8 (commit c2fca0bff on 2024-03-01 15:15:02 +0100)
% Linked with Z3 4.12.2.0 e417f7d78509b2d0c9ebc911fee7632e6ef546b6 z3-4.8.4-7517-ge417f7d78
% Termination reason: Time limit
% Termination phase: Saturation
% Memory used [KB]: 8294
% Time elapsed: 0.200 s
...
I killed Vampire after a couple of seconds, but all the configurations that ran only ran for something between 0-0.6s.
There was a problem hiding this comment.
I think that's the (ballpark) intended timescale, trying to solve benchmarks almost immediately or moving on to the next strategy.
There was a problem hiding this comment.
Yes, that's the intended ballpark.
And this should be the reassuring message:
% WARNING: time unlimited strategy and instruction limiting not in place - attempting to translate instructions to time
(along with the fact that you are seeing % Termination reason: Time limit)
@hzzv , I am pushing one extra line of help that should help users like you quickly fix fully the problem:
"(If you are seeing 'Permission denied' ask your admin to run 'sudo sysctl -w kernel.perf_event_paranoid=-1' for you.)" (Cf. https://sysctl-explorer.net/kernel/perf_event_paranoid/)
Could you please give it a try?
@hzzv I added comments where I saw fit (including stuff in |
This PR includes various improvements and features on (mostly) inductive reasoning:
define-fun[-rec]blocks in SMTLIB are handled specially for inductive reasoning via some new options, including using them as rewrite rules (-fnrw on) and creating induction schemas based on their case distinctions/well-founded orders (-sik recursion).define-funs-rec(exists in SMTLIB 2.6), allowing for mutually recursive functions.While creating the above mentioned schedules, the features were extensively tested, so hopefully everything works at least as well as they worked before.