Age | Commit message (Collapse) | Author |
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
independent (#2749)
--cegqi-si=none previously disabled pre/post-condition templates for invariant synthesis. This PR eliminates this dependency.
There are no major code changes in this PR, unfortunately a large block of code changed indentation so I refactored it to be more up to date with the coding guidelines.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Recognizes when the conjecture has conflicting I/O pairs. Also includes a minor change to the default behavior of PBE.
This change broke a delicate regression array_search_2, which I fixed by adding some additional options to make it more robust.
After this PR, we immediately find 4/7 unsolved in PBE strings of sygusComp 2018 to be infeasible.
|
|
|
|
|
|
|
|
|
|
|
|
Improves the existing implementation for sygus-active-gen=basic.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Use std::shuffle (with Random as the unified random generator) instead
of std::random_shuffle for deterministic, reproducable random shuffling.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|