From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,48e1a3c594fb62e8
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII
Path: 
 g2news2.google.com!postnews.google.com!f14g2000vbn.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@googlemail.com>
Newsgroups: comp.lang.ada
Subject: Re: SPARK
Date: Wed, 19 May 2010 01:09:33 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <42a7e70b-b780-4f86-83ca-6cf79ff81dd1@f14g2000vbn.googlegroups.com>
References: <op.vcl6900wule2fv@garhos> <op.vcr9heg2ule2fv@garhos>
	<op.vcwxo3zrule2fv@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1274256573 13636 127.0.0.1 (19 May 2010 08:09:33
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Wed, 19 May 2010 08:09:33 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: f14g2000vbn.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:11746
Date: 2010-05-19T01:09:33-07:00
List-Id: <comp.lang.ada>

On 18 May, 19:01, Yannick Duch=EAne (Hibou57) <yannick_duch...@yahoo.fr>
wrote:
> I've noticed Simplifier seems to read an .RUL file it is belongs to a =A0
> directory where it is reading .VCG files (I don't why it do that). I've =
=A0
> noticed that while I was playing a bit with it :p
>
> Will have to search for another way to add rules system-wide, if possible=
.

Yannick,

I don't think that the toolset provides what you are looking for*.

The only recognised way to supply additional rules to the Simplifier
are as user rules - the full details about this are in Section 7 of
the Simplifier user manual.  This section also describes how the user
rules are applied.

It is unfortunate that user rules are less effective than the rules
built into the Simplifier as they are only used once the normal
Simplifier strategies have failed to prove a conclusion (see the
introduction of Section 3).

For example an inference rule will only be used if it *directly*
proves a conclusion.
Section 7.2.1: "In order for the Simplifier to be able to make use of
the rule, it must find an instance of the rule by pattern-matching it
against the current VC (for inference rules, this essentially means
against the undischarged conclusions of the VC)"

Cheers,

Phil

* Except that, of course, the full source of the Simplifier is
available, and there is nothing to stop you making changes to it!