Add support to axioms for input constraints.

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

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
 
 

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

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. *)
 

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;
 }