Add bitvector concat and xor to ACI_NORM

include/cvc5/cvc5_proof_rule.h

@@ -212,8 +212,10 @@ enum ENUM(ProofRule)
    * This method normalizes currently based on two kinds of operators:
    * (1) those that are associative, commutative, idempotent, and have an
    * identity element (examples are or, and, bvand),
-   * (2) those that are associative and have an identity element (examples
-   * are str.++, re.++).
+   * (2) those that are associative, commutative and have an identity
+   * element (bvxor),
+   * (3) those that are associative and have an identity element (examples
+   * are concat, str.++, re.++).
    * \endverbatim
    */
   EVALUE(ACI_NORM),

proofs/eo/cpc/Cpc.eo

@@ -336,7 +336,7 @@
   :conclusion (not (= t s))
 )
 
-;;;;; ProofRule::DISTINCT_CARD_CONFLICT
+;;;;; ProofRule::ACI_NORM
 
 ; define: $get_aci_normal_form
 ; args:
@@ -352,14 +352,16 @@
               (xs1 (Seq U)) (xs2 (Seq U) :list))
     t
     (
-      ((or x1 x2)        ($get_aci_norm t))
-      ((and x1 x2)       ($get_aci_norm t))
-      ((re.union x1 x2)  ($get_aci_norm t))
-      ((re.inter x1 x2)  ($get_aci_norm t))
-      ((bvor xb1 xb2)    ($get_aci_norm t))
-      ((bvand xb1 xb2)   ($get_aci_norm t))
+      ((or x1 x2)        ($get_aci_norm t true))
+      ((and x1 x2)       ($get_aci_norm t true))
+      ((re.union x1 x2)  ($get_aci_norm t true))
+      ((re.inter x1 x2)  ($get_aci_norm t true))
+      ((bvor xb1 xb2)    ($get_aci_norm t true))
+      ((bvand xb1 xb2)   ($get_aci_norm t true))
+      ((bvxor xb1 xb2)   ($get_aci_norm t false))
       ((str.++ xs1 xs2)  ($get_a_norm t))
       ((re.++ x1 x2)     ($get_a_norm t))
+      ((concat xb1 xb2)  ($get_a_norm t))
       (x                 x)
     )
   )

proofs/eo/cpc/expert/CpcExpert.eo

@@ -54,9 +54,9 @@
   (eo::match ((x1 Bool) (x2 Bool :list) (m Int) (xf1 (FiniteField m)) (xf2 (FiniteField m) :list))
     t
     (
-      ((sep x1 x2)       ($get_aci_norm t))
-      ((ff.add xf1 xf2)  ($get_aci_norm t))
-      ((ff.mul xf1 xf2)  ($get_aci_norm t))
+      ((sep x1 x2)       ($get_aci_norm t true))
+      ((ff.add xf1 xf2)  ($get_aci_norm t true))
+      ((ff.mul xf1 xf2)  ($get_aci_norm t true))
     )
   )
 )

proofs/eo/cpc/programs/AciNorm.eo

@@ -29,18 +29,19 @@
 ; - id S: The nil terminator of f.
 ; - s1 S: The first term to process.
 ; - s2 S: The second term to process.
+; - isi Bool: Whether f is idempotent.
 ; return: the result of appending the children of two applications s1 and s2 of the ACI operator f.
