alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
6176 commits 6 branches 0 tags 36 MiB
Commit graph

124 commits

Author SHA1 Message Date
philipp
540b31dbd7 [buddy] Improve bdd_have_common_assignment 
* src/bddop.c: Improve here
* src/bddtest.cxx: Tests here
 2021-11-05 09:23:57 +01:00
philipp
c5a61da22b [buddy] Fix is_cube() and add tests 
* src/bddop.c: Fix is_cube with bddtrue as input
* src/bddtest.cxx: Add tests here
 2021-11-05 09:23:57 +01:00
Alexandre Duret-Lutz
ece7631e8c [buddy] fix a spurious failure 
* examples/bddtest/bddtest.cxx: reset some global BDDs to avoid
issues when they are destroyed after BuDDy.
 2021-11-04 23:19:31 +01:00
Alexandre Duret-Lutz
5a9c8aad0d [buddy] execute some of the tests during "make check" 
* examples/bddtest/Makefile.am, src/Makefile.am (TESTS):
Add this variable.
* examples/bddtest/bddtest.cxx: Return non-zero on error.
 2021-11-04 15:24:10 +01:00
philipp
3aef5f31c0 [buddy] Adding bdd_is_cube 
bdd_is_cube determines whether or not a given bdd
represents a cube.

* src/bddop.c: Here
* src/bddx.h: And here
 2021-09-16 14:53:45 +02:00
Alexandre Duret-Lutz
5a0fbf6cb9 [buddy] introduce a bdd_satoneshortest() function 
* src/bddop.c, src/bddx.h: Introduce this function.
* src/bddtest.cxx: Add some short tests.
 2021-09-16 14:53:45 +02:00
Alexandre Duret-Lutz
dfd168b048 [buddy] fix bdd_has_common_assignement 
* src/bddop.c, src/bddx.h (bdd_has_common_assignement): Rename as...
(bdd_have_common_assignment): ... this, and fix level comparisons.
Also add a cache.
 2021-07-30 11:35:10 +02:00
philipp
92239d8242 [buddy] Adding bdd_has_common_assignement 
bdd_has_common_assignement determines if two bdds a and b
have (at least) one common assignement.
That is it will return true iff bdd_and(a, b) != bddfalse.

* src/bddx.h: Here
* src/bddop.c: Here
 2021-07-27 16:45:44 +02:00
Alexandre Duret-Lutz
e6055c57a7 [buddy] typo coma -> comma 
* ChangeLog.1: Here.
 2021-06-11 11:47:34 +02:00
Alexandre Duret-Lutz
9ed2682f67 [buddy] introduce bdd_stable_cmp 
* src/bddx.h, misc/bddlt.hh (bdd_stable_cmp): Define this
new function, based on some code that was implemented in Spot, but was
unnecessarily doing reference counting.
 2021-06-11 11:47:29 +02:00
Alexandre Duret-Lutz
d2fe46136a [buddy] introduce minterm enumeration support 
* src/bddop.c, src/bddx.h (bdd_ibuildcube2, bdd_first_minterm,
bdd_next_minterm): New functions.
* src/bddx.h (minterms_of): New class.
 2021-04-12 17:52:47 +02:00
Alexandre Duret-Lutz
06b5a82950 [buddy] update obsolete autoconf constructs 
Part of #447.

* configure.ac, m4/bdebug.m4: Replace AC_ERROR and AC_HELP_STRING by
by AC_MSG_ERROR and AS_HELP_STRING.
 2021-01-14 15:15:39 +01:00
Alexandre Duret-Lutz
6f76121b89 [buddy] get rid of many recursive algorithms 
This patch addresses the BuDDy part of #396,
reported by Florian Renkin and Reed Oei.

* src/kernel.c, src/kernel.h: Declare a bddrecstack and
associated macros.  Resize it when new variable are declared.
* src/cache.h: Add a BddCache_index macro.
* src/bddop.c (not_rec, apply_rec, quant_rec, appquant_rec,
support_rec, ite_rec, compose_rec, restrict_rec, satone_rec,
satoneset_rec): Rewrite using this stack to get rid of the recursion.
 2020-08-05 23:25:28 +02:00
Alexandre Duret-Lutz
a7ff5b4eed [buddy] build in C++17 mode by default 
* configure.ac: Activate C++17, and replace --enable-c++17 by
--enable-c++20.
 2020-07-16 12:14:47 +02:00
