Having assertions inside definitions in SMT

Question

I want to capture the assertion inside fac.

int f( x )
{
     if( x == 1) return 1;
     else{
         assert( x > 0 );
         return 2;         
         }
}

int g (x)
{  assert( x > 5 );
   return f(x-1) + f(x-2);
}

I want an smt2 code for this. I can do this by striping the argument and making it global with unique name (also rename inside f), then do this 3 times each with a different name for function. Like below :

( declare-const x1 Int )
(define-fun f1 () Int 
            ( ite ( x1 > 0) 1 2 )
) 
(assert (> x1 0))

( declare-const x2 Int )
(define-fun f2 () Int 
            ( ite ( x2 > 0) 1 2 )
) 
(assert (> x2 0))

( declare-const x3 Int )
(define-fun g1 () Int 
            ( + f1 f2 )
) 
(assert (> x3 5))

I don't want to this. Is there any other way to do this without repeating ?

EDIT My purpose is to find values violating the asserts.

And what is the semantics you want for these asserts? To find if they can ever be called with arguments that can violate them, OR, to restrict the eventual proof to only the values that satisfy them? While these two questions might sound similar, they are important in how you end up modeling this construct. — alias
@JagadeepSai after the edit the "accepted" answer no longer answers your question. Either un-accept the answer, so I can self-delete it, or open a new question. — Patrick Trentin
@PatrickTrentin I think your answer is perfectly acceptable; should remain as accepted! — alias
Great.. What you're trying to do is neither easy, nor it would scale if you did it by hand. Since you seem to be interested in C programs, check out klee.github.io which will check these asserts for you automatically using symbolic simulation. (It'll use z3 as the underlying engine.) You can peruse their documentation to figure out how to do this in large scale. — alias

Patrick Trentin Patrick Trentin · Accepted Answer · 2019-11-02T12:37:07

As far as I know, it is not possible to embed assertions within function definitions.

What I would try to do is to separate the expected behavior, the input assumptions and the output guarantees (if any).

Example:

(define-fun f ((x Int)) Int
      (ite (= x 1) 1 2)
)

(define-fun f-helper ((x Int)) Bool
      (< 0 x)
)

(define-fun g ((x Int)) Int
    (+ (f (- x 1)) (f (- x 2)))
)

(define-fun g-helper ((x Int)) Bool
    (and (< 5 x)
         (f-helper (- x 1))
         (f-helper (- x 2))
    )
)

(declare-const x Int)
(declare-const y Int)

(assert (and (= y (g x))
             (g-helper x)
))

(check-sat)
(get-model)

In this example we use f to model the behavior of the original function f, and f-helper to model the assumptions of f. The output, using the online Z3 tool, is as follows:

sat
(model 
  (define-fun x () Int
    6)
  (define-fun y () Int
    4)
)

I would conclude saying that this approach could become tricky as soon as f and g are used inside both positive and negative contexts.. in this case one should pay extra attention that the polarity of the assertions is correct wrt. the expected result.

Having assertions inside definitions in SMT

1 Answers