xmt-lib 0.1.2

A grounder for SMT solvers
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72

(set-option :backend none)
(declare-datatype Color ( ( red ) ( green ) ))
(declare-datatype Pair (par (X) ((pair (first X) (second X)))))
(define-sort PairColor () (Pair Color))
(declare-fun bright (Color) Bool)
(declare-fun invert (Color) Color)
(declare-fun brightest ( (Pair Color) ) Color)
(declare-fun colorOf ( PairColor ) PairColor)
(x-debug solver sorts)
(x-debug solver functions)
(x-debug db tables)
------- RESULTS ------------------
(declare-datatype Color ((red) (green)))
(declare-datatype Pair (par (X) ((pair (first X) (second X)))))
(define-sort PairColor () (Pair Color))
(declare-fun bright (Color) Bool)
(declare-fun invert (Color) Color)
(declare-fun brightest ((Pair Color)) Color)
(declare-fun colorOf (PairColor) PairColor)
Sorts:
 - (Bool: 2) Bool: ((true) (false))
 - (infinite) Int
 - (infinite) Real
 - (infinite) RoundingMode
 - (infinite) String
 - (infinite) RegLan
 - (_xmt_sort_color: 2) Color: ((red) (green))
 - (Sort_7: 4) (Pair Color): ((pair (first Color) (second Color)))
 - (Sort_7: 4) PairColor (= (Pair Color)): ((pair (first Color) (second Color)))
Functions2:
 - true ()->Bool : Constructor
 - false ()->Bool : Constructor
 - not ()->Bool : Predefined (true)
 - => ()->Bool : Predefined (true)
 - and ()->Bool : Predefined (true)
 - or ()->Bool : Predefined (true)
 - xor ()->Bool : Predefined (true)
 - = ()->Bool : Predefined (true)
 - distinct ()->Bool : Predefined (true)
 - <= ()->Bool : Predefined (true)
 - < ()->Bool : Predefined (true)
 - >= ()->Bool : Predefined (true)
 - > ()->Bool : Predefined (true)
 - ite ()->Bool : Predefined (?)
 - let ()->Bool : Predefined (?)
 - + ()->Real : Predefined (false)
 - - ()->Real : Predefined (false)
 - * ()->Real : Predefined (false)
 - div ()->Real : Predefined (false)
 - mod ()->Real : Predefined (false)
 - abs ()->Real : Predefined (false)
 - red ()->Color : Constructor
 - green ()->Color : Constructor
 - (_ is red) (Color)->Bool : Predefined (true)
 - (_ is green) (Color)->Bool : Predefined (true)
 - pair (Color, Color)->(Pair Color) : Constructor
 - (_ is pair) ((Pair Color))->Bool : Boolean (_xmt_tester_sort_7_pair_t Complete, _xmt_tester_sort_7_pair_f Complete, _xmt_tester_sort_7_pair_g Complete)
 - first ((Pair Color))->Color : Non Boolean (_xmt_selector_sort_7_first_g Complete)
 - second ((Pair Color))->Color : Non Boolean (_xmt_selector_sort_7_second_g Complete)
 - bright (Color)->Bool : Not interpreted
 - invert (Color)->Color : Not interpreted
 - brightest ((Pair Color))->Color : Not interpreted
 - colorOf ((Pair Color))->(Pair Color) : Not interpreted
Tables and Views:
 - Bool (table)
 - _xmt_sort_color (table)
 - Sort_7 (table)
 - _xmt_tester_sort_7_pair_g (view)
 - _xmt_tester_sort_7_pair_t (view)
 - _xmt_tester_sort_7_pair_f (view)
 - _xmt_selector_sort_7_first_g (view)
 - _xmt_selector_sort_7_second_g (view)