aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'proofsearch-import/master'Richard Qin18 hours63-0/+6611
|\
| * feat: enhance clang-tidy configuration and improve code quality across ↵Richard Qin2026-04-0813-159/+198
| | | | | | | | multiple files
| * refactor: rename struct members to follow trailing underscore naming ↵Richard Qin2026-04-0731-809/+877
| | | | | | | | convention across core, search, and frontend components
| * style: reformat codebase with consistent indentationRichard Qin2026-04-0449-354/+294
| |
| * feat: add copyright and license disclaimer to program startup outputRichard Qin2026-04-041-0/+5
| |
| * feat: implement pretty-printing for variables and proof step references in ↵Richard Qin2026-04-042-8/+78
| | | | | | | | proof trace output
| * feat: implement command-line interface and add end-to-end propositional ↵Richard Qin2026-04-045-13/+275
| | | | | | | | logic test suite
| * feat: implement proof trace extraction and add proof trace testRichard Qin2026-04-044-9/+365
| |
| * feat: implement saturation-based resolution loop in Prover classRichard Qin2026-04-045-10/+349
| |
| * feat: implement clause subsumption and tautology detection logic with ↵Richard Qin2026-04-046-0/+250
| | | | | | | | associated unit tests
| * feat: implement variable renaming and update resolution logic to prevent ↵Richard Qin2026-04-043-3/+399
| | | | | | | | variable collisions
| * feat: implement substitution logic and unify/applySubstitution functions for ↵Richard Qin2026-04-036-10/+561
| | | | | | | | term resolution
| * feat: implement core term, symbol, and clause storage logic with ↵Richard Qin2026-04-038-14/+481
| | | | | | | | canonicalization support
| * fix: remove files that should be ignoredRichard Qin2026-04-0317-0/+0
| |
| * refactor: replace string-based formula representation with interned ↵Richard Qin2026-04-027-24/+416
| | | | | | | | SymbolIds and introduce stateful Clausifier for TPTP parsing
| * Initial commit: Build project architecture, define interfaces, write ↵Richard Qin2026-04-0274-0/+3476
| | | | documentation, with the help of Claude
* [Support] Add MathExtrasRichard Qin8 days3-0/+1148
|
* [Support] Add RCCSupport target and naming rulesRichard Qin8 days3-78/+35
|
* [ADT] Add function_ref to ADTRichard Qin9 days1-0/+112
| | | | Signed-off-by: Richard Qin <richard.qin.x@gmail.com>
* [Support] Format codeRichard Qin9 days6-239/+343
| | | | Signed-off-by: Richard Qin <richard.qin.x@gmail.com>
* [Utils] Use LLVM format and tidy toolsRichard Qin9 days7-322/+2806
| | | | Signed-off-by: Richard Qin <richard.qin.x@gmail.com>
* [Support] Add ErrorOr supportRichard Qin9 days1-0/+293
| | | | Signed-off-by: Richard Qin <richard.qin.x@gmail.com>
* [Support] Add errno supportRichard Qin9 days2-0/+140
| | | | Signed-off-by: Richard Qin <richard.qin.x@gmail.com>
* [Support] Add compiler abstraction supportRichard Qin9 days1-0/+843
|
* [CMake] Add RCC platform configuration checksRichard Qin10 days15-0/+3438
|
* [CMake] Generate RCC configuration headersRichard Qin10 days3-1/+477
|
* [RCC] Add Basic Data TypesRichard Qin10 days2-0/+102
| | | | Signed-off-by: Richard Qin <richard.qin.x@gmail.com>
* [Dev] Configure build presets and code checksRichard Qin10 days5-47/+160
|
* [CMake] Establish RCC and CFront builds and package exportsRichard Qin11 days19-78/+585
|
* [CMake] Add compiler options and target helpersRichard Qin11 days5-0/+1407
|
* Rename LICENSE to COPYINGRichard Qin12 days1-0/+0
| | | | Signed-off-by: Richard Qin <richard.qin.x@gmail.com>
* [MIR] Merge identical scalar type branchesRichard-Qin-X2026-08-291-5/+1
|
* [RISCV] Merge identical selector casesRichard-Qin-X2026-08-291-2/+0
|
* [RISCV] Widen jump table entry size arithmeticRichard-Qin-X2026-08-291-1/+1
|
* [RISCV] Reuse validated Zcmp frame offsetsRichard-Qin-X2026-08-291-8/+12
|
* [RISCV] Assert merged memory offset invariantsRichard-Qin-X2026-08-291-0/+2
|
* [RISCV] Reuse validated move registersRichard-Qin-X2026-08-291-5/+9
|
* [GlobalISel] Bind register bank optionals onceRichard-Qin-X2026-08-291-6/+9
|
* [GlobalISel] Assert vector element type invariantsRichard-Qin-X2026-08-291-3/+7
|
* [CodeGen] Bind virtual register types onceRichard-Qin-X2026-08-291-2/+3
|
* [CodeGen] Apply LLVM declaration styleRichard-Qin-X2026-08-293-3/+3
|
* [TableGen] Assert normalized MC pseudo operandsRichard-Qin-X2026-08-291-0/+2
|
* [TableGen] Preserve optional target description valuesRichard-Qin-X2026-08-292-9/+10
|
* [GlobalISel] Remove redundant PHI narrowing checksRichard-Qin-X2026-08-291-12/+7
|
* [CodeGen] Complete LaneMask bitwise operationsRichard-Qin-X2026-08-284-17/+19
|
* [Support] Use standard power-of-two checksRichard-Qin-X2026-08-288-39/+20
|
* [CMake] Remove unused clang-tidy file registrationRichard-Qin-X2026-08-2838-281/+81
|
* [RISCV] Complete Zcmp frame lowering and optimizationRichard-Qin-X2026-08-288-210/+439
|
* [RISCV] Generate complete Zcmp instruction definitionsRichard-Qin-X2026-08-286-44/+217
|
* [CodeGen] Add target machine registryRichard-Qin-X2026-08-2824-233/+735
|
generated by cgit v1.2.3 (git 2.46.0) at 2026-10-30 12:34:01 +0000