changed priorities of array rules

Author: pruemmer

src/main/scala/ap/theories/arrays/ExtArray.scala

@@ -774,9 +774,9 @@ class ExtArray (val indexSorts : Seq[Sort],
     override def handleGoal(goal : Goal) : Seq[Plugin.Action] =
       goalState(goal) match {
         case Plugin.GoalState.Eager =>
-          negPreds(goal)              elseDo
           store2store2Eager(goal)
         case Plugin.GoalState.Intermediate =>
+          negPreds(goal)              elseDo
           expandExtensionality(goal)  elseDo
           store2store2Lazy(goal)
         case Plugin.GoalState.Final =>

testcases/smtlib-parser/Answers

@@ -455,14 +455,14 @@ Loading interpolant-typing-bug.smt2 ...
 unsat
 Warning: not all asserted formulas are mentioned in interpolant specification, putting remaining formulas in the last/root partition
 ((and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (<= 0 (+ (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1))))
-(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (and (<= 0 (+ (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1))) (<= 0 (+ (* (- 1) (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) |test_fun_#t~mem11_1|))) (or (not (= test_fun_~x_ref~2.offset_-1 test_fun_~y_ref~2.offset_-1)) (= (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem11_1|))))
-(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1))) (or (and (exists ((var0 Int)) (<= 0 (+ var0 (* (- 1) (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1))))) (not (= test_fun_~x_ref~2.offset_-1 test_fun_~y_ref~2.offset_-1))) (<= 0 (+ (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (* (- 1) (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)))))))
-(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) |test_fun_#t~mem12_3|) oldRank0_-1))) (and (or (and (exists ((var0 Int)) (<= 0 (+ var0 (* (- 1) |test_fun_#t~mem12_3|)))) (not (= test_fun_~x_ref~2.offset_-1 test_fun_~y_ref~2.offset_-1))) (<= 0 (+ (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (* (- 1) |test_fun_#t~mem12_3|)))) (or (not (= test_fun_~x_ref~2.base_-1 test_fun_~y_ref~2.base_-1)) (= (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) (select |#memory_int_-1| test_fun_~y_ref~2.base_-1))))))
-(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (and (= (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem13_4|) (<= 0 (+ |test_fun_#t~mem13_4| (+ (* (- 1) |test_fun_#t~mem12_3|) oldRank0_-1)))) (and (and (or (or (not (= (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) (select |#memory_int_-1| test_fun_~y_ref~2.base_-1))) (not (= test_fun_~x_ref~2.offset_-1 test_fun_~y_ref~2.offset_-1))) (<= 0 (+ |test_fun_#t~mem13_4| (* (- 1) |test_fun_#t~mem12_3|)))) (or (not (= test_fun_~x_ref~2.base_-1 test_fun_~y_ref~2.base_-1)) (= (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) (select |#memory_int_-1| test_fun_~y_ref~2.base_-1)))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ |test_fun_#t~mem13_4| (+ (* (- 1) |test_fun_#t~mem12_3|) oldRank0_-1))) (= (select (select |#memory_int_-1| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem13_4|))))))
-(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (- 1) oldRank0_-1)) (and (and (or (not (= (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) (select |#memory_int_-1| test_fun_~y_ref~2.base_-1))) (not (= test_fun_~x_ref~2.offset_-1 test_fun_~y_ref~2.offset_-1))) (or (not (= test_fun_~x_ref~2.base_-1 test_fun_~y_ref~2.base_-1)) (= (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) (select |#memory_int_-1| test_fun_~y_ref~2.base_-1)))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (= (select (select |#memory_int_-1| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1))))))
-(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (- 1) oldRank0_-1)) (and (and (and (= (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem15_6|) (or (not (= (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) (select |#memory_int_-1| test_fun_~x_ref~2.base_-1))) (and (not (= test_fun_~x_ref~2.offset_-1 test_fun_~y_ref~2.offset_-1)) (= (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem15_6|)))) (or (not (= test_fun_~x_ref~2.base_-1 test_fun_~y_ref~2.base_-1)) (= (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) (select |#memory_int_-1| test_fun_~x_ref~2.base_-1)))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (= (select (select |#memory_int_-1| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem15_6|)))))
-(and (and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (<= 0 (+ (- 1) oldRank0_-1))) (and (<= 0 (+ (- 1) (+ (select (select |#memory_int_7| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1)))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (- 1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) (+ (select (select |#memory_int_7| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) oldRank0_-1)))) (<= 0 (+ (- 1) (+ (select (select |#memory_int_7| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1))))))))
-(and (and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (<= 0 (+ (- 1) oldRank0_-1))) (and (<= 0 (+ (- 1) (+ (select (select |#memory_int_7| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1)))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (or (<= 0 (+ (- 1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) (+ |test_fun_#t~mem18_8| oldRank0_-1)))) (not (= test_fun_~c~2.offset_-1 test_fun_~y_ref~2.offset_-1))) (<= 0 (+ (- 1) (+ (select (select |#memory_int_7| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1)))))))))
+(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (<= 0 (+ (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1))))
+(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (<= 0 (+ (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1))))
+(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) |test_fun_#t~mem12_3|) oldRank0_-1))) (or (not (= test_fun_~x_ref~2.base_-1 test_fun_~y_ref~2.base_-1)) (= (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) (select |#memory_int_-1| test_fun_~y_ref~2.base_-1)))))
+(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (and (= (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem13_4|) (<= 0 (+ |test_fun_#t~mem13_4| (+ (* (- 1) |test_fun_#t~mem12_3|) oldRank0_-1)))) (and (or (not (= test_fun_~x_ref~2.base_-1 test_fun_~y_ref~2.base_-1)) (= (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem13_4|)) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (= (select (select |#memory_int_-1| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem13_4|)))))
+(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (- 1) oldRank0_-1)) (and (or (not (= test_fun_~x_ref~2.base_-1 test_fun_~y_ref~2.base_-1)) (= (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (= (select (select |#memory_int_-1| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1))))))
+(and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (- 1) oldRank0_-1)) (and (and (= (select (select |#memory_int_-1| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem15_6|) (or (not (= test_fun_~x_ref~2.base_-1 test_fun_~y_ref~2.base_-1)) (= (select (select |#memory_int_-1| test_fun_~x_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem15_6|))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (= (select (select |#memory_int_-1| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) |test_fun_#t~mem15_6|)))))
+(and (and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (<= 0 (+ (- 1) oldRank0_-1))) (and (<= 0 (+ (- 1) (+ (select (select |#memory_int_7| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1)))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (<= 0 (+ (- 1) (+ (select (select |#memory_int_7| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1)))) (<= 0 (+ (- 1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) (+ (select (select |#memory_int_7| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) oldRank0_-1))))))))
+(and (and (not (= test_fun_~x_ref~2.base_-1 test_fun_~c~2.base_-1)) (<= 0 (+ (- 1) oldRank0_-1))) (and (<= 0 (+ (- 1) (+ (select (select |#memory_int_7| test_fun_~y_ref~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1)))) (or (not (= test_fun_~y_ref~2.base_-1 test_fun_~c~2.base_-1)) (and (= (select (select |#memory_int_7| test_fun_~c~2.base_-1) test_fun_~c~2.offset_-1) |test_fun_#t~mem18_8|) (and (<= 0 (+ (- 1) (+ (select (select |#memory_int_7| test_fun_~c~2.base_-1) test_fun_~y_ref~2.offset_-1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) oldRank0_-1)))) (or (not (= test_fun_~c~2.offset_-1 test_fun_~y_ref~2.offset_-1)) (<= 0 (+ (- 1) (+ (* (- 1) (select (select |#memory_int_7| test_fun_~x_ref~2.base_-1) test_fun_~x_ref~2.offset_-1)) (+ |test_fun_#t~mem18_8| oldRank0_-1)))))))))))
 Loading modelConstructionBug.smt2 ...
 unsat
 sat