Code

Model Counting extension#57

Code

Open

ssahai wants to merge 125 commits intomasteruclid-org/uclid:masterfrom ssahai/modelcountinguclid-org/uclid:ssahai/modelcountingCopy head branch name to clipboard

+1,988-93

Commits

Commits on Sep 30, 2020

• Initial commit on branch modelcounting.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  1142d19

• starting to parse the model counter files.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  97672c9

• parser is beginning to work.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  a1d02e7

• some more progress on the model counter.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  c5db3a9

• first baby proof is working.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  eff52b2

• intermediate commit.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  998f3b6

• Merge with master after all recent commits.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  3cf2f07

• Moving files for modelcounter into extensions.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  33da53f

• The toy file is being parsed.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  2189edc

• New syntax for counting op + rewriting infra setup.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  6a3dbdb

• Adding a parameter list to assert statements

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  f72dec4

• More fixes for assertion parameters.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  ba1bd5c

• Almost done with the initial working example.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  09b726f

• Refactoring the UMC ASTs.

  Show description for ee3ba88
  

  pramodsu

  authored and

  Shubham Sahai

  committed
  ee3ba88

• We have added support for the range rule.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  ad13306

• constlb and constub rules.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  d1b9ae3

• cover properties properly support.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  116a496

• New rewriter.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  818ea82

• a few minor additions to counting_2n.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  c5452e4

• adding the indLb rule which seems to work for now.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  78e49f2

• first attempt at model count proof.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  607f6fa

• Compilation fix after merge.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  5101ae0

• fixed disjoint to be or rule

  

  ssahai

  committed
  df5b162

• updated the test example

  

  ssahai

  committed
  999b2c1

• minor fix to example

  

  ssahai

  committed
  9475655

• added UB rule

  

  ssahai

  committed
  8fc244b

• minor edit: adding assert to UB rule - ensuring counting quantifier is applied on the same set of variables in each expression

  

  ssahai

  committed
  aedd7dd

• added AndUB rule

  

  ssahai

  committed
  ec2a756

• added Disjoint rule

  

  ssahai

  committed
  dff3427

• added injectivity rule

  

  ssahai

  committed
  ef7a803

• zkhat example

  

  ssahai

  committed
  3810704

• parsing indUB. Rewriting is pending for now.

  

  ssahai

  committed
  542183c

• added support for lemmas via lemma block - parsing successfully

  

  ssahai

  committed
  b59c15b

• verifying the lemmas in the control block

  

  ssahai

  committed
  356f303

• indLB for zk-hat working now

  

  ssahai

  committed
  89a6fff

• minor edits while playing around with examples.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  03b5ec1

• updated vim syntax file

  

  ssahai

  committed
  59743f7

• minor edit to syntax file

  

  ssahai

  committed
  9ec6f6a

• added assumptions to range statement to cater symbolic bounds

  

  ssahai

  committed
  2b2c951

• attempting Array shuffle example - constEQ going UNDEF

  

  ssahai

  committed
  595cf61

• fixed ite printing

  

  ssahai

  committed
  4fc0a23

• fixed satonly decorator and assert printing

  

  ssahai

  committed
  6ffabb8

• UFs can take more than one arguements now in IndLB

  

  ssahai

  committed
  598a14d

• indLB can take more than one ys values

  

  ssahai

  committed
  8e1a6cb

• asserts can be named

  

  ssahai

  committed
  cb4aa7c

• fixing printing of 2 : in case asserts have names

  

  ssahai

  committed
  a333c36

• added descriptive names to rewritten asserts

  

  ssahai

  committed
  60f345e

• fixed repetition of quantified variables in indLB

  

  ssahai

  committed
  c611648

• induction working for array shuffle

  

  ssahai

  committed
  18db170

• added test for indLB. Working fine now

  

  Shubham Sahai

  committed
  ebce038

• added indUB

  

  Shubham Sahai

  committed
  719e4a3

• updated/added tests for all the proof rules

  

  Shubham Sahai

  committed
  bf04408

• minor edit to fix warning while building the universal package

  

  Shubham Sahai

  committed
  29e99db

• update author info in modelcounting extension

  

  Shubham Sahai

  committed
  103a771

Commits on Oct 1, 2020

• config options works with UMC now

  

  Shubham Sahai

  committed
  ca5f2bd

Commits on Oct 27, 2020

• Add array reads to readset

  Show description for 6502265
  polgreen

  committed
  6502265

• remove parenthesis from file names

  polgreen

  committed
  2e1ffcc

• pre-emptively check for array selects on LHS of primed var assign

  polgreen

  committed
  c76ef1e

• Merge pull request #60 from polgreen/neater_filenmaes

  Show description for 41b55f0
  polgreen

  authored
  41b55f0

Commits on Oct 28, 2020

• Merge pull request #58 from polgreen/test_redundant_assign

  Show description for 33a24ca
  polgreen

  authored
  33a24ca

Commits on Oct 30, 2020

• added counting script for zkHAT - motivating example from CAV20 paper

  

  ssahai

  committed
  828c3c4

Commits on Nov 3, 2020

