## cool / HACKING @ master

History | View | Annotate | Download (5.24 KB)

1 | 2bda8737 | Hans-Peter Deifel | // -*- mode: adoc; fill-column: 80; -*- |
---|---|---|---|

2 | 69a71d22 | Thorsten Wißmann | HACKING COOL |

3 | ============ |
||

4 | |||

5 | 7198f96f | Hans-Peter Deifel | == Internal API Documentation |

6 | |||

7 | Run `ocaml setup.ml -doc` after `oasis setup`. It will generate HTML API |
||

8 | documentation for COOL's internal library in `cool_api.docdir/index.html`. |
||

9 | |||

10 | As most of the API currently doesn't have documentation comments, this is mainly |
||

11 | useful for getting hyperlinked `.mli`-files. But please feel free to add more |
||

12 | comments. |
||

13 | |||

14 | c2233aff | Hans-Peter Deifel | == Tests |

15 | |||

16 | There are two sets of tests: Integration tests in `src/testsuite` and unit tests |
||

17 | in `src/unit-tests`. The former can be used to test the whole reasoner on |
||

18 | example formulas with known satisfiability, the latter is for individual |
||

19 | functions. |
||

20 | |||

21 | To run all tests, run `make test`. You will need to install the additional |
||

22 | dependency `ounit`. The individual test suites can be run with |
||

23 | `./cool-testsuite.native` and `./cool_unit_tests.native` respectively. |
||

24 | |||

25 | If unit tests are not being build, use |
||

26 | |||

27 | ocaml setup.ml -configure --enable-tests |
||

28 | |||

29 | 69a71d22 | Thorsten Wißmann | Adding another Functor |

30 | ---------------------- |
||

31 | |||

32 | Extending Formula Syntax |
||

33 | ~~~~~~~~~~~~~~~~~~~~~~~~ |
||

34 | To add another functor, extend the algebraic type formula in CoAlgFormula.mli |
||

35 | *and* CoAlgFormula.ml in src/lib/ by adding another case. Note that normally, |
||

36 | you always need (at least) two constructors -- one for the negative and one for |
||

37 | the positive case. That is because in a later internal representation, the |
||

38 | assumption must hold that negations are only in front of atomic propositions |
||

39 | (i.e. variables). Concretely for implementation, every operator needs to have |
||

40 | its dual, as we convert to NNF later. For example: |
||

41 | |||

42 | | CONST of string (* constant functor with value string *) |
||

43 | c49eea11 | Thorsten Wißmann | | CONSTN of string (* constant functor with value string *) |

44 | 69a71d22 | Thorsten Wißmann | |

45 | bbfe7b6e | Dirk Pattinson | [ This is the data type generated at parse time ] |

46 | |||

47 | 69a71d22 | Thorsten Wißmann | Do the analogous thing for the type hcFormula_node in the same files! |

48 | |||

49 | c49eea11 | Thorsten Wißmann | | HCONST of string (* constant functor w *) |

50 | | HCONSTN of string (* constant functor w *) |
||

51 | 69a71d22 | Thorsten Wißmann | |

52 | bbfe7b6e | Dirk Pattinson | |

53 | 69a71d22 | Thorsten Wißmann | Recall: edit both the ml and the mli-file. Do the analogous thing for |

54 | formulaType in CoAlgMisc.mli and CoAlgMisc.ml: |
||

55 | |||

56 | | ConstF (* constant functor *) |
||

57 | c49eea11 | Thorsten Wißmann | | ConstnF (* constant functor *) |

58 | 69a71d22 | Thorsten Wißmann | |

59 | bbfe7b6e | Dirk Pattinson | [ This is the internal data type used by the reasoner ] |

60 | |||

61 | If you build now, you will see a lot of warnings concerning non-exhaustive |
||

62 | 69a71d22 | Thorsten Wißmann | pattern matchings. We will fix them later. |

63 | |||

64 | Extending Functor Syntax |
||

65 | ~~~~~~~~~~~~~~~~~~~~~~~~ |
||

66 | Before being able to solve them, we have to extend the functor type. |
||

67 | Therefore, extend the type functor in CoAlgMisc.mli *and* CoAlgMisc.ml. |
||

68 | |||

69 | | Constant |
||

70 | |||

71 | bbfe7b6e | Dirk Pattinson | Furthermore, in CoAlgMisc.ml you should extend the unaryfunctor2name array: |

72 | |||

73 | ; (NPa Identity, "Id") |
||

74 | |||

75 | for a functor (like identity) that doesn't take any parameters. For |
||

