; Sorts and terms:
(declare sort type)
(declare term type)

; Theory holds: term t holds, where t should have Boolean type
(declare holds (! t term type))

; function constructor :
(declare arrow (! s1 sort (! s2 sort sort)))

; high-order apply :
(declare apply (! t1 term (! t2 term term)))

; Booleans :
(declare true term)
(declare false term)

; Negation
(declare f_not term)
(define not (# t term (apply f_not t)))

; Conjunction
(declare f_and term)
(define and (# t1 term (# t2 term (apply (apply f_and t1) t2))))

; Disjunction
(declare f_or term)
(define or (# t1 term (# t2 term (apply (apply f_or t1) t2))))

; Implication
(declare f_=> term)
(define => (# t1 term (# t2 term (apply (apply f_=> t1) t2))))

; Xor
(declare f_xor term)
(define xor (# t1 term (# t2 term (apply (apply f_xor t1) t2))))

; ITE
(declare f_ite (! s sort term))
(define ite (# s sort (# condition term (# then_branch term (# else_branch term (apply (apply (apply (f_ite s) condition) then_branch) else_branch))))))

; Equality:
; f_= is an equality symbol, which is a term, to be used with an apply
(declare f_=  term)
; this macro enables writing (= t1 t2)
(define = (# t1 term (# t2 term (apply (apply f_= t1) t2))))

; Disequality:
; f_distinct is a disequality symbol, which is a term, to be used with an apply
(declare f_distinct term)
; this macro enables writing (distinct t1 t2)
(define distinct (# t1 term (# t2 term (apply (apply f_distinct t1) t2))))


; Free constants :
(declare var (! v mpz (! s sort term)))

; BOUND_VARIABLE, i.e. a variable
(declare bvar (! v mpz (! s sort term)))

; Quantifiers : 
; universals
(declare f_forall (! v mpz (! s sort term)))
(define forall (# v mpz (# s sort (# t term (apply (f_forall v s) t)))))

; existentials
(declare f_exists (! v mpz (! s sort term)))
(define exists (# v mpz (# s sort (# t term (apply (f_exists v s) t)))))

; witness
(declare f_witness (! v mpz (! s sort term)))
(define witness (# v mpz (# s sort (# t term (apply (f_witness v s) t)))))

; w must be a witness (verify in typechecking or whatever)
(declare skolem (! w term term))

;;;; To write (forall ((x Int)) (P x)):
; (apply (forall v Int) (apply P (bvar v Int)))

; proof-let
(declare plet (! f term (! g term (! p (holds g) (! u (! v (holds g) (holds f)) (holds f))))))
; scope, where note that this assumes f is in n-ary, null-terminated form
(declare scope (! f term (! g term (! u (! v (holds g) (holds f)) (holds (or (not g) f))))))
; trust
(declare trust (! f term (holds f)))
(declare flag type)
(declare tt flag)
(declare ff flag)

(declare Ok type)
(declare ok Ok)

; remove the first occurrence of l from t, where t is an n-ary, null-terminated chain
(program nary_rm_first ((f term) (t term) (l term)) term
  (match t
    ((apply t1 t2)  ; otherwise at end, l not found
      (match t1
        ((apply f t12) (ifequal t12 l t2 (apply t1 (nary_rm_first f t2 l)))))))   ; otherwise not in n-ary form (for f)
)

; also checks t == l, return nt if so, where nt is a null terminator
(program nary_rm_first_or_self ((f term) (t term) (l term) (nt term)) term
  (ifequal t l nt (nary_rm_first f t l))
)

; does t contain l? where t is an n-ary, null-terminated chain
(program nary_ctn ((f term) (t term) (l term)) flag
  (match t
    ((apply t1 t2)
      (match t1
        ((apply f t12) (ifequal t12 l tt (nary_ctn f t2 l)))))   ; otherwise not in n-ary form
    (default ff))
)

; also checks t == l
(program nary_ctn_or_self ((f term) (t term) (l term)) flag
  (ifequal t l tt (nary_ctn f t l))
)

; returns true if n-ary null-terminated chain t is a subset of s, interpreted as sets
(program nary_is_subset ((f term) (t term) (s term)) flag
  (match t
    ((apply t1 t2) 
      (match t1
        ((apply f t12) (ifequal (nary_ctn_or_self f s t12) tt (nary_is_subset f t2 s) ff)))) ; otherwise not in n-ary form
    (default tt))
)

(program nary_concat ((f term) (t1 term) (t2 term)) term
  (match t1
    ((apply f t12) (apply f (nary_concat f t12 t2)))
    (default t2))    ; any non-application term is interpreted as the end marker
)

; replaces e.g. (or P false) with P
(program nary_singleton_elim ((f term) (t term) (null term)) term
  (match t
    ((apply t1 t2) 
      ; if null terminated at this level, then we return the head, otherwise not in n-ary form
      (ifequal t2 null (match t1 ((apply f t12) t12)) t))
    (default t))
)

; extract the n^th child of n-ary chain of operator f
(program nary_extract ((f term) (t term) (n mpz)) term
  (match t
    ((apply t1 t2)
      (mp_ifzero n 
        (match t1 ((apply f t12) t12))
        (nary_extract f t2 (mp_add n (mp_neg 1)))
      )))
)
; sorts :
(declare Bool sort)
(declare Int sort)
(declare Real sort)
(declare String sort)
(declare RegLan sort)

;Arith:
(declare int (! v mpz term))
(declare f_int.+ term)
(define int.+ (# x term (# y term (apply (apply f_int.+ x) y))))
(declare f_int.- term)
(define int.- (# x term (# y term (apply (apply f_int.- x) y))))
(declare f_int.* term)
(define int.* (# x term (# y term (apply (apply f_int.* x) y))))
(declare f_int.> term)
(define int.> (# x term (# y term (apply (apply f_int.> x) y))))
(declare f_int.>= term)
(define int.>= (# x term (# y term (apply (apply f_int.>= x) y))))
(declare f_int.< term)
(define int.< (# x term (# y term (apply (apply f_int.< x) y))))
(declare f_int.<= term)
(define int.<= (# x term (# y term (apply (apply f_int.<= x) y))))

; Strings
(declare emptystr term)
(declare char (! v mpz term))
(declare f_str.len term)
(define str.len (# x term (apply f_str.len x)))
(declare f_str.++ term)
(define str.++ (# x term (# y term (apply (apply f_str.++ x) y))))
(declare f_str.substr term)
(define str.substr (# x term (# y term (# z term (apply (apply (apply f_str.substr x) y) z)))))
(declare f_str.contains term)
(define str.contains (# x term (# y term (apply (apply f_str.contains x) y))))
(declare f_str.replace term)
(define str.replace (# x term (# y term (# z term (apply (apply (apply f_str.replace x) y) z)))))
(declare f_str.indexof term)
(define str.indexof (# x term (# y term (# z term (apply (apply (apply f_str.indexof x) y) z)))))
(declare f_str.prefixof term)
(define str.prefixof (# x term (# y term (apply (apply f_str.prefixof x) y))))
(declare f_str.suffixof term)
(define str.suffixof (# x term (# y term (apply (apply f_str.suffixof x) y))))
; Regular expressions
(declare re.allchar term)
(declare re.none term)
(declare re.all term)
(declare f_str.to_re term)
(define str.to_re (# x term (apply f_str.to_re x)))
(declare f_re.* term)
(define re.* (# x term (apply f_re.* x)))
(declare f_re.comp term)
(define re.comp (# x term (apply f_re.comp x)))
(declare f_re.range term)
(define re.range (# x term (# y term (apply (apply f_re.range x) y))))
(declare f_re.++ term)
(define re.++ (# x term (# y term (apply (apply f_re.++ x) y))))
(declare f_re.inter term)
(define re.inter (# x term (# y term (apply (apply f_re.inter x) y))))
(declare f_re.union term)
(define re.union (# x term (# y term (apply (apply f_re.union x) y))))
(declare f_re.loop (! n1 mpz (! n2 mpz term)))
(define re.loop (# n1 mpz (# n2 mpz (# x term (apply (f_re.loop n1 n2) x)))))
; membership
(declare f_str.in_re term)
(define str.in_re (# x term (# y term (apply (apply f_str.in_re x) y))))








;  // ======== CNF And Neg
;  // Children: ()
;  // Arguments: ((and f1 ... Fn))
;  // ---------------------
;  // Conclusion: (or (and f1 ... Fn) (not f1) ... (not Fn))
;  CNF_AND_NEG,

; Note that all rules below add the null terminator "false" to the conclusion of or

(declare cnf_and_pos (! f1 term (! f2 term (! n mpz (! r (^ (nary_extract f_and f1 n) f2) (holds (or (not f1) (or f2 false))))))))
(declare cnf_or_pos (! f term (holds (or (not f) (or f false)))))
(declare cnf_or_neg (! f1 term (! f2 term (! n mpz (! r (^ (nary_extract f_or f1 n) f2) (holds (or f1 (or (not f2) false))))))))

(declare cnf_implies_pos (! f1 term (! f2 term (holds (or (not (=> f1 f2)) (or (not f1) (or f2 false)))))))
(declare cnf_implies_neg1 (! f1 term (! f2 term (holds (or (=> f1 f2) (or f1 false))))))
(declare cnf_implies_neg2 (! f1 term (! f2 term (holds (or (=> f1 f2) (or (not f2) false))))))

(declare cnf_equiv_pos1 (! f1 term (! f2 term (holds (or (not (= f1 f2)) (or (not f1) (or f2 false)))))))
(declare cnf_equiv_pos2 (! f1 term (! f2 term (holds (or (not (= f1 f2)) (or f1 (or (not f2) false)))))))
(declare cnf_equiv_neg1 (! f1 term (! f2 term (holds (or (= f1 f2) (or f1 (or f2 false)))))))
(declare cnf_equiv_neg2 (! f1 term (! f2 term (holds (or (= f1 f2) (or (not f1) (or (not f2) false)))))))

(declare cnf_xor_pos1 (! f1 term (! f2 term (holds (or (not (xor f1 f2)) (or f1 (or f2 false)))))))
(declare cnf_xor_pos2 (! f1 term (! f2 term (holds (or (not (xor f1 f2)) (or (not f1) (or (not f2) false)))))))
(declare cnf_xor_neg1 (! f1 term (! f2 term (holds (or (xor f1 f2) (or (not f1) (or f2 false)))))))
(declare cnf_xor_neg2 (! f1 term (! f2 term (holds (or (xor f1 f2) (or f1 (or (not f2) false)))))))

(declare cnf_ite_pos1 (! c term (! f1 term (! f2 term (holds (or (not ((ite Bool) c f1 f2)) (or (not c) (or f1 false))))))))
(declare cnf_ite_pos2 (! c term (! f1 term (! f2 term (holds (or (not ((ite Bool) c f1 f2)) (or c (or f2 false))))))))
(declare cnf_ite_pos3 (! c term (! f1 term (! f2 term (holds (or (not ((ite Bool) c f1 f2)) (or f1 (or f2 false))))))))
(declare cnf_ite_neg1 (! c term (! f1 term (! f2 term (holds (or ((ite Bool) c f1 f2) (or (not c) (or (not f1) false))))))))
(declare cnf_ite_neg2 (! c term (! f1 term (! f2 term (holds (or ((ite Bool) c f1 f2) (or c (or (not f2) false))))))))
(declare cnf_ite_neg3 (! c term (! f1 term (! f2 term (holds (or ((ite Bool) c f1 f2) (or (not f1) (or (not f2) false))))))))