[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] Help with (both-sides) strategy*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Wed, 25 May 2016 00:12:55 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> message dated "Mon, 23 May 2016 11:54:20 -0400."*In-reply-to*: <C92637B4-4BD1-4DE4-B44B-51B82DC80990@dependablecomputing.com>*List-archive*: <http://mls.csl.sri.com/pipermail/pvs-help>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <C92637B4-4BD1-4DE4-B44B-51B82DC80990@dependablecomputing.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Ben, I'm having trouble recreating this. With the spec ----- test: THEORY BEGIN p_Data_Type_Conversion: nat f: formula 1 <= p_Data_Type_Conversion => p_Data_Type_Conversion - 1 >= 0 END test ----- I get: f : |------- {1} 1 <= p_Data_Type_Conversion IMPLIES p_Data_Type_Conversion - 1 >= 0 Rule? (flatten) Applying disjunctive simplification to flatten sequent, this simplifies to: f : {-1} 1 <= p_Data_Type_Conversion |------- {1} p_Data_Type_Conversion - 1 >= 0 Rule? (both-sides "+" "1" 1) Applying + 1 to both sides of an inequality/equality conjunction, this simplifies to: f : [-1] 1 <= p_Data_Type_Conversion |------- {1} p_Data_Type_Conversion - 1 + 1 >= 0 + 1 Rule? I suspect that the decision procedures have already recorded something in your case that is affecting the behavior of both-sides (yours shows that you're in the fourth branch of the proof). Is it possible for you to send me your specs? Thanks, Sam Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote: > From: Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> > Date: Mon, 23 May 2016 11:54:20 -0400 > To: pvs-help@xxxxxxxxxxx > Subject: [PVS-Help] Help with (both-sides) strategy > Sender: pvs-help-bounces+owre=csl.sri.com@xxxxxxxxxxx > > I don’t use the (both-sides) strategy very often, so perhaps I’m using it wrong, but I’m not sure what I’m doing > wrong in the following: > Selector_TCC2.4 : > > [-1] (1 <= p_Data_Type_Conversion) > |------- > [1] p_Data_Type_Conversion - 1 >= 0 > > Rule? (both-sides "+" "1" 1) > Applying + 1 to both sides of an inequality/equality conjunction, > this yields 3 subgoals: > Selector_TCC2.4.1 : > > [-1] (1 <= p_Data_Type_Conversion) > |------- > {1} p_Data_Type_Conversion - 1 + 1 >= 0 + 1 > > Rule? (grind) > Trying repeated skolemization, instantiation, and if-lifting, > > This completes the proof of Selector_TCC2.4.1. > > Selector_TCC2.4.2 : > > [-1] (1 <= p_Data_Type_Conversion) > |------- > {1} p_Data_Type_Conversion - 1 >= 0 = > p_Data_Type_Conversion - 1 + 1 >= 0 + 1 > [2] p_Data_Type_Conversion - 1 >= 0 > > Rule? (assert) > Simplifying, rewriting, and recording with decision procedures, > this simplifies to: > Selector_TCC2.4.2 : > > [-1] (1 <= p_Data_Type_Conversion) > |------- > {1} FALSE = TRUE > [2] p_Data_Type_Conversion - 1 >= 0 > > At this point, since {1} is clearly false, I’m back to where I started (notwithstanding an additional TCC to prove > that real_pred(p_Data_Type_Conversion - 1), which can be proved with (lemma "reals.closed_minus" ("x" > "p_Data_Type_Conversion" "y" "1"))). > > Any idea what I’m doing wrong? > > And how does: > {1} p_Data_Type_Conversion - 1 >= 0 = > p_Data_Type_Conversion - 1 + 1 >= 0 + 1 > get resolved to: > {1} FALSE = TRUE > upon using (assert)? > > Best Regards, > Ben Hocking > ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx

**Follow-Ups**:**Re: [PVS-Help] Help with (both-sides) strategy***From:*Ben Hocking

**References**:**[PVS-Help] Help with (both-sides) strategy***From:*Ben Hocking

- Prev by Date:
**Re: [PVS-Help] Help with (both-sides) strategy** - Next by Date:
**Re: [PVS-Help] Help with (both-sides) strategy** - Previous by thread:
**Re: [PVS-Help] Help with (both-sides) strategy** - Next by thread:
**Re: [PVS-Help] Help with (both-sides) strategy** - Index(es):