From 38548f400ba9acfa45d70ca814080ca80a2f9aac Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 20 Apr 2007 15:33:27 +0000 Subject: [PATCH] The declarative rewriting step now tries auto timeout=3 before auto paramodulation timeout=3. This seems to work better then just auto paramodulation alone when the user tries to help the system. This because paramodulation is more confused than helped. --- components/tactics/declarative.ml | 16 +++++++++++----- components/tactics/tactics.mli | 2 +- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index 6c37acaa4..e36c86037 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -168,16 +168,22 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step = let just = match just with `Auto params -> - let params = - if not (List.exists (fun (k,_) -> k = "paramodulation") params) then - ("paramodulation","1")::params - else params in let params = if not (List.exists (fun (k,_) -> k = "timeout") params) then ("timeout","3")::params else params in - Tactics.auto ~dbd ~params ~universe + let params' = + if not (List.exists (fun (k,_) -> k = "paramodulation") params) then + ("paramodulation","1")::params + else params + in + if params = params' then + Tactics.auto ~dbd ~params ~universe + else + Tacticals.first + [Tactics.auto ~dbd ~params ~universe ; + Tactics.auto ~dbd ~params:params' ~universe] | `Term just -> Tactics.apply just in let plhs,prhs,prepare = diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli index 6000a98ad..34bc2d4f3 100644 --- a/components/tactics/tactics.mli +++ b/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Apr 20 15:46:14 CEST 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Apr 20 17:07:53 CEST 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : -- 2.39.2