Solver-level caching to skip re-solving identical constraint sets

[hassanaleem]

Hi team,

While experimenting with SymCC + QSYM, I noticed that the same constraint set is sometimes sent to Z3 multiple times. (The duplicates originate in Solver::addConstraint() → Solver::check() when successive branches add an already-solved conjunction.)

For reference, my test program is a branchless version of Prim's Algorithm for Minimum Spanning Tree

I prototyped a solution to hash the solution in an unordered map to avoid duplicated calls being sent to solver

Questions for maintainers

• Do you foresee scenarios where this hurts exploration? e.g., memory blow-up, interference with incremental solving or anything else

• SymCC already avoids trivial duplicates in the addJcc function —is there a design reason to let identical sets reach Z3 anyway?

Happy to adapt the approach to fit the codebase style or run larger benchmarks.

Thanks for the great work on SymCC!