blob: 25a7ac1fd445f0c79bf4c66f1d0a8c711a44f207 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
; Depends on th_real.plf, th_int.plf, smt.plf, sat.plf
; Types for arithmetic variables
; Specifically a real
(declare real_var type)
; Specifically an integer
(declare int_var type)
; Functions to map them to terms
(declare term_real_var (! v real_var (term Real)))
(declare term_int_var (! v int_var (term Int)))
; A function to cast an integer term to real.
(declare term_int_to_real (! i (term Int) (term Real)))
; The recursive functions `reify_int_term` and `reify_real_term` work
; together to reify or "make real" an integer term. That is, to convert it to
; a real term. More precisely, they take an integer term and return a real
; term in which any integer variables are immediately converted to real terms,
; and all non-leaves in the term are real-sorted.
;
; They explicitly do not work on integer division, because such a conversion
; would not be correct when integer division is involved.
; This function recursively converts an integer term to a real term.
(program reify_int_term ((t (term Int))) (term Real)
(match t
((term_int_var v) (term_int_to_real (term_int_var v)))
((a_int i) (a_real (mpz_to_mpq i)))
((+_Int x y) (+_Real (reify_int_term x) (reify_int_term y)))
((-_Int x y) (-_Real (reify_int_term x) (reify_int_term y)))
((u-_Int x) (u-_Real (reify_int_term x)))
((*_Int x y) (*_Real (reify_int_term x) (reify_int_term y)))
; Reifying integer division is an error, since it changes the value!
((/_Int x y) (fail (term Real)))
))
; This function recursively converts a real term to a real term.
; It will never change the top-level node in the term (since that node is
; real), but it may change subterms...
(program reify_real_term ((t (term Real))) (term Real)
(match t
((term_real_var v) (term_real_var v))
((a_real v) (a_real v))
; We've found an integer term -- reify it!
((term_int_to_real t') (reify_int_term t'))
((+_Real x y) (+_Real (reify_real_term x) (reify_real_term y)))
((-_Real x y) (-_Real (reify_real_term x) (reify_real_term y)))
((u-_Real x) (u-_Real (reify_real_term x)))
((*_Real x y) (*_Real (reify_real_term x) (reify_real_term y)))
((/_Real x y) (/_Real (reify_real_term x) (reify_real_term y)))
))
; Predicates of the form (term Integer) >= (term Real) or negations thereof
(declare >=_IntReal (! x (term Int) (! y (term Real) formula)))
; From an arith predicate, compute the equivalent real predicate
; All arith predicates are (possibly negated) >='s with a real on the right.
; Technically it's a real literal on the right, but we don't assume that here.
(program reify_arith_pred ((p formula)) formula
(match p
((not p') (not (reify_arith_pred p')))
((>=_Real x y) (>=_Real (reify_real_term x) (reify_real_term y)))
((>=_Int x y) (>=_Real (reify_int_term x) (reify_int_term y)))
((>=_IntReal x y) (>=_Real (reify_int_term x) (reify_real_term y)))
(default (fail formula))
))
|