Code

Counterexamples As Assumptions#5013

Code

Merged

atomb merged 86 commits intodafny-lang:masterdafny-lang/dafny:masterfrom Dargones:CounterexamplesAsPredicatesDargones/dafny:CounterexamplesAsPredicatesCopy head branch name to clipboardApr 9, 2024

+2,133-1,556

Commits

Commits on Sep 4, 2023

• Store Progress

  

  Aleksandr Fedchin

  committed
  00b7477

  Copy full SHA for 00b7477

Commits on Oct 25, 2023

• minor changes

  

  Aleksandr Fedchin

  committed
  cc874dc

  Copy full SHA for cc874dc

Commits on Nov 16, 2023

• Counterexample parity for extension vs command line

  

  Aleksandr Fedchin

  committed
  1be2388

  Copy full SHA for 1be2388

• Update DafnyRef and dev/news

  

  Aleksandr Fedchin

  committed
  d5505f4

  Copy full SHA for d5505f4

• Update ProverLogRegression

  

  Aleksandr Fedchin

  committed
  8d428bc

  Copy full SHA for 8d428bc

• Update existing test

  

  Aleksandr Fedchin

  committed
  77c4e8f

  Copy full SHA for 77c4e8f

Commits on Dec 2, 2023

• primitive types

  

  Aleksandr Fedchin

  committed
  6683cc7

  Copy full SHA for 6683cc7

• Merge branch 'CounterexampleParity' into CounterexamplesAsPredicates

  

  Aleksandr Fedchin

  committed
  94db77a

  Copy full SHA for 94db77a

Commits on Dec 7, 2023

• Save temp changes

  

  Aleksandr Fedchin

  committed
  8c87dff

  Copy full SHA for 8c87dff

Commits on Dec 10, 2023

• Sync with master

  

  Aleksandr Fedchin

  committed
  f38b9f1

  Copy full SHA for f38b9f1

• Add Values field

  

  Aleksandr Fedchin

  committed
  f358e51

  Copy full SHA for f358e51

• Calculate Cardinality

  

  Aleksandr Fedchin

  committed
  d3e50ec

  Copy full SHA for d3e50ec

Commits on Dec 13, 2023

• Separate constraints into their own class

  

  Aleksandr Fedchin

  committed
  038395a

  Copy full SHA for 038395a

Commits on Dec 14, 2023

• Fixes and testing

  

  Aleksandr Fedchin

  committed
  5cbe1de

  Copy full SHA for 5cbe1de

Commits on Dec 17, 2023

• Resolve all literals

  

  Aleksandr Fedchin

  committed
  acf2179

  Copy full SHA for acf2179

Commits on Dec 19, 2023

• push minor fixes

  

  Aleksandr Fedchin

  committed
  af19151

  Copy full SHA for af19151

• Prevent inifinite recursion

  

  Aleksandr Fedchin

  committed
  0e7da20

  Copy full SHA for 0e7da20

Commits on Dec 20, 2023

• Keep track of MapEmpty

  

  Aleksandr Fedchin

  committed
  b57b5f1

  Copy full SHA for b57b5f1

• Fix arities

  

  Aleksandr Fedchin

  committed
  726c164

  Copy full SHA for 726c164

• Modify definition selection

  

  Aleksandr Fedchin

  committed
  b8426f0

  Copy full SHA for b8426f0

• Another small fix

  

  Aleksandr Fedchin

  committed
  4ae99f6

  Copy full SHA for 4ae99f6

• Fix test

  

  Aleksandr Fedchin

  committed
  1e2e991

  Copy full SHA for 1e2e991

Commits on Dec 30, 2023

• Update wellformedness rules

  

  Aleksandr Fedchin

  committed
  b4eb8a9

  Copy full SHA for b4eb8a9

• Change order of definitions

  

  Aleksandr Fedchin

  committed
  0284161

  Copy full SHA for 0284161

Commits on Jan 12, 2024

• Pass Test Generation tests

  

  Aleksandr Fedchin

  committed
  d021fa2

  Copy full SHA for d021fa2

Commits on Jan 16, 2024

• Do not constrain elements of a sequence that are out of bounds

  

  Aleksandr Fedchin

  committed
  fe7d9aa

  Copy full SHA for fe7d9aa

Commits on Jan 19, 2024

• Merge remote-tracking branch 'origin/master' into CounterexampleParity

  

  Aleksandr Fedchin

  committed
  83cc425

  Copy full SHA for 83cc425

