From 712afe63283eee28868baf194a328b791b4a154f Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 19 Apr 2021 16:17:57 +0200
Subject: [PATCH] Add support to axioms for input constraints.

---
 engine.ml           | 12 +++++++++++-
 property.ml         |  7 ++++++-
 property_lexer.mll  |  5 ++++-
 property_parser.mly | 16 ++++++++--------
 property_types.mli  |  6 +++---
 5 files changed, 32 insertions(+), 14 deletions(-)

diff --git a/engine.ml b/engine.ml
index c66f486..735dc72 100644
--- a/engine.ml
+++ b/engine.ml
@@ -68,8 +68,18 @@ let check_compatibility solver model =
          S.name
          (Model.show_format model.format))
 
-let tasks_of_property solver { hypothesis; goals } =
+let tasks_of_property solver { axioms; goals } =
   let module S = (val solver: Solver.S) in
+  let hypothesis =
+    match axioms with
+    | [] ->
+      (* Axioms are non-empty lists. *)
+      assert false
+    | [ { formula; _ } ] ->
+      formula
+    | a :: aa ->
+      List.fold_left aa ~init:a.formula ~f:(fun acc a -> And (acc, a.formula))
+  in
   let table = Hashtbl.create (module String) in
   List.iter
     goals
diff --git a/property.ml b/property.ml
index c749d47..444763b 100644
--- a/property.ml
+++ b/property.ml
@@ -147,9 +147,14 @@ let pretty_goal fmt goal =
     goal.name
     pretty_formula goal.formula
 
+let pretty_axiom fmt axiom =
+  Format.fprintf fmt "@[<v 2>axiom %s:@ @[<hov>%a@]@]"
+    axiom.name
+    pretty_formula axiom.formula
+
 let pretty fmt t =
   Format.fprintf fmt "@[%a@]@\n@[<v>%a@]"
-    pretty_formula t.hypothesis
+    (Format.pp_print_list pretty_axiom) t.axioms
     (Format.pp_print_list pretty_goal) t.goals
 
 
diff --git a/property_lexer.mll b/property_lexer.mll
index e066004..8647c71 100644
--- a/property_lexer.mll
+++ b/property_lexer.mll
@@ -14,6 +14,7 @@ let output = 'y'['0'-'9']+
 (* Keywords. *)
 
 let goal = "goal"
+let axiom = "axiom"
 
 (* Macros. *)
 
@@ -42,10 +43,12 @@ rule token = parse
     { INPUT i }
 | output as o
     { OUTPUT o }
+| axiom
+    { AXIOM }
 | goal
     { GOAL }
 | (ident as gid) space* ":"
-    { GOALID gid }
+    { ID gid }
 | ('-'|'+')?['0'-'9']+'.'['0'-'9']+ as f
     { FLOAT (float_of_string f) }
 | ('-'|'+')?['0'-'9']+ as i
diff --git a/property_parser.mly b/property_parser.mly
index 6bdb619..2b8b351 100644
--- a/property_parser.mly
+++ b/property_parser.mly
@@ -8,12 +8,12 @@
 
 %token <int> INT
 %token <float> FLOAT
-%token <string> INPUT OUTPUT GOALID
+%token <string> INPUT OUTPUT ID
 %token EQ GT LT GE LE
 %token PLUS MINUS
 %token AND OR
 %token LPAREN RPAREN
-%token GOAL
+%token AXIOM GOAL
 %token EOF
 
 (* Starting rule. *)
@@ -26,22 +26,22 @@
 (* -------------------------------------------------------------------------- *)
 
 (* We parse a property given by
-   a hypothesis
+   a non-empty list of axioms
    a non-empty list of goals
    followed by an end-of-file. *)
 
 let main :=
-  ~ = hypothesis; goals = nonempty_list(goal); EOF; { { hypothesis; goals; } }
+  axioms = nonempty_list(axiom); goals = nonempty_list(goal); EOF; { { axioms; goals; } }
 
-(* A hypothesis is a conjunctive formula over constraints. *)
+(* An axiom is a conjunctive formula over constraints. *)
 
-let hypothesis ==
-  and_formula(constraint_)
+let axiom ==
+  AXIOM; name = ID; formula = and_formula(constraint_); { { name; formula; } }
 
 (* A goal has a name and a formula. *)
 
 let goal :=
-  GOAL; name = GOALID; ~ = formula; { { name; formula; } }
+  GOAL; name = ID; ~ = formula; { { name; formula; } }
 
 (* A formula is given by disjunctions of conjuctions of (delimited) formulae. *)
 
diff --git a/property_types.mli b/property_types.mli
index dd315b2..9b9c048 100644
--- a/property_types.mli
+++ b/property_types.mli
@@ -24,12 +24,12 @@ type formula =
   | And of formula * formula
   | Or of formula * formula
 
-type goal = {
+type named_formula = {
   name: string;
   formula: formula;
 }
 
 type t = {
-  hypothesis: formula;
-  goals: goal list;
+  axioms: named_formula list;
+  goals: named_formula list;
 }
-- 
GitLab