fix(Dolmen): Parse triggers from formula body for SMT-LIB

In the native format, triggers are annotated on the quantifier itself,
but in SMT-LIB format they are on the body of the quantifier. Alt-Ergo
only looks on the quantifier, which was not a problem because Dolmen
used to copy triggers from the body to the quantifier.

Since Gbury/dolmen#207 Dolmen no longer performs
this copy, which means that we ignore triggers in SMT-LIB format.

This patch makes Alt-Ergo looks for trigger on both the quantifier and
its body, to be compatible with both modes of operations. It also adds a
specific test for this (although the Dolmen change breaks a bunch
of existing tests already).

This patch also bumps the Dolmen version for obvious reasons.

alt-ergo-lib.opam

@@ -17,9 +17,9 @@ depends: [
   "ocaml" {>= "4.08.1"}
   "dune" {>= "3.0"}
   "dune-build-info"
-  "dolmen" {>= "0.9"}
-  "dolmen_type" {>= "0.9"}
-  "dolmen_loop" {>= "0.9"}
+  "dolmen" {>= "0.10"}
+  "dolmen_type" {>= "0.10"}
+  "dolmen_loop" {>= "0.10"}
   "ocplib-simplex" {>= "0.5"}
   "zarith" {>= "1.11"}
   "seq"

alt-ergo-lib.opam.locked

@@ -88,15 +88,15 @@ conflicts: [
 pin-depends: [
   [
     "dolmen.dev"
-    "git+https://github.com/Gbury/dolmen.git#b14eb8a2400c3dd2c34cded212c2135bbce1a57c"
+    "git+https://github.com/Gbury/dolmen.git#4637064b98d0af7e42e8a55845ca80cb19fe1f36"
   ]
   [
     "dolmen_loop.dev"
-    "git+https://github.com/Gbury/dolmen.git#b14eb8a2400c3dd2c34cded212c2135bbce1a57c"
+    "git+https://github.com/Gbury/dolmen.git#4637064b98d0af7e42e8a55845ca80cb19fe1f36"
   ]
   [
     "dolmen_type.dev"
-    "git+https://github.com/Gbury/dolmen.git#b14eb8a2400c3dd2c34cded212c2135bbce1a57c"
+    "git+https://github.com/Gbury/dolmen.git#4637064b98d0af7e42e8a55845ca80cb19fe1f36"
   ]
   [
     "js_of_ocaml.5.4.0"

dune-project

@@ -77,9 +77,9 @@ See more details on http://alt-ergo.ocamlpro.com/"
   (ocaml (>= 4.08.1))
   dune
   dune-build-info
-  (dolmen (>= 0.9))
-  (dolmen_type (>= 0.9))
-  (dolmen_loop (>= 0.9))
+  (dolmen (>= 0.10))
+  (dolmen_type (>= 0.10))
+  (dolmen_loop (>= 0.10))
   (ocplib-simplex (>= 0.5))
   (zarith (>= 1.11))
   seq

nix/sources.json

@@ -1,14 +1,14 @@
 {
     "dolmen": {
-        "branch": "b14eb8a2400c3dd2c34cded212c2135bbce1a57c",
+        "branch": "4637064b98d0af7e42e8a55845ca80cb19fe1f36",
         "description": "Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction",
         "homepage": "",
         "owner": "Gbury",
         "repo": "dolmen",
-        "rev": "b14eb8a2400c3dd2c34cded212c2135bbce1a57c",
-        "sha256": "0r1q1byys41snf7bydscp9raj406ypjz7rwri96hsswx3d7jd08b",
+        "rev": "4637064b98d0af7e42e8a55845ca80cb19fe1f36",
+        "sha256": "0r3p5dfp684xccqz9jm9cf1lr6xzjvrhsk6kb7ydnadls30xdvgw",
         "type": "tarball",
-        "url": "https://github.com/Gbury/dolmen/archive/b14eb8a2400c3dd2c34cded212c2135bbce1a57c.tar.gz",
+        "url": "https://github.com/Gbury/dolmen/archive/4637064b98d0af7e42e8a55845ca80cb19fe1f36.tar.gz",
         "url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz",
         "version": "dev"
     },

src/lib/frontend/d_cnf.ml

@@ -1565,13 +1565,20 @@ let rec mk_expr
           in
           let hyp = List.map aux_mk_expr hyp in
 
-          (* triggers *)
-          let trgs =
+          (* triggers - on quantifier for AE, on body for SMT-LIB *)
+          let root_trgs =
             begin match DStd.Tag.get root_tags DE.Tags.triggers with
               | Some t -> t
               | _ -> []
             end
           in
+          let body_trgs =
+            begin match DStd.Tag.get body.term_tags DE.Tags.triggers with
+              | Some t -> t
+              | _ -> []
+            end
+          in
+          let trgs = root_trgs @ body_trgs in
           let in_theory = decl_kind == E.Dtheory in
           let f = aux_mk_expr ~toplevel body in
           let qbody = E.purify_form f in

tests/quantifiers/testfile-trigger001.dolmen.expected

@@ -0,0 +1,2 @@
+
+unknown

tests/quantifiers/testfile-trigger001.dolmen.smt2

@@ -0,0 +1,14 @@
+(set-logic ALL)
+(declare-fun P (Int) Bool)
+(declare-fun f (Int) Int)
+
+; This quantifier is explicitly annotated with a (f x) trigger.
+; It should not cause this problem to be unsat.
+(assert
+ (forall ((x Int))
+  (! (not (P x)) :pattern ((f x)))))
+
+; Note that we don't use (f 0).
+(assert (P 0))
+
+(check-sat)