650 Commits (aa3586b855315c9739b5a2de0b54a696521ee2f7)

Author SHA1 Message Date
Josh Berdine fcd0e41ee6 [sledge] Return early for == args in Term compare and equal
5 years ago
Josh Berdine 76695690b8 [sledge] Do not simplify Mul and Div terms
5 years ago
Josh Berdine a3a6a5a6fe [sledge] Do not solve for Integer constants
5 years ago
Josh Berdine 32c5fb2837 [sledge] Do not represent Equality rep sparsely on constants
5 years ago
Josh Berdine de1689ac87 [sledge] Change And and Or terms from binary to flattened n-ary
5 years ago
Josh Berdine 87c8eb7c3a [sledge] Strengthen normalization of division
5 years ago
Josh Berdine cd72d3a82e [sledge] Simplify Term.Sum.to_term
5 years ago
Josh Berdine 2fc8bc1f84 [sledge] Export Term.map_rec_pre and add Term.fold_map_rec_pre
5 years ago
Josh Berdine 548928a839 [sledge] Strengthen Equality invariant to ensure carrier closed under subterms
5 years ago
Josh Berdine 2124be1c71 [sledge] Remove the "simplified" intermediate between interpreted and uninterpreted
5 years ago
Josh Berdine ee595f2ebf [sledge] Strengthen Equality.close to handle rep being sparse on constants
5 years ago
Josh Berdine 2f4f9801ed [sledge] Add Term.is_constant
5 years ago
Josh Berdine c91e09031f [sledge] Strengthen Equality normalization
5 years ago
Josh Berdine 0f50d3c248 [sledge] Do not solve polynomials for Mul or Div terms
5 years ago
Josh Berdine eb750ba6f9 [sledge] Avoid cyclic solutions to polynomial equations
5 years ago
Josh Berdine 1b20f02052 [sledge] Strengthen normalization of division, avoiding non-reals
5 years ago
Josh Berdine 4ea9eced05 [sledge] Improve Term.Sum.to_term
5 years ago
Josh Berdine 1a34e7eed2 [sledge] Add rational constants
5 years ago
Josh Berdine 7b33996072 [sledge] Use term height to avoid "pumpable" cyclic equations in Equality
5 years ago
Josh Berdine 6c03d88cf7 [sledge] Move Term.agg_size
5 years ago
Josh Berdine 0cee03aaa1 [sledge] Simplify identity type conversions only at initial construction
5 years ago
Josh Berdine 7e4673cbeb [sledge] Improve Equality invariant checking and debugging support
5 years ago
Josh Berdine 3c0924cf01 [sledge] Minor code improvement
5 years ago
Josh Berdine 60df5d6f3a [sledge] Fix Equality.Subst.compose to preserve physical equality
5 years ago
Josh Berdine 013b948dc4 [sledge] Rename extend to compose1 to avoid potential shadowing confusion
5 years ago
Josh Berdine fddb2fa991 [sledge] Add Map.map_endo
5 years ago
Josh Berdine ef63683a16 [sledge] Add Term.fold_map
5 years ago
Josh Berdine b35e3d30e0 [sledge] Add Map.fold_until
5 years ago
Josh Berdine b09f3774a4 [sledge] Add Qset.is_empty
5 years ago
Josh Berdine 165454e17d [sledge] Add Map and Qset operations to access top of underlying tree
5 years ago
Josh Berdine 7fdd3cccbb [sledge] Add Option.or_else
5 years ago
Josh Berdine 2aacc03880 [sledge] Remove eliminated existentials from equality relations
5 years ago
Josh Berdine 30c23f8cd6 [sledge] Fix term ordering bug between monomials and vars
5 years ago
Josh Berdine e7217ac5fe [sledge] Check equality of logical variables by id only
5 years ago
Josh Berdine c8e75e3b82 [sledge] Dump perf diagnostics and replays for slow queries to stderr
5 years ago
Josh Berdine a4e523b5b6 [sledge] Rename `*_preserves_phys_equal` to `*_endo` and clarify docs
5 years ago
Josh Berdine ec52259d31 [sledge] Substitute out alias of option when including Monad_syntax
5 years ago
Josh Berdine 1ae192dc0e [sledge] Use __LOC__ for Not_found_s
5 years ago
Josh Berdine ef0dfe0d70 [sledge] Fix doc of List.remove_exn
5 years ago
Josh Berdine d1de5db6c8 [sledge] Document Equality variable context handling
5 years ago
Josh Berdine 31dd2884f6 [sledge] Use a cookie instead of env var to enable ppx_trace
5 years ago
Josh Berdine 1ce5eb8033 [sledge] Suppress warning on dune build_info compilation
5 years ago
Josh Berdine 1364eccf18 [sledge] No longer need to Marshal with Closures support
5 years ago
Josh Berdine 461f88756d [sledge] Name the sledge library `sledge`
5 years ago
Josh Berdine ed82bca4a5 [sledge] Document that integer division and remainder use truncation semantics
5 years ago
Josh Berdine 3b4b2f3999 [sledge] Add replay debugging for Equality
5 years ago
Josh Berdine e83c6170e5 [sledge] Improve tracing in unit tests
5 years ago
Josh Berdine 9414cb4fb3 [sledge] Implement 'a iarray as ('a, immutable) Array.Permissioned.t
5 years ago
Josh Berdine fe62eeadab [sledge] Cleanup of Import
5 years ago
Josh Berdine 7ab19955bb [sledge] Implement Qset using Import.Map
5 years ago
Josh Berdine d5fe9aa11d [sledge] Define Map as a functor over the Tree underlying Core.Map
5 years ago
Josh Berdine ae3c059fe9 [sledge] Define Set as a functor over the Tree underlying Core.Set
5 years ago
Jules Villard 4e9f34efea [sledge] fix for `Equality.and_term`
5 years ago
Josh Berdine 6504f12029 [sledge] Rename Var.global to Var.is_global
5 years ago
Josh Berdine 9382b8120b [sledge] Improve IArray.map_adjacent
5 years ago
Josh Berdine 2fa0948e8d [sledge] Only fmt one (dbg) context, and suppress diff output
5 years ago
Josh Berdine fe09969a53 [sledge] Move basic function and tuple operations to Import0
5 years ago
Josh Berdine 8d6911416d [sledge] Add util for local exception to return early idiom
5 years ago
Josh Berdine 2ca98c80ff [sledge] Rename vector to iarray
5 years ago
Josh Berdine 2a5e0f692b [sledge] Move dep on Core to just bin
5 years ago
Josh Berdine 4d86832d7a [sledge] Do not open Base globally
5 years ago
Josh Berdine 06e4a2c08c [sledge] Dedup Qset interface
5 years ago
Josh Berdine 434c40e646 [sledge] Do not use Base.Map to implement Qset
5 years ago
Josh Berdine 152cc38e9b [sledge] Dedup Map signature
5 years ago
Josh Berdine 5dbb4a6fc2 [sledge] Dedup Set signature
5 years ago
Josh Berdine 42a8f774fd [sledge] Move Import.Map to separate module
5 years ago
Josh Berdine 252060ac7a [sledge] Remove unused ppx_custom_printf
5 years ago
Josh Berdine 93a9c823fc [sledge] Move Import.Set to separate module
5 years ago
Josh Berdine a4613f001d [sledge] Move Vector.pp out of Import.Vector wrapper
5 years ago
Josh Berdine c47881e664 [sledge] Remove dead Result.pp function
5 years ago
Josh Berdine 04df3ca460 [sledge] Move Import.List to separate module
5 years ago
Josh Berdine 24a26c8a23 [sledge] Move Import.Option to separate module
5 years ago
Josh Berdine 9c77d7b2a4 [sledge] Move some general type definitions from Import to Import0
5 years ago
Josh Berdine 124a1fed20 [sledge] Do not use Base.Set
5 years ago
Josh Berdine 57a8748e9f [sledge] Do not use Base.Map
5 years ago
Josh Berdine 134f9f930e [sledge] Adjust build system to allow building as a vendored dependency
5 years ago
Josh Berdine 8337097cf0 [sledge] Move Domain_itv and dependency on APRON from lib to bin
5 years ago
Josh Berdine 27f93b60da [sledge] Move ctypes dep from lib to bin
5 years ago
Josh Berdine 1c9bafc2a9 [sledge] Add beginnings of HACKING docs
5 years ago
Josh Berdine f5ab894675 [sledge] Dedup preprocess entries in dune files
5 years ago
Josh Berdine 0c7249b992 [sledge] Change build system to not generate dune files
5 years ago
Josh Berdine fff3a491bf [sledge] Bump version of dune language used, and format dune files
5 years ago
Josh Berdine 1798725632 [sledge] Add support to ppx_trace enable via environment variable
5 years ago
Josh Berdine c47199e31c [sledge] Simplify build for models
5 years ago
Josh Berdine 8880dd48eb [sledge] Remove base dep from ppx_trace
5 years ago
Josh Berdine b6ddd8fe8e [sledge] Rearrange into CLI binary and LLVM-independent library
5 years ago
Josh Berdine d5158f0787 [sledge] Move Reg.demangle to frontend
5 years ago
Josh Berdine 5eebe1c733 [sledge] Add entry-points config to Control.exec_opts
5 years ago
Josh Berdine dd026745af [sledge] Remove sledge/bin symlinks
5 years ago
Josh Berdine e6ccd3e497 [sledge] Minor tracing improvements
5 years ago
Josh Berdine 556739e17c [sledge] Minor optimization of Sh.bind_exists
5 years ago
Josh Berdine f80e0977cd [sledge] Make Sh.and_cong robust wrt conjoining to an unsat formula
5 years ago
Josh Berdine 37ddf95a49 [sledge] Strengthen and simplify canonizer for Extract terms
5 years ago
Josh Berdine f8a490d477 [sledge] Enforce variable context conditions in solver goals
5 years ago
Josh Berdine f8f47c0755 [sledge] Fix a few existential context fumbles
5 years ago
Josh Berdine 991c0c66e8 [sledge] Remove unnecessary vocabulary updates
5 years ago
Josh Berdine 8b8e156f83 [sledge] Make Solver.judgment a private type
5 years ago
Josh Berdine 9488a404ff [sledge] Compare logical variables by id only
5 years ago
Josh Berdine 0f1db1bd8b [sledge] Fix potential name clash when executing memmov
5 years ago
Josh Berdine 24c62fd39b [sledge] Strengthen canonizer of Extract terms
5 years ago