From bfd27b25d687b7acde20e36786870464e6147d31 Mon Sep 17 00:00:00 2001
From: Jochen Hoenicke <hoenicke@gmail.com>
Date: Mon, 10 Feb 2020 16:53:21 +0100
Subject: [PATCH] Added all split xor rules

---
 src/smtinterpol/proofrules_to_clauses.ml | 5 ++++-
 src/smtinterpol/prooftree_ast.ml         | 6 ++++--
 src/smtinterpol/smtlib_to_proofrules.ml  | 6 ++++--
 3 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/src/smtinterpol/proofrules_to_clauses.ml b/src/smtinterpol/proofrules_to_clauses.ml
index 34012e99..e518f402 100644
--- a/src/smtinterpol/proofrules_to_clauses.ml
+++ b/src/smtinterpol/proofrules_to_clauses.ml
@@ -273,7 +273,10 @@ let translate_rewrite rewritee_clause rewrite_rule rewrite_formula =
 
 let translate_split unsplit_clause split_rule =
   match split_rule with
-  | Split_xor_2 -> 
+  | Split_xor_plus_1 | Split_xor_minus_1 ->
+    let split_clause = lmkOther (ImmBuildDef unsplit_clause) None in
+    split_clause
+  | Split_xor_plus_2 | Split_xor_minus_2 -> 
     let split_clause = lmkOther (ImmBuildDef2 unsplit_clause) None in
     split_clause
   | Split_notOr ->
diff --git a/src/smtinterpol/prooftree_ast.ml b/src/smtinterpol/prooftree_ast.ml
index fc4a8920..aa6225f6 100644
--- a/src/smtinterpol/prooftree_ast.ml
+++ b/src/smtinterpol/prooftree_ast.ml
@@ -13,8 +13,10 @@ type rewrite_rule =
   | Rewrite_intern
 
 type split_rule =
-  | Split_xor_1
-  | Split_xor_2
+  | Split_xor_minus_1
+  | Split_xor_minus_2
+  | Split_xor_plus_1
+  | Split_xor_plus_2
   | Split_notOr
 
 type equality_proof =
diff --git a/src/smtinterpol/smtlib_to_proofrules.ml b/src/smtinterpol/smtlib_to_proofrules.ml
index ba9a1df4..6e374133 100644
--- a/src/smtinterpol/smtlib_to_proofrules.ml
+++ b/src/smtinterpol/smtlib_to_proofrules.ml
@@ -8,8 +8,10 @@ let string_of_single_atttribute = function
   | (_, [AttributeKeyword (_, s)]) -> s
 
 let from_split_annotation = function
-  | ":xor-1" -> Split_xor_1
-  | ":xor-2" -> Split_xor_2
+  | ":xor-1" -> Split_xor_minus_1
+  | ":xor-2" -> Split_xor_minus_2
+  | ":xor+1" -> Split_xor_plus_1
+  | ":xor+2" -> Split_xor_plus_2
   | ":notOr" -> Split_notOr
 
 let from_rewrite_annotation = function