• Enable counterexamples for multiple locations in the program

  

  Aleksandr Fedchin

  committed
  d182a13

  Copy full SHA for d182a13

• Temprorarily add boogie submodule

  

  Aleksandr Fedchin

  committed
  65d2c04

  Copy full SHA for 65d2c04

• Fix test-generation translation pass and Update tests

  

  Aleksandr Fedchin

  committed
  00fa2a5

  Copy full SHA for 00fa2a5

• Fix variable printing order and update tests

  

  Aleksandr Fedchin

  committed
  0d7789f

  Copy full SHA for 0d7789f

• Merge branch 'CounterexampleParity' into CounterexamplesAsPredicates

  

  Aleksandr Fedchin

  committed
  d510eaa

  Copy full SHA for d510eaa

• Remove accidentally committed fiels

  

  Aleksandr Fedchin

  committed
  d5ea6e3

  Copy full SHA for d5ea6e3

Commits on Jan 22, 2024

• Updated tests

  

  Aleksandr Fedchin

  committed
  b180b1e

  Copy full SHA for b180b1e

• Revert "Temprorarily add boogie submodule"

  Show description for 8aa183b
  

  Aleksandr Fedchin

  committed
  8aa183b

  Copy full SHA for 8aa183b

• Update Boogie version

  

  Aleksandr Fedchin

  committed
  10002e4

  Copy full SHA for 10002e4

• Fix customBoogie.patchj

  

  Aleksandr Fedchin

  committed
  76700d7

  Copy full SHA for 76700d7

• Merge branch 'master' into CounterexampleParity

  

  Aleksandr Fedchin

  committed
  37bf3aa

  Copy full SHA for 37bf3aa

• Update Prover Log test

  

  Aleksandr Fedchin

  committed
  8515c8e

  Copy full SHA for 8515c8e

• Update Inverses test

  

  Aleksandr Fedchin

  committed
  c06d769

  Copy full SHA for c06d769

• Merge branch 'CounterexampleParity' into CounterexamplesAsPredicates

  

  Aleksandr Fedchin

  committed
  3f2eb86

  Copy full SHA for 3f2eb86

Commits on Jan 25, 2024

• Pass all server tests

  

  Aleksandr Fedchin

  committed
  fdaa5c6

  Copy full SHA for fdaa5c6

• Merge remote-tracking branch 'origin/master' into CounterexamplesAsPredicates

  

  Aleksandr Fedchin

  committed
  ab0ec83

  Copy full SHA for ab0ec83

• Remove unused code

  

  Aleksandr Fedchin

  committed
  c72299d

  Copy full SHA for c72299d

• Format and test output fies

  

  Aleksandr Fedchin

  committed
  7e7f0f8

  Copy full SHA for 7e7f0f8

Commits on Feb 1, 2024

• Fix tests

  Dargones

  committed
  b111ba2

  Copy full SHA for b111ba2

Commits on Feb 9, 2024

• Refactor the constraints mechanism

  

  Aleksandr Fedchin

  committed
  43436e2

  Copy full SHA for 43436e2

Commits on Feb 10, 2024

• Refactor Constraint.cs

  

  Aleksandr Fedchin

  committed
  a19dc32

  Copy full SHA for a19dc32

• Minor fixes

  

  Aleksandr Fedchin

  committed
  dce077d

  Copy full SHA for dce077d

Commits on Feb 11, 2024

• Fix an inconsistent counterexample

  

  Aleksandr Fedchin

  committed
  4f71e2c

  Copy full SHA for 4f71e2c

• Merge remote-tracking branch 'origin/master' into CounterexamplesAsPredicates

  

  Aleksandr Fedchin

  committed
  61e5b9a

  Copy full SHA for 61e5b9a

• Fix whitespace

  

  Aleksandr Fedchin

  committed
  ca31a49

  Copy full SHA for ca31a49

• Fix Arity

  

  Aleksandr Fedchin

  committed
  931e0df

  Copy full SHA for 931e0df

• Deal with Empty Sequences

  

  Aleksandr Fedchin

  committed
  7042d0e

  Copy full SHA for 7042d0e

• Handle collection types with no argument

  

  Aleksandr Fedchin

  committed
  42c62b3

  Copy full SHA for 42c62b3

Commits on Feb 19, 2024

• Support constraints over function return values

  

  Aleksandr Fedchin

  committed
  c58a225

  Copy full SHA for c58a225

• Generate on test method at a time

  

  Aleksandr Fedchin

  committed
  581d51f

  Copy full SHA for 581d51f