76 | functors that do take parameters, such as the constant functor, also add |
||

77 | a constructor to parametricFunctorName, such as |
||

78 | |||

79 | | NameConstant |
||

80 | |||

81 | and reflect the fact that the functor takes parameters in the |
||

82 | addition of |
||

83 | |||

84 | ; (Pa NameConstant , "Const") |
||

85 | ; (Pa NameConstant , "Constant") |
||

86 | |||

87 | in unaryfunctor2name. |
||

88 | 69a71d22 | Thorsten Wißmann | |

89 | |||

90 | You are also allowed to give multiple names which can be used for parsing. |
||

91 | |||

92 | bbfe7b6e | Dirk Pattinson | Extending Formula parsing |

93 | 69a71d22 | Thorsten Wißmann | ~~~~~~~~~~~~~~~~~~~~~~~~~~ |

94 | Now, force the rebuild to get all non-exhaustive pattern matchings. You can |
||

95 | force it for example via: |
||

96 | |||

97 | ocaml setup.ml -clean |
||

98 | |||

99 | And then rebuild with: |
||

100 | |||

101 | ocaml setup.ml -build |
||

102 | |||

103 | c49eea11 | Thorsten Wißmann | You have to extend the parsing in the parse_rest function in CoAlgFormula.ml. If |

104 | you introduce another symbol that was not used before, you have to extend the |
||

105 | global variable lexer in CoAlgFormula.ml accordingly. |
||

106 | |||

107 | 69a71d22 | Thorsten Wißmann | These contain: |

108 | |||

109 | bbfe7b6e | Dirk Pattinson | In file CoAlgMisc.ml: |

110 | |||

111 | 69a71d22 | Thorsten Wißmann | - detClosure: Check that a formula has the correct sort and call detClosure if |

112 | needed on subformulae. This is the first time where you should pick a |
||

113 | concrete syntax for the operators of your new functor. (I.e. the syntax |
||

114 | visible to the user may differ from the internal name of the constructor, |
||

115 | and here it is the first time where the user sees it. So take care that the |
||

116 | error message here fits the actual functor syntax) |
||

117 | |||

118 | | C.HCCONST _ -> |
||

119 | if func <> Constant || List.length sortlst <> 1 |
||

120 | then raise (C.CoAlgException "=-formula is used in wrong sort.") |
||

121 | else (); |
||

122 | c49eea11 | Thorsten Wißmann | | C.HCCONSTN _ -> |

123 | if func <> Constant || List.length sortlst <> 1 |
||

124 | then raise (C.CoAlgException "=-formula is used in wrong sort.") |
||

125 | else (); |
||

126 | 69a71d22 | Thorsten Wißmann | |

127 | - in initTables: Destruct the algebraic datatype into its parts. |
||

128 | |||

129 | | C.HCCONST val -> |
||

130 | !arrayType.(s).(n) <- ConstF; |
||

131 | !arrayDest3.(s).(n) <- .... [see sourcecode ...] |
||

132 | |||

133 | bbfe7b6e | Dirk Pattinson | In file CoAlgFormula.ml: |

134 | |||

135 | - sizeFormula: determine the size of the tree representation of a |
||

136 | formula |
||

137 | |||

138 | 69a71d22 | Thorsten Wißmann | - in iter: iter func formula lets the funciton func iterate over all |

139 | subformulars of formula. |
||

140 | |||

141 | - convert_post -- totally analogous to iter. |
||

142 | bbfe7b6e | Dirk Pattinson | - exportFormula_buffer: string representation of a formula |

143 | - exportTatlFormula_buffer: used for ATL, you probably want to |
||

144 | raise an exception here |
||

145 | 69a71d22 | Thorsten Wißmann | - nnfNeg -- return the negated formula in nnf. |

146 | c49eea11 | Thorsten Wißmann | - nnf -- return the formula in nnf. |

147 | - simplify -- simplifiy the formula |
||

148 | - And other utility functions: equal_hcFormula_node, equal_hcFormula_node, |
||

149 | bbfe7b6e | Dirk Pattinson | hash_hcFormula_node (possibly extend the base value), toFml_hcFormula_node, negNde_hcFormula_node, hc_formula |

150 | |||

151 | |||

152 | In file CoAlgLogics.ml: |
||

153 | 69a71d22 | Thorsten Wißmann | |

154 | bbfe7b6e | Dirk Pattinson | - getExpandingFunctionProduce: this is where you need to implement |

155 | the actual logical rule. |
||

156 | 69a71d22 | Thorsten Wißmann | // vim: tw=80 ft=asciidoc |