bug #61

regression-tests/horn-adt/Answers

@@ -83,5 +83,11 @@ adt-bug.smt2
 sat
 (define-fun pred1 ((A Int) (B abi_type) (C f_type) (D f_type)) Bool (or (not (= B a)) (and (= D C) (= A 0))))
 
+de-brujin-bug.smt2
+sat
+(define-fun mmin ((A f)) Bool (= (h 0 g) A))
+(define-fun n ((A f)) Bool (or (or (and (and (= (_size A) (_size g)) (= (_size e) 1)) (>= (_size g) 1)) (and (and (and (is-b e) (= (_size e) 3)) (and (>= (_size A) 1) (>= (_size g) 1))) (is-b e))) (and (and (and (is-b e) (and (and (and (and (or (and (is-g A) (>= (_size e) 4)) (and (is-h A) (>= (_size e) 5))) (or (and (is-g A) (>= (_size e) 5)) (and (is-h A) (>= (_size e) 4)))) (>= (+ (_size A) (_size e)) 6)) (>= (_size A) 1)) (>= (_size g) 1))) (is-b e)) (= (mod (+ 1 (_size e)) 2) 0))))
+(define-fun p ((A f) (B d1) (C f)) Bool (or (or (and (and (= (_size A) (_size C)) (= (_size B) 1)) (>= (_size C) 1)) (and (and (and (is-b B) (= (_size B) 3)) (and (>= (_size A) 1) (>= (_size C) 1))) (is-b B))) (and (and (and (is-b B) (and (and (and (and (or (and (is-g A) (>= (_size B) 4)) (and (is-h A) (>= (+ (- 1) (_size B)) 4))) (or (and (is-g A) (>= (_size B) 5)) (and (is-h A) (>= (+ 1 (_size B)) 5)))) (>= (+ (_size A) (_size B)) 6)) (>= (_size A) 1)) (>= (_size C) 1))) (is-b B)) (= (mod (+ 1 (_size B)) 2) 0))))
+
 list-synasc-unsat.smt2
 unsat

regression-tests/horn-adt/de-brujin-bug.smt2

@@ -0,0 +1,17 @@
+; Case in which we previously produced an incorrect solution due
+; to incorrect handling of de Brujin indexes
+; Bug #61
+
+(set-logic HORN)
+
+( declare-datatypes ( ( f 0 ) ) ( ( ( g ) ( h ( i Int ) ( j f ) ) ) ) )
+( declare-datatypes ( ( d1 0 ) ) ( ( ( b ( c d1 ) ( d111 d1 ) ) ( e ) ) ) )
+( declare-fun n ( f ) Bool )
+( declare-fun mmin ( f ) Bool )
+( declare-fun p ( f d1 f ) Bool )
+( assert ( forall ( ( q f ) ) ( => ( and ( mmin q ) ( n q ) ) false ) ) )
+( assert ( forall ( ( s f ) ( w d1 ) ( y d1 ) ( z f ) ) ( => ( and ( p s w s ) ( p z y z ) ) ( p s ( b w y ) z ) ) ) )
+( assert ( forall ( ( q f ) ) ( p q e q ) ) )
+( assert ( forall ( ( q f ) ) ( => ( p q e g ) ( n q ) ) ) )
+( assert ( mmin ( h 0 g ) ) )
+(check-sat)

regression-tests/horn-adt/runtests

@@ -21,6 +21,14 @@ for name in $TESTS; do
     $LAZABS -pngNo -ssol -cex -abstract:off "$@" $name 2>&1 | grep -v "^Elapsed Time"
 done
 
+TESTS="de-brujin-bug.smt2"
+
+for name in $TESTS; do
+    echo
+    echo $name
+    $LAZABS -pngNo -ssol -cex "$@" $name 2>&1 | grep -v "^Elapsed Time"
+done
+
 # Examples with currently unstable output, do not show the counterexample
 
 TESTS="list-synasc-unsat.smt2"

src/main/scala/lazabs/prover/PrincessWrapper.scala

@@ -60,9 +60,6 @@ object PrincessWrapper {
        : (List[IExpression], LinkedHashMap[String, ConstantTerm]) =
     localWrapper.value.formula2Princess(ts, initialSymbolMap, keepReservoir)
 
-  def reduceDeBruijn(e: Expression): Expression =
-    localWrapper.value.reduceDeBruijn(e)
-
   def formula2Eldarica(t: IFormula,
                        symMap : Map[ConstantTerm, String],
                        removeVersions: Boolean): Expression =
@@ -364,22 +361,6 @@ class PrincessWrapper {
       throw new Exception ("" + t + " is not an array type")
   }
 
-  /**
-   * reduces all the debruijn indices by one
-   */
-  def reduceDeBruijn(e: Expression): Expression = e match {
-    case Existential(bv, body) => Existential(bv, reduceDeBruijn(body))
-    case Universal(bv, body) => Universal(bv, reduceDeBruijn(body))
-    case BinaryExpression(e1, op, e2) => BinaryExpression(reduceDeBruijn(e1), op, reduceDeBruijn(e2)).stype(IntegerType())
-    case TernaryExpression(op, e1, e2, e3) => TernaryExpression(op, reduceDeBruijn(e1), reduceDeBruijn(e2), reduceDeBruijn(e3)).stype(IntegerType())
-    case UnaryExpression(op, e) => UnaryExpression(op, reduceDeBruijn(e)).stype(IntegerType())
-    case v@Variable(name,Some(i)) => i match {
-      case 0 => Variable(name,None).stype(IntegerType())
-      case i => Variable("_" + (i-1),Some(i-1)).stype(IntegerType())
-    }
-    case _ => e
-  }
-
 
   /**
    * converts a formula in Princess format to a formula in Eldarica format
@@ -633,7 +614,7 @@ class PrincessWrapper {
       case ISortedQuantified(Quantifier.EX,
                              Sort.Integer, Var0Eq(varCoeff, remainder)) =>
        lazabs.ast.ASTree.Equality(
-         lazabs.ast.ASTree.Modulo(reduceDeBruijn(rvT(remainder)).stype(IntegerType()),
+         lazabs.ast.ASTree.Modulo(rvT(shiftVars(remainder, 1, -1)).stype(IntegerType()),
                                   rvT(varCoeff.abs).stype(IntegerType())),
          NumericalConst(0)).stype(BooleanType())
       case ISortedQuantified(Quantifier.EX, s, e) =>