Modify the SMT-LIB printer to declare arrays in a deterministic (alphabetical) order.

2 files changed, 28 insertions, 16 deletions

diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index 812c1e9a..c32b5bf9 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -454,14 +454,26 @@ void ExprSMTLIBPrinter::printSetLogic() {
   *o << " )" << std::endl;
 }
 
+namespace {
+
+struct ArrayPtrsByName {
+  bool operator()(const Array *a1, const Array *a2) const {
+    return a1->name < a2->name;
+  }
+};
+
+}
+
 void ExprSMTLIBPrinter::printArrayDeclarations() {
   // Assume scan() has been called
   if (humanReadable)
     *o << "; Array declarations" << endl;
 
-  // declare arrays
-  for (set<const Array *>::iterator it = usedArrays.begin();
-       it != usedArrays.end(); it++) {
+  // Declare arrays in a deterministic order.
+  std::vector<const Array *> sortedArrays(usedArrays.begin(), usedArrays.end());
+  std::sort(sortedArrays.begin(), sortedArrays.end(), ArrayPtrsByName());
+  for (std::vector<const Array *>::iterator it = sortedArrays.begin();
+       it != sortedArrays.end(); it++) {
     *o << "(declare-fun " << (*it)->name << " () "
                                             "(Array (_ BitVec "
        << (*it)->getDomain() << ") "
@@ -477,8 +489,8 @@ void ExprSMTLIBPrinter::printArrayDeclarations() {
     const Array *array;
 
     // loop over found arrays
-    for (set<const Array *>::iterator it = usedArrays.begin();
-         it != usedArrays.end(); it++) {
+    for (std::vector<const Array *>::iterator it = sortedArrays.begin();
+         it != sortedArrays.end(); it++) {
       array = *it;
       int byteIndex = 0;
       if (array->isConstantArray()) {
diff --git a/test/Expr/print-smt.smt2.good b/test/Expr/print-smt.smt2.good
index cca282af..7b2002b9 100644
--- a/test/Expr/print-smt.smt2.good
+++ b/test/Expr/print-smt.smt2.good
@@ -859,9 +859,9 @@
 ;SMTLIBv2 Query 72
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr2 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr2 (_ bv0 32) ) (_ bv121 8) ) )
 (assert (=  (select const_arr2 (_ bv1 32) ) (_ bv101 8) ) )
 (assert (=  (select const_arr2 (_ bv2 32) ) (_ bv115 8) ) )
@@ -881,8 +881,8 @@
 ;SMTLIBv2 Query 73
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (let (  (?B0 ((_ extract 31  0)  (bvadd  (_ bv18446744073709533360 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B1 (bvadd  (_ bv18446744073709533360 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B2 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and (=  false (bvult  ?B2 (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31312 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31760 64) ?B2 ) (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv111120 64) ?B2 ) (_ bv1 64) ) ) (and (bvult  ?B1 (_ bv1 64) ) (=  false (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed (bvadd  (_ bv3 32) ?B0 ) ) (concat  (select  unnamed (bvadd  (_ bv2 32) ?B0 ) ) (concat  (select  unnamed (bvadd  (_ bv1 32) ?B0 ) ) (select  unnamed ?B0 ) ) ) ) ) ) ) ) ) ) ) )  )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )
@@ -898,9 +898,9 @@
 ;SMTLIBv2 Query 74
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr5 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr5 (_ bv0 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr5 (_ bv1 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr5 (_ bv2 32) ) (_ bv171 8) ) )
@@ -920,9 +920,9 @@
 ;SMTLIBv2 Query 75
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr1 (_ bv0 32) ) (_ bv12 8) ) )
 (assert (=  (select const_arr1 (_ bv1 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr1 (_ bv2 32) ) (_ bv0 8) ) )
@@ -954,9 +954,9 @@
 ;SMTLIBv2 Query 76
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr4 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr4 (_ bv0 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr4 (_ bv1 32) ) (_ bv171 8) ) )
 (assert (=  (select const_arr4 (_ bv2 32) ) (_ bv171 8) ) )
@@ -976,9 +976,9 @@
 ;SMTLIBv2 Query 77
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
-(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun const_arr3 () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (=  (select const_arr3 (_ bv0 32) ) (_ bv12 8) ) )
 (assert (=  (select const_arr3 (_ bv1 32) ) (_ bv0 8) ) )
 (assert (=  (select const_arr3 (_ bv2 32) ) (_ bv0 8) ) )
@@ -1010,8 +1010,8 @@
 ;SMTLIBv2 Query 78
 (set-option :produce-models true)
 (set-logic QF_AUFBV )
-(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) )
 (assert (let (  (?B0 ((_ extract 31  0)  (bvadd  (_ bv18446744073709532800 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B1 (bvadd  (_ bv18446744073709532800 64) (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B2 (bvmul  (_ bv4 64) ((_ sign_extend 32)  (concat  (select  unnamed_1 (_ bv3 32) ) (concat  (select  unnamed_1 (_ bv2 32) ) (concat  (select  unnamed_1 (_ bv1 32) ) (select  unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and (=  false (bvult  ?B2 (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31312 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv31760 64) ?B2 ) (_ bv13 64) ) ) (and (=  false (bvult  (bvadd  (_ bv111120 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv18446744073709533360 64) ?B2 ) (_ bv1 64) ) ) (and (=  false (bvult  (bvadd  (_ bv18446744073709533328 64) ?B2 ) (_ bv1 64) ) ) (and (bvult  ?B1 (_ bv1 64) ) (=  (concat  (select  unnamed (_ bv3 32) ) (concat  (select  unnamed (_ bv2 32) ) (concat  (select  unnamed (_ bv1 32) ) (select  unnamed (_ bv0 32) ) ) ) ) (concat  (select  unnamed_1 (bvadd  (_ bv3 32) ?B0 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv2 32) ?B0 ) ) (concat  (select  unnamed_1 (bvadd  (_ bv1 32) ?B0 ) ) (select  unnamed_1 ?B0 ) ) ) ) ) ) ) ) ) ) ) ) )  )
 (check-sat)
 (get-value ( (select unnamed_1 (_ bv0 32) ) ) )