author | boehmes |
Fri, 20 Jan 2017 21:05:11 +0100 | |
changeset 64927 | a5a09855e424 |
parent 63960 | 3daf02070be5 |
child 67560 | 0fa87bd86566 |
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_simplex.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 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
4 |
Linear arithmetic reasoning based on the simplex algorithm. 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
|
5 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
6 |
* simplification and normalization of arithmetic expressions |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
7 |
* decision procedure for reals |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
8 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
9 |
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
|
10 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
11 |
* propagating implied inequality literals while 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
|
12 |
* propagating equalities for fixed variables 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
|
13 |
* pruning the tableau after new atoms have been added: eliminate unnecessary |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
14 |
variables |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
15 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
16 |
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
|
17 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
18 |
Bruno Dutertre and Leonardo de Moura. A fast linear-arithmetic solver |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
19 |
for DPLL(T). In Computer Aided Verification, pages 81-94. Springer, 2006. |
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 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
22 |
signature ARGO_SIMPLEX = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
23 |
sig |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
24 |
(* context *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
25 |
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
|
26 |
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
|
27 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
28 |
(* 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
|
29 |
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
|
30 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
31 |
(* 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
|
32 |
val prepare: 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
|
33 |
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
|
34 |
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
|
35 |
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
|
36 |
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
|
37 |
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
|
38 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
39 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
40 |
structure Argo_Simplex: ARGO_SIMPLEX = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
41 |
struct |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
42 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
43 |
(* extended rationals *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
44 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
45 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
46 |
Extended rationals (c, k) are reals (c + k * e) where e is some small positive real number. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
47 |
Extended rationals are used to represent a strict inequality by a non-strict inequality: |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
48 |
c < x ~~ c + k * e <= e |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
49 |
x < c ~~ x <= c - k * e |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
50 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
51 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
52 |
type erat = Rat.rat * Rat.rat |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
53 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
54 |
val erat_zero = (@0, @0) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
55 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
56 |
fun add (c1, k1) (c2, k2) = (c1 + c2, k1 + k2) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
57 |
fun sub (c1, k1) (c2, k2) = (c1 - c2, k1 - k2) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
58 |
fun mul n (c, k) = (n * c, n * k) |
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 |
val erat_ord = prod_ord Rat.ord Rat.ord |
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 |
fun less_eq n1 n2 = (erat_ord (n1, n2) <> GREATER) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
63 |
fun less n1 n2 = (erat_ord (n1, n2) = LESS) |
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 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
66 |
(* term functions *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
67 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
68 |
fun dest_monom (Argo_Term.T (_, Argo_Expr.Mul, [Argo_Term.T (_, Argo_Expr.Num n, _), t])) = (t, n) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
69 |
| dest_monom t = (t, @1) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
70 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
71 |
datatype node = Var of Argo_Term.term | Num of Rat.rat |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
72 |
datatype ineq = Lower of Argo_Term.term * erat | Upper of Argo_Term.term * erat |
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 |
fun dest_node (Argo_Term.T (_, Argo_Expr.Num n, _)) = Num n |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
75 |
| dest_node t = Var t |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
76 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
77 |
fun dest_atom true (k as Argo_Expr.Le) t1 t2 = SOME (k, dest_node t1, dest_node t2) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
78 |
| dest_atom true (k as Argo_Expr.Lt) t1 t2 = SOME (k, dest_node t1, dest_node t2) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
79 |
| dest_atom false Argo_Expr.Le t1 t2 = SOME (Argo_Expr.Lt, dest_node t2, dest_node t1) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
80 |
| dest_atom false Argo_Expr.Lt t1 t2 = SOME (Argo_Expr.Le, dest_node t2, dest_node t1) |
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_atom _ _ _ _ = NONE |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
82 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
83 |
fun ineq_of pol (Argo_Term.T (_, k, [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
|
84 |
(case dest_atom pol k t1 t2 of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
85 |
SOME (Argo_Expr.Le, Var x, Num n) => SOME (Upper (x, (n, @0))) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
86 |
| SOME (Argo_Expr.Le, Num n, Var x) => SOME (Lower (x, (n, @0))) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
87 |
| SOME (Argo_Expr.Lt, Var x, Num n) => SOME (Upper (x, (n, @~1))) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
88 |
| SOME (Argo_Expr.Lt, Num n, Var x) => SOME (Lower (x, (n, @1))) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
89 |
| _ => NONE) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
90 |
| ineq_of _ _ = NONE |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
91 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
92 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
93 |
(* proofs *) |
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 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
96 |
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
|
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 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
99 |
fun mk_ineq is_lt = if is_lt then Argo_Expr.mk_lt else Argo_Expr.mk_le |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
100 |
fun ineq_rule_of is_lt = if is_lt then Argo_Proof.Lt else Argo_Proof.Le |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
101 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
102 |
fun rewrite_top f = Argo_Rewr.rewrite_top (f 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
|
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 |
fun unnegate_conv (e as Argo_Expr.E (Argo_Expr.Not, [Argo_Expr.E (Argo_Expr.Le, [e1, e2])])) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
105 |
Argo_Rewr.rewr (Argo_Proof.Rewr_Not_Ineq Argo_Proof.Le) (Argo_Expr.mk_lt e2 e1) e |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
106 |
| unnegate_conv (e as Argo_Expr.E (Argo_Expr.Not, [Argo_Expr.E (Argo_Expr.Lt, [e1, e2])])) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
107 |
Argo_Rewr.rewr (Argo_Proof.Rewr_Not_Ineq Argo_Proof.Lt) (Argo_Expr.mk_le e2 e1) e |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
108 |
| unnegate_conv e = Argo_Rewr.keep e |
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 |
fun scale_conv r mk n e1 e2 = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
111 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
112 |
fun scale e = Argo_Expr.mk_mul (Argo_Expr.mk_num n) e |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
113 |
val (e1, e2) = if n > @0 then (scale e1, scale e2) else (scale e2, scale e1) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
114 |
val conv = Argo_Rewr.rewr (Argo_Proof.Rewr_Ineq_Mul (r, n)) (mk e1 e2) |
64927
a5a09855e424
less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
boehmes
parents:
63960
diff
changeset
|
115 |
in Argo_Rewr.seq [conv, Argo_Rewr.args (rewrite_top Argo_Rewr.norm_mul)] end |
a5a09855e424
less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
boehmes
parents:
63960
diff
changeset
|
116 |
|
a5a09855e424
less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
boehmes
parents:
63960
diff
changeset
|
117 |
fun dest_ineq (Argo_Expr.E (Argo_Expr.Le, [e1, e2])) = SOME (false, e1, e2) |
a5a09855e424
less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
boehmes
parents:
63960
diff
changeset
|
118 |
| dest_ineq (Argo_Expr.E (Argo_Expr.Lt, [e1, e2])) = SOME (true, e1, e2) |
a5a09855e424
less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
boehmes
parents:
63960
diff
changeset
|
119 |
| dest_ineq _ = NONE |
63960
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
120 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
121 |
fun scale_ineq_conv n e = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
122 |
if n = @1 then Argo_Rewr.keep e |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
123 |
else |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
124 |
(case dest_ineq e of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
125 |
NONE => raise Fail "bad inequality" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
126 |
| SOME (is_lt, e1, e2) => scale_conv (ineq_rule_of is_lt) (mk_ineq is_lt) n e1 e2 e) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
127 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
128 |
fun simp_lit (n, (lit, p)) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
129 |
let val conv = Argo_Rewr.seq [unnegate_conv, scale_ineq_conv n] |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
130 |
in Argo_Rewr.with_proof conv (Argo_Lit.signed_expr_of lit, p) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
131 |
|
64927
a5a09855e424
less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
boehmes
parents:
63960
diff
changeset
|
132 |
val combine_conv = rewrite_top Argo_Rewr.norm_add |
63960
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
133 |
fun reduce_conv r = Argo_Rewr.rewr (Argo_Proof.Rewr_Ineq_Nums (r, false)) Argo_Expr.false_expr |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
134 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
135 |
fun simp_combine es 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
|
136 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
137 |
fun dest e (is_lt, (es1, es2)) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
138 |
let val (is_lt', e1, e2) = the (dest_ineq e) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
139 |
in (is_lt orelse is_lt', (e1 :: es1, e2 :: es2)) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
140 |
val (is_lt, (es1, es2)) = fold_rev dest es (false, ([], [])) |
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 e = uncurry (mk_ineq is_lt) (apply2 Argo_Expr.mk_add (es1, es2)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
142 |
val conv = Argo_Rewr.seq [Argo_Rewr.args combine_conv, reduce_conv (ineq_rule_of is_lt)] |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
143 |
in prf |> Argo_Rewr.with_proof conv (e, p) |>> snd end |
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 linear_combination nlps prf = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
146 |
let val ((es, ps), prf) = fold_map simp_lit nlps prf |>> split_list |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
147 |
in prf |> Argo_Proof.mk_linear_comb ps |-> simp_combine es |-> Argo_Proof.mk_lemma [] end |
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 proof_of (lit, SOME p) (ls, prf) = ((lit, p), (ls, prf)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
150 |
| proof_of (lit, NONE) (ls, prf) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
151 |
let val (p, prf) = 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
|
152 |
in ((lit, p), (Argo_Lit.negate lit :: ls, 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
|
153 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
154 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
155 |
(* tableau *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
156 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
157 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
158 |
The tableau consists of equations x_i = a_i1 * x_1 + ... a_ik * x_k where |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
159 |
the variable on the left-hand side is called a basic variable and |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
160 |
the variables on the right-hand side are called non-basic variables. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
161 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
162 |
For each basic variable, the polynom on the right-hand side is stored as a map |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
163 |
from variables to coefficients. Only variables with non-zero coefficients are stored. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
164 |
The map is sorted by the term order of the variables for a deterministic order when |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
165 |
analyzing a polynom. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
166 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
167 |
Additionally, for each basic variable a boolean flag is kept that, when false, |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
168 |
indicates that the current value of the basic variable might be outside its bounds. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
169 |
The value of a non-basic variable is always within its bounds. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
170 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
171 |
The tableau is stored as a table indexed by variables. For each variable, |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
172 |
both basic and non-basic, its current value is stored as extended rational |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
173 |
along with either the equations or the occurrences. |
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 |
type basic = bool * (Argo_Term.term * Rat.rat) Ord_List.T |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
177 |
type entry = erat * basic option |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
178 |
type tableau = entry 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
|
179 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
180 |
fun dirty ms = SOME (false, ms) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
181 |
fun checked ms = SOME (true, ms) |
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 |
fun basic_entry ms = (erat_zero, dirty ms) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
184 |
val non_basic_entry: entry = (erat_zero, NONE) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
185 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
186 |
fun value_of tableau x = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
187 |
(case Argo_Termtab.lookup tableau x of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
188 |
NONE => erat_zero |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
189 |
| SOME (v, _) => v) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
190 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
191 |
fun first_unchecked_basic tableau = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
192 |
Argo_Termtab.get_first (fn (y, (v, SOME (false, ms))) => SOME (y, v, ms) | _ => NONE) tableau |
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 |
local |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
195 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
196 |
fun coeff_of ms x = the (AList.lookup Argo_Term.eq_term ms x) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
197 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
198 |
val eq_var = Argo_Term.eq_term |
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 monom_ord sp = prod_ord Argo_Term.term_ord (K EQUAL) sp |
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 add_monom m ms = Ord_List.insert monom_ord m ms |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
202 |
fun update_monom (m as (x, a)) = if a = @0 then AList.delete eq_var x else AList.update eq_var m |
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_scaled_monom n (x, a) ms = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
205 |
(case AList.lookup eq_var ms x of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
206 |
NONE => add_monom (x, n * a) ms |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
207 |
| SOME b => update_monom (x, n * a + b) ms) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
208 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
209 |
fun replace_polynom x n ms' ms = fold (add_scaled_monom n) ms' (AList.delete eq_var x ms) |
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 map_basic f (v, SOME (_, ms)) = f v ms |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
212 |
| map_basic _ e = e |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
213 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
214 |
fun map_basic_entries x f = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
215 |
let |
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 apply (e as (v, SOME (_, ms))) = if AList.defined eq_var ms x then f v ms else e |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
217 |
| apply ve = ve |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
218 |
in Argo_Termtab.map (K apply) end |
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 put_entry x e = Argo_Termtab.update (x, e) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
221 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
222 |
fun add_new_entry (y as Argo_Term.T (_, Argo_Expr.Add, ts)) tableau = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
223 |
let val ms = Ord_List.make monom_ord (map dest_monom ts) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
224 |
in fold (fn (x, _) => put_entry x non_basic_entry) ms (put_entry y (basic_entry ms) tableau) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
225 |
| add_new_entry x tableau = put_entry x non_basic_entry tableau |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
226 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
227 |
fun with_non_basic update_basic x f tableau = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
228 |
(case Argo_Termtab.lookup tableau x of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
229 |
NONE => tableau |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
230 |
| SOME (v, NONE) => f v tableau |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
231 |
| SOME (v, SOME (_, ms)) => if update_basic then put_entry x (v, dirty ms) tableau else tableau) |
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 |
in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
234 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
235 |
fun add_entry x tableau = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
236 |
if Argo_Termtab.defined tableau x then tableau |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
237 |
else add_new_entry x tableau |
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 |
fun basic_within_bounds y = Argo_Termtab.map_entry y (map_basic (fn v => fn ms => (v, checked ms))) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
240 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
241 |
fun eliminate _ tableau = tableau |
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 |
fun update_non_basic pred x v' = with_non_basic true x (fn v => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
244 |
let fun update_basic n v ms = (add v (mul (coeff_of ms x) n), dirty ms) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
245 |
in pred v ? put_entry x (v', NONE) o map_basic_entries x (update_basic (sub v' v)) end) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
246 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
247 |
fun update_pivot y vy ms x c v = with_non_basic false x (fn vx => |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
248 |
let |
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 a = Rat.inv c |
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 v' = mul a (sub v vy) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
251 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
252 |
fun scale_or_drop (x', b) = if Argo_Term.eq_term (x', x) then NONE else SOME (x', ~ 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
|
253 |
val ms = add_monom (y, a) (map_filter scale_or_drop ms) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
254 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
255 |
fun update_basic v ms' = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
256 |
let val n = coeff_of ms' x |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
257 |
in (add v (mul n v'), dirty (replace_polynom x n ms ms')) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
258 |
in |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
259 |
put_entry x (add vx v', dirty ms) #> |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
260 |
put_entry y (v, NONE) #> |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
261 |
map_basic_entries x update_basic |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
262 |
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 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
265 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
266 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
267 |
(* bounds *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
268 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
269 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
270 |
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
|
271 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
272 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
273 |
type bound = (erat * Argo_Common.literal) option |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
274 |
type atoms = (erat * 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
|
275 |
type bounds_atoms = ((bound * bound) * (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
|
276 |
type bounds = bounds_atoms 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
|
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 |
val empty_bounds_atoms: bounds_atoms = ((NONE, NONE), ([], [])) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
279 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
280 |
fun on_some pred (SOME (n, _)) = pred n |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
281 |
| on_some _ NONE = false |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
282 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
283 |
fun none_or_some pred (SOME (n, _)) = pred n |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
284 |
| none_or_some _ NONE = true |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
285 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
286 |
fun bound_of (SOME (n, _)) = n |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
287 |
| bound_of NONE = raise Fail "bad bound" |
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 |
fun reason_of (SOME (_, r)) = r |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
290 |
| reason_of NONE = raise Fail "bad reason" |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
291 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
292 |
fun bounds_atoms_of bounds x = the_default empty_bounds_atoms (Argo_Termtab.lookup bounds x) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
293 |
fun bounds_of bounds x = fst (bounds_atoms_of bounds x) |
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 |
fun put_bounds x bs bounds = Argo_Termtab.map_default (x, empty_bounds_atoms) (apfst (K bs)) bounds |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
296 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
297 |
fun has_bound_atoms bounds x = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
298 |
(case Argo_Termtab.lookup bounds x of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
299 |
NONE => false |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
300 |
| SOME (_, ([], [])) => false |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
301 |
| _ => true) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
302 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
303 |
fun add_new_atom f x n t = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
304 |
let val ins = f (insert (eq_snd Argo_Term.eq_term) (n, t)) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
305 |
in Argo_Termtab.map_default (x, empty_bounds_atoms) (apsnd ins) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
306 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
307 |
fun del_atom x t = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
308 |
let fun eq_atom (t1, (_, t2)) = Argo_Term.eq_term (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
|
309 |
in Argo_Termtab.map_entry x (apsnd (apply2 (remove eq_atom t))) end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
310 |
|
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 |
(* context *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
313 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
314 |
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
|
315 |
tableau: tableau, (* values of variables and tableau entries for each variable *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
316 |
bounds: bounds, (* bounds and unassigned atoms for each variable *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
317 |
prf: Argo_Proof.context, (* 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
|
318 |
back: bounds list} (* stack storing previous bounds and unassigned atoms *) |
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 |
fun mk_context tableau bounds 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
|
321 |
{tableau=tableau, bounds=bounds, 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
|
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 |
val context = mk_context Argo_Termtab.empty Argo_Termtab.empty Argo_Proof.simplex_context [] |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
324 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
325 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
326 |
(* 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
|
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_ineq_atom f t x n ({tableau, bounds, 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
|
329 |
(* TODO: check whether the atom is already known to hold *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
330 |
(NONE, mk_context (add_entry x tableau) (add_new_atom f x n t bounds) 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
|
331 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
332 |
fun add_atom 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
|
333 |
(case ineq_of true 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
|
334 |
SOME (Lower (x, n)) => add_ineq_atom apfst t x n cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
335 |
| SOME (Upper (x, n)) => add_ineq_atom apsnd t x n cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
336 |
| NONE => (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
|
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 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
339 |
(* preparing the solver after new atoms have been added *) |
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 |
(* |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
342 |
Variables that do not directly occur in atoms can be eliminated from the tableau |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
343 |
since no bounds will ever limit their value. This can reduce the tableau size |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
344 |
substantially. |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
345 |
*) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
346 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
347 |
fun prepare ({tableau, bounds, 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
|
348 |
let fun drop (xe as (x, _)) = not (has_bound_atoms bounds x) ? eliminate xe |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
349 |
in mk_context (Argo_Termtab.fold drop tableau tableau) bounds 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
|
350 |
|
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 |
(* 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
|
353 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
354 |
fun bounds_conflict r1 r2 ({tableau, bounds, 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
|
355 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
356 |
val ((lp2, lp1), (lits, prf)) = ([], prf) |> proof_of r2 ||>> proof_of r1 |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
357 |
val (p, prf) = linear_combination [(@~1, lp1), (@1, lp2)] prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
358 |
in (Argo_Common.Conflict (lits, p), mk_context tableau bounds 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
|
359 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
360 |
fun assume_bounds order x c bs ({tableau, bounds, 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
|
361 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
362 |
val lits = [] |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
363 |
val bounds = put_bounds x bs bounds |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
364 |
val tableau = update_non_basic (fn v => erat_ord (v, c) = order) x c tableau |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
365 |
in (Argo_Common.Implied lits, mk_context tableau bounds 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
|
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 assume_lower r x c (low, upp) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
368 |
if on_some (fn l => less_eq c l) low then (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
|
369 |
else if on_some (fn u => less u c) upp then bounds_conflict r (reason_of upp) cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
370 |
else assume_bounds LESS x c (SOME (c, r), upp) cx |
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 |
fun assume_upper r x c (low, upp) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
373 |
if on_some (fn u => less_eq u c) upp then (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
|
374 |
else if on_some (fn l => less c l) low then bounds_conflict (reason_of low) r cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
375 |
else assume_bounds GREATER x c (low, SOME (c, r)) cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
376 |
|
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 with_bounds r t f x n ({tableau, bounds, 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
|
378 |
f r x n (bounds_of bounds x) (mk_context tableau (del_atom x t bounds) 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
|
379 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
380 |
fun choose f (SOME (Lower (x, n))) cx = f assume_lower x n cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
381 |
| choose f (SOME (Upper (x, n))) cx = f assume_upper x n cx |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
382 |
| choose _ NONE 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
|
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 |
fun assume (r as (lit, _)) cx = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
385 |
let val (t, pol) = Argo_Lit.dest lit |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
386 |
in choose (with_bounds r t) (ineq_of pol t) 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
|
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 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
389 |
(* 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
|
390 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
391 |
fun basic_bounds_conflict lower y ms ({tableau, bounds, 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
|
392 |
let |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
393 |
val (a, low, upp) = if lower then (@1, fst, snd) else (@~1, snd, fst) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
394 |
fun coeff_proof f a x = apfst (pair a) o proof_of (reason_of (f (bounds_of bounds x))) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
395 |
fun monom_proof (x, a) = coeff_proof (if a < @0 then low else upp) a x |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
396 |
val ((alp, alps), (lits, prf)) = ([], prf) |> coeff_proof low a y ||>> fold_map monom_proof ms |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
397 |
val (p, prf) = linear_combination (alp :: alps) prf |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
398 |
in (Argo_Common.Conflict (lits, p), mk_context tableau bounds 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
|
399 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
400 |
fun can_compensate ord tableau bounds (x, a) = |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
401 |
let val (low, upp) = bounds_of bounds x |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
402 |
in |
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 Rat.ord (a, @0) = ord then none_or_some (fn u => less (value_of tableau x) u) upp |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
404 |
else none_or_some (fn l => less l (value_of tableau x)) low |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
405 |
end |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
406 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
407 |
fun check (cx as {tableau, bounds, 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
|
408 |
(case first_unchecked_basic tableau of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
409 |
NONE => (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
|
410 |
| SOME (y, v, ms) => |
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 (low, upp) = bounds_of bounds y |
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 on_some (fn l => less v l) low then adjust GREATER true y v ms (bound_of low) 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 if on_some (fn u => less u v) upp then adjust LESS false y v ms (bound_of upp) 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 |
else check (mk_context (basic_within_bounds y tableau) bounds 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
|
416 |
end) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
417 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
418 |
and adjust ord lower y vy ms v (cx as {tableau, bounds, 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
|
419 |
(case find_first (can_compensate ord tableau bounds) ms of |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
420 |
NONE => basic_bounds_conflict lower y ms 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 |
| SOME (x, a) => check (mk_context (update_pivot y vy ms x a v tableau) bounds 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
|
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 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
424 |
(* explanations *) |
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 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
|
427 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
428 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
429 |
(* backtracking *) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
430 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
431 |
fun add_level ({tableau, bounds, 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
|
432 |
mk_context tableau bounds prf (bounds :: back) |
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
433 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
434 |
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
|
435 |
| backtrack ({tableau, prf, back=bounds :: 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
|
436 |
mk_context tableau bounds 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
|
437 |
|
3daf02070be5
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
boehmes
parents:
diff
changeset
|
438 |
end |