[Delta] Add only storing of distance information
- Handle a little of floor and ceil as (- (floor (- x)))
Showing
- src_colibri2/stdlib/std.ml 2 additions, 0 deletionssrc_colibri2/stdlib/std.ml
- src_colibri2/stdlib/std.mli 2 additions, 0 deletionssrc_colibri2/stdlib/std.mli
- src_colibri2/tests/solve/smt_nra/sat/ceil.smt2 11 additions, 0 deletionssrc_colibri2/tests/solve/smt_nra/sat/ceil.smt2
- src_colibri2/tests/solve/smt_nra/sat/dune.inc 2 additions, 0 deletionssrc_colibri2/tests/solve/smt_nra/sat/dune.inc
- src_colibri2/tests/solve/smt_nra/unsat/ceil.smt2 11 additions, 0 deletionssrc_colibri2/tests/solve/smt_nra/unsat/ceil.smt2
- src_colibri2/tests/solve/smt_nra/unsat/dune.inc 4 additions, 0 deletionssrc_colibri2/tests/solve/smt_nra/unsat/dune.inc
- src_colibri2/tests/solve/smt_nra/unsat/floor.smt2 11 additions, 0 deletionssrc_colibri2/tests/solve/smt_nra/unsat/floor.smt2
- src_colibri2/theories/LRA/delta.ml 114 additions, 0 deletionssrc_colibri2/theories/LRA/delta.ml
- src_colibri2/theories/LRA/delta.mli 19 additions, 0 deletionssrc_colibri2/theories/LRA/delta.mli
- src_colibri2/theories/LRA/dom_interval.ml 23 additions, 13 deletionssrc_colibri2/theories/LRA/dom_interval.ml
- src_colibri2/theories/LRA/dom_interval.mli 1 addition, 0 deletionssrc_colibri2/theories/LRA/dom_interval.mli
- src_colibri2/theories/LRA/dune 2 additions, 1 deletionsrc_colibri2/theories/LRA/dune
- src_colibri2/theories/LRA/fourier.ml 34 additions, 21 deletionssrc_colibri2/theories/LRA/fourier.ml
- src_colibri2/theories/LRA/integer_sign_domain.ml 127 additions, 0 deletionssrc_colibri2/theories/LRA/integer_sign_domain.ml
- src_colibri2/theories/LRA/integer_sign_domain.mli 18 additions, 0 deletionssrc_colibri2/theories/LRA/integer_sign_domain.mli
- src_colibri2/theories/LRA/realValue.ml 2 additions, 0 deletionssrc_colibri2/theories/LRA/realValue.ml
- src_colibri2/theories/LRA/sign_domain.mli 7 additions, 1 deletionsrc_colibri2/theories/LRA/sign_domain.mli
- src_colibri2/theories/quantifier/pattern.ml 5 additions, 2 deletionssrc_colibri2/theories/quantifier/pattern.ml
- src_colibri2/theories/quantifier/trigger.ml 1 addition, 2 deletionssrc_colibri2/theories/quantifier/trigger.ml
- src_common/colibri2.drv 3 additions, 6 deletionssrc_common/colibri2.drv
Loading
Please register or sign in to comment