From 35e5e30e93ed32ea0775fea449457ab9cc483af5 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 22 Dec 2020 14:59:21 -0500
Subject: [PATCH] fix(smtlib): handle "xor"

---
 src/smtlib/Form.ml      | 1 +
 src/smtlib/Typecheck.ml | 4 ++++
 2 files changed, 5 insertions(+)

diff --git a/src/smtlib/Form.ml b/src/smtlib/Form.ml
index 417fd943..2dc21cfc 100644
--- a/src/smtlib/Form.ml
+++ b/src/smtlib/Form.ml
@@ -134,6 +134,7 @@ let imply_l st xs y = match xs with
   | _ -> T.app_fun st Funs.imply (IArray.of_list @@ y :: xs)
 
 let imply st a b = imply_a st (IArray.singleton a) b
+let xor st a b = not_ st (equiv st a b)
 
 let distinct_l tst l =
   match l with
diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index 80337856..17df956b 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -144,6 +144,10 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
             errorf_ctx ctx "expected term, not type; got `%s`" f
         end
     end
+  | PA.App ("xor", [a;b]) ->
+    let a = conv_term ctx a in
+    let b = conv_term ctx b in
+    Form.xor ctx.tst a b
   | PA.App (f, args) ->
     let args = List.map (conv_term ctx) args in
     begin match find_id_ ctx f with