Alexandre Duret-Lutz
da96a509e9 [buddy] avoid cache errors in bdd_satcount() and friends 
* src/bddop.c (bdd_satcount, bdd_satcountln): If the number of
declared variables changed since we last used it, reset misccache.
Otherwise, bdd_satcount() and friends might return incorrect results
after the number of variable is changed.  These is needed for the next
patch in Spot to pass all tests.
(misccache_varnum): New global variable to track that.
(bdd_satcountset): Make sure that bdd_satcountset(bddtrue, bddtrue)
return 1.0 and not 0.0.
 2020-05-18 20:49:14 +02:00
Alexandre Duret-Lutz
118df55bc3 [buddy] workaround newer clang warning 
It seems clang now warn about fallthrough case statements in C, but
ignore any /* fall through */ comment if that comes from a macro.

* src/bddop.c: Use the fallthrough attribute if available.
 2020-04-30 08:14:50 +02:00
Alexandre Duret-Lutz
7e44016d38 [buddy] improve C++ backward compatibility around bdd_allsat change 
* src/bddx.h (bdd_allsat): Add a version with the old prototype.
 2019-09-27 20:43:07 +02:00
Alexandre Duret-Lutz
a7e4cb4182 [buddy] fix ARM compilation 
* src/bddop.c, src/bddx.h, examples/bddtest/bddtest.cxx: Use signed
char* instead of char*.
 2019-09-26 14:40:44 +02:00
Alexandre Duret-Lutz
d0b9806500 [buddy] remember to free bddhash on exit 
* src/kernel.c (bdd_done): Free bddhash.
 2019-02-05 18:12:30 +01:00
Alexandre Duret-Lutz
057e67e7f6 [buddy] do not use ACLOCAL_AMFLAGS anymore 
Fixes #326.

* Makefile.am: Here.
 2018-03-09 20:24:37 +01:00
Alexandre Duret-Lutz
7f42782701 [buddy] switch to C++14 compilation 
* configure.ac: Here.  Rename --enable-c++14 into --enable-c++17.
 2017-08-22 18:21:46 +02:00
Alexandre Duret-Lutz
361b44e571 [buddy] use powers of two for the sizes of all hash tables 
* src/bddop.c, src/bddx.h, src/cache.c, src/cache.h, src/kernel.c,
src/kernel.h, src/prime.c, src/prime.h, src/reorder.c: Use power of
two for the sizes of all hash tables, in order to reduce the amount of
divisions performed.  Also allow bddhash to be smaller than bddnodes.
 2017-07-24 13:42:21 +02:00
Alexandre Duret-Lutz
819cd7b8b6 [buddy] fix handling of bdd_apply_biimp 
* src/bddop.c: Fix shortcut.
 2017-06-20 15:19:00 +02:00
Alexandre Duret-Lutz
613c485c24 [buddy] rename ChangeLog 
We generate ChangeLog from git log now.

* ChangeLog: Rename as...
* ChangeLog.1: ... this.
* Makefile.am: Distribute the latter.
 2017-05-04 13:32:52 +02:00
Alexandre Duret-Lutz
800db9c251 [buddy] fix libbddx.pc generation 
Report from Jeroen Meijer.

* src/Makefile.am (libbddx.pc): Depends on Makefile.  Use a
temporary.  Declare in CLEANFILES instead of DISTCLEANFILES.
 2017-05-04 11:13:19 +02:00
Alexandre Duret-Lutz
cb920242a7 [buddy] fix previous patch 
* src/fdd.c: C++ comments are not supported in C90.
 2017-04-19 13:25:07 +02:00
Michael Weber
44ca086f5d [buddy] Addref in fdd_intaddvarblock 
* src/fdd.c (fdd_intaddvarblock): Add missing addref.

Signed-off-by: Jaco van de Pol <J.C.vandepol@ewi.utwente.nl>
Signed-off-by: Michael Weber <michaelw@cs.utwente.nl>
 2017-04-19 11:22:20 +02:00
Alexandre Duret-Lutz
42e5cd955e [buddy] Typos in comments 
* src/kernel.c (bdd_addref): Fix typo documentation.
* src/bddop.c (bdd_appall, bdd_appallcomp): Likewise.
 2017-03-30 21:45:22 +02:00
Alexandre Duret-Lutz
63776d9c93 [buddy] add -Wno-gnu if supported 
* m4/gccwarns.m4: Add -Wno-gnu to workaround a diagnostic from
clang 3.9.1 on arch Linux.  clang was complaining whtat assert()
is using a GNU extension.
 2017-03-14 12:03:10 +01:00
Alexandre Duret-Lutz
bd4e0f19b9 [buddy] remove useless #include<assert.h> 
* src/bddio.c, src/bddop.c, src/imatrix.c, src/pairs.c: Here.
 2017-03-13 22:26:47 +01:00
Alexandre Duret-Lutz
33f9e03e83 [buddy] update the warning flags to match Spot's 
* m4/gccwarns.m4: Add more flags taken from Spot.
Also add -Wno-long-long to suppress one warning.
 2017-02-01 18:50:54 +01:00
