From 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Fri, 8 Mar 2019 09:56:49 +0100
Subject: Several improvements and fixes of Lia

- Improved reification for Micromega (support for #8764)

- Fixes #9268: Do not take universes into account in lia reification

  Improve #9291 by threading the evar_map during reification.
  Universes are unified.

- Remove (potentially cyclic) dependency over lra for Rle_abs

- Towards a complete simplex-based lia

  fixes  #9615

Lia is now exclusively using cutting plane proofs.
For this to always work, all the variables need to be positive.
Therefore, lia is pre-processing the goal  for each variable x
it introduces the constraints x = y - z , y>=0 , z >= 0
for some fresh variable y and z.

For scalability, nia is currently NOT performing this pre-processing.

- Lia is using the FSet library

  manual merge of commit #230899e87c51c12b2f21b6fedc414d099a1425e4
  to work around a "leaked" hint breaking compatibility of eauto
---
 plugins/micromega/VarMap.v | 30 +++++++++++++++---------------
 1 file changed, 15 insertions(+), 15 deletions(-)

(limited to 'plugins/micromega/VarMap.v')

diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index c888f9af45..8148c7033c 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -33,14 +33,14 @@ Section MakeVarMap.
   #[universes(template)]
   Inductive t  : Type :=
   | Empty : t
-  | Leaf : A -> t
-  | Node : t  -> A -> t  -> t .
+  | Elt : A -> t
+  | Branch : t  -> A -> t  -> t .
 
   Fixpoint find (vm : t) (p:positive) {struct vm} : A :=
     match vm with
       | Empty => default
-      | Leaf i => i
-      | Node l e r => match p with
+      | Elt i => i
+      | Branch l e r => match p with
                         | xH => e
                         | xO p => find l p
                         | xI p => find r p
@@ -50,25 +50,25 @@ Section MakeVarMap.
 
   Fixpoint singleton (x:positive) (v : A) : t :=
     match x with
-    | xH => Leaf v
-    | xO p => Node (singleton p v) default Empty
-    | xI p => Node Empty default (singleton p v)
+    | xH => Elt v
+    | xO p => Branch (singleton p v) default Empty
+    | xI p => Branch Empty default (singleton p v)
     end.
   
   Fixpoint vm_add (x: positive) (v : A) (m : t) {struct m} : t :=
     match m with
     | Empty   => singleton x v
-    | Leaf vl =>
+    | Elt vl =>
       match x with
-      | xH => Leaf v
-      | xO p => Node (singleton p v) vl Empty
-      | xI p => Node Empty vl (singleton p v)
+      | xH => Elt v
+      | xO p => Branch (singleton p v) vl Empty
+      | xI p => Branch Empty vl (singleton p v)
       end
-    | Node l o r => 
+    | Branch l o r =>
       match x with
-      | xH => Node l v r
-      | xI p => Node l o (vm_add p v r)
-      | xO p => Node (vm_add p v l) o r
+      | xH => Branch l v r
+      | xI p => Branch l o (vm_add p v r)
+      | xO p => Branch (vm_add p v l) o r
       end
     end.
 
-- 
cgit v1.2.3