Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Fewer side-conditions on zsimplify | Jason Gross | 2016-08-24 | |
* | Fix a Hint Resolve typo | Jason Gross | 2016-08-23 | |
* | More ZUtil | Jason Gross | 2016-08-23 | |
* | More ZUtil | Jason Gross | 2016-08-23 | |
* | Add Z.rewrite_mod_small | Jason Gross | 2016-08-19 | |
* | More powerful Z.div_mod_to_quot_rem | Jason Gross | 2016-08-19 | |
* | More ZUtil | Jason Gross | 2016-08-18 | |
* | Add ZUtil | Jason Gross | 2016-08-18 | |
* | Add a ZUtil hint | Jason Gross | 2016-08-18 | |
* | Add some ZUtil lemmas and hints | Jason Gross | 2016-08-18 | |
* | Add versions of ZUtil lemmas without nonzero assumptions | Jason Gross | 2016-08-18 | |
* | Add Z.opp_involutive to Zshift_to_pow | Jason Gross | 2016-08-18 | |
* | Add a ZUtil hint | Jason Gross | 2016-08-17 | |
* | Add Z.div_mod_to_quot_rem | Jason Gross | 2016-08-17 | |
* | Add [Z.linear_solve_for], [Z.linear_substitute] | Jason Gross | 2016-08-17 | |
* | More zsimplify | Jason Gross | 2016-08-16 | |
* | Add a faster zsimplify database | Jason Gross | 2016-08-16 | |
* | Merge of conversion development branch with master | jadep | 2016-08-16 | |
|\ | ||||
| * | Moved Z lemmas useful for conversion proofs (mostly about bitwise operations)... | jadep | 2016-08-16 | |
* | | More shift lemmas | Jason Gross | 2016-08-16 | |
* | | More shift logic | Jason Gross | 2016-08-16 | |
* | | More ZUtil | Jason Gross | 2016-08-16 | |
* | | More ZUtil simplification | Jason Gross | 2016-08-16 | |
* | | Add zutil for div lemma | Jason Gross | 2016-08-15 | |
* | | Support shiftl in Zshift_to_pow | Jason Gross | 2016-08-15 | |
* | | Work around bug #5019 (loopy [zify]) | Jason Gross | 2016-08-15 | |
* | | More ZUtil | Jason Gross | 2016-08-15 | |
* | | Add Z.shift{r,l} databases | Jason Gross | 2016-08-15 | |
* | | Add upper_bound_uniform | Jason Gross | 2016-08-12 | |
* | | More ZUtil | Jason Gross | 2016-08-12 | |
* | | More ZUtil | Jason Gross | 2016-08-11 | |
* | | Add ZUtil | Jason Gross | 2016-08-11 | |
* | | Add {pull,push}_Zof_nat | Jason Gross | 2016-08-11 | |
|/ | ||||
* | More ZUtil | Jason Gross | 2016-08-09 | |
* | More ZUtil | Jason Gross | 2016-08-09 | |
* | More ZUtil | Jason Gross | 2016-08-09 | |
* | zsimplify: Better support for existentials | Jason Gross | 2016-08-08 | |
* | More zarith hints | Jason Gross | 2016-08-08 | |
* | Add ZUtil lemmas | Jason Gross | 2016-08-08 | |
* | Handle [_ mod 0] in pull_Zmod | Jason Gross | 2016-08-05 | |
* | Add Z.mod_mod case to pull_Zmod | Jason Gross | 2016-08-05 | |
* | Handle [((-_) mod n) mod n] in {push,pull}_Zmod | Jason Gross | 2016-08-04 | |
* | More zsimplify | Jason Gross | 2016-08-03 | |
* | Add some autogenerated zsimplify lemmas | Jason Gross | 2016-08-03 | |
* | Better Zmod manipulation | Jason Gross | 2016-08-03 | |
* | Weaken some ZUtil assumptions | Jason Gross | 2016-08-03 | |
* | More ZUtil | Jason Gross | 2016-08-03 | |
* | More ZUtil | Jason Gross | 2016-08-03 | |
* | Add ZUtil lemmas, and Util.Bool | Jason Gross | 2016-08-03 | |
* | More zsimplify hints | Jason Gross | 2016-08-03 |