[sv-ec] mantis 2183 (solve-before constraints)

From: Ryan, Ray <Ray_Ryan_at_.....>
Date: Mon Mar 24 2008 - 15:08:21 PDT
In considering the champions feedback and the SV-EC discussion, I tried
to find a better way to state restriction on expressions in a
solve-before constraints (that still allowed)
- names of random 'variables' 
- rand fields of random variables 
- bit selects of random varialbes 
- references to elements of a random array 
- field of an element of ...
- ...

My conclusion is that special restrictions for expesssion in a
solve-before constraint (beyond those for constraints in general) are
not required.

For the case where an solve-before expression is not a "simple random
variable or field of a random variable). IE
    rand int x,y,z;
    ...
    constraint C {
        solve (x+y) before z;
    }
This should have the same semantics as
    rand int x,y,z;
    rand int t1;
    constraint C {
        t1 == x+y;
        solve t1 before x;
    }

Since the latter can be coded with the current LRM, allowing expressions
in a solve-before constraint doesn't add any new solver capabilities -
rather it is a simplification.


I have added a modified proposal (errata_2183d.htm) that allows
expression in solve-before constaints and removes the prior resrictions.


Regards,
Ray Ryan


-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.
Received on Mon Mar 24 15:09:10 2008

This archive was generated by hypermail 2.1.8 : Mon Mar 24 2008 - 15:09:21 PDT