Merge branch 'feature/michele/rework-sat-marabou' into 'master'

Rework Marabou support in terms of satisfiability.

See merge request laiser/caisar!4

marabou.ml

@@ -16,8 +16,14 @@ let re_version = Str.regexp "[0-9]\\(\\.[0-9]\\)*\\(\\.?[A-Za-z-+]\\)*"
 let re_of_result result =
   Str.regexp
     (match result with
-     | Solver.Result.Valid -> "\\(s\\|S\\)at\\|SAT"
-     | Invalid -> "\\(u\\|U\\)nsat\\|UNSAT"
+     | Solver.Result.Valid ->
+       (* The original formula is valid iff [result], computed on the negation
+          of the original formula as typical in SAT/SMT, is unsat. *)
+       "^\\(u\\|U\\)nsat\\|UNSAT"
+     | Invalid ->
+       (* The original formula is invalid iff [result], computed on the negation
+          of the original formula as typical in SAT/SMT, is sat. *)
+       "^\\(s\\|S\\)at\\|SAT"
      | Timeout -> "\\(t\\|T\\)imeout\\|TIMEOUT"
      | Unknown -> "\\(u\\|U\\)nknown\\|UNKNOWN"
      | Failure -> assert false)
@@ -38,10 +44,15 @@ let options ~model ~property ~output =
     "--verbosity"; Int.to_string verbosity_level;
     "--summary-file"; output ]
 
+(* Recall that Marabou is a SAT/SMT-like solver that supports conjunctive
+   formulae only, meaning that disjunctive formulae need to be split into
+   multiple files. If consolidation of formulae is needed, then the original
+   formula, ie before taking the negation as typical in SAT/SMT, was a
+   conjunctive formula: we consolidate wrt logical and-operator semantics. *)
 let consolidate r1 r2=
   match r1, r2 with
-  | _, Solver.Result.Valid | Solver.Result.Valid, _ -> Solver.Result.Valid
-  | Invalid, result | result, Invalid -> result
+  | result, Solver.Result.Valid | Solver.Result.Valid, result -> result
+  | Invalid, _ | _, Invalid -> Invalid
   | Failure, _ | _, Failure -> Failure
   | Timeout, _ | _, Timeout -> Timeout
   | Unknown, Unknown -> Unknown
@@ -75,8 +86,39 @@ let rec constant_rhs formula =
   | Or (p1, p2) ->
     Or (constant_rhs p1, constant_rhs p2)
 
+(* Marabou does not support greater-than (ie Gt) and less-than (ie Lt)
+   comparison operators. Then, transform these into their non-strict versions by
+   adding (Gt) or subtracting (Lt) an [epsilon]. For example, [k_y_0 > c] iff
+   [k_y_0 >= c + epsilon]. *)
+let rec epsilon_rhs ~epsilon formula =
+  match formula with
+  | Constraint (terms, Gt, Constant cst) ->
+    let fcst =
+      (match cst with
+       | Int i -> Float.of_int i
+       | Float f -> f)
+      +. epsilon
+    in
+    Constraint (terms, Ge, Constant (Float fcst))
+  | Constraint (terms, Lt, Constant cst) ->
+    let fcst =
+      (match cst with
+       | Int i -> Float.of_int i
+       | Float f -> f)
+      -. epsilon
+    in
+    Constraint (terms, Le, Constant (Float fcst))
+  | Constraint _ ->
+    formula
+  | And (p1, p2) ->
+    And (epsilon_rhs ~epsilon p1, epsilon_rhs ~epsilon p2)
+  | Or (p1, p2) ->
+    Or (epsilon_rhs ~epsilon p1, epsilon_rhs ~epsilon p2)
+
 let translate ~hypothesis ~goal =
+  let goal = Property.negation goal in
   let goal = constant_rhs goal in
+  let goal = epsilon_rhs ~epsilon:0.00001 goal in
   Property.dnf_of_formula (And (hypothesis, goal))
 
 let repr = Property.get_disjuncts

property.ml

@@ -158,7 +158,28 @@ let pretty fmt t =
     (Format.pp_print_list pretty_goal) t.goals
 
 
-(* Normal forms. *)
+(* Transformations and normal forms. *)
+
+let rec negation f =
+  let negate_cop = function
+    | Eq -> assert false (* We do not support Neq for the moment. *)
+    | Ge -> Lt
+    | Le -> Gt
+    | Lt -> Ge
+    | Gt -> Le
+  in
+  match f with
+  | Constraint (tt, cop, t) ->
+    let ncop = negate_cop cop in
+    Constraint (tt, ncop, t)
+  | And (f1, f2) ->
+    let nf1 = negation f1 in
+    let nf2 = negation f2 in
+    Or (nf1, nf2)
+  | Or (f1, f2) ->
+    let nf1 = negation f1 in
+    let nf2 = negation f2 in
+    And (nf1, nf2)
 
 type conjunct = formula
 type disjunct = formula

property.mli

@@ -12,6 +12,7 @@ type t = Property_types.t
 (** Builds a property out of the content of the given [filename], if possible. *)
 val build: filename:string -> (t, string) Result.t
 
+
 (** {2 Pretty printing.} *)
 
 type 'a printer = Caml.Format.formatter -> 'a -> unit
@@ -38,7 +39,10 @@ val pretty_terms: term printer -> term list printer
 val pretty: Caml.Format.formatter -> t -> unit
 
 
-(** {2 Normal forms.} *)
+(** {2 Transformations and normal forms.} *)
+
+val negation: formula -> formula
+
 
 type conjunct
 type disjunct