Fine-grained strategy improvement #7
Conversation
…headers for reducible CFG rather than an arbitrary loop header per loop
allows quantify_consts functions to take in formulae with free variable as input
…ngine as datalog engine does not produce a solution
… specifying which assertions should be considered in core
| @@ -506,6 +509,40 @@ module Solver = struct | |||
| let get_reason_unknown solver = Z3.Solver.get_reason_unknown solver.s | |||
| end | |||
|
|
|||
| module UnsatCoreSolver = struct | |||
There was a problem hiding this comment.
How can this be used? It looks like it's allocating a boolean symbol for each tracked assert, but there's no way to get at that symbol. The unsat core will be a list of these symbols, but there's no way for a client of UnsatCoreSolver to know chich formulas these symbols correspond to.
There was a problem hiding this comment.
When you call Z3.Solver.get_unsat_core, any boolean symbols and any formulas added via Z3.Solver.assert_and_track_l that are involved in the unsat core will be returned.
It seems Z3 keeps an internal mapping between the tracked formula and associated boolean variable. Then will return the formula instead of the boolean variable in the unsat core.
There was a problem hiding this comment.
If this is all managed by Z3, can you just add assert_and_track to the Solver interface rather than creating a new module?
| @@ -76,9 +78,50 @@ module Solver : sig | |||
| [ `Sat | `Unsat of ('a formula) list | `Unknown ] | |||
|
|
|||
| val get_reason_unknown : 'a t -> string | |||
| end | |||
| end with type 'a t = 'a solver | |||
There was a problem hiding this comment.
You can use "type 'a t = 'a solver" right in the signature rather than constraining it later
| @@ -423,10 +421,96 @@ let term_of_virtual_term srk vt = | |||
| in | |||
| mk_add srk [term_over_div; offset] | |||
|
|
|||
| let miniscope srk phi : 'a formula = | |||
| module FineGrain = struct | ||
| module IM = SrkUtil.Int.Map | ||
|
|
||
| (* (* A path is actually a tree since we need a path for every conjuct, not just one conjuct *) |
| | SForall (_, _, t) -> nb_paths t | ||
| | SExists (_, mm) -> MM.enum mm /@ (fun (_, t) -> nb_paths t) |> BatEnum.sum | ||
|
|
||
| (* (* Create a new skeleton where the only path is the given path *) |
| | SExists (k, mm) -> | ||
| MM.enum mm | ||
| /@ (fun (move, skeleton) -> substitute srk k move (go skeleton)) | ||
| (* |
| ctx.skeleton <- Skeleton.FineGrain.union srk ctx.skeleton skel; | ||
| Smt.Solver.add ctx.solver new_loss_conditions | ||
|
|
||
| (* let initialize_pair select_term srk ?(init=Interpretation.empty srk) phi = |
| end | ||
|
|
||
| type 'a cg_formula = ([`Forall | `Exists] * symbol) list * 'a formula | ||
| module CoarseGrainStrategyImprovement = struct |
There was a problem hiding this comment.
Is there any reason to keep this as a separate implementation? (E.g., if I convert to prenex and then compute a fg_formula that's just a sequence of quantifiers followed by an atom, and then compute a fine-grained strategy, is that the same as computing a coarse-grained strategy?) On the other hand, I recall that the story for non-forwards fine-grained strategy improvement is complicated and the algorithm is dominated by the forwards variant. So maybe it would make to have (non-forwards) coarse grained + (forwards) fine grained. Hopefully we can also get some code re-use too. E.g., if you use polymorphic variants to define skeletons, then coarse-grained skeletons are a subtype of fine-grained skeletons, so we can re-use fine-grained code for coarse-grained.
There was a problem hiding this comment.
It's been a while since I read through the coarse-grained implementation. The fine-grained implementation can certainly produce coarse-grained strategies in the construction you gave. At an algorithmic level the fine-grained implementation should behave the same as the coarse-grained implementation for formulas in prenex-normal form. But I'm unsure if the coarse-grained implementation has any optimizations that require the formula be in prenex-normal form (e.g. cannot be used for the fine-grained implementation).
I can review the coarse-grained implementation and then suggest either keeping just the fine-grained or the two variants you suggested.
Updates Quantifier interface with a Strategy Improvement module and provides two implementations: CoarseGrained and FineGrained.
The CoarseGrained is what was previously implemented (converts to prenex normal form and provides strategies for quantifiers only).
The FineGrained converts formulas to negation normal form and provides strategies for quantifiers and connectives. By default FineGrained.simsat converts the input formula to negation normal form, mini-scopes the formula, and only provides strategies for connectives if any sub-formula contains a quantifier. If you'd like to avoid these transformations, you may call FineGrained.winning_skeleton or FineGrained.winning_strategy instead (note: winning_skeleton and winning_strategy use the base simsat algorithm and not the forward algorithm).
The commits also include Jake's miniscoping code, improved conversion from Z3's CHC solutions to Srk formulas---FineGrained.winning_strategy exercised solutions that were not properly converted by pervious implementation.
Created SrkZ3.Unsatcore solver that allows specifying which assertions should be considered in unsat core. The solver object may be used interchangeably with the Unsatcore solver module and the default solver modules.
Provides new options to Bigtop for running coarse or fine-grained simsat.