diff options
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 22 | ||||
| -rw-r--r-- | test/Expr/print-smt.smt2.good | 22 |
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) ) ) ) |