Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 481


Synopsis:        (ASSERT :linear? T)
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Wed Sep  6 12:00:01 2000
Originator:      Bruno Dutertre
Organization:    csl.sri.com
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Setting :linear? to T does no seem to have any effect 
  on what assert does, or is some kind of interaction
  with flush? 
  
  For example,
  
  assert_linear : THEORY
  
    BEGIN
  
    a, b, c, d: VAR nzreal
  
    test: LEMMA a * b * (c / b) = d
  
    END assert_linear
  
  then 
  
  test :  
  
    |-------
  {1}   FORALL (a, b, c, d: nzreal): a * b * (c / b) = d
  
  Rule? (skolem!)
  Skolemizing,
  this simplifies to: 
  test :  
  
    |-------
  {1}   a!1 * b!1 * (c!1 / b!1) = d!1
  
  Rule? (assert :linear? T)
  Simplifying, rewriting, and recording with decision procedures,
  this simplifies to: 
  test :  
  
    |-------
  {1}   (c!1 / b!1) * a!1 * b!1 = d!1
  
  
  That can be annoying if you try to use a rewrite rule like 
  
  x * y * (z / y) = x * z
  
  
  There's also a minor bug in the way auto-rewrite with antecedent
  formulas work. If you have 
  
  (AUTO-REWRITE -1)
  ...
  (AUTO-REWRITE -1)
  
  in a proof branch, then show-auto-rewrites will show two rewrite
  rules with the same name, even though formula -1 may not be the 
  same in the two cases.
  
  Bruno

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools