Commits

Branch selector

 main

User selector

All users

Datepicker

All time

Commit History

Commits on Oct 21, 2024

• Generalize more string RARE rules to sequences (cvc5#11291)

  ajreynol

  authored
  63eb5e6

• Fix proof checker for quant var reodering (cvc5#11295)

  ajreynol

  authored
  504fcaa

Commits on Oct 19, 2024

• Make arith operator elimination proof producing (cvc5#11280)

  ajreynol

  authored
  79b5507

Commits on Oct 18, 2024

• Implement proof support for preprocessing str.from_code (cvc5#11285)

  ajreynol

  authored
  4b5a81f

• Expand ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV (cvc5#11288)

  

  ajreynol

  and

  abdoo8080

  authored
  a9d5a44

Commits on Oct 17, 2024

• Add missing proofs for conflicts in sets (cvc5#11292)

  ajreynol

  authored
  69e0d08

Commits on Oct 16, 2024

• [proofs] [alethe] Print valid arguments in hole steps (cvc5#11287)

  HanielB

  authored
  ff5c97b

• Minor change to TrustId::SUBS_EQ (cvc5#11289)

  ajreynol

  authored
  8c74b38

• Make BvEagerAtom pass proof producing (cvc5#11279)

  ajreynol

  authored
  c4d8bce

• Add rational parsing to RARE (cvc5#11282)

  ajreynol

  authored
  ad7ce61

Commits on Oct 15, 2024

• Fix internal FP operator printing in LFSC (cvc5#11281)

  ajreynol

  authored
  0e9f8d6

• Guard more corner cases of safe-options (cvc5#11274)

  ajreynol

  authored
  fb47b96

Commits on Oct 14, 2024

• [proofs] [alethe] Improve error flagging to catch unsupported types (cvc5#11235)

  HanielB

  authored
  7ec5106

• Fix DSL proof reconstruction for several corner cases (cvc5#11270)

  ajreynol

  authored
  9ddaa54

• Fix proofs for alpha equivalence with variable shadowing (cvc5#11237)

  ajreynol

  authored
  0570e78

Commits on Oct 11, 2024

• cmake: Require Java 1.8 (cvc5#11275)

  daniel-larraz

  authored
  3f52b26

Commits on Oct 10, 2024

• Cleanup and improve instantiation level tracking (cvc5#11269)

  ajreynol

  authored
  e6bcb31

• Adding missing check for bagsExp (cvc5#11273)

  ajreynol

  authored
  49e23e7

• Fix proofs + cadical in set defaults (cvc5#11272)

  ajreynol

  authored
  20250cf

Commits on Oct 9, 2024

• Remove special handling of proofs in PropPfManager (cvc5#11254)

  ajreynol

  authored
  4198c44

Commits on Oct 8, 2024

• Allow theories to occur in a logic name in any order (cvc5#11207)

  daniel-larraz

  authored
  f1f33a2

• Fix model unsoundness in bounded set quantification (cvc5#11268)

  ajreynol

  authored
  6c6e365

Commits on Oct 4, 2024

• cadical: Initialize external propagator prior to adding clauses. (cvc5#11264)

  

  mpreiner

  and

  aniemetz

  authored
  bb35335

• Minor fixes for print benchmark utility (cvc5#11266)

  

  ajreynol

  and

  aniemetz

  authored
  fc5678d

• cadical: Properly disable obsolete activation literals. (cvc5#11263)

  

  mpreiner

  and

  aniemetz

  authored
  af60e1c

• Downgrade the required use of fresh-binder to a warning (cvc5#11256)

  

  ajreynol

  and

  aniemetz

  authored
  9e7ee41

• preprocessing: Refactor to not use NodeManager::currentNM() (cvc5#11250)

  

  daniel-larraz

  and

  aniemetz

  authored
  f50a593

• parser: Introduce parsing mode to configure level of strictness. (cvc5#11261)

  aniemetz

  authored
  ecd9558

• Improve support for non-closed kinds in mbqi (cvc5#11258)

  ajreynol

  authored
  d3ea670

• printer: Refactor to enforce deterministic order of declarations. (cvc5#11259)

  aniemetz

  authored
  907c17c

• alethe/alf/lfsc: Refactor to not use NodeManager::currentNM() (cvc5#11253)

  daniel-larraz

  authored
  2baeefe

Commits on Oct 3, 2024

• Simplifications and improvements for the CPC printer (cvc5#11242)

  ajreynol

  authored
  b08221c

• Generate consistent variable names in CPC+RARE signature (cvc5#11247)

  ajreynol

  authored
  e601d9c

• Do not check for shadowed variables with --wf-checking (cvc5#11260)

  ajreynol

  authored
  f996d33

• Fix format specifiers in QuickStart C example (cvc5#11251)

  daniel-larraz

  authored
  4f582c1

Pagination

PreviousNext