Commits

Breadcrumbs

History for

on9a3ac3f

User selector

All users

Datepicker

All time

Commit History

Commits on Nov 19, 2024

• Fix some bugs with ARITH_TIGHT_* rules. (#145)

  abdoo8080

  authored
  9a3ac3f

Commits on Nov 17, 2024

• Sync with cvc5 main. (#144)

  Show description for 71ac743
  abdoo8080

  authored
  71ac743

• Update toolchain to 4.13. (#143)

  Show description for 4803bab
  abdoo8080

  authored
  4803bab

Commits on Oct 23, 2024

• Optimize Rat's polynorm and fix bugs. (#138)

  Show description for f0e6b56
  abdoo8080

  authored
  f0e6b56

Commits on Oct 11, 2024

• Optimize congruence proof step reconstruction. (#135)

  Show description for 4fcc41d
  abdoo8080

  authored
  4fcc41d

Commits on Oct 10, 2024

• Add profiling information. (#134)

  abdoo8080

  authored
  6078d77

Commits on Oct 6, 2024

• Refactor smt_rw tactic. (#132)

  abdoo8080

  authored
  563b1be

Commits on Oct 5, 2024

• Further fixes to duplicate variable names. (#131)

  abdoo8080

  authored
  68ba819

Commits on Oct 2, 2024

• Re-enable caching during translation. (#130)

  abdoo8080

  authored
  0b41804

Commits on Oct 1, 2024

• Fix duplicate variable naming issues. (#129)

  Show description for 82a6584
  abdoo8080

  authored
  82a6584

Commits on Sep 26, 2024

• Support ARITH_POLY_NORM_REL. (#127)

  abdoo8080

  authored
  d5c894b

Commits on Jul 12, 2024

• Fix bug with Iff elimination. (#123)

  abdoo8080

  authored
  b332ae4

Commits on Jul 8, 2024

• chore: bump Lean to v4.9.0 (#119)

  Show description for 91ac7f4
  joewatt95

  authored
  91ac7f4

Commits on Jun 24, 2024

• Split proof reconstruction for integers and reals. (#112)

  abdoo8080

  authored
  2899f02

• Fix solver tests. (#117)

  abdoo8080

  authored
  921d31e

Commits on Jun 12, 2024

• chore: bump to v4.8.0 (#113)

  Show description for 9dff101
  AdrienChampion

  authored
  9dff101

Commits on Jun 7, 2024

• Support more arithmetic rewrites. (#111)

  abdoo8080

  authored
  64d482b

Commits on Jun 6, 2024

• Add support for QUANT_MINISCOPE rewrite rule. (#108)

  abdoo8080

  authored
  fb6743a

Commits on Jun 2, 2024

• Sync with cvc5 main. (#107)

  abdoo8080

  authored
  6c40c29

Commits on May 27, 2024

• Support MacOS AArch64. (#105)

  abdoo8080

  authored
  3049bb1

• Fix bugs and support more Bool and quantifier rewrites. (#104)

  Show description for 46c5a9e
  abdoo8080

  authored
  46c5a9e

Commits on May 25, 2024

• Only track fvars needed by translation. (#102)

  abdoo8080

  authored
  b720017

Commits on May 23, 2024

• Split smt tactic into a meta program and a tactic driver. (#101)

  abdoo8080

  authored
  73e3fdf

• Fix and optimize reconstruction of proofs with quantifiers. (#99)

  Show description for 40caffd
  abdoo8080

  authored
  40caffd

• Fix and optimize AC norm. (#98)

  Show description for b28f919
  abdoo8080

  authored
  b28f919

Commits on May 9, 2024

• Support bitblasted addition. (#93)

  abdoo8080

  authored
  0404837

• Cleanup tracing and profiling options. (#92)

  abdoo8080

  authored
  fc8b5f9

Commits on May 6, 2024

• Fix and optimize smtCongr tactic. (#90)

  abdoo8080

  authored
  65720b9

• Support EXISTS_ELIM and DISTINCT_ELIM rules. (#89)

  Show description for f5a2b42
  abdoo8080

  authored
  f5a2b42

Commits on Apr 29, 2024

• Support linear Integer and Real arithmetic. (#84)

  Show description for 53d77a6
  abdoo8080

  authored
  53d77a6

Commits on Mar 5, 2024

• Breakdown proof reconstruction file. (#81)

  abdoo8080

  authored
  8e98543

• Replace Rat with Real and stop unfolding type class instantiations. (#80)

  Show description for d529a59
  abdoo8080

  authored
  d529a59

Commits on Feb 27, 2024

• Add minimum support for BitVec. (#79)

  abdoo8080

  authored
  f8cfd76

Commits on Feb 26, 2024

• Initial Non-linear arithmetic + Porting Rat to Real (#73)

  Show description for 25beb64
  tomaz1502

  authored
  25beb64

• Add initial support for skolems. (#78)

  abdoo8080

  authored
  b3c3b41

Pagination

Previous

Next