Fix propagation for Geq
- Allow theories to define symbols to skip for trigger computation - Arithmetic skips <= < > >=
Showing
- dolmen 1 addition, 1 deletiondolmen
- src/bin/main.ml 5 additions, 3 deletionssrc/bin/main.ml
- src_colibri2/bin/main.ml 6 additions, 4 deletionssrc_colibri2/bin/main.ml
- src_colibri2/popop_lib/debug.ml 1 addition, 1 deletionsrc_colibri2/popop_lib/debug.ml
- src_colibri2/solver/input.ml 9 additions, 6 deletionssrc_colibri2/solver/input.ml
- src_colibri2/tests/solve/all/sat/dune.inc 3 additions, 0 deletionssrc_colibri2/tests/solve/all/sat/dune.inc
- src_colibri2/tests/solve/all/sat/union-Union-is_singletonqtvc_2.psmt2 10 additions, 0 deletions.../tests/solve/all/sat/union-Union-is_singletonqtvc_2.psmt2
- src_colibri2/tests/solve/all/unsat/dune.inc 3 additions, 0 deletionssrc_colibri2/tests/solve/all/unsat/dune.inc
- src_colibri2/tests/solve/all/unsat/union-Union-is_singletonqtvc_1.psmt2 89 additions, 0 deletions...ests/solve/all/unsat/union-Union-is_singletonqtvc_1.psmt2
- src_colibri2/theories/LRA/dom_interval.ml 2 additions, 2 deletionssrc_colibri2/theories/LRA/dom_interval.ml
- src_colibri2/theories/LRA/realValue.ml 6 additions, 0 deletionssrc_colibri2/theories/LRA/realValue.ml
- src_colibri2/theories/quantifier/trigger.ml 8 additions, 0 deletionssrc_colibri2/theories/quantifier/trigger.ml
- src_colibri2/theories/quantifier/trigger.mli 4 additions, 0 deletionssrc_colibri2/theories/quantifier/trigger.mli
- src_common/union.mlw 8 additions, 1 deletionsrc_common/union.mlw
- src_common/union/why3session.xml 59 additions, 42 deletionssrc_common/union/why3session.xml
Loading
Please register or sign in to comment