Moving formulas in LIRA theory towards core LIRA#77
Moving formulas in LIRA theory towards core LIRA#77nclskoh wants to merge 20 commits intozkincaid:flintfrom
Conversation
…ebra. Nonlinear.linearize now ensures floor terms are removed from the guard of the transition.
…n preimage. If we can remove it, SrkSimplify.eliminate_floor can be removed
…ed to handle floor because term selection can introduce it
| (* TODO: floor can be present in transition due to e.g., integer division. | ||
| Change to eliminate_floor_mod_div? | ||
| *) | ||
| mk_and srk [SrkSimplify.eliminate_floor srk (K.guard transition); |
There was a problem hiding this comment.
Currently left as-is. Is it sound to eliminate floor using new symbols here, and should we also eliminate mod?
| (mk_real srk QQ.zero) | ||
| V.scalar_mul (QQ.inverse (QQ.of_zz divisor)) linterm | ||
| |> Linear.of_linterm srk | ||
| |> mk_is_int srk |
There was a problem hiding this comment.
Change t % c = 0 to Int(t/c).
| in | ||
| mk_and srk (formula::floor_constraints) | ||
|
|
||
| let simplify_integer_atom srk op s t = |
There was a problem hiding this comment.
Remove simplify_integer_atom from SrkSimplify. The implementation is copied from Quantifier.ml, and is no longer necessary in view of the current interface for Quantifier.
| division with a dominator less than [max]. *) | ||
| val eliminate_idiv : ?max:int -> 'a context -> 'a formula -> 'a formula | ||
|
|
||
| (** Purify floor functions in an expression: replace each function |
There was a problem hiding this comment.
Not used outside of SrkSimplify.ml, and this overlaps somewhat with Syntax.eliminate_floor_mod_div, so we should probably expose the logic there instead when needed.
| let lower_bound = mk_leq srk (mk_real srk QQ.zero) fractional_part in | ||
| let upper_bound = mk_lt srk fractional_part (mk_real srk QQ.one) in | ||
| [mk_eq srk t sum; lower_bound; upper_bound] | ||
| (* floor(t) --> [s = floor(t)], iff t - 1 < s <= t /\ Int(s); Int(s) is handled by type of symbol *) |
There was a problem hiding this comment.
Reduce the number of symbols introduced.
| module XSeq = struct | ||
| let seq_of_exp modulus lambda = | ||
| UltimatelyPeriodic.unfold (fun power -> (power * lambda) mod modulus) 1 | ||
| let seq_of_exp modulus lambda = |
There was a problem hiding this comment.
Formatting changes up to line 295
| |> Quantifier.mbp srk (fun s -> Symbol.Set.mem s gz_symbols_set) | ||
| |> SrkSimplify.simplify_dda srk | ||
| |> SrkSimplify.eliminate_floor srk | ||
| (* |
There was a problem hiding this comment.
SrkSimplify.eliminate_floor is kept as-is here, because it removes floor without introducing new symbols when it arises from integer division with divisor up to 10. But this is otherwise unsound, and we should change Quantifier.mbp to not introduce floor when the input formula is LIA, and remove SrkSimplify.eliminate_floor here.
| | `Or xs -> Periodic.mapn (mk_or srk) xs | ||
| | `Not x -> Periodic.map (mk_not srk) x | ||
| | `Atom (`Arith (op, s, t)) -> | ||
| let normalize typ v = |
There was a problem hiding this comment.
Inline the logic in simplify_integer_atom for handling inequalities and equations with LRA terms, i.e., no mod/divisibility constraints. Logic for divisibility is moved to IsInt below.
| XSeq.seq_of_compare_atom srk predicate cf term_of_dim | ||
| | `Quantify _ -> failwith "should not see quantifiers in the TF" | ||
| | `Atom (`ArrEq _) -> failwith "should not see ArrEq in the TF" | ||
| | `Atom (`IsInt t) -> |
There was a problem hiding this comment.
Handle divisibility constraints.
nclskoh
left a comment
nclskoh
left a comment
There was a problem hiding this comment.
Comments on what's changed.
nclskoh
changed the title
1 participant
Core LIRA formulas have terms in LRA and atoms in LIA (i.e., LRA atoms +
is_intpredicates). This PR refactors some components to use formulas that are closer to core LIRA.Iteration.Solvercurrently allows LIRA formulas in the solver to have floor and mod terms, which makes abstraction complex. This PR changes pre-processing of the formula so that only core LIRA formulas are in the solver.Iteration.Solveris used for e.g., summarizing loops.Quantifier.ml) currently introduces divisibility constraints in the form oft % c = 0, which comingles divisibility with equality. This PR changes it toInt(t/c).TODO: We should have a future PR that removes the introduction of floor symbols when doing QE for LIA formulas.
TerminationDTA.mphas to eliminate floor right now because of this, and it is correct for integer division up to divisor = 10, but is unsound in the general case, because new symbols are introduced.