Fine-grained strategy improvement#7

Open

tm507211 wants to merge 12 commits intozkincaid:modernfrom tm507211:modern

+3,151-1,036

Commits on Jun 7, 2021

Fixes nested loop forest computation, to compute the "expected" loop headers for reducible CFG rather than an arbitrary loop header per loop
tm507211
committed

Commits on May 31, 2022

quantify_consts decapture fix
JakeSilverman
authored

Commits on Jun 13, 2022

miniscoping

JakeSilverman
authored and
tm507211
committed
simpler miniscoping

JakeSilverman
authored and
tm507211
committed
flattening

JakeSilverman
authored and
tm507211
committed
Merge branch 'zkincaid/duet/srk/modern' into 'tm507211/srk/modern'
tm507211
committed
Adds the ability to compute Fine-Grain Strategies
tm507211
committed
Refines parsing Z3's CHC solution response and ensure we use spacer engine as datalog engine does not produce a solution
tm507211
committed
Adds simsat_forward for fine-grained strategy improvement
tm507211
committed
Add SMT UnsatCoreSolver that behaves like Solver interface but allows specifying which assertions should be considered in core
tm507211
committed
Adds options to run simsat with either coarse-grained or fine-grained semantics
tm507211
committed

Commits on Aug 31, 2023

Updates readme to point to patched sv-opam for ocaml >= 4.10
tm507211
committed