summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SMTLibLineariser.cs
Commit message (Collapse)AuthorAge
* Changed the syntax reading of the float typeGravatar Checkmate502016-07-16
|
* Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
|
* modified floating point syntax and modified floating point constants to use ↵Gravatar Checkmate502016-03-17
| | | | bitvector values
* Modified BigFloat and parser to accept correct SMT-LIB syntaxGravatar Checkmate502016-02-20
|
* Special fp types (such as infinity and NaN are now translated by boogieGravatar Checkmate502015-11-29
|
* Modified translation so that z3 runs with type checking for simple binary ↵Gravatar Checkmate502015-10-14
| | | | operations
* Modified BigFloat to avoid evaluating the floating point value before ↵Gravatar Checkmate502015-09-23
| | | | sending it to z3
* Float type now works correctly for simple variable declaration and comparison.Gravatar Dietrich2015-07-20
|
* Modified internal abstract float representation to allow user-defined ↵Gravatar Dietrich2015-07-13
| | | | mantissa and exponent
* integrated the named float type to act as a real in boogieGravatar Dietrich2015-05-04
|
* Began adding the float type to VC expressionGravatar Dietrich2015-04-27
|
* more work on reducing call stack consumptionGravatar qadeer2014-12-18
|
* patched two occurrences of StackOverflowException on benchmarks from IronCladGravatar qadeer2014-12-16
|
* Fix nasty bug introduced by commit 61a94f409975.Gravatar Dan Liew2014-07-15
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | There were many calls in the code to ``` new TokenTextWriter("<buffer>", buffer, false) ``` Prior to 61a94f409975 this was a call to the following constructor ``` TokenTextWriter(string filename, TextWriter writer, bool setTokens) ``` After that commit these then became calls to ``` TokenTextWriter(string filename, TextWriter writer, bool pretty) ``` An example of where this would cause issues was if ToString() was called on an AbsyCmd then the its token would be modified because the setTokens parameter was effectively set to True when the original intention was for it to be set to false! To fix this I've * Removed the default parameter value for pretty and fixed all uses so that we pass false where it was implicitly being set before * Where the intention was to set setTokens to false this has been fixed so it is actually set to false! Unfortunately I couldn't find a way of observing this bug from the Boogie executable so I couldn't create a test case. I could only observe it when I was using Boogie's APIs.
* Fixed bug in printing real literalsGravatar Rustan Leino2014-02-10
|
* fixed vc generation so that even when builtin array functions are used,Gravatar qadeer2013-12-28
| | | | the program can be verified without the use of /useArrayTheory
* Adding fixedpoint engine backendGravatar Ken McMillan2013-05-07
|
* added support for linear sets without useArrayTheory (but there is some ↵Gravatar Unknown2013-03-07
| | | | incompletness)
* Boogie: added type 'real' with overloaded arithmetic operations plus real ↵Gravatar boehmes2012-09-27
| | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
* Implement support for alternative SMT solvers -- CVC3 and CVC4Gravatar Peter Collingbourne2012-09-06
|
* Get Boogie and GPUVerify to compile and run with MonoGravatar Peter Collingbourne2012-05-02
|
* fixed problems with datatypesGravatar qadeer2011-12-29
| | | | | removed stale contracts in stratified inlining added test to datatypes
* Fixed the generation of names for datatype functions to use the API forGravatar Mike Barnett2011-10-31
| | | | | | getting SMT-approved names. Fixed a bug in VisitDistinctOp where a bad axiom was being generated when no grouping had more than one occurrence.
* added membership testsGravatar qadeer2011-10-05
|
* implementing datatypesGravatar qadeer2011-10-05
|
* check in support for generalized array theoryGravatar Unknown2011-09-06
|
* Fix printing of (Array ...) types with /useArrayTheoryGravatar Michal Moskal2011-09-06
|
* Support multi-dimensional arrays in SMTLib2 backend (using Z3 extension though)Gravatar Michal Moskal2011-09-06
|
* further fixes; temporarily commented outGravatar qadeer2011-09-03
|
* adding support for accessing Z3's generalized array theoryGravatar qadeer2011-09-02
|
* Use SMT2 syntax for sign_extendGravatar Michal Moskal2011-08-22
|
* Use (get-model) Z3 command; quote skolem-idsGravatar Michal Moskal2011-04-28
|
* Updates for the latest changes in Z3's SMT2 parserGravatar Michal Moskal2011-04-22
|
* Use new, SMT2 compliant, Z3 syntax for labelsGravatar MichalMoskal2011-04-02
|
* Don't ever put a label under a quantifier.Gravatar MichalMoskal2011-02-23
|
* Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)Gravatar MichalMoskal2011-02-23
|
* Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly ↵Gravatar MichalMoskal2011-02-23
| | | | different syntax in SMT than in Simplify
* Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq ↵Gravatar MichalMoskal2011-02-23
| | | | thing in Simplify frontend)
* Fixes in /useArrayTheory handlingGravatar MichalMoskal2011-02-23
|
* Pass :skolemid to SMTLib proverGravatar MichalMoskal2011-02-23
|
* Handle /useArrayTheoryGravatar MichalMoskal2011-02-18
|
* Remove workaround for Z3 scanner problems (fixed now); fix one commentGravatar MichalMoskal2011-02-18
|
* Handle bitvectorsGravatar MichalMoskal2011-02-18
|
* Use explicit mechanism for skipping to the next assertionGravatar MichalMoskal2011-02-17
|
* Fix printing of type-proxiesGravatar MichalMoskal2011-02-16
|
* Fix let scopingGravatar MichalMoskal2011-02-15
|
* Use the new UniformArguments property; formattingGravatar MichalMoskal2011-02-15
|
* Print terms in SMT2 syntax (drop term/formula distinction)Gravatar MichalMoskal2011-02-15
|
* Move name-quoting (already for SMT2 not SMT1) into a seprate classGravatar MichalMoskal2011-02-15
|
* Add USE_PREDICATES option to TPTP and SMT proversGravatar MichalMoskal2011-02-11
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 13:32:52 +0000