summaryrefslogtreecommitdiff
path: root/Source/Core/AbsyQuant.cs
Commit message (Expand)AuthorAge
* Add experimental support for optimization (requires Z3 build after changeset ...Gravatar Valentin Wüstholz2015-11-18
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
* Fix performance issue in ComputeHashCode() methods of Expr classes.Gravatar Dan Liew2015-02-02
* Protect the body of ForAllExpr, ExistsExpr and LambdaExpr when theyGravatar Dan Liew2015-01-29
* Fix ForAllExpr, ExistsExpr and LambdaExpr constructors so it is possibleGravatar Dan Liew2015-01-29
* Add the ability to declare Expr to be immutable at construction time.Gravatar Dan Liew2015-01-29
* Fixed minor issue.Gravatar wuestholz2015-01-26
* Minor changeGravatar wuestholz2015-01-26
* Merging changes from wuestholz/BoogieInvariantFixesIIIIGravatar wuestholz2015-01-13
|\
| * Made invariant of class 'Trigger' robust by:Gravatar wuestholz2015-01-09
| * Made invariant of class 'QKeyValue' robust by:Gravatar wuestholz2015-01-09
* | Tiny change ('Trigger' class)Gravatar 0biha2015-01-08
* | Tiny fix (made field 'tr' of class 'Trigger' private)Gravatar 0biha2015-01-08
* | Made invariant of class 'Trigger' robust byGravatar 0biha2015-01-01
|/
* Minor refactoringGravatar wuestholz2014-11-05
* MergeGravatar Dan Rosén2014-08-01
|\
* | Add alpha equivalence check for Expr, and use it when lambda liftingGravatar Dan Rosén2014-08-01
| * Fix bug in BinderExpr where is was possible for A.Equals(B) to returnGravatar Dan Liew2014-07-29
| * Fix bug in BinderExpr where Equals() was not corrected implemented.Gravatar Dan Liew2014-07-28
|/
* Add some pretty-printing, on by default. Turn off with the flag "/pretty:0"Gravatar Dan Rosén2014-06-24
* checkpointGravatar qadeer2014-05-03
* disabled quantifier merging, except when no triggers are provided (as discuss...Gravatar Unknown2014-03-03
* Changed all lambda-expression rewriting to be done as a pre-processing step b...Gravatar Rustan Leino2014-02-28
* (Fixed and) strengthened contracts of ReadOnlyVisitor. The postconditions of...Gravatar Rustan Leino2014-02-24
* Fixed errors in the use of Code ContractsGravatar Rustan Leino2014-02-10
* more bug fixesGravatar qadeer2013-12-24
* Fixed another :never_pattern bug related to nested quantifiersGravatar Rustan Leino2013-12-16
* Fixed bug in never_pattern functionality. In the new design, never_pattern d...Gravatar Rustan Leino2013-12-16
* All ...Seq classes now goneGravatar Ally Donaldson2013-07-22
* ExprSeq: farewellGravatar Ally Donaldson2013-07-22
* Started to remove ...Seq classesGravatar Ally Donaldson2013-07-22
* More refactoringGravatar Ally Donaldson2013-07-22
* More refactoring towards replacing PureCollections.Sequence with ListGravatar Ally Donaldson2013-07-22
* Refactoring of TypeVariableSeqGravatar Ally Donaldson2013-07-22
* Changed Has method of PureSequence to Contains to make refactoring easier.Gravatar Ally Donaldson2013-07-22
* Allow attributes on procedure formals, function formals, and bound variablesGravatar Unknown2013-01-07
* Removed old comments about "BASEMOVE" and other constructor calls, where the ...Gravatar Unknown2013-01-07
* Removed AIFramework from Boogie -- use native trivial or native interval-base...Gravatar boehmes2012-09-27
* Make set iteration order deterministicGravatar Michal Moskal2011-12-07
* changed the semantics of requires and ensures for inlined proceduresGravatar qadeer2011-11-17
* Fix a bug in cloning of nested lambda expressions in AI engineGravatar MichalMoskal2011-02-11
* Boogie: Commented out all occurences of repeated inherited contracts - makes ...Gravatar tabarbe2010-08-27
* Boogie: Committing changed source filesGravatar tabarbe2010-08-20
* Boogie: Renaming core sources in preparation for port commitGravatar tabarbe2010-08-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 14:06:48 +0000