-(program $ac_append ((T Type) (S Type) (U Type) (f (-> T U S)) (id S) (x S) (x1 T) (x2 U :list) (y1 T) (y2 U :list))
-  ((-> T U S) S S S) S
+(program $ac_append ((T Type) (S Type) (U Type) (f (-> T U S)) (id S) (x S) (x1 T) (x2 U :list) (y1 T) (y2 U :list) (isi Bool))
+  ((-> T U S) S S S Bool) S
   (
-    (($ac_append f id (f x1 x2) (f y1 y2)) (eo::ite (eo::is_eq x1 y1)
-                                             ($ac_append f id (f x1 x2) y2)
-                                           (eo::ite ($compare_var x1 y1)
-                                             (eo::cons f x1 ($ac_append f id x2 (f y1 y2)))
-                                             (eo::cons f y1 ($ac_append f id (f x1 x2) y2)))))
-    (($ac_append f id (f x1 x2) id)        (f x1 x2))
-    (($ac_append f id id (f y1 y2))        (f y1 y2))
-    (($ac_append f id id id)               id)
+    (($ac_append f id (f x1 x2) (f y1 y2) isi)  (eo::ite (eo::ite (eo::is_eq x1 y1) isi false)
+                                                  ($ac_append f id (f x1 x2) y2 isi)
+                                                  (eo::ite ($compare_var x1 y1)
+                                                    (eo::cons f x1 ($ac_append f id x2 (f y1 y2) isi))
+                                                    (eo::cons f y1 ($ac_append f id (f x1 x2) y2 isi)))))
+    (($ac_append f id (f x1 x2) id isi)         (f x1 x2))
+    (($ac_append f id id (f y1 y2) isi)         (f y1 y2))
+    (($ac_append f id id id isi)                id)
   )
 )
 
@@ -49,25 +50,27 @@
 ; - f (-> T U S): The function, which is assumed to be associative, commutative, idempotent and has the given identity.
 ; - id S: The nil terminator of f.
 ; - s S: The term to process.
+; - isi Bool: Whether f is idempotent.
 ; return: the result of normalizing s based on ACI reasoning.
-(program $get_aci_norm_rec ((T Type) (S Type) (U Type) (f (-> T U S)) (id S) (x S) (x1 T) (x2 U :list))
-  ((-> T U S) S S) S
+(program $get_aci_norm_rec ((T Type) (S Type) (U Type) (f (-> T U S)) (id S) (x S) (x1 T) (x2 U :list) (isi Bool))
+  ((-> T U S) S S Bool) S
   (
-    (($get_aci_norm_rec f id (f id x2))   ($get_aci_norm_rec f id x2))
-    (($get_aci_norm_rec f id (f x1 x2))   ($ac_append f id ($get_aci_norm_rec f id x1) ($get_aci_norm_rec f id x2)))
-    (($get_aci_norm_rec f id id)          id)
-    (($get_aci_norm_rec f id x)           (eo::cons f x id))
+    (($get_aci_norm_rec f id (f id x2) isi)   ($get_aci_norm_rec f id x2 isi))
+    (($get_aci_norm_rec f id (f x1 x2) isi)   ($ac_append f id ($get_aci_norm_rec f id x1 isi) ($get_aci_norm_rec f id x2 isi) isi))
+    (($get_aci_norm_rec f id id isi)          id)
+    (($get_aci_norm_rec f id x isi)           (eo::cons f x id))
   )
 )
 
 ; define: $get_aci_norm
 ; args:
 ; - t T: The term to process.
+; - isi Bool: Whether f is idempotent.
 ; return: the result of normalizing s based on ACI reasoning.
-(define $get_aci_norm ((T Type :implicit) (t T))
+(define $get_aci_norm ((T Type :implicit) (t T) (isi Bool))
   (eo::match ((S Type) (U Type) (V Type) (f (-> S U V)) (x S) (y U :list))
     t
-    (((f x y) (eo::define ((id (eo::nil f x y))) ($singleton_elim_aci f id ($get_aci_norm_rec f id t))))))
+    (((f x y) (eo::define ((id (eo::nil f x y))) ($singleton_elim_aci f id ($get_aci_norm_rec f id t isi))))))
 )
 
 ;; =============== for ACI_NORM associative

src/expr/aci_norm.cpp

@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Definition of ProofRule::ACI_NORM
+ * Definition of ProofRule::ACI_NORM.
  */
 
 #include "expr/aci_norm.h"
@@ -133,10 +133,16 @@ bool isAssocCommIdem(Kind k)
   return false;
 }
 
+bool isAssocComm(Kind k)
+{
+  return (k==Kind::BITVECTOR_XOR);
+}
+
 bool isAssoc(Kind k)
 {
   switch (k)
   {
+    case Kind::BITVECTOR_CONCAT:
     case Kind::STRING_CONCAT:
     case Kind::REGEXP_CONCAT: return true;
     default: break;
@@ -161,7 +167,8 @@ Node getACINormalForm(Node a)
   }
   Kind k = a.getKind();
   bool aci = isAssocCommIdem(k);
-  if (!aci && !isAssoc(k))
+  bool ac = isAssocComm(k) || aci;
+  if (!ac && !isAssoc(k))
   {
     // not associative, return self
     a.setAttribute(nfa, a);
@@ -201,7 +208,7 @@ Node getACINormalForm(Node a)
       children.push_back(cur);
     }
   } while (!toProcess.empty());
-  if (aci)
+  if (ac)
   {
     // sort if commutative
     std::sort(children.begin(), children.end());

src/expr/aci_norm.h

@@ -10,7 +10,7 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * Definition of ProofRule::ACI_NORM
+ * Definition of ProofRule::ACI_NORM.
  */
 
 #include "cvc5_private.h"