ed8ae1ed55* src/bdd.h: Declare bdd_copypair(). * src/pairs.c (bdd_copypair, bdd_pairalloc): New functions. (bdd_newpair): Use bdd_pairalloc.
Alexandre Duret-Lutz
2003-05-19 15:58:44 +00:00
38f7ae9a46* src/ltlvisit/dotty.cc: Rewrite to display formulae as graphs rather than trees, to show how nodes are shared.
Alexandre Duret-Lutz
2003-05-16 09:35:21 +00:00
1cdfea31b0Check trivial multop equality at build time. The makes the equal visitor useless, since two equals formulae will now share the same address.
Alexandre Duret-Lutz
2003-05-16 07:39:41 +00:00
9123e56ff9Implements spot::ltl::destroy() and exercise it.
Alexandre Duret-Lutz
2003-05-15 18:06:54 +00:00
5f6d8b6234Massage the AST so that identical sub-formula share the same reference-counted formula*. One can't call constructors for AST items anymore, everything need to be acquired through instance() class methods.
Alexandre Duret-Lutz
2003-05-15 13:39:39 +00:00
f1838ab8ef* src/ltlparse/ltlscan.ll (to_parse_size): Declare as size_t to remove a warning with newer versions of Flex.
Alexandre Duret-Lutz
2003-05-15 08:55:52 +00:00
a92327d30b* src/ltlparse/ltlparse.yy (error_list, parse_environment, result): CVS Bison now supports %parse-param for the C++ skeleton; pass these variables as arguments to the Parser::Parser constructor instead of using globals. (parse): Adjust Parser::Parser call.
Alexandre Duret-Lutz
2003-05-15 08:10:38 +00:00
8e988470b1* src/ltlvisit/tostring.cc: Reindent and strip out superfluous spot::ltl:: prefixes. (to_string(formula)): New function. * src/ltlvisit/tostring.hh (to_string(formula)): Likewise. * src/ltltest/tostring.cc: Use this new to_string function to simplify.
Alexandre Duret-Lutz
2003-05-12 12:41:41 +00:00
fec4f04a2f* src/ltlenv/defaultenv.hh: Do not include atomic_prop.hh here... * src/ltlenv/defaultenv.cc: ... but here.
Alexandre Duret-Lutz
2003-04-29 12:59:45 +00:00
d17a86e87d* src/ltltest/tostring.test: Simplify with set -e. Move the description of the test ... * src/ltltest/tostring.cc: ... here, where it is actually coded. * src/ltltest/lunabbrev.test, src/ltltest/tunabbrev.test, src/ltltest/nenoform.test, src/ltltest/tunenoform.test: Simplify with set -e.
Alexandre Duret-Lutz
2003-04-29 11:26:16 +00:00
03e893b23d* configure.ac (AM_INIT_AUTOMAKE): Use nostdinc, to make sure we always use paths relative to src/ in src/'s subdirectories.
Alexandre Duret-Lutz
2003-04-29 11:15:00 +00:00
cc519254c5* src/ltlparse/Makefile.am (CXXFLAGS): Turn on GCC warnings now that CVS Bison is fixed. * src/ltlparse/ltlscan.ll: Use yyunput to shut up a GCC warning.
Alexandre Duret-Lutz
2003-04-28 15:58:41 +00:00
7cb2aa5b84empty commit to check scripts
rebiha
2003-04-24 10:47:08 +00:00
eed40025be* src/ltltest/tostring.test: New file. * src/ltltest/tostring.cc: New files. * src/ltlvisit/tostring.hh: From ast to string New files. * src/ltlvisit/tostring.cc: From ast to string New files.
rebiha
2003-04-24 10:43:26 +00:00
2a0f88373e* src/ltlenv/environment.hh (require): Return a formula, not an atomic_prop. * src/ltlast/atomic_prop.hh (atomic_prop): New argument env. (environment_): New member. (env): New method. * src/ltlast/atomic_prop.cc (atomic_prop, env): Likewise. * src/ltlenv/defaultenv.cc (require): Pass *this as the environment argument to atomic_prop. * src/ltlvisit/clone.cc (visit(const atomic_prop*)): Also copy the environment. * src/ltlvisit/nenoform.cc (visit(const atomic_prop*)): Likewise.
Alexandre Duret-Lutz
2003-04-17 15:47:56 +00:00
a30a0638b9* configure.ac: Output src/ltlenv/Makefile. * src/ltlenv/Makefile.am, src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh, src/ltlenv/environment.hh: New files. * src/ltlparse/public.hh (parse): Take an environment as third argument. * src/ltlparse/ltlparse.yy (ATOMIC_PROP, parse): Require the atomic proposition via the environment. * src/ltltest/readltl.cc (main): Adjust the call to parse(). * src/ltltest/Makefile.am (LDADD): Add ../ltlenv/libltlenv.a.
Alexandre Duret-Lutz
2003-04-17 15:09:49 +00:00
ae7fdeba59* src/ltlvisit/clone.hh, src/ltlvisit/clone.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltlvisit/lunabbrev.hh, src/ltlvisit/lunabbrev.cc: Inherit from clone_visitor and remove all useless methods (now inherited).
Alexandre Duret-Lutz
2003-04-17 13:59:15 +00:00
0c7a2412a4* src/ltlvisit/nenoform.hh, src/ltlvisit/nenoform.cc: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltltest/equals.cc (main) [NENOFORM]: Call negative_normal_form. * src/ltltest/nenoform.test, src/ltltest/tunenoform.test: New files. * src/ltltest/Makefile.am (check_PROGRAMS): Add nenoform and tunenoform. (nenoform_SOURCES, nenoform_CPPFLAGS, tunenoform_SOURCES, tunenoform_CPPFLAGS): New variables. (TESTS): Add nenoform.test and tunenoform.test.
Alexandre Duret-Lutz
2003-04-17 13:12:11 +00:00
e58aae95c0* src/ltlvisit/lunabbrev.hh: Fix include guard.
Alexandre Duret-Lutz
2003-04-17 10:03:49 +00:00
080214ebb8* src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add them. * src/ltltest/tunabbrev.test: New file. * src/ltltest/lunabbrev.test: Fix comment. * src/ltltest/Makefile.am (TESTS): Add tunabbrev.test. (check_PROGRAMS): Add tunabbrev. (tunabbrev_SOURCES, tunabbrev_CPPFLAGS): New variables. * src/ltltest/equals.cc (main) [TUNABBREV]: Call unabbreviate_ltl. * src/ltlvisit/lunabbrev.hh (unabbreviate_logic_visitor::recurse): New virtual function. * src/ltlvisit/lunabbrev.cc (unabbreviate_logic_visitor::recurse): Likewise. (unabbreviate_logic_visitor::visit): Use it instead of calling unabbreviate_logic directly.
Alexandre Duret-Lutz
2003-04-16 16:10:58 +00:00
526012a795* src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh: New files. * 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.
Alexandre Duret-Lutz
2003-04-16 15:30:44 +00:00
5d714612a3* src/ltltest/equals.test (check0, check1): Remove. Use check 0, and check 1 instead.
Alexandre Duret-Lutz
2003-04-16 15:05:57 +00:00
ef2d6323e0* src/ltlast/formulae.hh: Rename as ... * 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.
Alexandre Duret-Lutz
2003-04-16 13:11:34 +00:00
532f9131f5* src/ltlparse/public.hh (format_parse_errors): New function. * src/ltlparse/fmterror.cc: New file. * src/ltlparse/Makefile.am (libltlparse_a_SOURCES): Add fmterror.cc. * src/ltltests/equals.cc, src/ltltests/readltl.cc: Simplify using format_parse_errors.
Alexandre Duret-Lutz
2003-04-16 12:58:17 +00:00
7425f4a91e* src/ltlvisit/equals.cc, src/ltlvisit/equals.hh: New files. * src/ltlvisit/Makefile.am (libltlvisit_a_SOURCES): Add equals.hh and equals.cc. * src/ltltest/equals.cc, src/ltltest/equals.test: New files. * src/ltltest/Makefile.am (check_PROGRAMS): Add equals. (equals_SOURCES): New variable. (TESTS): Add equals.test.
Alexandre Duret-Lutz
2003-04-16 12:30:21 +00:00
eec66e6d07* src/ltlast/multop.cc (multop::multop): Use multop::add. (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.
Alexandre Duret-Lutz
2003-04-16 11:27:06 +00:00
Alexandre Duret-Lutz
rebiha