PR to track HOL changes, don't merge#822

Open

mezpusz wants to merge 221 commits into

Commits on Jul 19, 2022

Commits on Aug 2, 2022

Commits on Aug 3, 2022

Commits on Aug 4, 2022

Commits on Aug 8, 2022

Commits on Aug 9, 2022

fixing bugs relating to pseudo-higher-order problems (first-order problems in higher-order syntax)
ibnyusuf
committed
file missing from previous commit
ibnyusuf
committed

Commits on Aug 15, 2022

bug fix
ibnyusuf
committed

Commits on Aug 16, 2022

Merge branch 'master' into ahmed-uwa-stack-of-handlers
Martin Suda
committed

Commits on Aug 23, 2022

substitutions by default have no constraints
ibnyusuf
committed

Commits on Aug 31, 2022

merging in latest master
ibnyusuf
committed
removed NOT_IMPLEMENTED from mismatch handler hierarchy
Johannes Schoisswohl
committed
made AtomicMismatchHandler not inherit from TermTransformer
Johannes Schoisswohl
committed
replaced linkedlist by stack
Johannes Schoisswohl
committed

Commits on Sep 1, 2022

prelaced raw pointers by unique_ptr
Johannes Schoisswohl
committed
made uwa option a field of uwa handler instead of static read from options
Johannes Schoisswohl
committed
made switch future proof so the compiler will emit warnings when variants of UWA options are being added
Johannes Schoisswohl
committed
renamed getHandler() -> mismatchHandler() to increase readability at caller sites
Johannes Schoisswohl
committed
removing code related to combinators and started work on new calculus
ibnyusuf
committed
made unit tests for uwa machine checked
Johannes Schoisswohl
committed
performance improvement
Johannes Schoisswohl
committed
Merge pull request #414 from vprover/joe-uwa-stack-of-handlers
joe-hauns
authored
merging Joe's changes with mine
ibnyusuf
committed
code refinement
ibnyusuf
committed
changing beta reduction code
ibnyusuf
committed
merging in new term transformer code
ibnyusuf
committed
finishing beta reduction and adding unit tests
ibnyusuf
committed

Commits on Sep 6, 2022

working on lambda higher-order calculus
ibnyusuf
committed

Commits on Sep 8, 2022

bug fixes and code improvements
ibnyusuf
committed

Commits on Sep 13, 2022

intermediate stage, working on Imitation Projection
ibnyusuf
committed

Commits on Sep 14, 2022

adding pretty HOL printing and completing implementation of ImitateProject
ibnyusuf
committed

Commits on Sep 19, 2022

improving term printing and refactoring code for producing general bindings
ibnyusuf
committed

Commits on Sep 20, 2022

refactoring primitive instantiation to use general bindings. Attempting to redefine empty clause
ibnyusuf
committed

Commits on Sep 22, 2022

various extensions and bug fixes. Can currently solve many problems not provable by other solvers
ibnyusuf
committed

Commits on Sep 23, 2022

now project terms with De Bruijn indices at their head
ibnyusuf
committed

Commits on Sep 25, 2022

Commits on Sep 26, 2022

minor bug fix and adding comments
ibnyusuf
committed

Commits on Sep 27, 2022

updating injectivity reasoning WIP
ibnyusuf
committed

Commits on Oct 13, 2022

removing stray print
ibnyusuf
committed

Commits on Feb 17, 2023

adding missing compiler directive and improving pretty printing
ibnyusuf
committed

Commits on Mar 21, 2023

merging into new abstraction branch. also adding some missing compiler directives for HOL stuff
ibnyusuf
committed

Commits on Mar 24, 2023

merging in latest changes from substitution tree refactor. Starting work in higher-order unification and matching.
ibnyusuf
committed

Commits on Mar 31, 2023

Commits on Apr 2, 2023

fixing a bug relating to equality factoring and polymorphism
ibnyusuf
committed

Commits on Apr 3, 2023

new unit test for equality factoring
ibnyusuf
committed

Commits on Apr 4, 2023

preparing to create non-splittable tree nodes
ibnyusuf
committed

Commits on Apr 5, 2023

further work on adding non-splitting functionality. Looking harder than I had hoped
ibnyusuf
committed

Commits on Apr 11, 2023

Commits on Apr 13, 2023

working on HOL unification. need to add many unit tests to ensure that things working as expected
ibnyusuf
committed

Commits on Apr 15, 2023

adding unit tests for unification with unsplittable nodes and fixpoint oracle. seems to be working nices
ibnyusuf
committed

Commits on Apr 23, 2023

HOU still in a state of flux. About to start major change relating to storing of variables in Vampire. May need reverting
ibnyusuf
committed

Commits on Apr 28, 2023

major changes to facilitate RobSubstitution with both TermSpecs and TermLists. Compiling. UNTESTED
ibnyusuf
committed

Commits on May 2, 2023

Commits on May 5, 2023

about to start work on higher-order unification proper
ibnyusuf
committed

Commits on May 9, 2023

