Added all split xor rules

dan-blank · Feb 10, 2020 · bfd27b2 · bfd27b2
1 parent 949ee20
commit bfd27b2
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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