Add option :bv-sort-ac true

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/ast/ast_lt.cpp

@@ -134,6 +134,16 @@ bool lt(ast * n1, ast * n2) {
     }
 }
 
+bool is_sorted(unsigned num, expr * const * ns) {
+    for (unsigned i = 1; i < num; i++) {
+        ast * prev = ns[i-1];
+        ast * curr = ns[i];
+        if (lt(curr, prev))
+            return false;
+    }
+    return true;
+}
+
 bool lex_lt(unsigned num, ast * const * n1, ast * const * n2) {
     for (unsigned i = 0; i < num; i ++) {
         if (n1[i] == n2[i])

src/ast/ast_lt.h

@@ -22,6 +22,7 @@ Revision History:
 class ast;
 
 bool lt(ast * n1, ast * n2);
+bool is_sorted(unsigned num, expr * const * ns);
 
 struct ast_to_lt {
     bool operator()(ast * n1, ast * n2) const { return lt(n1, n2); }

src/ast/rewriter/bv_rewriter.cpp

@@ -64,6 +64,7 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_split_concat_eq = p.split_concat_eq();
     m_udiv2mul = p.udiv2mul();
     m_bvnot2arith = p.bvnot2arith();
+    m_bv_sort_ac = p.bv_sort_ac();
     m_mkbv2num = _p.get_bool("mkbv2num", false);
 }
 
@@ -1315,7 +1316,7 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
         return BR_REWRITE2;
     }
 
-    if (!flattened && !merged && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero()))) {
+    if (!flattened && !merged && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero())) && (!m_bv_sort_ac || is_sorted(num, args))) {
         return BR_FAILED;
     }
 
@@ -1331,6 +1332,8 @@ br_status bv_rewriter::mk_bv_or(unsigned num, expr * const * args, expr_ref & re
         result = new_args[0];
         return BR_DONE;
     default:
+        if (m_bv_sort_ac)
+            std::sort(new_args.begin(), new_args.end(), ast_to_lt());
         result = m_util.mk_bv_or(new_args.size(), new_args.c_ptr());
         return BR_DONE;
     }
@@ -1456,7 +1459,8 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
         return BR_REWRITE3;
     } 
 
-    if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1)))))
+    if (!merged && !flattened && (num_coeffs == 0 || (num_coeffs == 1 && !v1.is_zero() && v1 != (rational::power_of_two(sz) - numeral(1)))) &&
+        (!m_bv_sort_ac || is_sorted(num, args)))
         return BR_FAILED;
 
     ptr_buffer<expr> new_args;
@@ -1497,6 +1501,8 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
         }
         __fallthrough;
     default:
+        if (m_bv_sort_ac)
+            std::sort(new_args.begin(), new_args.end(), ast_to_lt());
         result = m_util.mk_bv_xor(new_args.size(), new_args.c_ptr());
         return BR_DONE;
     }

src/ast/rewriter/bv_rewriter.h

@@ -68,6 +68,7 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_split_concat_eq;
     bool       m_udiv2mul;
     bool       m_bvnot2arith;
+    bool       m_bv_sort_ac;
 
     bool is_zero_bit(expr * x, unsigned idx);
 

src/ast/rewriter/bv_rewriter_params.pyg

@@ -8,5 +8,6 @@ def_module_params(module_name='rewriter',
                           ("elim_sign_ext", BOOL, True, "expand sign-ext operator using concat and extract"),
                           ("hi_div0", BOOL, True, "use the 'hardware interpretation' for division by zero (for bit-vector terms)"),
                           ("mul2concat", BOOL, False, "replace multiplication by a power of two into a concatenation"),
-                          ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)")
+                          ("bvnot2arith", BOOL, False, "replace (bvnot x) with (bvsub -1 x)"),
+                          ("bv_sort_ac", BOOL, False, "sort the arguments of all AC operators")
                           ))