Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | refuted candidates are exchanged in memory using a concurrent dictionary ↵ | 2013-09-26 | ||
| | | | | instead of using an IO csv file as before | |||
* | improvements to the refuted annotations exchange process | 2013-08-20 | ||
| | ||||
* | new option for reversing the topological order - this could potentially help ↵ | 2013-08-19 | ||
| | | | | to speedup houdini refutation of candidates | |||
* | changes in the parallel houdini script | 2013-07-30 | ||
| | ||||
* | added script for running the portfolio solver (parallel houdini) | 2013-07-30 | ||
| | ||||
* | parallel houdini prototype working | 2013-07-26 | ||
| | ||||
* | ExprSeq: farewell | 2013-07-22 | ||
| | ||||
* | CmdSeq: farewell | 2013-07-22 | ||
| | ||||
* | Started to remove ...Seq classes | 2013-07-22 | ||
| | ||||
* | More refactoring | 2013-07-22 | ||
| | ||||
* | More refactoring towards replacing PureCollections.Sequence with List | 2013-07-22 | ||
| | ||||
* | merge | 2013-07-22 | ||
|\ | ||||
| * | Requires/EnsuresSeq replaced by List<Requires/Ensures> | 2013-07-22 | ||
| | | ||||
| * | Large refactoring of Hashtable to Dictionary. | 2013-07-22 | ||
| | | ||||
| * | Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a ↵ | 2013-07-22 | ||
| | | | | | | | | plain Hashtable. | |||
* | | merge | 2013-07-19 | ||
|\| | ||||
| * | Revamp of staged Houdini, and completion of parallel support. | 2013-07-18 | ||
| | | ||||
| * | Extracted Houdini statistics into a record, and parametersied Houdini class ↵ | 2013-07-16 | ||
| | | | | | | | | with a statistics object. This means that if one runs multiple Houdini instances, each can record its own statistics. | |||
| * | Some cleanup in HoudiniSession | 2013-07-16 | ||
| | | ||||
| * | Reworking of Staged Houdini in preparation for parallelising it. | 2013-07-16 | ||
| | | ||||
* | | Merge | 2013-07-15 | ||
|\ \ | |/ |/| | ||||
* | | Worked on the parallelization. | 2013-07-10 | ||
| | | ||||
| * | merge | 2013-07-06 | ||
| |\ | |/ |/| | ||||
* | | Did some refactoring in the execution engine and worked on the parallelization. | 2013-07-01 | ||
| | | ||||
* | | Addressed some \n versus \r\n issues | 2013-06-29 | ||
| | | ||||
* | | Method in Houdini to allow an expression to be turned into non-candidate form | 2013-06-21 | ||
| | | ||||
* | | Merge | 2013-06-19 | ||
|\ \ | ||||
| * | | AbsHoudini: Bug fix, with bv constants. | 2013-06-19 | ||
| | | | ||||
* | | | Merge | 2013-06-19 | ||
|\| | | ||||
| * | | AbsHoudini: Bug fix | 2013-06-19 | ||
| | | | ||||
* | | | Merge | 2013-06-18 | ||
|\| | | ||||
| * | | AbsHoudini: Few more abstract domains | 2013-06-16 | ||
| | | | ||||
| * | | AbsHoudini: added an implication domain | 2013-06-15 | ||
| | | | ||||
| | * | CVC4 Parser | 2013-06-12 | ||
| |/ | ||||
* / | Some work on staged Houdini | 2013-06-07 | ||
|/ | ||||
* | Improvements to Staged Houdini | 2013-05-29 | ||
| | ||||
* | Merge | 2013-05-27 | ||
|\ | ||||
* | | Staged Houdini can now take a path to a file of ignored variables | 2013-05-27 | ||
| | | ||||
| * | AbsHoudini: Added support for quantifiers | 2013-05-27 | ||
|/ | ||||
* | Fixed bug in staged Houdini. | 2013-05-22 | ||
| | ||||
* | Adapted Houdini algorithm to take staging into account | 2013-05-18 | ||
| | ||||
* | AbsHoudini: Tolerate some assertion failing. Updated regression baseline. | 2013-05-10 | ||
| | ||||
* | AbsHoudini: Each function can specify its own abstract domain. Also added | 2013-05-05 | ||
| | | | | typechecking | |||
* | Some code refactoring | 2013-05-03 | ||
| | ||||
* | Merge | 2013-04-30 | ||
|\ | ||||
* | | Staged Houdini | 2013-04-30 | ||
| | | ||||
| * | AbsHoudini: Bug fix | 2013-04-28 | ||
| | | ||||
| * | AbsHoudini: Added support for /errorLimit:n, n > 1 | 2013-04-25 | ||
| | | ||||
| * | AbsHoudini: Added predicate-abstraction domain and some examples. | 2013-04-25 | ||
| | | ||||
| * | AbsHoudini: Added support for DoNotUsLabels, domain for simulating Houdini, | 2013-04-25 | ||
| | | | | | | | | few bug fixes, hack to support missing prover declarations. |