Alexandre Duret-Lutz
a2f174f721 [buddy] fix some -Wpedantic messages 
* src/bddop.c: Empty macro arguments are undefined ISO C90 and
ISO C++98.  Use '+' when calling APPLY_SHORTCUTS.
* src/fdd.c, src/kernel.c: Avoid constructs invalid in C90.
* src/bddop.c, src/bddx.h, src/kernel.c, src/kernel.h,
examples/cmilner/cmilner.c: Remove C++ comments.
 2017-02-01 18:50:37 +01:00
Alexandre Duret-Lutz
a9b056baa4 [buddy] install a pkg-config file 
* src/libbddx.pc.in: New file.
* src/Makefile.am: Generate libbddx.pc, and install it.
Distribute libbddx.pc.in.
* src/.gitignore: Ignore *.pc.
 2017-01-14 17:55:58 +01:00
Maximilien Colange
878649c823 [buddy] Add an option to enable C++14. 
* configure.ac: add an option --enable-c++14.
 2016-12-13 17:42:22 +01:00
Alexandre Duret-Lutz
38c4fc8812 [buddy] fix bdd_noderesize 
* src/kernel.c: Fix error introduced by 5a862295.
Report from Tomáš Babiak.
 2016-11-19 16:46:10 +01:00
Alexandre Duret-Lutz
0ac14e9ca2 [buddy] avoid costly calls to setjmp() when BDD_REORDER_NONE 
* src/reorder.c, src/kernel.h: Expose bddreordermethod.
* src/bddop.c: Test bddreordermethod before ever calling setjmp().
 2016-11-09 14:52:04 +01:00
Alexandre Duret-Lutz
84b16aa6bd [buddy] consolidate shortcuts for binary operation 
* src/bddop.c (apply_rec, appquant_rec): Define missing shortcuts
for bddop_less, bddop_diff, bddop_revimpl and define them once.
 2016-11-09 10:29:00 +01:00
Alexandre Duret-Lutz
5a862295d3 [buddy] improve initialization of bddnode 
* src/kernel.c, src/kernel.h: Here.
 2016-11-08 19:03:08 +01:00
Alexandre Duret-Lutz
63818a3e69 [buddy] Fix several PVS-Studio warnings 
For #192.

* src/bddio.c, src/cppext.cxx, src/kernel.c: Fix printf formats, calls
to new, and simplify one check in bdd_delref_nc().
 2016-10-28 17:12:21 +02:00
Alexandre Duret-Lutz
a32ccd649d [buddy] slight optimization of bdd_implies 
* src/bddop.c: Avoid the first recursion when it is obvious that the
second will fail.
 2016-10-20 20:59:28 +02:00
Alexandre Duret-Lutz
57a055b656 [buddy] typo in comment 
* src/bddop.c (bdd_implies): Fix documentation.
 2016-10-20 09:37:24 +02:00
Alexandre Duret-Lutz
4c1147e497 [buddy] speedup bdd_init and bdd_noderesize 
* src/kernel.c: The initialization code of the BDD cache was
awfully slow due to multiple references to global variables.
 2016-10-19 10:51:38 +02:00
Alexandre Duret-Lutz
8e69530023 [buddy] fix an undefined behavior 
* src/prime.c (BitIsSet): Do not shift signed
int by 31 places; shift unsigned int instead.
 2016-07-27 19:47:30 +02:00
Alexandre Duret-Lutz
86abd6c1c0 Use -Bsymbolic-functions and -Bsymbolic 
This avoids dynamic lookups to resolve symbols inside the library, but
disallows symbol interposition.

* m4/symbolic.m4: New file.
* buddy/m4/symbolic.m4: New link.
* configure.ac, buddy/configure.ac: Add AX_SYMBOLIC.
* buddy/src/Makefile.am, iface/ltsmin/Makefile.am, src/Makefile.am,
wrap/python/Makefile.am: Link with $(SYMBOLIC_LDFLAGS).
 2015-11-10 15:10:11 +01:00
