Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Aug 23, 2022

• don't be too smart around unsigneds

  

  Martin Suda

  committed
  f8866a3

  Copy full SHA for f8866a3

Commits on Aug 22, 2022

• Merge pull request #411 from vprover/martin-shuffling

  Show description for 42fd6b8
  quickbeam123

  authored
  42fd6b8

  Copy full SHA for 42fd6b8

• Merge branch 'master' into martin-shuffling

  

  Martin Suda

  committed
  76a2fe9

  Copy full SHA for 76a2fe9

• typo

  quickbeam123

  committed
  c0de882

  Copy full SHA for c0de882

• added a coefficient option for tweaking LRS's agressiveness (inspired by a discussion with Bernhard Gleiss)

  quickbeam123

  committed
  73e0f41

  Copy full SHA for 73e0f41

• whitespace

  quickbeam123

  committed
  f27144e

  Copy full SHA for f27144e

• comments and typos

  

  Martin Suda

  authored and

  quickbeam123

  committed
  5c2a294

  Copy full SHA for 5c2a294

• encompassment for Backward

  quickbeam123

  committed
  af6b3fb

  Copy full SHA for af6b3fb

• encompassment for Forward

  quickbeam123

  committed
  eb5108d

  Copy full SHA for eb5108d

• the option and first steps towards functionality

  quickbeam123

  committed
  7745898

  Copy full SHA for 7745898

Commits on Aug 20, 2022

• an option to keep old generators in sbeam enumeration strategy (without it, "-sa fmb -fmbas expand" on Problems/KRS/KRS185+1.p shamefully cycles)

  

  Martin Suda

  committed
  1e7ce18

  Copy full SHA for 1e7ce18

Commits on Aug 19, 2022

• no (deep) input shuffling with just randomTraversals

  quickbeam123

  committed
  1ed6637

  Copy full SHA for 1ed6637

• all other comments from Michael taken into account

  quickbeam123

  committed
  53ec168

  Copy full SHA for 53ec168

• fix comment

  quickbeam123

  committed
  2c3251f

  Copy full SHA for 2c3251f

• fix comment

  quickbeam123

  committed
  6900245

  Copy full SHA for 6900245

• a more informative comment

  quickbeam123

  committed
  c6d6d10

  Copy full SHA for c6d6d10

• add Shell/Shuffling.hpp

  quickbeam123

  committed
  cb7621e

  Copy full SHA for cb7621e

Commits on Aug 18, 2022

• don't count parsing into the limit

  

  Martin Suda

  authored and

  quickbeam123

  committed
  f2a0298

  Copy full SHA for f2a0298

• made polarity flipping proof documenting

  quickbeam123

  committed
  96123d2

  Copy full SHA for 96123d2

• flipped eq_proxy predicate must be translated as such to Z3

  quickbeam123

  committed
  c27a1d9

  Copy full SHA for c27a1d9

• a less strict warning about shapes (under inst_gen)

  quickbeam123

  committed
  432aeb3

  Copy full SHA for 432aeb3

• special default theorySplitQueueCutoffs need to go as well

  quickbeam123

  committed
  5177a12

  Copy full SHA for 5177a12

• theories imply equality for options checking

  quickbeam123

  committed
  cbab3dc

  Copy full SHA for cbab3dc

• make these two other queues defaultable

  quickbeam123

  committed
  b192594

  Copy full SHA for b192594

• thsq OK also without theories

  quickbeam123

  committed
  6cdff35

  Copy full SHA for 6cdff35

• is this the right header?

  quickbeam123

  committed
  6ee56cf

  Copy full SHA for 6ee56cf

• Revert "also randomize buckets, under randomAWTiebreak"

  Show description for 6d2f342
  quickbeam123

  committed
  6d2f342

  Copy full SHA for 6d2f342

Commits on Aug 16, 2022

• not only Units but also Clauses and FormulaUnits should hash on number() and not on the raw pointer (mostly, for the reproducibility of interation orders over Maps and Sets)

  Show description for c84b1d6
  

  Martin Suda

  committed
  c84b1d6

  Copy full SHA for c84b1d6

• fix: makes factorial time subterm investigation linear

  

  Johannes Schoisswohl

  authored and

  quickbeam123

  committed
  fd37d9b

  Copy full SHA for fd37d9b

• more uniform index names

  quickbeam123

  committed
  d52d662

  Copy full SHA for d52d662

• using Set instead of DHSet will make the order deterministic (as soon as Michael fixes Hash to specialize to Clauses and FormulaUnits the same way it specializes to Units, i.e. by hashing by number())

  quickbeam123

  committed
  a90b6db

  Copy full SHA for a90b6db

• don't special-hack reserve GENERATING_SUBST_TREE for SaturationAlgorithm in IndexManager

  quickbeam123

  committed
  5a81abb

  Copy full SHA for 5a81abb

• have active clauses carry their own content in a DHSet (no reliance on any index)

  quickbeam123

  committed
  ef73b5f

  Copy full SHA for ef73b5f

Commits on Aug 4, 2022

• Revert "explicit instantiations not needed" - they are with gcc

  Show description for e5671f8
  quickbeam123

  committed
  e5671f8

  Copy full SHA for e5671f8

Commits on Aug 3, 2022

• Merge pull request #391 from vprover/ahmed-improved-ski-kbo

  Show description for d0e1a65
  quickbeam123

  authored
  d0e1a65

  Copy full SHA for d0e1a65