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

Open

yvizel wants to merge 21 commits intodiffblue:developfrom

yvizel:develop

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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

Commits on Feb 24, 2025

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

Enabling large step encoding using a flag

Comparison operators for chcs

Clean up old code

Small fix

Extracting new chcs after transformation

Moving from std::set to std::unordered_set

Naming conventions, unsigned -> size_t

Renaming types and function names, and adjusments to changes in API

Adjusting API changes

Equivalent query clauses may represent different properties. Allow it in CHC db

Adding regression tests for large step encoding of CHCs

Some comments and minor modifications

Removed whitespace

Removed include

Missing commit

Removing redundant include, and fixing function arguments

Changing user_relations function declaration

clang format, and minor fixes to is_query, is_fact

Small fix

Commits on Apr 5, 2025

Merge branch 'diffblue:develop' into develop