FMCAD25 - #1

Open

kunalsheth wants to merge 79 commits into

mainfrom

fmcad25-experiments

Commits on Apr 10, 2025

Delete unnecessary 3rd party implementation of `std::optional`.
kunalsheth
committed
87a02d4
Updated IDE configuration files
kunalsheth
committed
fc1a28e
Add statistics counters to pattern matching code.
kunalsheth
committed
4182249
Sort clause prior to pattern matching to avoid fruitless substitution branches.
kunalsheth
committed
e0f2fa5
Fruitless attempt at creating estimation heuristic for cost of pattern matching.
kunalsheth
committed
f8f5c79
Implement predicate statistics collector for future heuristic development.
kunalsheth
committed
72c7cd9
Plumbing for efficient/cached heuristics collection.
kunalsheth
committed
b4d3491
Fruitless attempt at optimizing `attempt_substitution()`.
kunalsheth
committed
8c076f4
Write `make_conjunction_SKIP_CHECKS_KUNAL_HACK()` to slightly speed up creation on conjunctions for learned clauses.
kunalsheth
committed
c505d6c
sat_solver.cc cleanup.
kunalsheth
committed
e39067a
Bolt in statistics, telemetry, and logging for benchmarking run - April 10, 2025.
kunalsheth
committed
3282241

Commits on Apr 11, 2025

Commits on Apr 14, 2025

Move pattern_matching_test.cc from /solver to /util to match it's corresponding /src file.
kunalsheth
committed
4e22b15
Upgrade regression model to small neural network.
kunalsheth
committed
a31ba7e
Revert "REVERT ME - changes for blasty training."
kunalsheth
committed
fa82b66
Fix subtle segfault in trace mode.
kunalsheth
committed
6d58de6
Improve logging for benchmarking run!
kunalsheth
committed
ecf8067
Revert "Upgrade SAT solver from PicoSAT to CaDiCaL."
kunalsheth
committed
9b68c59

Commits on Apr 17, 2025

Commits on Apr 21, 2025

Commits on Apr 23, 2025

Commits on Apr 25, 2025

Fix build on CentOS with GCC 14 (sherlock).
kunalsheth
committed
37e2900
Fix includes for more restrictive headers on CentOS
kunalsheth
committed
f76a99a

Commits on Apr 26, 2025

Make cmake STATIC
kunalsheth
committed
4122e06
Consolidate experimental build flags into version.h to avoid accidents when benchmarking.
kunalsheth
committed
7539e55
Add additional build flags for using partial v.s. full SAT models.
kunalsheth
committed
e953754
Add pattern matching upper timeout to version.h.
kunalsheth
committed
d9f2842
Downgrade verbose `Finding matches for:...` logs to DEBUG.
kunalsheth
committed
2d3b259
Remove no longer necessary permutation check in pmtg.cc.
kunalsheth
committed
9f40016

Commits on Apr 27, 2025

Commits on Apr 30, 2025

Commits on May 13, 2025

Add labels to theory auditor.
kunalsheth
committed
c6d544a

Commits on May 14, 2025

Remove SAT inverval behavior from pattern matching.
kunalsheth
committed
2e74821

Commits on Jul 22, 2025

Get rid of `EST` heuristic mess.
kunalsheth
committed
9a660e7
Improve pattern matching performance using alpha-aware hashing.
kunalsheth
committed
4bb5528

Commits on Aug 11, 2025

ASPLOS circuit tweaks.
kunalsheth
committed
b56bb15

Commits on Aug 12, 2025

Tweak PM thresholds and timeouts
kunalsheth
committed
cf6dc89
Speed up prints for benchmarking.
kunalsheth
committed
0eb5200
Remove lemma/assertion statistics from collected data for benchmarking.
kunalsheth
committed
484e65f