• Fix wellformedness checks

  

  Aleksandr Fedchin

  committed
  bfcb31e

  Copy full SHA for bfcb31e

• Merge remote-tracking branch 'origin/CounterexamplesAsPredicates' into CounterexamplesDev

  

  Aleksandr Fedchin

  committed
  4c14080

  Copy full SHA for 4c14080

Commits on Feb 22, 2024

• Better Documentation and formatting

  

  Aleksandr Fedchin

  committed
  9d7e2c8

  Copy full SHA for 9d7e2c8

• Dotnet format

  

  Aleksandr Fedchin

  committed
  7b85179

  Copy full SHA for 7b85179

• Delete accidentally committed files

  

  Aleksandr Fedchin

  committed
  80c3838

  Copy full SHA for 80c3838

• Fix tests

  

  Aleksandr Fedchin

  committed
  7de5b4a

  Copy full SHA for 7de5b4a

Commits on Feb 25, 2024

• Merge branch 'CounterexamplesAsPredicates' into CounterexamplesDev

  

  Aleksandr Fedchin

  committed
  6f98747

  Copy full SHA for 6f98747

• Minor fixes

  

  Aleksandr Fedchin

  committed
  70d516e

  Copy full SHA for 70d516e

• Add SetDisplay Constraint

  

  Aleksandr Fedchin

  committed
  0bec799

  Copy full SHA for 0bec799

• Minor fix

  

  Aleksandr Fedchin

  committed
  548e79b

  Copy full SHA for 548e79b

• More fixes

  

  Aleksandr Fedchin

  committed
  c85769f

  Copy full SHA for c85769f

• Undo the tuple ignoring principle

  

  Aleksandr Fedchin

  committed
  5319003

  Copy full SHA for 5319003

Commits on Mar 7, 2024

• Merge recent changes

  

  Aleksandr Fedchin

  committed
  32f7be5

  Copy full SHA for 32f7be5

• Merge remote-tracking branch 'origin/master' into CounterexamplesAsPredicates

  

  Aleksandr Fedchin

  committed
  699f52e

  Copy full SHA for 699f52e

• Apply suggested changes

  

  Aleksandr Fedchin

  committed
  9c111f8

  Copy full SHA for 9c111f8

• Update Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs

  Show description for 36cd8d2
  

  Dargones

  and

  atomb

  authored
  36cd8d2

  Copy full SHA for 36cd8d2

• Fix counterexample for recursive functions

  

  Aleksandr Fedchin

  committed
  40cabcf

  Copy full SHA for 40cabcf

Commits on Mar 13, 2024

• Pretty-printing changes

  

  Aleksandr Fedchin

  committed
  a5149a9

  Copy full SHA for a5149a9

• Fix tests

  

  Aleksandr Fedchin

  committed
  e38dbc1

  Copy full SHA for e38dbc1

• Merge remote-tracking branch 'origin/master' into CounterexamplesAsPredicates

  

  Aleksandr Fedchin

  committed
  2e6415a

  Copy full SHA for 2e6415a

• Fix test

  

  Aleksandr Fedchin

  committed
  53904c3

  Copy full SHA for 53904c3

Commits on Mar 21, 2024

• Add a warning indicating that the counterexample may be inconsistent of invalid

  

  Aleksandr Fedchin

  committed
  5975ea7

  Copy full SHA for 5975ea7

Commits on Apr 8, 2024

• Merge remote-tracking branch 'origin/master' into CounterexamplesAsPredicates

  

  Aleksandr Fedchin

  committed
  6f36f77

  Copy full SHA for 6f36f77

• Fix nitpick

  

  Aleksandr Fedchin

  committed
  203f725

  Copy full SHA for 203f725

• Lift note on counterexample validity into its own section

  

  Aleksandr Fedchin

  committed
  48812d5

  Copy full SHA for 48812d5

• Fix tests

  

  Aleksandr Fedchin

  committed
  275db10

  Copy full SHA for 275db10

Commits on Apr 9, 2024

• Merge branch 'master' into CounterexamplesAsPredicates

  atomb

  authored
  d964f3c

  Copy full SHA for d964f3c

• Merge branch 'master' into CounterexamplesAsPredicates

  atomb

  authored
  fac4c7c

  Copy full SHA for fac4c7c

• Merge branch 'master' into CounterexamplesAsPredicates

  Dargones

  authored
  a58755c

  Copy full SHA for a58755c