author | wenzelm |
Sun, 08 Jan 2017 13:03:14 +0100 | |
changeset 64832 | f6a09ac4e640 |
parent 63960 | 3daf02070be5 |
child 64927 | a5a09855e424 |
permissions | -rw-r--r-- |
63960
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
1 |
(* Title: Tools/Argo/argo_cc.ML |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
3 |
Author: Dmitriy Traytel and Matthias Franze, TU Muenchen |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
4 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
5 |
Equality reasoning based on congurence closure. It features: |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
6 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
7 |
* congruence closure for any term that participates in equalities |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
8 |
* support for predicates |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
9 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
10 |
These features might be added: |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
11 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
12 |
* caching of explanations while building proofs to obtain shorter proofs |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
13 |
and faster proof checking |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
14 |
* propagating relevant merges of equivalence classes to all other theory solvers |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
15 |
* propagating new relevant negated equalities to all other theory solvers |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
16 |
* creating lemma "f ~= g | a ~= b | f a = g b" for asserted negated equalities |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
17 |
between "f a" and "g b" (dynamic ackermannization) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
18 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
19 |
The implementation is inspired by: |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
20 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
21 |
Robert Nieuwenhuis and Albert Oliveras. Fast Congruence Closure and |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
22 |
Extensions. In Information and Computation, volume 205(4), |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
23 |
pages 557-580, 2007. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
24 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
25 |
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
26 |
Cesare Tinelli. DPLL(T): Fast decision procedures. In Lecture Notes in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
27 |
Computer Science, volume 3114, pages 175-188. Springer, 2004. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
28 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
29 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
30 |
signature ARGO_CC = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
31 |
sig |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
32 |
(* context *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
33 |
type context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
34 |
val context: context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
35 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
36 |
(* simplification *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
37 |
val simplify: Argo_Rewr.context -> Argo_Rewr.context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
38 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
39 |
(* enriching the context *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
40 |
val add_atom: Argo_Term.term -> context -> Argo_Lit.literal option * context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
41 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
42 |
(* main operations *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
43 |
val assume: Argo_Common.literal -> context -> Argo_Lit.literal Argo_Common.implied * context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
44 |
val check: context -> Argo_Lit.literal Argo_Common.implied * context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
45 |
val explain: Argo_Lit.literal -> context -> (Argo_Cls.clause * context) option |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
46 |
val add_level: context -> context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
47 |
val backtrack: context -> context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
48 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
49 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
50 |
structure Argo_Cc: ARGO_CC = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
51 |
struct |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
52 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
53 |
(* tables indexed by pairs of terms *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
54 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
55 |
val term2_ord = prod_ord Argo_Term.term_ord Argo_Term.term_ord |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
56 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
57 |
structure Argo_Term2tab = Table(type key = Argo_Term.term * Argo_Term.term val ord = term2_ord) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
58 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
59 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
60 |
(* equality certificates *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
61 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
62 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
63 |
The solver keeps assumed equalities to produce explanations later on. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
64 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
65 |
A flat equality (lp, (t1, t2)) consists of the assumed literal and its proof |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
66 |
as well as the terms t1 and t2 that are assumed to be equal. The literal expresses |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
67 |
the equality t1 = t2. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
68 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
69 |
A congruence equality (t1, t2) is an equality t1 = t2 where both terms are |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
70 |
applications (f a) and (g b). |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
71 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
72 |
A symmetric equality eq is a marker for applying the symmetry rule to eq. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
73 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
74 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
75 |
datatype eq = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
76 |
Flat of Argo_Common.literal * (Argo_Term.term * Argo_Term.term) | |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
77 |
Cong of Argo_Term.term * Argo_Term.term | |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
78 |
Symm of eq |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
79 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
80 |
fun dest_eq (Flat (_, tp)) = tp |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
81 |
| dest_eq (Cong tp) = tp |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
82 |
| dest_eq (Symm eq) = swap (dest_eq eq) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
83 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
84 |
fun symm (Symm eq) = eq |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
85 |
| symm eq = Symm eq |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
86 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
87 |
fun negate (Flat ((lit, p), tp)) = Flat ((Argo_Lit.negate lit, p), tp) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
88 |
| negate (Cong tp) = Cong tp |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
89 |
| negate (Symm eq) = Symm (negate eq) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
90 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
91 |
fun dest_app (Argo_Term.T (_, Argo_Expr.App, [t1, t2])) = (t1, t2) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
92 |
| dest_app _ = raise Fail "bad application" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
93 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
94 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
95 |
(* context *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
96 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
97 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
98 |
Each representative keeps track of the yet unimplied atoms in which this any member of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
99 |
this representative's equivalence class occurs. An atom is either a list of equalities |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
100 |
between two terms, a list of predicates or a certificate. The certificate denotes that |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
101 |
this equivalence class contains already implied predicates, and the literal accompanying |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
102 |
the certificate specifies the polarity of these predicates. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
103 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
104 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
105 |
datatype atoms = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
106 |
Eqs of (Argo_Term.term * Argo_Term.term) list | |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
107 |
Preds of Argo_Term.term list | |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
108 |
Cert of Argo_Common.literal |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
109 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
110 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
111 |
Each representative has an associated ritem that contains the members of the |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
112 |
equivalence class, the yet unimplied atoms and further information. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
113 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
114 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
115 |
type ritem = { |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
116 |
size: int, (* the size of the equivalence class *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
117 |
class: Argo_Term.term list, (* the equivalence class as a list of distinct terms *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
118 |
occs: Argo_Term.term list, (* a list of all application terms in which members of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
119 |
the equivalence class occur either as function or as argument *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
120 |
neqs: (Argo_Term.term * eq) list, (* a list of terms from disjoint equivalence classes, |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
121 |
for each term of this list there is a certificate of a negated equality that is |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
122 |
required to explain why the equivalence classes are disjoint *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
123 |
atoms: atoms} (* the atoms of the representative *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
124 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
125 |
type repr = Argo_Term.term Argo_Termtab.table |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
126 |
type rdata = ritem Argo_Termtab.table |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
127 |
type apps = Argo_Term.term Argo_Term2tab.table |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
128 |
type trace = (Argo_Term.term * eq) Argo_Termtab.table |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
129 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
130 |
type context = { |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
131 |
repr: repr, (* a table mapping terms to their representatives *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
132 |
rdata: rdata, (* a table mapping representatives to their ritems *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
133 |
apps: apps, (* a table mapping a function and an argument to their application *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
134 |
trace: trace, (* the proof forest used to trace assumed and implied equalities *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
135 |
prf: Argo_Proof.context, (* the proof context *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
136 |
back: (repr * rdata * apps * trace) list} (* backtracking information *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
137 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
138 |
fun mk_context repr rdata apps trace prf back: context = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
139 |
{repr=repr, rdata=rdata, apps=apps, trace=trace, prf=prf, back=back} |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
140 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
141 |
val context = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
142 |
mk_context Argo_Termtab.empty Argo_Termtab.empty Argo_Term2tab.empty Argo_Termtab.empty |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
143 |
Argo_Proof.cc_context [] |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
144 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
145 |
fun repr_of repr t = the_default t (Argo_Termtab.lookup repr t) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
146 |
fun repr_of' ({repr, ...}: context) = repr_of repr |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
147 |
fun put_repr t r = Argo_Termtab.update (t, r) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
148 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
149 |
fun mk_ritem size class occs neqs atoms: ritem = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
150 |
{size=size, class=class, occs=occs, neqs=neqs, atoms=atoms} |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
151 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
152 |
fun as_ritem t = mk_ritem 1 [t] [] [] (Eqs []) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
153 |
fun as_pred_ritem t = mk_ritem 1 [t] [] [] (Preds [t]) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
154 |
fun gen_ritem_of mk rdata r = the_default (mk r) (Argo_Termtab.lookup rdata r) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
155 |
fun ritem_of rdata = gen_ritem_of as_ritem rdata |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
156 |
fun ritem_of_pred rdata = gen_ritem_of as_pred_ritem rdata |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
157 |
fun ritem_of' ({rdata, ...}: context) = ritem_of rdata |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
158 |
fun put_ritem r ri = Argo_Termtab.update (r, ri) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
159 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
160 |
fun add_occ r occ = Argo_Termtab.map_default (r, as_ritem r) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
161 |
(fn {size, class, occs, neqs, atoms}: ritem => mk_ritem size class (occ :: occs) neqs atoms) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
162 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
163 |
fun put_atoms atoms ({size, class, occs, neqs, ...}: ritem) = mk_ritem size class occs neqs atoms |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
164 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
165 |
fun add_eq_atom r atom = Argo_Termtab.map_default (r, as_ritem r) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
166 |
(fn ri as {atoms=Eqs atoms, ...}: ritem => put_atoms (Eqs (atom :: atoms)) ri |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
167 |
| ri => put_atoms (Eqs [atom]) ri) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
168 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
169 |
fun lookup_app apps tp = Argo_Term2tab.lookup apps tp |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
170 |
fun put_app tp app = Argo_Term2tab.update_new (tp, app) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
171 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
172 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
173 |
(* traces for explanations *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
174 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
175 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
176 |
Assumed and implied equalities are collected in a proof forest for being able to |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
177 |
produce explanations. For each equivalence class there is one proof tree. The |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
178 |
equality certificates are oriented towards a root term, that is not necessarily |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
179 |
the representative of the equivalence class. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
180 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
181 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
182 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
183 |
Whenever two equivalence classes are merged due to an equality t1 = t2, the shorter |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
184 |
of the two paths, either from t1 to its root or t2 to its root, is re-oriented such |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
185 |
that the relevant ti becomes the new root of its tree. Then, a new edge between ti |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
186 |
and the other term of the equality t1 = t2 is added to connect the two proof trees. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
187 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
188 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
189 |
fun depth_of trace t = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
190 |
(case Argo_Termtab.lookup trace t of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
191 |
NONE => 0 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
192 |
| SOME (t', _) => 1 + depth_of trace t') |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
193 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
194 |
fun reorient t trace = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
195 |
(case Argo_Termtab.lookup trace t of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
196 |
NONE => trace |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
197 |
| SOME (t', eq) => Argo_Termtab.update (t', (t, symm eq)) (reorient t' trace)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
198 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
199 |
fun new_edge from to eq trace = Argo_Termtab.update (from, (to, eq)) (reorient from trace) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
200 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
201 |
fun with_shortest f (t1, t2) eq trace = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
202 |
(if depth_of trace t1 <= depth_of trace t2 then f t1 t2 eq else f t2 t1 (symm eq)) trace |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
203 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
204 |
fun add_edge eq trace = with_shortest new_edge (dest_eq eq) eq trace |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
205 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
206 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
207 |
To produce an explanation that t1 and t2 are equal, the paths to their root are |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
208 |
extracted from the proof forest. Common ancestors in both paths are dropped. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
209 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
210 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
211 |
fun path_to_root trace path t = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
212 |
(case Argo_Termtab.lookup trace t of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
213 |
NONE => (t, path) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
214 |
| SOME (t', _) => path_to_root trace (t :: path) t') |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
215 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
216 |
fun drop_common root (t1 :: path1) (t2 :: path2) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
217 |
if Argo_Term.eq_term (t1, t2) then drop_common t1 path1 path2 else root |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
218 |
| drop_common root _ _ = root |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
219 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
220 |
fun common_ancestor trace t1 t2 = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
221 |
let val ((root, path1), (_, path2)) = apply2 (path_to_root trace []) (t1, t2) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
222 |
in drop_common root path1 path2 end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
223 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
224 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
225 |
The proof of an assumed literal is typically a hypothesis. If the assumed literal is |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
226 |
already known to be a unit literal, then there is already a proof for it. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
227 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
228 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
229 |
fun proof_of (lit, NONE) lits prf = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
230 |
(insert Argo_Lit.eq_lit (Argo_Lit.negate lit) lits, Argo_Proof.mk_hyp lit prf) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
231 |
| proof_of (_, SOME p) lits prf = (lits, (p, prf)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
232 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
233 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
234 |
The explanation of equality between two terms t1 and t2 is computed based on the |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
235 |
paths from t1 and t2 to their common ancestor t in the proof forest. For each of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
236 |
the two paths, a transitive proof of equality t1 = t and t = t2 is constructed, |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
237 |
such that t1 = t2 follows by transitivity. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
238 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
239 |
Each edge of the paths denotes an assumed or implied equality. Implied equalities |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
240 |
might be due to congruences (f a = g b) for which the equalities f = g and a = b |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
241 |
need to be explained recursively. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
242 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
243 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
244 |
fun mk_eq_proof trace t1 t2 lits prf = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
245 |
if Argo_Term.eq_term (t1, t2) then (lits, Argo_Proof.mk_refl t1 prf) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
246 |
else |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
247 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
248 |
val root = common_ancestor trace t1 t2 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
249 |
val (lits, (p1, prf)) = trans_proof I I trace t1 root lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
250 |
val (lits, (p2, prf)) = trans_proof swap symm trace t2 root lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
251 |
in (lits, Argo_Proof.mk_trans p1 p2 prf) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
252 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
253 |
and trans_proof sw sy trace t root lits prf = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
254 |
if Argo_Term.eq_term (t, root) then (lits, Argo_Proof.mk_refl t prf) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
255 |
else |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
256 |
(case Argo_Termtab.lookup trace t of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
257 |
NONE => raise Fail "bad trace" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
258 |
| SOME (t', eq) => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
259 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
260 |
val (lits, (p1, prf)) = proof_step trace (sy eq) lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
261 |
val (lits, (p2, prf)) = trans_proof sw sy trace t' root lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
262 |
in (lits, uncurry Argo_Proof.mk_trans (sw (p1, p2)) prf) end) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
263 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
264 |
and proof_step _ (Flat (cert, _)) lits prf = proof_of cert lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
265 |
| proof_step trace (Cong tp) lits prf = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
266 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
267 |
val ((t1, t2), (u1, u2)) = apply2 dest_app tp |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
268 |
val (lits, (p1, prf)) = mk_eq_proof trace t1 u1 lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
269 |
val (lits, (p2, prf)) = mk_eq_proof trace t2 u2 lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
270 |
in (lits, Argo_Proof.mk_cong p1 p2 prf) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
271 |
| proof_step trace (Symm eq) lits prf = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
272 |
proof_step trace eq lits prf ||> uncurry Argo_Proof.mk_symm |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
273 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
274 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
275 |
All clauses produced by a theory solver are expected to be a lemma. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
276 |
The lemma proof must hence be the last proof step. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
277 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
278 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
279 |
fun close_proof lit lits (p, prf) = (lit :: lits, Argo_Proof.mk_lemma [lit] p prf) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
280 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
281 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
282 |
The explanation for the equality of t1 and t2 used the above algorithm. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
283 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
284 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
285 |
fun explain_eq lit t1 t2 ({repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
286 |
let val (lits, (p, prf)) = mk_eq_proof trace t1 t2 [] prf |-> close_proof lit |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
287 |
in ((lits, p), mk_context repr rdata apps trace prf back) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
288 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
289 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
290 |
The explanation that t1 and t2 are distinct uses the negated equality u1 ~= u2 that |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
291 |
explains why the equivalence class containing t1 and u1 and the equivalence class |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
292 |
containing t2 and u2 are disjoint. The explanations for t1 = u1 and u2 = t2 are |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
293 |
constructed using the above algorithm. By transitivity, it follows that t1 ~= t2. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
294 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
295 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
296 |
fun finish_proof (Flat ((lit, _), _)) lits p prf = close_proof lit lits (p, prf) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
297 |
| finish_proof (Cong _) _ _ _ = raise Fail "bad equality" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
298 |
| finish_proof (Symm eq) lits p prf = Argo_Proof.mk_symm p prf |-> finish_proof eq lits |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
299 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
300 |
fun explain_neq eq eq' ({repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
301 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
302 |
val (t1, t2) = dest_eq eq |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
303 |
val (u1, u2) = dest_eq eq' |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
304 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
305 |
val (lits, (p, prf)) = proof_step trace eq' [] prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
306 |
val (lits, (p1, prf)) = mk_eq_proof trace t1 u1 lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
307 |
val (lits, (p2, prf)) = mk_eq_proof trace u2 t2 lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
308 |
val (lits, (p, prf)) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
309 |
Argo_Proof.mk_trans p p2 prf |-> Argo_Proof.mk_trans p1 |-> finish_proof eq lits |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
310 |
in ((lits, p), mk_context repr rdata apps trace prf back) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
311 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
312 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
313 |
(* propagating new equalities *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
314 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
315 |
exception CONFLICT of Argo_Cls.clause * context |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
316 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
317 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
318 |
comment missing |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
319 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
320 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
321 |
fun same_repr repr r (t, _) = Argo_Term.eq_term (r, repr_of repr t) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
322 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
323 |
fun has_atom rdata r eq = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
324 |
(case #atoms (ritem_of rdata r) of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
325 |
Eqs eqs => member (Argo_Term.eq_term o snd) eqs eq |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
326 |
| _ => false) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
327 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
328 |
fun add_implied mk_lit repr rdata r neqs (atom as (t, eq)) (eqs, ls) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
329 |
let val r' = repr_of repr t |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
330 |
in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
331 |
if Argo_Term.eq_term (r, r') then (eqs, insert Argo_Lit.eq_lit (mk_lit eq) ls) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
332 |
else if exists (same_repr repr r') neqs andalso has_atom rdata r' eq then |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
333 |
(eqs, Argo_Lit.Neg eq :: ls) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
334 |
else (atom :: eqs, ls) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
335 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
336 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
337 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
338 |
comment missing |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
339 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
340 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
341 |
fun copy_occ repr app (eqs, occs, apps) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
342 |
let val rp = apply2 (repr_of repr) (dest_app app) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
343 |
in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
344 |
(case lookup_app apps rp of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
345 |
SOME app' => (Cong (app, app') :: eqs, occs, apps) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
346 |
| NONE => (eqs, app :: occs, put_app rp app apps)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
347 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
348 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
349 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
350 |
comment missing |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
351 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
352 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
353 |
fun add_lits (Argo_Lit.Pos _, _) = fold (cons o Argo_Lit.Pos) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
354 |
| add_lits (Argo_Lit.Neg _, _) = fold (cons o Argo_Lit.Neg) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
355 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
356 |
fun join_atoms f (Eqs eqs1) (Eqs eqs2) ls = f eqs1 eqs2 ls |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
357 |
| join_atoms _ (Preds ts1) (Preds ts2) ls = (Preds (union Argo_Term.eq_term ts1 ts2), ls) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
358 |
| join_atoms _ (Preds ts) (Cert lp) ls = (Cert lp, add_lits lp ts ls) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
359 |
| join_atoms _ (Cert lp) (Preds ts) ls = (Cert lp, add_lits lp ts ls) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
360 |
| join_atoms _ (Cert lp) (Cert _) ls = (Cert lp, ls) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
361 |
| join_atoms _ _ _ _ = raise Fail "bad atoms" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
362 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
363 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
364 |
comment missing |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
365 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
366 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
367 |
fun join r1 ri1 r2 ri2 eq (eqs, ls, {repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
368 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
369 |
val {size=size1, class=class1, occs=occs1, neqs=neqs1, atoms=atoms1}: ritem = ri1 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
370 |
val {size=size2, class=class2, occs=occs2, neqs=neqs2, atoms=atoms2}: ritem = ri2 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
371 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
372 |
val repr = fold (fn t => put_repr t r1) class2 repr |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
373 |
val class = fold cons class2 class1 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
374 |
val (eqs, occs, apps) = fold (copy_occ repr) occs2 (eqs, occs1, apps) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
375 |
val trace = add_edge eq trace |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
376 |
val neqs = AList.merge Argo_Term.eq_term (K true) (neqs1, neqs2) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
377 |
fun add r neqs = fold (add_implied Argo_Lit.Pos repr rdata r neqs) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
378 |
fun adds eqs1 eqs2 ls = ([], ls) |> add r2 neqs2 eqs1 |> add r1 neqs1 eqs2 |>> Eqs |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
379 |
val (atoms, ls) = join_atoms adds atoms1 atoms2 ls |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
380 |
(* TODO: make sure that all implied literals are propagated *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
381 |
val rdata = put_ritem r1 (mk_ritem (size1 + size2) class occs neqs atoms) rdata |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
382 |
in (eqs, ls, mk_context repr rdata apps trace prf back) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
383 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
384 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
385 |
comment missing |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
386 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
387 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
388 |
fun find_neq ({repr, ...}: context) ({neqs, ...}: ritem) r = find_first (same_repr repr r) neqs |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
389 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
390 |
fun check_join (r1, r2) (ri1, ri2) eq (ecx as (_, _, cx)) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
391 |
(case find_neq cx ri2 r1 of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
392 |
SOME (_, eq') => raise CONFLICT (explain_neq (negate (symm eq)) eq' cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
393 |
| NONE => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
394 |
(case find_neq cx ri1 r2 of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
395 |
SOME (_, eq') => raise CONFLICT (explain_neq (negate eq) eq' cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
396 |
| NONE => join r1 ri1 r2 ri2 eq ecx)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
397 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
398 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
399 |
comment missing |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
400 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
401 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
402 |
fun with_max_class f (rp as (r1, r2)) (rip as (ri1: ritem, ri2: ritem)) eq = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
403 |
if #size ri1 >= #size ri2 then f rp rip eq else f (r2, r1) (ri2, ri1) (symm eq) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
404 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
405 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
406 |
comment missing |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
407 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
408 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
409 |
fun propagate ([], ls, cx) = (rev ls, cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
410 |
| propagate (eq :: eqs, ls, cx) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
411 |
let val rp = apply2 (repr_of' cx) (dest_eq eq) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
412 |
in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
413 |
if Argo_Term.eq_term rp then propagate (eqs, ls, cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
414 |
else propagate (with_max_class check_join rp (apply2 (ritem_of' cx) rp) eq (eqs, ls, cx)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
415 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
416 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
417 |
fun without lit (lits, cx) = (Argo_Common.Implied (remove Argo_Lit.eq_lit lit lits), cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
418 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
419 |
fun flat_merge (lp as (lit, _)) eq cx = without lit (propagate ([Flat (lp, eq)], [], cx)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
420 |
handle CONFLICT (cls, cx) => (Argo_Common.Conflict cls, cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
421 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
422 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
423 |
comment missing |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
424 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
425 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
426 |
fun app_merge app tp (cx as {repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
427 |
let val rp as (r1, r2) = apply2 (repr_of repr) tp |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
428 |
in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
429 |
(case lookup_app apps rp of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
430 |
SOME app' => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
431 |
(case propagate ([Cong (app, app')], [], cx) of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
432 |
([], cx) => cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
433 |
| _ => raise Fail "bad application merge") |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
434 |
| NONE => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
435 |
let val rdata = add_occ r1 app (add_occ r2 app rdata) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
436 |
in mk_context repr rdata (put_app rp app apps) trace prf back end) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
437 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
438 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
439 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
440 |
A negated equality between t1 and t2 is only recorded if t1 and t2 are not already known |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
441 |
to belong to the same class. In that case, a conflict is raised with an explanation |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
442 |
why t1 and t2 are equal. Otherwise, the classes of t1 and t2 are marked as disjoint by |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
443 |
storing the negated equality in the ritems of t1's and t2's representative. All equalities |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
444 |
between terms of t1's and t2's class are implied as negated equalities. Those equalities |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
445 |
are found in the ritems of t1's and t2's representative. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
446 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
447 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
448 |
fun note_neq eq (r1, r2) (t1, t2) ({repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
449 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
450 |
val {size=size1, class=class1, occs=occs1, neqs=neqs1, atoms=atoms1}: ritem = ritem_of rdata r1 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
451 |
val {size=size2, class=class2, occs=occs2, neqs=neqs2, atoms=atoms2}: ritem = ritem_of rdata r2 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
452 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
453 |
fun add r (Eqs eqs) ls = fold (add_implied Argo_Lit.Neg repr rdata r []) eqs ([], ls) |>> Eqs |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
454 |
| add _ _ _ = raise Fail "bad negated equality between predicates" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
455 |
val ((atoms1, atoms2), ls) = [] |> add r2 atoms1 ||>> add r1 atoms2 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
456 |
val ri1 = mk_ritem size1 class1 occs1 ((t2, eq) :: neqs1) atoms1 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
457 |
val ri2 = mk_ritem size2 class2 occs2 ((t1, symm eq) :: neqs2) atoms2 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
458 |
in (ls, mk_context repr (put_ritem r1 ri1 (put_ritem r2 ri2 rdata)) apps trace prf back) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
459 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
460 |
fun flat_neq (lp as (lit, _)) (tp as (t1, t2)) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
461 |
let val rp = apply2 (repr_of' cx) tp |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
462 |
in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
463 |
if Argo_Term.eq_term rp then |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
464 |
let val (cls, cx) = explain_eq (Argo_Lit.negate lit) t1 t2 cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
465 |
in (Argo_Common.Conflict cls, cx) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
466 |
else without lit (note_neq (Flat (lp, tp)) rp tp cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
467 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
468 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
469 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
470 |
(* simplification *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
471 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
472 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
473 |
Only equalities are subject to normalizations. An equality between two expressions e1 and e2 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
474 |
is normalized, if e1 is less than e2 based on the expression ordering. If e1 and e2 are |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
475 |
syntactically equal, the equality between these two expressions is normalized to the true |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
476 |
expression. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
477 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
478 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
479 |
fun norm_eq env = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
480 |
let val e1 = Argo_Rewr.get env 1 and e2 = Argo_Rewr.get env 2 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
481 |
in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
482 |
(case Argo_Expr.expr_ord (e1, e2) of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
483 |
EQUAL => SOME (Argo_Proof.Rewr_Eq_Refl, Argo_Rewr.E Argo_Expr.true_expr) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
484 |
| LESS => NONE |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
485 |
| GREATER => SOME (Argo_Proof.Rewr_Eq_Symm, Argo_Rewr.E (Argo_Expr.mk_eq e2 e1))) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
486 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
487 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
488 |
val simplify = Argo_Rewr.func "(eq (? 1) (? 2))" norm_eq |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
489 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
490 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
491 |
(* declaring atoms *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
492 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
493 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
494 |
Only a genuinely new equality term t for the equality "t1 = t2" is added. If t1 and t2 belong |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
495 |
to the same equality class or if the classes of t1 and t2 are known to be disjoint, the |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
496 |
respective literal is returned together with an unmodified context. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
497 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
498 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
499 |
fun add_eq_term t t1 t2 (rp as (r1, r2)) (cx as {repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
500 |
if Argo_Term.eq_term rp then (SOME (Argo_Lit.Pos t), cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
501 |
else if is_some (find_neq cx (ritem_of rdata r1) r2) then (SOME (Argo_Lit.Neg t), cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
502 |
else |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
503 |
let val rdata = add_eq_atom r1 (t2, t) (add_eq_atom r2 (t1, t) rdata) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
504 |
in (NONE, mk_context repr rdata apps trace prf back) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
505 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
506 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
507 |
Only a genuinely new predicate t, which is an application "t1 t2", is added. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
508 |
If there is a predicate that is known to be congruent to the representatives of t1 and t2, |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
509 |
and that predicate or its negation has already been assummed, the respective literal of t |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
510 |
is returned together with an unmodified context. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
511 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
512 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
513 |
fun add_pred_term t rp (cx as {repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
514 |
(case lookup_app apps rp of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
515 |
NONE => (NONE, mk_context repr (put_ritem t (as_pred_ritem t) rdata) apps trace prf back) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
516 |
| SOME app => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
517 |
(case `(ritem_of_pred rdata) (repr_of repr app) of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
518 |
({atoms=Cert (Argo_Lit.Pos _, _), ...}: ritem, _) => (SOME (Argo_Lit.Pos t), cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
519 |
| ({atoms=Cert (Argo_Lit.Neg _, _), ...}: ritem, _) => (SOME (Argo_Lit.Neg t), cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
520 |
| (ri as {atoms=Preds ts, ...}: ritem, r) => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
521 |
let val rdata = put_ritem r (put_atoms (Preds (t :: ts)) ri) rdata |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
522 |
in (NONE, mk_context repr rdata apps trace prf back) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
523 |
| ({atoms=Eqs _, ...}: ritem, _) => raise Fail "bad predicate")) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
524 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
525 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
526 |
For each term t that is an application "t1 t2", the reflexive equality t = t1 t2 is added |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
527 |
to the context. This is required for propagations of congruences. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
528 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
529 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
530 |
fun flatten (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
531 |
flatten t1 (flatten t2 (app_merge t (t1, t2) cx)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
532 |
| flatten _ cx = cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
533 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
534 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
535 |
Atoms to be added to the context must either be an equality "t1 = t2" or |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
536 |
an application "t1 t2" (a predicate). Besides adding the equality or the application, |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
537 |
reflexive equalities for for all applications in the terms t1 and t2 are added. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
538 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
539 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
540 |
fun add_atom (t as Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
541 |
add_eq_term t t1 t2 (apply2 (repr_of' cx) (t1, t2)) (flatten t1 (flatten t2 cx)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
542 |
| add_atom (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
543 |
let val cx = flatten t1 (flatten t2 (app_merge t (t1, t2) cx)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
544 |
in add_pred_term t (apply2 (repr_of' cx) (t1, t2)) cx end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
545 |
| add_atom _ cx = (NONE, cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
546 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
547 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
548 |
(* assuming external knowledge *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
549 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
550 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
551 |
Assuming a predicate r replaces all predicate atoms of r's ritem with the assumed certificate. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
552 |
The predicate atoms are implied, either with positive or with negative polarity based on |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
553 |
the assumption. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
554 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
555 |
There must not be a certificate for r since otherwise r would have been assumed before already. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
556 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
557 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
558 |
fun assume_pred lit mk_lit cert r ({repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
559 |
(case ritem_of_pred rdata r of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
560 |
{size, class, occs, neqs, atoms=Preds ts}: ritem => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
561 |
let val rdata = put_ritem r (mk_ritem size class occs neqs cert) rdata |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
562 |
in without lit (map mk_lit ts, mk_context repr rdata apps trace prf back) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
563 |
| _ => raise Fail "bad predicate assumption") |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
564 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
565 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
566 |
Assumed equalities "t1 = t2" are treated as flat equalities between terms t1 and t2. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
567 |
If t1 and t2 are applications, congruences are propagated as part of the merge between t1 and t2. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
568 |
Negated equalities are handled likewise. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
569 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
570 |
Assumed predicates do not trigger congruences. Only predicates of the same class are implied. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
571 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
572 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
573 |
fun assume (lp as (Argo_Lit.Pos (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])), _)) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
574 |
flat_merge lp (t1, t2) cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
575 |
| assume (lp as (Argo_Lit.Neg (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])), _)) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
576 |
flat_neq lp (t1, t2) cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
577 |
| assume (lp as (lit as Argo_Lit.Pos (t as Argo_Term.T (_, Argo_Expr.App, [_, _])), _)) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
578 |
assume_pred lit Argo_Lit.Pos (Cert lp) (repr_of' cx t) cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
579 |
| assume (lp as (lit as Argo_Lit.Neg (t as Argo_Term.T (_, Argo_Expr.App, [_, _])), _)) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
580 |
assume_pred lit Argo_Lit.Neg (Cert lp) (repr_of' cx t) cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
581 |
| assume _ cx = (Argo_Common.Implied [], cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
582 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
583 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
584 |
(* checking for consistency and pending implications *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
585 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
586 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
587 |
The internal model is always kept consistent. All implications are propagated as soon as |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
588 |
new information is assumed. Hence, there is nothing to be done here. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
589 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
590 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
591 |
fun check cx = (Argo_Common.Implied [], cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
592 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
593 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
594 |
(* explanations *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
595 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
596 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
597 |
The explanation for the predicate t, which is an application of t1 and t2, is constructed |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
598 |
from the explanation of the predicate application "u1 u2" as well as the equalities "u1 = t1" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
599 |
and "u2 = t2" which both are constructed from the proof forest. The substitution rule is |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
600 |
the proof step that concludes "t1 t2" from "u1 u2" and the two equalities "u1 = t1" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
601 |
and "u2 = t2". |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
602 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
603 |
The atoms part of the ritem of t's representative must be a certificate of an already |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
604 |
assumed predicate for otherwise there would be no explanation for t. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
605 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
606 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
607 |
fun explain_pred lit t t1 t2 ({repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
608 |
(case ritem_of_pred rdata (repr_of repr t) of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
609 |
{atoms=Cert (cert as (lit', _)), ...}: ritem => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
610 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
611 |
val (u1, u2) = dest_app (Argo_Lit.term_of lit') |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
612 |
val (lits, (p, prf)) = proof_of cert [] prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
613 |
val (lits, (p1, prf)) = mk_eq_proof trace u1 t1 lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
614 |
val (lits, (p2, prf)) = mk_eq_proof trace u2 t2 lits prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
615 |
val (lits, (p, prf)) = Argo_Proof.mk_subst p p1 p2 prf |> close_proof lit lits |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
616 |
in ((lits, p), mk_context repr rdata apps trace prf back) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
617 |
| _ => raise Fail "no explanation for bad predicate") |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
618 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
619 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
620 |
Explanations are produced based on the proof forest that is constructed while assuming new |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
621 |
information and propagating this among the internal data structures. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
622 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
623 |
For predicates, no distinction between both polarities needs to be done here. The atoms |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
624 |
part of the relevant ritem knows the assumed polarity. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
625 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
626 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
627 |
fun explain (lit as Argo_Lit.Pos (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2]))) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
628 |
SOME (explain_eq lit t1 t2 cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
629 |
| explain (lit as Argo_Lit.Neg (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2]))) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
630 |
let val (_, eq) = the (find_neq cx (ritem_of' cx (repr_of' cx t1)) (repr_of' cx t2)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
631 |
in SOME (explain_neq (Flat ((lit, NONE), (t1, t2))) eq cx) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
632 |
| explain (lit as (Argo_Lit.Pos (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])))) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
633 |
SOME (explain_pred lit t t1 t2 cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
634 |
| explain (lit as (Argo_Lit.Neg (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])))) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
635 |
SOME (explain_pred lit t t1 t2 cx) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
636 |
| explain _ _ = NONE |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
637 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
638 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
639 |
(* backtracking *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
640 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
641 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
642 |
All information that needs to be reconstructed on backtracking is stored on the backtracking |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
643 |
stack. On backtracking any current information is replaced by what was stored before. No copying |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
644 |
nor subtle updates are required thanks to immutable data structures. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
645 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
646 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
647 |
fun add_level ({repr, rdata, apps, trace, prf, back}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
648 |
mk_context repr rdata apps trace prf ((repr, rdata, apps, trace) :: back) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
649 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
650 |
fun backtrack ({back=[], ...}: context) = raise Empty |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
651 |
| backtrack ({prf, back=(repr, rdata, apps, trace) :: back, ...}: context) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
652 |
mk_context repr rdata apps trace prf back |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
653 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
654 |
end |