[Abs_product] add a multiplicative constant
and print better algebraic number
Showing
- libpoly/accessors.h 10 additions, 0 deletionslibpoly/accessors.h
- libpoly/dune 3 additions, 2 deletionslibpoly/dune
- libpoly/function_description.ml 55 additions, 31 deletionslibpoly/function_description.ml
- libpoly/ocaml_poly.ml 40 additions, 3 deletionslibpoly/ocaml_poly.ml
- libpoly/ocaml_poly.mli 12 additions, 2 deletionslibpoly/ocaml_poly.mli
- libpoly/type_description.ml 29 additions, 12 deletionslibpoly/type_description.ml
- src_colibri2/stdlib/std.ml 8 additions, 2 deletionssrc_colibri2/stdlib/std.ml
- src_colibri2/stdlib/std.mli 5 additions, 1 deletionsrc_colibri2/stdlib/std.mli
- src_colibri2/tests/solve/models/dune.inc 2 additions, 0 deletionssrc_colibri2/tests/solve/models/dune.inc
- src_colibri2/tests/solve/models/sqrt.smt2 9 additions, 0 deletionssrc_colibri2/tests/solve/models/sqrt.smt2
- src_colibri2/tests/solve/models/sqrt.smt2.oracle 2 additions, 0 deletionssrc_colibri2/tests/solve/models/sqrt.smt2.oracle
- src_colibri2/theories/LRA/dom_product.ml 87 additions, 53 deletionssrc_colibri2/theories/LRA/dom_product.ml
- src_colibri2/theories/LRA/dom_product.mli 1 addition, 1 deletionsrc_colibri2/theories/LRA/dom_product.mli
- src_colibri2/theories/LRA/fourier.ml 4 additions, 3 deletionssrc_colibri2/theories/LRA/fourier.ml
- src_colibri2/theories/LRA/pivot.ml 39 additions, 50 deletionssrc_colibri2/theories/LRA/pivot.ml
- src_colibri2/theories/LRA/pivot.mli 1 addition, 2 deletionssrc_colibri2/theories/LRA/pivot.mli
- src_colibri2/theories/LRA/product.ml 49 additions, 37 deletionssrc_colibri2/theories/LRA/product.ml
- src_colibri2/theories/LRA/product.mli 6 additions, 2 deletionssrc_colibri2/theories/LRA/product.mli
- src_colibri2/theories/LRA/realValue.ml 15 additions, 3 deletionssrc_colibri2/theories/LRA/realValue.ml
- src_colibri2/theories/LRA/realValue.mli 1 addition, 0 deletionssrc_colibri2/theories/LRA/realValue.mli
Loading
Please register or sign in to comment