1. 31 Jul, 2003 1 commit
  2. 16 May, 2003 1 commit
    • Alexandre Duret-Lutz's avatar
      Check trivial multop equality at build time. The makes the · 1cdfea31
      Alexandre Duret-Lutz authored
      equal visitor useless, since two equals formulae will now
      share the same address.
      
      * src/ltlast/multop.hh (add_sorted): New function.
      (paircmp): New comparison functor.
      (map): Use paircmp, we want to compare the vectors' contents,
      not their addresses.
      * src/ltlast/multop.cc (add_sorted): New function.
      (add): Use it.
      * src/ltltest/equals.cc, src/ltltest/tostring.cc: Compare
      pointers instead of calling equal.
      * src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: Delete.
      * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Remove
      equals.cc and equals.hh.
      * wrap/spot.i: Do not include equals.hh.
      1cdfea31
  3. 15 May, 2003 2 commits
    • Alexandre Duret-Lutz's avatar
      Implements spot::ltl::destroy() and exercise it. · 9123e56f
      Alexandre Duret-Lutz authored
      * src/ltlast/atomic_prop.hh: Declare instance_count().
      * src/ltlast/binop.hh, src/ltlast/unop.hh, src/ltlast/multop.hh:
      Likewise.  Also, really inherit for ref_formula this time.
      * src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
      src/ltlast/unop.cc, src/ltlast/multop.cc: On destruction, suppress
      the instance from the instance map.  Implement instance_count().
      * src/ltlast/formula.cc, src/ltlast/formula.hh,
      src/ltlast/ref_formula.cc, src/ltlast/ref_formula.hh: Add virtual
      destructors.
      * src/ltlparse/ltlparse.yy: Recover from binary operators with
      missing right hand operand (the point is just to destroy the
      the left hand operand).
      * src/ltltest/equals.cc, src/ltltest/readltl.cc,
      src/ltltest/tostring.cc: Destroy used formulae.  Make sure
      instance_count()s are null are the end.
      * src/ltltest/parseerr.test: Adjust expected result, now
      that the parser lnows about missing right hand operands.
      * src/ltlvisit/destroy.hh, src/ltlvisit/destroy.cc,
      src/ltlvisit/postfix.hh, src/ltlvisit/postfix.cc: New files.
      * src/ltlvisit/Makefile.am (libltlvisit_la_SOURCES): Add them.
      * src/ltlvisit/lunabbrev.cc (Xor, Equiv): Clone formulae
      occurring twice in the rewritten expression.
      9123e56f
    • Alexandre Duret-Lutz's avatar
      Massage the AST so that identical sub-formula share the same · 5f6d8b62
      Alexandre Duret-Lutz authored
      reference-counted formula*.  One can't call constructors for AST
      items anymore, everything need to be acquired through instance()
      class methods.
      
      * src/ltlast/formula.cc, src/ltlast/refformula.cc,
      src/ltlast/refformula.hh: New files.
      * src/ltlast/Makefile.am (libltlast_la_SOURCES): Add them.
      * src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/unop.cc, src/ltlast/unop.hh,
      src/ltlast/binop.cc, src/ltlast/binop.hh: Make the constructor
      and destructor protected.  Define a static function `instance()'
      to get an instance with specific argument.  Use a map called
      `instances' to store all known instances.  Inherit from
      ref_formula.
      * src/ltlast/constant.hh, src/ltlast/constant.cc: Protect
      the constructor and destructor.  Provide the false_instance()
      and true_instance() functions instead.
      * src/formula.hh (ref, unref, ref_, unref_): New methods.
      * src/ltlast/multop.cc, src/ltlast/multop.hh: Protect
      the constructor, destructor, as well as the add() method.
      Provides the instance(), and add() class methods instead.
      Store children_ as a pointer.
      * src/ltlenv/defaultenv.cc (require): Adjust to
      call atomic_prop::instance.
      * src/ltlparse/ltlparse.yy: Adjust to call instance() functions
      instead of constructors.
      * src/ltltest/Makefile.am (LDADD): Tweak library ordering.
      * src/ltlvisit/clone.hh (clone_visitor): Inherit from visitor,
      not const_visitor, and adjust all prototypes appropriately.
      * src/ltlvisit/clone.cc (clone_visitor): Likewise.
      Call ref() or instance() methods instead of copy constructors.
      * src/ltlvisit/equals.cc: Simplify atomic_prop and constant
      cases.
      * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc,
      src/ltlvisit/tunabbrev.hh, src/ltlvisit/tunabbrev.cc,
      src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: Use instance()
      methods instead of constructor.  Make these children of visitor, not
      const_visitor.
      * src/ltltest/readltl.c (main): Do not delete the formula.
      5f6d8b62
  4. 16 Apr, 2003 3 commits
    • Alexandre Duret-Lutz's avatar
      * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files. · 526012a7
      Alexandre Duret-Lutz authored
      * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them.
      * src/ltlast/multop.cc (multop::multop(type)): New constructor.
      * src/ltlast/multop.hh (multop::multop(type)): New constructor.
      * src/ltltest/lunabbrev.test: New file.
      * src/ltltest/Makefile.am (TESTS): Add lunabbrev.test.
      (check_PROGRAMS): Add lunabbrev.
      (lunabbrev_SOURCES, lunabbrev_CPPFLAGS): New variables.
      * src/ltltest/equals.cc (main) [LUNABBREV]: Call unabbreviate_logic.
      526012a7
    • Alexandre Duret-Lutz's avatar
      * src/ltlast/formulae.hh: Rename as ... · ef2d6323
      Alexandre Duret-Lutz authored
      * src/ltlast/formula.hh: ... this.
      * src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust.
      * src/ltlast/formula.hh (formulae): Rename as ...
      (formula): ... this.
      Adjust all uses.
      ef2d6323
    • Alexandre Duret-Lutz's avatar
      * src/ltlast/multop.cc (multop::multop): Use multop::add. · eec66e6d
      Alexandre Duret-Lutz authored
      (multop::add): If the formulae we add is itself a multop for the
      same operator, merge its children with ours.
      * src/ltltest/parseerr.test: Add two tests for multop merging.
      eec66e6d
  5. 15 Apr, 2003 2 commits
    • Alexandre Duret-Lutz's avatar
      * src/ltlast/formulae.hh (formulae::equals): Remove. · dfc82ee3
      Alexandre Duret-Lutz authored
      * src/ltlast/unop.hh (unop::equals): Remove.
      * src/ltlast/unop.cc (unop::equals): Remove.
      * src/ltlast/binop.hh (binop::equals): Remove.
      * src/ltlast/binop.cc (binop::equals): Remove.
      * src/ltlast/multop.hh (multop::equals): Remove.
      * src/ltlast/multop.cc (multop::equals): Remove.
      * src/ltlast/atomic_prop.hh (atomic_prop::equals): Remove.
      * src/ltlast/atomic_prop.cc (atomic_prop::equals): Remove.
      * src/ltlast/constant.hh (constant::equals): Remove.
      * src/ltlast/constant.cc (constant::equals): Remove.
      dfc82ee3
    • Alexandre Duret-Lutz's avatar
      * HACKING, Makefile.am, configure.ac, m4/gccwarn.m4, · f0a8d0ae
      Alexandre Duret-Lutz authored
      src/Makefile.am, src/ltlast/Makefile.am, src/ltlast/allnodes.hh,
      src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
      src/ltlast/binop.cc, src/ltlast/binop.hh, src/ltlast/constant.cc,
      src/ltlast/constant.hh, src/ltlast/formulae.hh,
      src/ltlast/multop.cc, src/ltlast/multop.hh, src/ltlast/predecl.hh,
      src/ltlast/unop.cc, src/ltlast/unop.hh, src/ltlast/visitor.hh,
      src/ltlparse/Makefile.am, src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
      src/ltlparse/public.hh, src/ltlvisit/Makefile.am,
      src/ltlvisit/dotty.cc, src/ltlvisit/dotty.hh,
      src/ltlvisit/dump.cc, src/ltlvisit/dump.hh,
      src/ltlvisit/rewrite.cc, src/ltlvisit/rewrite.hh,
      src/ltltest/Makefile.am, src/ltltest/defs.in, src/ltltest/readltl.cc,
      src/ltltest/parse.test, src/ltltest/parseerr.test,
      src/misc/Makefile.am, src/misc/const_sel.hh: New files.
      f0a8d0ae