SMT constraints for the FORTE conference paper on string refinements for Jolie language

newsboard-constraints.smt2

(declare-sort Type)
(declare-sort Term)
(declare-fun HasType (Term Type) Bool)

(declare-fun string () Type) ; type of strings of a programming language
(declare-fun nat () Type)    ; type of natural numbers of a programming language
(declare-fun list () Type)   ; type of lists should be parametrized by type of elements but we ignore it for simplicity

(declare-fun BoxString (String) Term)

(declare-fun string-term-val (Term) String)

(assert (forall ((str String))
  (= (string-term-val (BoxString str)) str)))

(assert (forall ((s String))
  (HasType (BoxString s) string)))


(declare-fun guid () Type)
(define-fun guid-re () (RegEx String)
  (let ((hexdigit (re.union (re.range "A" "F") (re.range "0" "9"))))
    (let ((first ((_ re.loop 8 8) hexdigit))
          (second ((_ re.loop 4 4) hexdigit))
          (third ((_ re.loop 4 4) hexdigit))
          (fourth ((_ re.loop 4 4) hexdigit))
          (fifth ((_ re.loop 12 12) hexdigit))
          (dash (str.to.re "-")))
      (re.++ first dash second dash third dash fourth dash fifth))))

(assert (forall ((x Term))
  (! (iff (HasType x guid)
          (and (HasType x string)
               (str.in.re (string-term-val x) guid-re)))
    :pattern ((HasType x guid)))))


(declare-fun user () Type)
(declare-fun mkuser (Term Term Term) Term)
(declare-fun user.uid (Term) Term)
(declare-fun user.name (Term) Term)
(declare-fun user.age (Term) Term)

(assert (forall ((x1 Term) (x2 Term) (x3 Term))
  (! (implies (and (HasType x1 guid)
                   (HasType x2 string)
                   (HasType x3 nat))
      (HasType (mkuser x1 x2 x3) user))

    :pattern ((mkuser x1 x2 x3)))))

(assert (forall ((x1 Term) (x2 Term) (x3 Term))
  (! (implies (HasType (mkuser x1 x2 x3) user)
              (and (HasType x1 guid)
                   (HasType x2 string)
                   (HasType x3 nat)))

  :pattern ((HasType (mkuser x1 x2 x3) user)))))

(assert (forall ((x0 Term) (x1 Term) (x2 Term))
  (! (= (user.uid (mkuser x0 x1 x2))
        x0)
  :pattern ((mkuser x0 x1 x2)))))

(assert (forall ((x0 Term) (x1 Term) (x2 Term))
  (! (= (user.name (mkuser x0 x1 x2))
        x1)
  :pattern ((mkuser x0 x1 x2)))))

(assert (forall ((x0 Term) (x1 Term) (x2 Term))
(! (= (user.age (mkuser x0 x1 x2))
     x2)
:pattern ((mkuser x0 x1 x2)))))

(assert (forall ((t Term))
  (implies (HasType t user)
    (and (HasType (user.uid t)  guid)
         (HasType (user.name t) string)
         (HasType (user.age t)  nat)))))


;find_user_by_name : string -> user
(declare-fun find_user_by_name (Term) Term)
;get_all_users_posts : guid -> list post
(declare-fun get_all_users_posts (Term) Term)
;all_posts_by_user : string -> list post
(declare-fun all_posts_by_user (Term) Term)

(assert (forall ((name Term))
  (! (implies (HasType name string)
      (HasType (find_user_by_name name) user))
  :pattern ((find_user_by_name name)))))

(assert (forall ((uid Term))
  (! (implies (HasType uid guid)
      (HasType (get_all_users_posts uid) list))
  :pattern ((get_all_users_posts uid)))))

(assert (forall ((name Term))
  (! (implies (HasType name string)
      (HasType (all_posts_by_user name) list))
  :pattern ((all_posts_by_user name)))))

(assert (forall ((name Term))
  (! (implies (HasType name string)
      (= (all_posts_by_user name)
         (get_all_users_posts (user.uid (find_user_by_name name)))))
  :pattern ((all_posts_by_user name)))))


(declare-fun label_2846 () Bool)


(push)
(set-info :status unsat)

(assert (not (forall ((t Term))
  (implies (HasType t string)
    (or label_2846
        (HasType (user.uid (find_user_by_name t)) guid))))))

(check-sat)
(pop)

;;; This is a negation of previous theorem so it should be satisfiable but actually we don't get a model in reasonable time
;(push)
;(set-info :status sat)
;
;(assert (forall ((t Term))
;  (implies (HasType t string)
;    (or label_2846
;        (HasType (user.uid (find_user_by_name t)) guid)))))
;
;(check-sat)
;(get-model)
;(pop)

;(push)
;(set-info :status sat)
;
;(assert (not (forall ((t Term))
;  (implies (HasType t string)
;    (or label_2846
;        (HasType (user.name (find_user_by_name t)) guid))))))
;
;(check-sat)
;(get-model)
;(pop)

(push)
(set-info :status unsat)

(assert(forall ((t Term))
  (implies (HasType t string)
    (or label_2846
        (HasType (user.name (find_user_by_name t)) guid)))))

(check-sat)
(pop)