From 721637c98514a77d05d080f53f226cab3a8da1e7 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 30 Aug 2016 17:12:27 +0200 Subject: plugin micromega : nra also handles non-linear rational arithmetic over Q (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R. --- plugins/micromega/coq_micromega.ml | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) (limited to 'plugins/micromega/coq_micromega.ml') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index b8e5e66ca..edcb00b90 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2100,11 +2100,7 @@ let tauto_lia ff = * solvers *) -let psatzl_Z = - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec - [ linear_Z ] - -let psatzl_Q = +let lra_Q = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ linear_prover_Q ] @@ -2112,7 +2108,7 @@ let psatz_Q i = micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] -let psatzl_R = +let lra_R = micromega_genr [ linear_prover_R ] let psatz_R i = @@ -2136,21 +2132,21 @@ let sos_R = micromega_genr [ non_linear_prover_R "pure_sos" None ] -let xlia = - try - micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec +let xlia = micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ linear_Z ] - with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let xnlia = - try micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec [ nlinear_Z ] - with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise let nra = micromega_genr [ nlinear_prover_R ] +let nqa = + micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec + [ nlinear_prover_R ] + + (* Local Variables: *) (* coding: utf-8 *) -- cgit v1.2.3