usage
python run.py xxx.aag
- one-context-for-all-frame solver (good to re-use the solving context) [arbrad 15]
- on-demand logic cone extraction (partially implemented) [arbrad 15]
- ctgDown / Down in MIC [Z Hassan 13]
- ternary simulation - for predecessor aggresive generalization (not suitable for python implementation) [N Een 11]
- infinite mic attempt (suggestion from arbrad) [arbrad 15]
- literals ordering according to their appearance in the trace (frequency), both in predecessor generalization (ternary sim) and inductive generalization (mic) [arbrad 15]
- IC3 with innards for better generalization [WIP] [Rohit Dureja 21]
- robust sanity checker
- rich console output for logging and monitoring
- cube and frame management system (add, join, push, etc.)
- unsat core extraction for inductive generalization and predecessor generalization
- dynamically load the transition relation in solver
- reset solver with some frequency (keep the loaded logic relatively small)
- every time check assumption, some part (such as tr, should not be loaded every time, rather than push it to the solver at the beginning)
- use kissat or some SOTA SAT solver rather than z3
- use graceful strategy for propagating phase when solving the SAT problem (adjust the solving tactic in sovlver)
- backward ic3
- frame extending for solving SAT problem faster (mentioned in IC3, PDR and friends)
- bring in the literal add/drop info (times, etc.) to the sat solver to facilitate the solving process (CDCL, etc.)