Adding large-step encoding for CHCs in CProver (no [required] changes to the solver)#8465

Open

yvizel wants to merge 22 commits intodiffblue:developfrom

Commits on Feb 24, 2025

Adding CHCs data structures and utilities for resolution-based large step encoding

Yakir Vizel
authored and
yvizel
committed
Enabling large step encoding using a flag

Yakir Vizel
authored and
yvizel
committed
Comparison operators for chcs

Yakir Vizel
authored and
yvizel
committed
Clean up old code

Yakir Vizel
authored and
yvizel
committed
Small fix

Yakir Vizel
authored and
yvizel
committed
Extracting new chcs after transformation

Yakir Vizel
authored and
yvizel
committed
Moving from std::set to std::unordered_set

Yakir Vizel
authored and
yvizel
committed
Naming conventions, unsigned -> size_t

Yakir Vizel
authored and
yvizel
committed
Renaming types and function names, and adjusments to changes in API

Yakir Vizel
authored and
yvizel
committed
Adjusting API changes

Yakir Vizel
authored and
yvizel
committed
Equivalent query clauses may represent different properties. Allow it in CHC db

Yakir Vizel
authored and
yvizel
committed
Adding regression tests for large step encoding of CHCs

Yakir Vizel
authored and
yvizel
committed
Some comments and minor modifications

Yakir Vizel
authored and
yvizel
committed
Removed whitespace

Yakir Vizel
authored and
yvizel
committed
Removed include

Yakir Vizel
authored and
yvizel
committed
Missing commit

Yakir Vizel
authored and
yvizel
committed
Removing redundant include, and fixing function arguments

Yakir Vizel
authored and
yvizel
committed
Changing user_relations function declaration
yvizel
committed
clang format, and minor fixes to is_query, is_fact
yvizel
committed
Small fix
yvizel
committed

Commits on Apr 5, 2025

Merge branch 'diffblue:develop' into develop
yvizel
authored

Commits on Feb 7, 2026

Merge branch 'diffblue:develop' into develop
yvizel
authored