From 2b0a6470fd516900f2c1b0fe7ee368a269e7d191 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 18 Dec 2020 18:28:48 +0100
Subject: [PATCH] Add support for properties between vars.
---
property.ml | 7 ++++++-
property_parser.mly | 4 +++-
property_syntax.mli | 3 ++-
solver.ml | 4 +++-
4 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/property.ml b/property.ml
index 4414673..f677587 100644
--- a/property.ml
+++ b/property.ml
@@ -77,11 +77,16 @@ let rec repr t =
| Float f -> Format.sprintf "float %f" f
in
match t with
- | Atomic (var, cop, cst) ->
+ | Atomic_cst (var, cop, cst) ->
let var_s = string_of_var var in
let cop_s = string_of_cop cop in
let cst_s = string_of_cst cst in
Format.sprintf "%s %s %s" var_s cop_s cst_s
+ | Atomic_var (var1, cop, var2) ->
+ let var1_s = string_of_var var1 in
+ let cop_s = string_of_cop cop in
+ let var2_s = string_of_var var2 in
+ Format.sprintf "%s %s %s" var1_s cop_s var2_s
| And (p1, p2) ->
Format.sprintf "And (%s, %s)" (repr p1) (repr p2)
diff --git a/property_parser.mly b/property_parser.mly
index e10923a..6cf5926 100644
--- a/property_parser.mly
+++ b/property_parser.mly
@@ -27,7 +27,9 @@ main:
property:
| var cop cst
- { Atomic ($1, $2, $3) }
+ { Atomic_cst ($1, $2, $3) }
+| var cop var
+ { Atomic_var ($1, $2, $3) }
var:
| i = INPUT
diff --git a/property_syntax.mli b/property_syntax.mli
index 4b4472c..c81a3ea 100644
--- a/property_syntax.mli
+++ b/property_syntax.mli
@@ -15,5 +15,6 @@ type cst =
| Float of float
type t =
- | Atomic of var * cop * cst
+ | Atomic_cst of var * cop * cst
+ | Atomic_var of var * cop * var
| And of t * t
diff --git a/solver.ml b/solver.ml
index 985cebc..8beda3a 100644
--- a/solver.ml
+++ b/solver.ml
@@ -33,8 +33,10 @@ let rec pp_property_marabou property =
| Float f -> Stdlib.string_of_float f
in
match property with
- | Atomic ((Input v | Output v), cop, cst) ->
+ | Atomic_cst ((Input v | Output v), cop, cst) ->
Format.sprintf "%s %s %s" v (string_of_cop cop) (string_of_cst cst)
+ | Atomic_var ((Input v1 | Output v1), cop, (Input v2 | Output v2)) ->
+ Format.sprintf "%s %s %s" v1 (string_of_cop cop) v2
| And (p1, p2) ->
let s1 = pp_property_marabou p1 in
let s2 = pp_property_marabou p2 in
--
GitLab