diff --git a/packages/cplint/doc/manual.html b/packages/cplint/doc/manual.html index df314f7e8..fb4fe51f3 100644 --- a/packages/cplint/doc/manual.html +++ b/packages/cplint/doc/manual.html @@ -392,7 +392,7 @@ determination(student/1,hasposition/2).

  • verbosity (values: integer in [1,3], default value: 1): level of verbosity of the algorithms

  • beamsize (values: integer, default value: 20, valid for SLIPCASE and SLIPCOVER): size of the beam

  • mcts_beamsize (values: integer, default value: 3, valid for LEMUR): size of the MCTS beam

    • -

  • mcts_visits (values: integer, default value: +inf, valid for LEMUR): maximum number of visits (Nicola controlla)

    • +

  • mcts_visits (values: integer, default value: +inf, valid for LEMUR): maximum number of visits

  • megaex_bottom (values: integer, default value: 1, valid for SLIPCOVER): number of mega-examples on which to build the bottom clauses

  • initial_clauses_per_megaex (values: integer, default value: 1, valid for SLIPCOVER): number of bottom clauses to build for each mega-example

  • d (values: integer, default value: 10000, valid for SLIPCOVER): number of saturation steps when building the bottom clause

    • @@ -426,7 +426,7 @@ determination(student/1,hasposition/2). 
    ?:- use_module(library('cplint/lemur')).

    and call

    ?:- "mcts(stem,depth,c,iter,rules,covering)
    -

    where depth (integer) is the maximum number of random specialization steps in the default policy, C (real) is the value of the MCTS C constant, iter (integer) is the number of UCT rounds, rules (integer) is the maximum number of clauses to be learned and covering (Boolean) dentoes whether the search is peformed in the space of clauses (true) or theories (false) (Nicola controlla).

    +

    where depth (integer) is the maximum number of random specialization steps in the default policy, C (real) is the value of the MCTS C constant, iter (integer) is the number of UCT rounds, rules (integer) is the maximum number of clauses to be learned and covering (Boolean) dentoes whether the search is peformed in the space of clauses (true) or theories (false).

    Testing

    To test the theories learned, load test.pl with

    ?:- use_module(library('cplint/test')).
    diff --git a/packages/cplint/doc/manual.pdf b/packages/cplint/doc/manual.pdf index adde428d6..7163fb227 100644 Binary files a/packages/cplint/doc/manual.pdf and b/packages/cplint/doc/manual.pdf differ diff --git a/packages/cplint/doc/manual.tex b/packages/cplint/doc/manual.tex index 8f7720b1a..d076dacad 100644 --- a/packages/cplint/doc/manual.tex +++ b/packages/cplint/doc/manual.tex @@ -632,7 +632,7 @@ SLIPCOVER and LEMUR): maximum number of distinct variables in a clause \item \verb|beamsize| (values: integer, default value: 20, valid for SLIPCASE and SLIPCOVER): size of the beam \item \verb|mcts_beamsize| (values: integer, default value: 3, valid for LEMUR): size of the MCTS beam -\item \verb|mcts_visits| (values: integer, default value: +inf, valid for LEMUR): maximum number of visits (Nicola controlla) +\item \verb|mcts_visits| (values: integer, default value: +inf, valid for LEMUR): maximum number of visits \item \verb|megaex_bottom| (values: integer, default value: 1, valid for SLIPCOVER): number of mega-examples on which to build the bottom clauses \item \verb|initial_clauses_per_megaex| (values: integer, default value: 1, valid for SLIPCOVER): @@ -701,7 +701,7 @@ where \verb|depth| (integer) is the maximum number of random specialization steps in the default policy, \verb|C| (real) is the value of the MCTS $C$ constant, \verb|iter| (integer) is the number of UCT rounds, \verb|rules| (integer) is the maximum number of clauses to be learned and \verb|covering| (Boolean) dentoes whether the search is peformed in -the space of clauses (true) or theories (false) (Nicola controlla). +the space of clauses (true) or theories (false). \subsection{Testing} To test the theories learned, load \texttt{test.pl} with