Etienne Renault
5f4b7e1f3f Remove all cvsignore files. 
* .cvsignore, bench/.cvsignore,
bench/emptchk/.cvsignore, bench/emptchk/models/.cvsignore,
bench/ltl2tgba/.cvsignore, buddy/.cvsignore,
buddy/doc/.cvsignore, buddy/examples/.cvsignore,
buddy/examples/adder/.cvsignore,
buddy/examples/bddcalc/.cvsignore,
buddy/examples/bddtest/.cvsignore,
buddy/examples/calculator/.cvsignore,
buddy/examples/cmilner/.cvsignore,
buddy/examples/fdd/.cvsignore,
buddy/examples/internal/.cvsignore,
buddy/examples/milner/.cvsignore,
buddy/examples/money/.cvsignore,
buddy/examples/queen/.cvsignore,
buddy/examples/solitare/.cvsignore,
buddy/src/.cvsignore, buddy/tools/.cvsignore,
doc/.cvsignore, iface/.cvsignore,
src/.cvsignore, src/ltlast/.cvsignore,
src/ltlenv/.cvsignore, src/ltlparse/.cvsignore,
src/ltlvisit/.cvsignore, src/misc/.cvsignore,
src/sanity/.cvsignore, src/tests/.cvsignore,
src/twa/.cvsignore, tools/.cvsignore,
wrap/.cvsignore, wrap/python/.cvsignore,
wrap/python/tests/.cvsignore: here.
 2015-04-24 13:57:56 +02:00
Alexandre Duret-Lutz
1ffdd57383 [buddy] backport some fixes from upstream 
* src/fdd.c, src/imatrix.c, src/kernel.c, src/reorder.c: Here.
 2015-03-11 23:45:00 +01:00
Alexandre Duret-Lutz
787e3f9315 [buddy] fix undefined behavior 
The bug was found while running Spot's src/tgbatest/randpsl.test
on Debian i386 with gcc-4.9.2.  The following call would crash:

./ltl2tgba -R3 -t '(!(F(({{{(p0) |
{[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) &
(G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))'

On amd64 the call does not crash, but valgrind nonetheless
report that uninitialized memory is being read by bdd_gbc()
during the second garbage collect.

* src/kernel.h (PUSHREF): Define as a function rather than a macro
to avoid undefined behavior.  See comments for details.
 2015-03-10 15:44:08 +01:00
Alexandre Duret-Lutz
e55bcd95aa hoa: preliminary implementation of a parser 
* src/hoaparse/Makefile.am, src/hoaparse/fmterror.cc,
src/hoaparse/hoaparse.yy, src/hoaparse/hoascan.ll,
src/hoaparse/parsedecl.hh, src/hoaparse/public.hh: New files.
* src/Makefile.am, configure.ac, README: Adjust.
* src/tgbatest/ltl2tgba.cc: Add a -XH option.
* src/tgbatest/hoaparse.test: New file.
* src/tgbatest/Makefile.am: Adjust.
* buddy/src/bddx.h: Add a bdd_from_int() function.
 2014-11-19 19:29:29 +01:00
Alexandre Duret-Lutz
ad8d24222a buddy: rename libbdd to libbddx 
* buddy/src/bdd.h, buddy/src/bvec.h, buddy/src/fdd.h: Rename as...
* buddy/src/bddx.h, buddy/src/bvecx.h, buddy/src/fddx.h: ... these.
* buddy/src/Makefile.am: Build libbddx.la instead of libbdd.la.
* buddy/examples/Makefile.def: Use it.
* Makefile.am, buddy/src/bddtest.cxx, buddy/src/bvec.c,
buddy/src/cppext.cxx, buddy/src/fdd.c, buddy/src/imatrix.h,
buddy/src/kernel.h, buddy/examples/adder/adder.cxx,
buddy/examples/bddcalc/parser_.h, buddy/examples/bddtest/bddtest.cxx,
buddy/examples/cmilner/cmilner.c, buddy/examples/fdd/fdd.cxx,
buddy/examples/milner/milner.cxx, buddy/examples/money/money.cxx,
buddy/examples/queen/queen.cxx, buddy/examples/solitare/solitare.cxx,
m4/buddy.m4, src/ltlvisit/apcollect.hh, src/ltlvisit/simplify.hh,
src/misc/bddlt.hh, src/misc/bddop.hh, src/misc/minato.hh,
src/priv/acccompl.hh, src/priv/accconv.hh, src/priv/accmap.hh,
src/priv/bddalloc.cc, src/tgba/bdddict.hh, src/tgba/bddprint.hh,
src/tgba/tgbamask.hh, src/tgba/tgbasafracomplement.cc,
src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.cc,
src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.hh,
src/tgbaalgos/weight.hh, wrap/python/buddy.i: Adjust.
* NEWS, README: Document it.
 2014-10-30 20:58:10 +01:00
Alexandre Duret-Lutz
971788fdbe [buddy] pack cache entry on 16 bytes, not 20. 
The double result is never used with a triple keys,
so we can pack the cache entry more tightly.

* src/cache.h: Reorganize the cache entry the structure.
* src/cache.c: Cleanup the code while we are at it.
* src/bddop.c: Adjust to accesses to cache entries.
 2014-10-28 13:13:05 +01:00