| 1 | % evaluate ProB AST predicates | |
| 2 | ||
| 3 | :- use_module(library(lists),[is_list/1]). | |
| 4 | :- use_module(library(sets)). | |
| 5 | ||
| 6 | pint(b(truth,pred,_),true). | |
| 7 | pint(b(falsity,pred,_),false). | |
| 8 | ||
| 9 | % conjunct, disjunct, implication, equivalence | |
| 10 | pint(b(conjunct(Pred1,Pred2),pred,_),Value) :- | |
| 11 | pint(Pred1,Value1) , | |
| 12 | pint(Pred2,Value2) , | |
| 13 | (Value1 , Value2 | |
| 14 | -> Value = true | |
| 15 | ; Value = false). | |
| 16 | pint(b(disjunct(Pred1,Pred2),pred,_),Value) :- | |
| 17 | pint(Pred1,Value1) , | |
| 18 | pint(Pred2,Value2) , | |
| 19 | ((Value1 ; Value2) | |
| 20 | -> Value = true | |
| 21 | ; Value = false). | |
| 22 | pint(b(implication(Pred1,Pred2),pred,_),Value) :- | |
| 23 | pint(Pred1,Res1) , | |
| 24 | pint(Pred2,Res2) , | |
| 25 | ((\+Res1 ; Res2) | |
| 26 | -> Value = true | |
| 27 | ; Value = false). | |
| 28 | pint(b(equivalence(Pred1,Pred2),pred,_),Value) :- | |
| 29 | pint(Pred1,Res1) , | |
| 30 | pint(Pred2,Res2) , | |
| 31 | (Res1 = Res2 | |
| 32 | -> Value = true | |
| 33 | ; Value = false). | |
| 34 | pint(b(negation(Pred),pred,_),Value) :- | |
| 35 | pint(Pred,Temp) , | |
| 36 | (Temp | |
| 37 | -> Value = false | |
| 38 | ; Value = true). | |
| 39 | ||
| 40 | %%%%%%%%%%%% | |
| 41 | pint(b(finite(_),pred,_),true). | |
| 42 | %%%%%%%%%%%% | |
| 43 | ||
| 44 | % equal, not_equal | |
| 45 | pint(b(equal(b(value(Set1),_,_),b(value(Set2),_,_)),pred,_),true) :- | |
| 46 | Set1 == Set2. | |
| 47 | pint(b(equal(b(value(Set1),_,_),b(value(Set2),_,_)),pred,_),false) :- | |
| 48 | Set1 \== Set2. | |
| 49 | pint(b(equal(b(set_extension(Set1),_,_),b(set_extension(Set2),_,_)),pred,_),true) :- | |
| 50 | Set1 == Set2. | |
| 51 | pint(b(equal(b(set_extension(Set1),_,_),b(set_extension(Set2),_,_)),pred,_),false) :- | |
| 52 | Set1 \== Set2. | |
| 53 | ||
| 54 | pint(b(equal(b(Expr1,integer,_),b(Expr2,integer,_)),pred,_),true) :- | |
| 55 | int(Expr1,Value1) , | |
| 56 | int(Expr2,Value2) , | |
| 57 | Value1 == Value2. | |
| 58 | pint(b(equal(b(Expr1,integer,_),b(Expr2,integer,_)),pred,_),false) :- | |
| 59 | int(Expr1,Value1) , | |
| 60 | int(Expr2,Value2) , | |
| 61 | Value1 \== Value2. | |
| 62 | ||
| 63 | pint(b(equal(Set1,Set2),pred,_),true) :- | |
| 64 | Set1 == Set2. | |
| 65 | pint(b(equal(Set1,Set2),pred,_),false) :- | |
| 66 | Set1 \== Set2. | |
| 67 | ||
| 68 | pint(b(not_equal(Pred1,Pred2),pred,_),true) :- | |
| 69 | pint(b(equal(Pred1,Pred2),pred,_),false). | |
| 70 | pint(b(not_equal(Pred1,Pred2),pred,_),false) :- | |
| 71 | pint(b(equal(Pred1,Pred2),pred,_),true). | |
| 72 | ||
| 73 | % less, less_equal, greater, greater_equal | |
| 74 | pint(b(less_equal(Expr1,Expr2),pred,_),Value) :- | |
| 75 | int(Expr1,Value1) , | |
| 76 | int(Expr2,Value2) , | |
| 77 | (Value1 =< Value2 | |
| 78 | -> Value = true | |
| 79 | ; Value = false). | |
| 80 | pint(b(less(Expr1,Expr2),pred,_),Value) :- | |
| 81 | int(Expr1,Value1) , | |
| 82 | int(Expr2,Value2) , | |
| 83 | (Value1 < Value2 | |
| 84 | -> Value = true | |
| 85 | ; Value = false). | |
| 86 | pint(b(greater_equal(Expr1,Expr2),pred,_),Value) :- | |
| 87 | int(Expr1,Value1) , | |
| 88 | int(Expr2,Value2) , | |
| 89 | (Value1 >= Value2 | |
| 90 | -> Value = true | |
| 91 | ; Value = false). | |
| 92 | pint(b(greater(Expr1,Expr2),pred,_),Value) :- | |
| 93 | int(Expr1,Value1) , | |
| 94 | int(Expr2,Value2) , | |
| 95 | (Value1 > Value2 | |
| 96 | -> Value = true | |
| 97 | ; Value = false). | |
| 98 | ||
| 99 | % member, not_member | |
| 100 | pint(b(member(Set,SetOfSet),pred,_),Value) :- | |
| 101 | Set = b(_,set(_),_) , | |
| 102 | SetOfSet = b(_,set(set(_)),_) , | |
| 103 | sint(Set,ValueList) , | |
| 104 | sint(SetOfSet,SetValue) , | |
| 105 | (member(ValueList,SetValue) | |
| 106 | -> Value = true | |
| 107 | ; Value = false). | |
| 108 | pint(b(member(b(Elm,integer,_),b(set_extension(Set),_,_)),pred,_),Value) :- | |
| 109 | maplist(ast_to_value,Set,List) , | |
| 110 | int(b(Elm,_,_),ElmValue) , | |
| 111 | (member(ElmValue,List) | |
| 112 | -> Value = true | |
| 113 | ; Value = false). | |
| 114 | pint(b(member(b(Elm,integer,_),b(set_extension(Set),_,_)),pred,_),Value) :- | |
| 115 | int(b(Elm,_,_),ElmValue) , | |
| 116 | (member(ElmValue,Set) | |
| 117 | -> Value = true | |
| 118 | ; Value = false). | |
| 119 | % value list set | |
| 120 | pint(b(member(b(Elm,integer,_),b(value(Set),_,_)),pred,_),Value) :- | |
| 121 | is_list(Set) , | |
| 122 | int(b(Elm,_,_),ElmValue) , | |
| 123 | (member(ElmValue,Set) | |
| 124 | -> Value = true | |
| 125 | ; Value = false). | |
| 126 | % value avl set | |
| 127 | pint(b(member(b(Elm,integer,_),b(value(avl_set(Set)),_,_)),pred,_),Value) :- | |
| 128 | int(b(Elm,_,_),ElmValue) , | |
| 129 | avl_to_list(Set,TempList) , | |
| 130 | findall(Key,member(Key-_,TempList),List) , | |
| 131 | (member(ElmValue,List) | |
| 132 | -> Value = true | |
| 133 | ; Value = false). | |
| 134 | pint(b(member(b(Elm,_,_),b(set_extension(Set),_,_)),pred,_),Value) :- | |
| 135 | maplist(ast_to_value,Set,List) , | |
| 136 | sint(b(Elm,_,_),ElmValue) , | |
| 137 | (member(ElmValue,List) | |
| 138 | -> Value = true | |
| 139 | ; Value = false). | |
| 140 | pint(b(member(b(Elm,_,_),b(set_extension(Set),_,_)),pred,_),Value) :- | |
| 141 | sint(b(Elm,_,_),ElmValue) , | |
| 142 | (member(ElmValue,Set) | |
| 143 | -> Value = true | |
| 144 | ; Value = false). | |
| 145 | % value list set | |
| 146 | pint(b(member(b(Elm,_,_),b(value(Set),_,_)),pred,_),Value) :- | |
| 147 | is_list(Set) , | |
| 148 | sint(b(Elm,_,_),ElmValue) , | |
| 149 | (member(ElmValue,Set) | |
| 150 | -> Value = true | |
| 151 | ; Value = false). | |
| 152 | % value avl set | |
| 153 | pint(b(member(b(Elm,_,_),b(value(avl_set(Set)),_,_)),pred,_),Value) :- | |
| 154 | sint(b(Elm,_,_),ElmValue) , | |
| 155 | avl_to_list(Set,TempList) , | |
| 156 | findall(Key,member(Key-_,TempList),List) , | |
| 157 | (member(ElmValue,List) | |
| 158 | -> Value = true | |
| 159 | ; Value = false). | |
| 160 | ||
| 161 | pint(b(not_member(Elm,Set),pred,_),Value) :- | |
| 162 | pint(b(member(Elm,Set),pred,_),R) , | |
| 163 | (R = true | |
| 164 | -> Value = false | |
| 165 | ; Value = true). | |
| 166 | ||
| 167 | % subset, not_subset, | |
| 168 | pint(b(subset(Set1,Set2),pred,_),Value) :- | |
| 169 | sint(Set1,ValueSet1) , | |
| 170 | sint(Set2,ValueSet2) , | |
| 171 | (subset(ValueSet1,ValueSet2) | |
| 172 | -> Value = true | |
| 173 | ; Value = false). | |
| 174 | pint(b(not_subset(Set1,Set2),pred,_),Value) :- | |
| 175 | sint(Set1,ValueSet1) , | |
| 176 | sint(Set2,ValueSet2) , | |
| 177 | (\+subset(ValueSet1,ValueSet2) | |
| 178 | -> Value = true | |
| 179 | ; Value = false). | |
| 180 | ||
| 181 | % subset_strict, not_subset_strict | |
| 182 | pint(b(subset_strict(Set1,Set2),pred,_),Value) :- | |
| 183 | sint(Set1,ValueSet1) , | |
| 184 | sint(Set2,ValueSet2) , | |
| 185 | (subset_strict(ValueSet1,ValueSet2) | |
| 186 | -> Value = true | |
| 187 | ; Value = false). | |
| 188 | pint(b(not_subset_strict(Set1,Set2),pred,_),Value) :- | |
| 189 | sint(Set1,ValueSet1) , | |
| 190 | sint(Set2,ValueSet2) , | |
| 191 | (subset(ValueSet1,ValueSet2) | |
| 192 | -> Value = false | |
| 193 | ; Value = true). | |
| 194 | ||
| 195 | %%% placeholder, needs some improvement | |
| 196 | pint(b(exists(_,_),_,_),true). | |
| 197 | pint(b(forall(_,_,_),_,_),true). | |
| 198 | ||
| 199 | % check if set is strict subset | |
| 200 | subset_strict([],[]). | |
| 201 | subset_strict(Subset,Set) :- | |
| 202 | append(Subset,_,Set). | |
| 203 | subset_strict(Set,[_|T]) :- | |
| 204 | subset_strict(Set,T). |