summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
* Add the ability to declare Expr to be immutable at construction time.Gravatar Dan Liew2015-01-29
| | | | | | | | | | | | This is currently not enforced (it really should be). So right now it only amounts to a promise by the client that the Expr will not be modified after it is constructed. We should actually enforce this by protecting various fields of the Expr classes so they can't be changed if an Expr is constructed as Immutable. The motivation for doing this is it allows the value of GetHashCode() to be cached. Expr classes now implement ComputeHashCode() to do the actuall hash code computation.
* minor fix to the golden fileGravatar qadeer2015-01-28
|
* added lit stuff at the top of the file and the golden outputGravatar qadeer2015-01-28
|
* Work stealing queue (PLDI '12 Vechev et al.)Gravatar Unknown2015-01-28
|
* Handle timeout in refinement loopGravatar akashlal2015-01-28
|
* MergeGravatar qadeer2015-01-27
|\
* | removed unused functions and axioms to make the verification fasterGravatar qadeer2015-01-27
| |
| * Fixed minor issue.Gravatar wuestholz2015-01-26
| |
| * Worked on the verification result caching (statement checksums).Gravatar wuestholz2015-01-26
| |
| * Minor changeGravatar wuestholz2015-01-26
| |
| * Minor changeGravatar wuestholz2015-01-26
| |
| * Worked on the verification result caching (trace output).Gravatar wuestholz2015-01-26
| |
| * Change the return type of StandardVisitor.VisitLiteralExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | LiteralExpr to Expr. Enforcing the return type be LiteralExpr is too restrictive. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
| * Change the return type of StandardVisitor.VisitExistsExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | ExistsExpr to Expr. Enforcing the return type be ExistsExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
| * Change the return type of StandardVisitor.VisitForAllExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | ForAllExpr to Expr. Enforcing the return type be ForAllExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
| * Change the return type of StandardVisitor.VisitBvExtractExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | BvExtractExpr to Expr. Enforcing the return type be BvExtractExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type. a visitor that does constant folding of an Expr tree
| * Change the return type of StandardVisitor.VisitBvConcatExpr() fromGravatar Dan Liew2015-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | BvConcatExpr to Expr. Enforcing the return type be BvConcatExpr is too restrictive. For example it prevents anyone from implementing a visitor that does constant folding of an Expr tree. There is precedence for this. For example VisitNAryExpr() returns an Expr not an NAryExpr. Unfortunately this a breaking API change so anyone who subclasses the StandardVisitor (or one of its sub classes) and overrides this method will get compilation errors until they change the return type.
| * Worked on the verification result caching (use weights for extracted functions).Gravatar wuestholz2015-01-24
| |
| * Worked on the verification result caching (use native support for partially ↵Gravatar wuestholz2015-01-16
| | | | | | | | verified assertions).
| * Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-23
| |
| * MergeGravatar Ally Donaldson2015-01-22
| |\ | |/ |/|
| * Fixes to StagedHoudiniGravatar Ally Donaldson2015-01-22
| |
* | MergeGravatar qadeer2015-01-16
|\|
* | removed "layer" attribute from the desugared programGravatar qadeer2015-01-16
| |
| * Worked on StagedHoudiniGravatar Ally Donaldson2015-01-16
| |
| * Fix related to limitations in CVC4 model parsingGravatar Ally Donaldson2015-01-14
| |
| * MergeGravatar Ally Donaldson2015-01-13
| |\
| | * Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
| | |\
| | * | Merging changes from 0biha/BoogieInvariantFixesIIIaGravatar wuestholz2015-01-13
| |/| | |/| | |
| * | | Removed unnecessary stage-related attributes from candidate annotations.Gravatar Ally Donaldson2015-01-10
| | | |
| | | * Made 2 invariants of class 'VariableCollector' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field protected - exposing IEnumerables (with help from David Rohr)
| | | * Made invariant of class 'Trigger' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - adding getter/setter - copying incoming list - exposing read-only list (with help from David Rohr)
| | | * Made invariant of class 'StmtList' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private and readonly - exposing IEnumerable - adding 'AddLabel' method (with help from David Rohr)
| | | * Made invariant of class 'StmtList' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - adding private field - exposing read-only list - copying incoming list (with help from David Rohr)
| | | * Made invariant of class 'QKeyValue' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing read-only list - copying incoming list - adding methods 'AddParam', 'AddParams', and 'ClearParams' (with help from David Rohr)
| | | * Made invariant of class 'EEDTemplate' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable - copying incoming list (with help from David Rohr)
| | | * Made invariant of class 'Block' robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable (with help from David Rohr)
| | | * Made invariant of class CommandLineOptions robust by:Gravatar wuestholz2015-01-09
| | | | | | | | | | | | | | | | | | | | | | | | - making field private - exposing an IEnumerable (with help from David Rohr)
| | | * Made 2 invariants of class 'CommandLineOptions' robust by:Gravatar wuestholz2015-01-09
| |_|/ |/| | | | | | | | | | | | | | | | | - making fields private - exposing IEnumerables - adding methods 'AddProverOption', 'RemoveAllProverOptions', and 'AddZ3Option' (with help from David Rohr)
* | | Minor changes to the "Checked" build configurationGravatar wuestholz2015-01-09
|/ /
| * Tiny change ('Trigger' class)Gravatar 0biha2015-01-08
| |
* | Updated to Staged HoudiniGravatar Ally Donaldson2015-01-08
| |
| * Fixed a null reference problem in class 'Constant'.Gravatar 0biha2015-01-08
| |
| * Tiny fix (made field 'tr' of class 'Trigger' private)Gravatar 0biha2015-01-08
| |
| * Made 2 invariants of class 'DeclWithFormals' robust by changing the designGravatar 0biha2015-01-07
| | | | | | | | (replaced public fields by private fields + getters/setters)
| * Rewrote 'globalVariablesCache' invariant fix of class 'Program'Gravatar 0biha2015-01-08
| |
| * Made invariant of class 'Constant' robust by making list 'Parents' read-onlyGravatar 0biha2015-01-05
| |
| * Made invariant of class 'AtomicRE' robust by changing the designGravatar 0biha2015-01-05
| | | | | | | | (replaced public field by private field + getter/setter)
| * Made invariant of class 'Trigger' robust byGravatar 0biha2015-01-01
| | | | | | | | | | | | -replacing public field by private field + getter -using read-only wrappers (to avoid leaking) -cloning the tr list in the setter and constructor (to avoid capturing)
| * Made invariant of class 'ListOfMiningStrategies' robust by changing the designGravatar 0biha2015-01-01
| | | | | | | | (replaced public field by private field + getter/setter)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 04:17:47 +0000