summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3Gravatar MichalMoskal2011-02-18
|
* Accomodate for recent changes in Z3 V2 model formatGravatar MichalMoskal2011-02-18
|
* Ask Z3 to generate models, in V2 format, when neededGravatar MichalMoskal2011-02-18
| | | | | Add supported :prover commands Minor fixes
* Handle /useArrayTheoryGravatar MichalMoskal2011-02-18
|
* Intercept Z3 warnings and pass them onGravatar MichalMoskal2011-02-18
|
* Remove workaround for Z3 scanner problems (fixed now); fix one commentGravatar MichalMoskal2011-02-18
|
* Recognize () as identifier terminatorsGravatar MichalMoskal2011-02-18
|
* Handle bitvectorsGravatar MichalMoskal2011-02-18
|
* Expose ToByteArray()Gravatar MichalMoskal2011-02-18
|
* Dafny:Gravatar rustanleino2011-02-17
| | | | | | | | | | | | | | | | | | * Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case). * Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.) * Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type. * More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal") * Add axioms about idempotence of set union and intersection * The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one * In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase * Fixed error in translation of while(*)
* Boogie: Fixed problem with binding power of .[.] versus type coercions in ↵Gravatar rustanleino2011-02-17
| | | | pretty printing
* Use explicit mechanism for skipping to the next assertionGravatar MichalMoskal2011-02-17
|
* Disable MBQI and AUTO_CONFIGGravatar MichalMoskal2011-02-17
|
* Kill the solver process when ctrl-c is pressedGravatar MichalMoskal2011-02-17
|
* Provide /p: as the short form of /proverOpt:.Gravatar MichalMoskal2011-02-17
| | | | | Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT. Add default Z3 options when using Z3.
* Read prover responses; handle labelsGravatar MichalMoskal2011-02-17
|
* Make it possible to run Z3 on pipe; use generic PROVER_LOG optionsGravatar MichalMoskal2011-02-17
|
* Add IEnumerable.IterGravatar MichalMoskal2011-02-17
|
* Kill {:prover "..."} attribute support; no one ever used this stuffGravatar MichalMoskal2011-02-17
|
* Don't use Simplify's LogProverInterfaceGravatar MichalMoskal2011-02-17
|
* Indentation.Gravatar MichalMoskal2011-02-17
|
* Start implementation of pipe communication in SMTLIB backendGravatar MichalMoskal2011-02-17
|
* Stratified inlining: Added concrete values to error traces. Added an extra ↵Gravatar akashlal2011-02-17
| | | | flag "inferLeastForUnsat".
* Fix printing of type-proxiesGravatar MichalMoskal2011-02-16
|
* Bugfixes in select-of-store axiomsGravatar MichalMoskal2011-02-16
|
* Skip "(assert true)" in output; skip "Linearing..." messages when they are fastGravatar MichalMoskal2011-02-16
|
* Fix let scopingGravatar MichalMoskal2011-02-15
|
* Workaround bug in Z3 SMT parserGravatar MichalMoskal2011-02-15
|
* Use SMT2 top-level syntaxGravatar MichalMoskal2011-02-15
|
* Use the new UniformArguments property; formattingGravatar MichalMoskal2011-02-15
|
* Add VCExprNAry.UniformArguments property to return arguments of nested ↵Gravatar MichalMoskal2011-02-15
| | | | And/Or nodes.
* Add some extension methods to IEnumberable<T>Gravatar 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
|
* Fix with timeoutGravatar akashlal2011-02-12
|
* Better support for timeoutGravatar akashlal2011-02-12
|
* Fix a bug in cloning of nested lambda expressions in AI engineGravatar MichalMoskal2011-02-11
|
* Add USE_PREDICATES option to TPTP and SMT proversGravatar MichalMoskal2011-02-11
|
* Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP ↵Gravatar MichalMoskal2011-02-11
| | | | provers. Add handling of help message about /proverOpt.
* Get rid of some warnings.Gravatar MichalMoskal2011-02-11
|
* Minor change to stratified inliningGravatar akashlal2011-02-11
|
* Changed the API for Declaration.AddAttribute so it takes a params argument ↵Gravatar mikebarnett2011-02-09
| | | | so multiple parameters can be added to an attribute at one go. No calls had to be changed because of the way params arguments work.
* Boogie: Yet another refinement of how Z3 is found. Previously, it would ↵Gravatar rustanleino2011-02-09
| | | | only look in one of "c:\Program Files\Microsoft Research" and "c:\Program Files (x86)\Microsoft Research", even if both existed (which meant that it might have looked in the wrong one). Now, both are considered.
* Added a new method StratifiedVC for refinement.Gravatar akashlal2011-02-08
| | | | Added a method to copy a FunctionCall.
* implemented /UseUnsatCoreForInlining option for use in stratified inliningGravatar qadeer2011-02-06
|
* deleted debugging statementGravatar akashlal2011-02-05
|
* Fix to counterexample generation for over-approx queryGravatar akashlal2011-02-05
|
* Dafny: every decreases clause implicitly ends with a never-ending sequence ↵Gravatar rustanleino2011-02-03
| | | | of TOP elements; this reduces the need for manually supplied decreases clauses (see the Outer/Inner example in Test/dafny0/Termination.dfy and the Substitute/SubstSeq example in Test/dafny1/Substitution.dfy).
* Dafny: allow self-calls in function postconditions--these simply refer to ↵Gravatar rustanleino2011-02-03
| | | | the result value of the current call
* Dafny: implemented a more precise scheme for allowing use of a function's ↵Gravatar rustanleino2011-02-03
| | | | rep axiom
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-05 21:53:09 +0000