higher-order unification implemented and compiling. not tested
ibnyusuf
committed

Commits on May 11, 2023

various bug fixes. HOL unification seems to be working at the moment. To start on HOL matching
ibnyusuf
committed

Commits on May 12, 2023

changes to support higher-order (lambda-free) matching. WIP
ibnyusuf
committed

Commits on May 15, 2023

lambda-free matching now implemented. more unit tests need to be written
ibnyusuf
committed

Commits on May 16, 2023

Commits on May 17, 2023

adding literal matching and updating various subsumption inferences. these are untested as yet
ibnyusuf
committed

Commits on May 19, 2023

fixing HOL matching. Need to test subsumption still
ibnyusuf
committed

Commits on May 23, 2023

fixing HOL unification. WIP. Problem with constraints that contain loose bound vars
ibnyusuf
committed

Commits on May 25, 2023

bug fixing, but many remain
ibnyusuf
committed

Commits on May 26, 2023

Commits on May 27, 2023

Commits on May 28, 2023

Commits on May 29, 2023

bug fixing
ibnyusuf
committed

Commits on May 30, 2023

Commits on May 31, 2023

Commits on Jun 1, 2023

Commits on Jun 2, 2023

Commits on Jun 5, 2023

bug fixing and adding enw inference, bool instantiation (not well tested yet)
ibnyusuf
committed
a comment and a minor extension of allowed literal selection values

Martin Suda
authored and
ibnyusuf
committed
extended StringUtils

Martin Suda
authored and
ibnyusuf
committed
starting to work on strategy sampling in Options

Martin Suda
authored and
ibnyusuf
committed
Resolving conflict in cherry-pick

Martin Suda
authored and
ibnyusuf
committed
put kbo things under OptionTag::SATURATION

Martin Suda
authored and
ibnyusuf
committed
Fixing cherry-pick conflict

Martin Suda
authored and
ibnyusuf
committed
more robust value lookup

Martin Suda
authored and
ibnyusuf
committed
more precise description

Martin Suda
authored and
ibnyusuf
committed
shifted geometric distribution

Martin Suda
authored and
ibnyusuf
committed
sine_tolerance should actually allow -1.0 (and not 0.0) as a special value

Martin Suda
authored and
ibnyusuf
committed
allow for negation in rule conditions

Martin Suda
authored and
ibnyusuf
committed
uniform float sampling and some avatar stuff

Martin Suda
authored and
ibnyusuf
committed
_splittingFlushQuotient only makes sense with non-zero _splittingFlushPeriod

Martin Suda
authored and
ibnyusuf
committed
need a different separator for ~u2r, and finished avatar

Martin Suda
authored and
ibnyusuf
committed
added ~ui sampler
Martin Suda
committed
added HO stuff uniformly
Martin Suda
committed
sampler file update
quickbeam123
committed

Commits on Jun 7, 2023

bug fixing
ibnyusuf
committed
fixing bugs
ibnyusuf
committed

Commits on Jun 8, 2023

Commits on Jun 9, 2023

Commits on Jun 10, 2023

Commits on Jun 11, 2023

Commits on Jun 12, 2023

Commits on Jun 13, 2023

Commits on Jun 15, 2023

fixing printing issue that was causing SIGSEG on a few proof prints
ibnyusuf
committed

Commits on Jun 17, 2023

sample new options
quickbeam123
committed

Commits on Jun 19, 2023

Commits on Jun 22, 2023

some post CASC submission code cleanup
ibnyusuf
committed

Commits on Jul 12, 2023

actually use HoFeaturesMultiSplitPassiveClauseContainer
Martin Suda
committed

Commits on Jul 13, 2023

Commits on Jul 14, 2023

new SLH sched using a bit of hfsq now made official under SNAKE_SLH while the debug SNAKE_SLH2 is gone
quickbeam123
committed

Commits on Jul 16, 2023

also a new HOL sched sprinkled with hfsq
quickbeam123
committed

Commits on Aug 8, 2023

Commits on Aug 17, 2023

fixing TH1 bug wherein we were attempting to turn type quantifiers into PI and SIGMA functions
ibnyusuf
committed

Commits on Aug 21, 2023

added first-order sub-schedule to SLH
quickbeam123
committed

Commits on Aug 23, 2023

fixing TH1 bug. Along the way, making SortHelper::tryGetVariableSort poly safe
ibnyusuf
committed

Commits on Aug 29, 2023

fix leaking index bug
ibnyusuf
committed

Commits on Sep 7, 2023

adding a prelim version of a TH1 schedule
Martin Suda
committed

Commits on Sep 11, 2023

th1_sledgehammering/TH1.txt - but done in a weighted way (problems already covered by the other subscheds weigh less)
quickbeam123
committed

Commits on Oct 4, 2023

samplerEx named officially samplerHOL
Martin Suda
committed
two more options officially sampled
Martin Suda
committed

Commits on Jan 2, 2025

adding check to esnure we don't run UWA with HOL problems
bhayat-quantinuum
committed