1

I am defining time steps using an Int in SMT-LIB, which forces me to assert things to make sure nothing happens in the negatives:

(declare-sort Pkg) ; A package
(define-sort Time () Int) ; The installation step
; ...
(assert (forall ((t Time) (p Pkg)) (=> (< t 0) (not (installed p t)))))

I saw that in Z3 we can define inductive Nats in the usual style. Would it be good to use the inductive definition of Nat or is there a better way of doing what I am trying to do above?

buggymcbugfix
  • 321
  • 1
  • 11

1 Answers1

3

You should really stick to Int, and put in >= 0 constraints appropriately. Z3 knows a lot about Int, has all sorts of proof rules and tricks to deal with it. While you can indeed define an inductive Nat type, you'll lose all the internal machinery for dealing with integers, and due to the recursive definition Z3's decision procedures will be less effective; especially in combination with other theories.

Having said that, it is impossible to know unless you try: There might be some problem domains where the inductive definition might fit better. But just by purely looking at the kind of you're problem dealing with, good old Int seems to be the right choice for you.

Also see this related question: Representing temporal constraints in SMT-LIB which is definitely relevant in your context.

alias
  • 28,120
  • 2
  • 23
  • 40
  • Thanks for your view. I had seen the question you linked to (_Representing temporal constraints_), but I'm not sure how I would use Reals in my case, because I am looking at discrete steps like in a state machine. If I manage to use Reals anyway I'll feed back how that went. – buggymcbugfix Mar 03 '18 at 19:46