Code

Counter Example generation#652

Code

Draft

RobinWebbers wants to merge 35 commits intoucsd-progsys:developucsd-progsys/liquid-fixpoint:developfrom RobinWebbers:developRobinWebbers/liquid-fixpoint:developCopy head branch name to clipboard

+1,979-63

Commits

Commits on Apr 20, 2023

• WIP counter example generation

  RobinWebbers

  committed
  8f574a1

Commits on May 3, 2023

• BFS Counter example generator

  RobinWebbers

  committed
  61fa746

Commits on May 11, 2023

• Fixed typing issues of counter examples. Fixed issue of running multiple bodies, causing no counter example to be generated. Actually fetches counter examples from the smt solve now.

  RobinWebbers

  committed
  9914197

Commits on May 12, 2023

• Put counter example in output result. Only runs tests for failing clauses (if any). Put feature gate behind counter example generation.

  RobinWebbers

  committed
  0cb062b

Commits on May 25, 2023

• Now tracks counter examples per constraint id. Added a max depth to avoid infinite recursion on cyclic kvars.

  RobinWebbers

  committed
  37d9405

• Removed dead code previously introduced

  RobinWebbers

  committed
  57e55b8

• Added some comments and reduced exports for CounterExample.hs

  RobinWebbers

  committed
  4188204

• Solved hlint warnings

  RobinWebbers

  committed
  8548f4c

Commits on Jun 13, 2023

• WIP Counterexample depth first run with location info

  RobinWebbers

  committed
  9d79fda

Commits on Jul 5, 2023

• Merge branch 'ucsd-progsys:develop' into develop

  RobinWebbers

  authored
  5fdd8d8

Commits on Jul 7, 2023

• Modified to depth first counter example search. Added stack traces to counterexample.

  RobinWebbers

  committed
  a2d8fee

• Split counterexample build and check

  RobinWebbers

  committed
  13dabbc

Commits on Nov 2, 2023

• Improved readback from SMT. Added back recursion limit

  RobinWebbers

  committed
  705a2ce

Commits on Nov 14, 2023

• Fixed issues with duplicate naming and SMT model parsing

  RobinWebbers

  committed
  8702a1c

Commits on Feb 15, 2024

• Counterexamples now include Result generic, symbol and type. Moved counterexample files with incorrect spelling

  RobinWebbers

  committed
  82ca427

Commits on Feb 19, 2024

• Changed name scheme in counterexample to use BindId as a path instead of Symbol

  RobinWebbers

  committed
  9f91f76

• Changed the format of counterexamles. The extension to full counterexample now uses the local bind environment to get accurate types.

  RobinWebbers

  committed
  876804d

• Removed obsolete where binding from toFullCex

  RobinWebbers

  committed
  3b84915

Commits on Feb 28, 2024

• Obsolete environments are now deleted from the counterexample

  RobinWebbers

  committed
  558306f

• Split SMT interface of counterexamples from checker

  RobinWebbers

  committed
  3a656bc

• Squashed calls to not incorrectly unfold multiple kvars if they were conjuncted in Counterexample checker

  RobinWebbers

  committed
  f0f0967

Commits on Mar 7, 2024

• Changed counterexample SMT scope to just include top level subcid. Added JSON output for Counterexample

  RobinWebbers

  committed
  bca8208

Commits on Mar 8, 2024

• Solved issue where counterexamples were not correctly inserted. Solved issue where head constraint was removed from the environment.

  RobinWebbers

  committed
  2852c27

Commits on Mar 14, 2024

• Used internal location information for producing spans in a counterexample

  RobinWebbers

  committed
  3b43016

• Merged with latest branch of main repo

  RobinWebbers

  committed
  63211db

Commits on Mar 19, 2024

• Removed spurous counterexamples from declarations after assume/call/assert and underconstraint kvars when recursion depth was reached

  RobinWebbers

  committed
  bb27151

Commits on Mar 20, 2024

• Fixed wrong naming on 'fix$' names. Fixed wrong recursion limit, that caused the checker to do nothing

  RobinWebbers

  committed
  f50e50c

Commits on Mar 24, 2024

• Added define axioms to counterexample constraints, such that we generate lists of the correct length. Renamed counterexample SMT functions.

  RobinWebbers

  committed
  72ac0fa

• Removed debug print

  RobinWebbers

  committed
  d308c7e

Commits on Mar 25, 2024

• Added support for SMT Sequence theory

  RobinWebbers

  committed
  d8049fb

• Definitions as quantified axioms proved too slow, so for now I removed it from the counterexample generation.

  RobinWebbers

  committed
  d1cec55

Commits on Apr 1, 2024

• Resolved issue where the counterexample build would ignore other refinements if it included kvars

  RobinWebbers

  committed
  b504b47

Commits on Apr 2, 2024

• Added early pruning of paths and removal of duplicate kvars (i.e. identical module transitively equivalent variables)

  RobinWebbers

  committed
  b5bbb84

• Changed search strategy from DFS to iterative deepening DFS

  RobinWebbers

  committed
  2e88e2c

• Removed obsolete import

  RobinWebbers

  committed
  677d322