• update z3 version in readme

  polgreen

  authored
  7e6ce29

• Merge pull request #61 from uclid-org/polgreen-patch-1

  Show description for 2e0caa2
  polgreen

  authored
  2e0caa2

Commits on Nov 5, 2020

• README: Improve clarity

  

  Yatin Manerkar

  committed
  4d13e51

Commits on Nov 6, 2020

• README.md: Add hyperlinks to help people navigate README

  

  Yatin Manerkar

  committed
  791e283

• Merge pull request #62 from ymanerka/master

  Show description for 1defdfb
  ymanerka

  authored
  1defdfb

• add minimalist contribution guidelines

  polgreen

  committed
  69199e1

• Merge pull request #63 from polgreen/contrib

  Show description for 25f2fc3
  polgreen

  authored
  25f2fc3

Commits on Nov 10, 2020

• Initial commit on branch modelcounting.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  09fb91e

• starting to parse the model counter files.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  113c42d

• parser is beginning to work.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  539ef60

• some more progress on the model counter.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  90e5ec5

• first baby proof is working.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  33d0d4b

• intermediate commit.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  60a2aae

• Merge with master after all recent commits.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  09727b7

• Moving files for modelcounter into extensions.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  e8ba396

• The toy file is being parsed.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  f384992

• New syntax for counting op + rewriting infra setup.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  0db408e

• Adding a parameter list to assert statements

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  104d419

• More fixes for assertion parameters.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  5ade17d

• Almost done with the initial working example.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  ee56eaf

• Refactoring the UMC ASTs.

  Show description for 57afb53
  

  pramodsu

  authored and

  Shubham Sahai

  committed
  57afb53

• We have added support for the range rule.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  02a20ad

• constlb and constub rules.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  be834da

• cover properties properly support.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  8120ee5

• New rewriter.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  f77c40e

• a few minor additions to counting_2n.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  100792e

• adding the indLb rule which seems to work for now.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  8f2e1f1

• first attempt at model count proof.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  73ac002

• Compilation fix after merge.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  d6c6459

• fixed disjoint to be or rule

  

  ssahai

  committed
  97105bb

• updated the test example

  

  ssahai

  committed
  2caf963

• minor fix to example

  

  ssahai

  committed
  afd8fa0

• added UB rule

  

  ssahai

  committed
  4734acd

• minor edit: adding assert to UB rule - ensuring counting quantifier is applied on the same set of variables in each expression

  

  ssahai

  committed
  d696a7c

• added AndUB rule

  

  ssahai

  committed
  c7e0650

• added Disjoint rule

  

  ssahai

  committed
  249d920

• added injectivity rule

  

  ssahai

  committed
  8079384

• zkhat example

  

  ssahai

  committed
  80dcbb6

• parsing indUB. Rewriting is pending for now.

  

  ssahai

  committed
  b15cd63

• added support for lemmas via lemma block - parsing successfully

  

  ssahai

  committed
  2f19e33

• verifying the lemmas in the control block

  

  ssahai

  committed
  6ad096a

• indLB for zk-hat working now

  

  ssahai

  committed
  13466ed

• minor edits while playing around with examples.

  

  pramodsu

  authored and

  Shubham Sahai

  committed
  d5d1d02

• updated vim syntax file

  

  ssahai

  committed
  5829b6e

• minor edit to syntax file

  

  ssahai

  committed
  cbd5241

• added assumptions to range statement to cater symbolic bounds

  

  ssahai

  committed
  e18f5a4

• attempting Array shuffle example - constEQ going UNDEF

  

  ssahai

  committed
  d40d5c4

• fixed ite printing

  

  ssahai

  committed
  2d7a524

• fixed satonly decorator and assert printing

  

  ssahai

  committed
  d493f5b

• UFs can take more than one arguements now in IndLB

  

  ssahai

  committed
  5037993

• indLB can take more than one ys values

  

  ssahai

  committed
  049edb1

• asserts can be named

  

  ssahai

  committed
  9e0d1f8

• fixing printing of 2 : in case asserts have names

  

  ssahai

  committed
  8bb817f

• added descriptive names to rewritten asserts

  

  ssahai

  committed
  245a590

• fixed repetition of quantified variables in indLB

  

  ssahai

  committed
  d7824fd

• induction working for array shuffle

  

  ssahai

  committed
  04f9709

• added test for indLB. Working fine now

  

  Shubham Sahai

  committed
  4beacbc

• added indUB

  

  Shubham Sahai

  committed
  409de53

• updated/added tests for all the proof rules

  

  Shubham Sahai

  committed
  9b0eb83

• minor edit to fix warning while building the universal package

  

  Shubham Sahai

  committed
  eefb68b

• update author info in modelcounting extension

  

  Shubham Sahai

  committed
  8c9832c

• config options works with UMC now

  

  Shubham Sahai

  committed
  aa89b1a

• added counting script for zkHAT - motivating example from CAV20 paper

  

  ssahai

  committed
  b6677d0

• Merge branch 'ssahai/modelcounting' of github.com:uclid-org/uclid into ssahai/modelcounting

  

  Shubham Sahai

  committed
  a83a564