Tracking of asserts

[ndreuu]

Is there a way to match statements from a refutation with statements from the original system? I tried to use datalog for using keyword "named". But for the example below, I received a refutation without named asserts.

(declare-datatype list ((nil) (cons (car Int) (cdr list))))

(declare-rel Inv (list Int Int) )
(declare-rel length (list Int) )
(declare-rel error_taintHypAssert_0 ())

(rule (! (length nil 0) :named name1))

(declare-var x Int) 
(declare-var xs list) 
(declare-var n Int)
(rule (! (=> (length xs n) (length (cons x xs) (- n 1))) :named name))

(declare-var y1 list) 
(declare-var i1 Int)
(rule (! (=> (length y1 i1) (Inv y1 i1 i1)) :named name2))

(declare-var y2 list) 
(declare-var i2 Int) 
(declare-var j2 Int) 
(declare-var y12 list) 
(declare-var j12 Int) 
(declare-var tmp2 Int)
(rule (! (=> (and (Inv y2 i2 j2) (length y2 j2) (= y2 (cons tmp2 y12)) (length y12 j12)) (Inv y12 (- i2 1) j12)) :named name3))

(declare-var y3 list)
(declare-var i3 Int) 
(declare-var j3 Int)
(rule (! (=> (and (Inv y3 i3 j3) (length y3 j3) (< i3 0)) error_taintHypAssert_0) :named name4))

(query error_taintHypAssert_0 :print-answer true)

sat
(let ((a!1 (forall ((A list) (B Int) (C Int))
             (! (=> (and (Inv A C B) (length A B) (not (<= 0 C))) query!0)
                :weight 0)))
      (a!2 (asserted (forall ((A list) (B Int))
                       (! (=> (length A B) (Inv A B B)) :weight 0))))
      (a!3 (forall ((A Int) (B list) (C Int) (D list) (E Int))
             (! (=> (and (length D E) (= B (cons C D)) (= A (+ (- 1) E)))
                    (length B A))
                :weight 0))))
(let ((a!4 ((_ hyper-res 0 0 0 1)
             (asserted a!3)
             ((_ hyper-res 0 0) (asserted (length nil 0)) (length nil 0))
             (length (cons 2 nil) (- 1)))))
(let ((a!5 ((_ hyper-res 0 0 0 1 0 2)
             (asserted a!1)
             ((_ hyper-res 0 0 0 1) a!2 a!4 (Inv (cons 2 nil) (- 1) (- 1)))
             a!4
             query!0)))
  (mp a!5 (asserted (=> query!0 false)) false))))

[NikolajBjorner]

I don't think there is systematic support for this.

You can add tracking literals and disable some inlining pre-processing. fp.xform.inline_eager=false fp.xform.inline_linear=false fp.xform.subsumption_checker=false

(declare-datatype list ((nil) (cons (car Int) (cdr list))))

(declare-rel name1 ())
(declare-rel Inv (list Int Int) )
(declare-rel length (list Int) )
(declare-rel error_taintHypAssert_0 ())

(rule name1)
(rule (=> name1 (length nil 0)))

(declare-rel name ())
(declare-var x Int) 
(declare-var xs list) 
(declare-var n Int)
(rule name)
(rule (=> (and name (length xs n)) (length (cons x xs) (- n 1))))

(declare-var y1 list) 
(declare-var i1 Int) 
(rule (! (=> (length y1 i1) (Inv y1 i1 i1)) :named name2))

(declare-rel name3 ())
(declare-var y2 list) 
(declare-var i2 Int) 
(declare-var j2 Int) 
(declare-var y12 list) 
(declare-var j12 Int) 
(declare-var tmp2 Int)
(rule name3)
(rule (! (=> (and name3 (Inv y2 i2 j2) (length y2 j2) (= y2 (cons tmp2 y12)) (length y12 j12)) (Inv y12 (- i2 1) j12)) :named name3xx))

You may also be able to use quantifier tagging if you use the SMTLIB front-end, but the tags don't get printed by the default pretty printer.

(rule (forall ((y1 list) (i1 Int)) (! (=> (length y1 i1) (Inv y1 i1 i1)) :qid name2)))