Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|

Synopsis: Rewrite rule TCC simplified to wrong value Severity: serious Priority: medium Responsible: shankar State: open Class: sw-bug Arrival-Date: Thu Jun 21 15:35:00 2001 Originator: "Ben L. Di Vito" Organization: larc.nasa.gov Release: PVS 2.3 Environment: System: Architecture: Description: We sometimes find that prelude rewrite rules don't fire when it looks like they should. I was able to isolate a very simple example that shows one instance. Under the assumption that 0 < a, the prover simplified a*a /= 0 to false. It happened after an (assert) as a setup step, but gave correct results when (prop) was used instead. Ben Di Vito ----------------------- rewrite_bug: THEORY BEGIN a: VAR real test1: LEMMA 0 < a IMPLIES a > 1 %% not a theorem END rewrite_bug -------------------- test1 : |------- {1} FORALL (a: real): 0 < a IMPLIES a > 1 Rule? (skosimp*) Repeatedly Skolemizing and flattening, this simplifies to: test1 : {-1} 0 < a!1 |------- {1} a!1 > 1 Rule? (case "2 * a!1 * a!1 /= 0") Case splitting on 2 * a!1 * a!1 /= 0, this yields 2 subgoals: test1.1 : {-1} 2 * a!1 * a!1 /= 0 [-2] 0 < a!1 |------- [1] a!1 > 1 Rule? (postpone) Postponing test1.1. test1.2 : [-1] 0 < a!1 |------- {1} 2 * a!1 * a!1 /= 0 [2] a!1 > 1 Rule? (assert) Simplifying, rewriting, and recording with decision procedures, this simplifies to: test1.2 : {-1} 2 * (a!1 * a!1) = 0 [-2] 0 < a!1 |------- [1] a!1 > 1 Rule? (rewrite "nonzero_times3") Found matching substitution: n0y: nonzero_real gets a!1 * a!1, n0x gets 2, *WARNING*: TCC a!1 * a!1 /= 0 simplifies to FALSE No change on: (REWRITE "nonzero_times3") test1.2 : {-1} 2 * (a!1 * a!1) = 0 [-2] 0 < a!1 |------- [1] a!1 > 1 Rule? (rewrite$ "zero_times3") Found matching substitution: y: real gets a!1 * a!1, x gets 2, Applying zero_times3 where y gets a!1 * a!1, x gets 2, this simplifies to: test1.2 : {-1} 2 * (a!1 * a!1) = 0 IFF 2 = 0 OR a!1 * a!1 = 0 [-2] 2 * (a!1 * a!1) = 0 [-3] 0 < a!1 |------- [1] a!1 > 1 Rewriting directly with -1, this simplifies to: test1.2 : [-1] 0 < a!1 |------- [1] a!1 > 1 Postponing test1.2. test1.2 : [-1] 0 < a!1 |------- [1] a!1 > 1 Rule? (undo 3) This will undo the proof to: test1.2 : [-1] 0 < a!1 |------- {1} 2 * a!1 * a!1 /= 0 [2] a!1 > 1 Sure?(Y or N): y test1.2 : [-1] 0 < a!1 |------- {1} 2 * a!1 * a!1 /= 0 [2] a!1 > 1 Rule? (prop) Applying propositional simplification, this simplifies to: test1.2 : {-1} 2 * a!1 * a!1 = 0 [-2] 0 < a!1 |------- [1] a!1 > 1 Rule? (rewrite "zero_times3") Found matching substitution: y: real gets a!1, x gets 2 * a!1, Rewriting using zero_times3, matching in *, this simplifies to: test1.2 : {-1} 2 * a!1 = 0 OR a!1 = 0 [-2] 0 < a!1 |------- [1] a!1 > 1 How-To-Repeat: Fix:

Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|