Optimise propositional encoding of object_size

Avoid creating equalities over the postponed bitvector when the object
literals trivially aren't equal, and directly encode bitwise equality
when the object literals are trivially equal (and stop searching for a
matching object). In all other cases, avoid unnecessary Tseitin
variables to encode the postponed bitvector equality.

When running on various proofs done for AWS open-source projects, this
changes the performance as follows (when comparing to #7021): with
CaDiCaL as back-end, the total solver time for the hardest 46 proofs
changes from 26779.7 to 22409.9 seconds (4369.8 seconds speed-up); with
Minisat, however, the hardest 49 proofs take 28616.7 instead of 28420.4
seconds (196.3 seconds slow-down). Across these benchmarks, 11.7% of
variables and 12.8% of clauses are removed.

Author: tautschnig

src/solvers/flattening/bv_pointers.cpp

@@ -958,9 +958,26 @@ void bv_pointerst::do_postponed(
       PRECONDITION(size_bv.size() == postponed.bv.size());
 
       literalt l1=bv_utils.equal(bv, saved_bv);
+      if(l1.is_true())
+      {
+        for(std::size_t i = 0; i < postponed.bv.size(); ++i)
+          prop.set_equal(postponed.bv[i], size_bv[i]);
+        break;
+      }
+      else if(l1.is_false())
+        continue;
+#define COMPACT_OBJECT_SIZE_EQ
+#ifndef COMPACT_OBJECT_SIZE_EQ
       literalt l2=bv_utils.equal(postponed.bv, size_bv);
 
       prop.l_set_to_true(prop.limplies(l1, l2));
+#else
+      for(std::size_t i = 0; i < postponed.bv.size(); ++i)
+      {
+        prop.lcnf({!l1, !postponed.bv[i], size_bv[i]});
+        prop.lcnf({!l1, postponed.bv[i], !size_bv[i]});
+      }
+#endif
     }
   }
   else