1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
; depends: nary_programs.plf theory_def.plf
; This side condition takes two terms c1 and c2. Via nary_intro,
; we consider theses terms to be either non-unit clauses if they are
; or-applications, or otherwise consider them to be unit clauses if they are
; not. For example, if c1 is (= x y), then (nary_intro f_or c1 false) returns
; (or (= x y) false)
; which we use to compute the concatenation described in following. After
; converting to n-ary form for both c1 and c2, we then concatenate the result
; of removing the first occurrence of l from c1, and the first occurrence of the negation of l from v2
; when pol is tt, or vice versa when pol is ff. Since the resolution may result
; in a singleton list, we run nary_elim as a last step, which ensures that
; we conclude e.g. L and not (or L false), as done in PfRule::RESOLUTION.
; This side condition may fail if c1 or c2 does not contain l with the required
; polarity.
(program sc_resolution ((c1 term) (c2 term) (pol flag) (l term)) term
(nary_elim f_or
(nary_concat f_or
(nary_rm_first_or_self f_or (nary_intro f_or c1 false) (ifequal pol tt l (apply f_not l)) false)
(nary_rm_first_or_self f_or (nary_intro f_or c2 false) (ifequal pol tt (apply f_not l) l) false)
false)
false)
)
; Helper for sc_not_and below, which pushes a not below an application of and.
; In terms of SMT-LIB, this side condition converts:
; (and F1 ... Fn) to (or (not F1) ... (not Fn))
; This side condition may fail if t is not an and-application in n-ary form.
(program sc_not_and_rec ((t term)) term
(match t
((apply t1 t2)
(let t12 (getarg f_and t1)
(apply (apply f_or (apply f_not t12)) (sc_not_and_rec t2)))) ; otherwise not in n-ary form
(true false)) ; note we must flip true to false
)
; Pushes a not below an application of and. In terms of SMT-LIB syntax, this
; side condition converts:
; (not (and F1 ... Fn)) to (or (not F1) ... (not Fn))
(program sc_not_and ((t term)) term
(nary_elim f_or (sc_not_and_rec t) false)
)
; Helper for sc_not_and_rev, which is the inverse of sc_not_and.
; (or (not F1) ... (not Fn)) to (and F1 ... Fn)
; This side condition may fail if t is not an or-application in n-ary form.
(program sc_not_and_rev_rec ((t term)) term
(match t
((apply t1 t2)
(let t12 (getarg f_or t1)
(let t122 (getarg f_not t12)
(apply (apply f_and t122) (sc_not_and_rev_rec t2))))) ; otherwise not in n-ary form
(false true)) ; note we must flip true to false
)
; Pulls not from a list of children of an or-application. In terms of SMT-LIB
; syntax, this side condition converts:
; (or (not F1) ... (not Fn)) to (and F1 ... Fn)
(program sc_not_and_rev ((t term)) term
(nary_elim f_and (sc_not_and_rev_rec t) true)
)
; Process scope side condition. This side condition is used for constructing the
; proven formula for the two cases of PfRule::SCOPE. In particular, it takes:
; - a term t which is expected to be an or-application
; - a term c which is expected to be a suffix of t.
; It may conclude an implication, or the negation of t, based on whether c
; is false, according to the definition of PfRule::SCOPE.
; This side condition may fail if t and c do not have the above properties.
(program sc_process_scope ((t term) (c term)) term
(let premise (sc_not_and_rev (nary_truncate f_or t c false))
(match c
(false (not premise))
(default (=> premise c)))))
|
