1. 17 Mar, 2010 7 commits
    • Erwan Jahier's avatar
      lurette 0.128 Mon, 03 Mar 2003 10:01:09 +0100 by jahier · 8d595778
      Erwan Jahier authored
      Parent-Version:      0.127
      Version-Log:
      
      source/parse_env.ml:
      source/env_state.ml:
      source/env_state.mli:
         Add support for transient /recurrent nodes (not plugged yet).
      
      source/parse_env.ml:
      source/solver.ml:
      source/formula.ml
      source/formula.mli:
      test/*.luc:
        Add the possibity to define formula and num expr aliases
        (a request from Bertrand).
      
      test/losange.luc: [new file]
      test/losange-3d.luc: [new file]
      test/test_losange.lus: [new file]
      user-rules:
         Add the losange in the non-regression test
      
      source/luc_exe.ml:
      source/command_line_luc_exe.ml:
         Add an option that lets one see local vars in lucky output.
      
      Project-Description: Lurette
      8d595778
    • Erwan Jahier's avatar
      lurette 0.126 Fri, 21 Feb 2003 18:49:20 +0100 by jahier · 5a165497
      Erwan Jahier authored
      Parent-Version:      0.125
      Version-Log:
      
      source/command_line_luc_exe.ml:
      source/command_line_luc_exe.mli:
      source/command_line.ml:
      source/command_line.mli:
      source/luc_exe.ml:
      source/lurette.ml:
      source/lurettetop.ml:
         Add the possibility to set the precision from lucky and lurette command
      lines.
      
         Remove the draw-vertices stuff.
      
      source/command_line_luc_exe.ml:
      source/command_line_luc_exe.mli:
      source/luc_exe.ml:
         Also add the --edges and the inside options for lucky.
      
      source/parse_env.ml:
        Allow to forget empty fields in the automata format.
      
      source/store.ml:
         Plug the new drawing heuristic
      
      Project-Description: Lurette
      5a165497
    • Erwan Jahier's avatar
      lurette 0.125 Fri, 21 Feb 2003 16:30:11 +0100 by jahier · 27272998
      Erwan Jahier authored
      Parent-Version:      0.124
      Version-Log:
      
      source/parse_env.ml:
         Make most fields of the automata syntax optional so that
         people are not obliged to refer to empty list of, eg,
         formula.
      
         Also add a field formula that let one defines global formula.
         This field is currently unplugged (ie, it parses, but the information
         contained in that fied in ignored).
      
      Project-Description: Lurette
      27272998
    • Erwan Jahier's avatar
      lurette 0.124 Fri, 21 Feb 2003 14:29:21 +0100 by jahier · 3ea22e95
      Erwan Jahier authored
      Parent-Version:      0.123
      Version-Log:
      
      Implement the polyhedron drawing primitives.
      
      source/util.ml.in:
         Change my_string_of_float so that it truncates floats 4 digits after the
      dot.
         The rational is that, for testing, we do not care the extra precision and
         too much precision may kill Polka. This precison ougth to be a parameter
         though.
      
      source/solver.ml:
      source/polyhedron.ml:
      source/store.ml:
          Implement the polyhedron drawing primitives.
      
      source/store.ml:
         Apply the substitutions in store.subtsl to the cstr to add.
      
      Project-Description: Lurette
      3ea22e95
    • Erwan Jahier's avatar
      lurette 0.122 Mon, 17 Feb 2003 14:50:50 +0100 by jahier · 78f40b65
      Erwan Jahier authored
      Parent-Version:      0.121
      Version-Log:
      
      When delayed constraints are remaining at bdd leaves, we were
      printing a message saying that one shoud use a polyhedron solver
      based instead.  Now, I really call such a polyhedron solver in order
      to solve those constraints.
      
      This means that I use to different solvers to handle interval and
      polyhedron of dimension > 1.
      
      It also means that the satisfiability of constraints over polyhedra
      is only checked at bdd leaves, which, in some circumstances, migth be
      inefficient. The point is that, if we chose to check the formula
      satisfiability during the bdd traversal, we take the risk that a very
      polyhedron is created whereas it was not necessary (because of
      forthcoming equalities). And creating polyhedron with big (>15)
      dimension simply runs forever, which is really bad.
      
      nb : drawing in poyhedron not yet plugged.
      
      source/polyhedron.ml:
      source/polyhedron.mli: (new files)
          misc functions over polyhedra. The rational for creating that file
          is that rnumsolver is already much too big (and should be splitted
          some more btw).
      
      source/solver.ml:
         One of the main change is that now, draw_in_bdd returns 2 stores.
         One is Range based, the other one is polyhedron-based.
      
      source/rnumsolver.mli:
      source/rnumsolver.ml:
         Add the function switch_to_polyhedron_representation which
         handle delayed constraint if necessary. It is meant to be called
         at bdd leaves.
      
      source/solver.ml:
      source/rnumsolver.ml:
         Also do not use split_store anymore but add_constraint. This allows
         a much more elegant and efficient implementation of draw_in_bdd and
         draw_in_bdd_eq (Now the store is buid when and only when a new branch
         should be tried because of backtracking). It is also more efficient.
      
      source/constraint.mli
      source/constraint.ml
      source/ne.mli
      source/ne.ml
         Implement get_vars that retreive the variables occuring in a contraint
         or an expression.
      
      Project-Description: Lurette
      78f40b65
    • Erwan Jahier's avatar
      lurette 0.121 Tue, 11 Feb 2003 11:20:37 +0100 by jahier · 34cdff0c
      Erwan Jahier authored
      Parent-Version:      0.120
      Version-Log:
      
      source/pnumsolver.ml:
      source/pnumsolver.mli: [new files]
         Implements a numeric solver based on Polka.
         (not plugged yet).
      
      source/rnumsolver.ml:
         Reimplement split_store so that it uses 2 calls of add_constraint
         instead of doing the work twice inside split_store (in order to avoid code
         duplication).
      
         Also, whenever delayed constraints becomes of dimension 1, when a
      add_constraint
         binds a value, add them to the store.
      
         Enhance error msgs whenever int and float are mixed in the same lucky
         expressions.
      
      source/rnumsolver.ml:
      source/ne.ml:
         rename Ne.resolve_triangular_system into get_subst_from_solved_system
         and move it into rnumsolver. The rational is that is was not
         really solving any triangular system: the system ougth to be already solved.
      
      source/parce_env.ml:
         Set the max_float to max_int, otherwise, the conversion into polka rational
         fails...
      
      Project-Description: Lurette
      34cdff0c
    • Erwan Jahier's avatar
      lurette 0.119 Thu, 19 Dec 2002 10:29:35 +0100 by jahier · 566a6b90
      Erwan Jahier authored
      Parent-Version:      0.118
      Version-Log:
      
      user-rules:
          Add the name of the host in the timing result files.
      
          Also runs the timing tests on ecrins.
      
      Project-Description: Lurette
      566a6b90