Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On Monday 05 April 2010, Mohsen Vakilian wrote:
> http://stackoverflow.com/questions/2579516/how-should-i-go-about-implementi
> ng-a-points-to-analysis-in-maude
> 

Maude uses BDDs for a couple of things at the moment: Order sorted 
unification 
and the propositional part of Buchi automata computation. In the slides you 
reference you will see that propositional satisfiability is polynomial time 
reducible to order sorted unification in the free theory (the NP-hardness 
proof). Also propositional satifiability is a special case of LTL 
satisfiability 
which is available in model-checker.maude

However accessing the BDD package by either of these routes is unlikely to be 
very efficient though the LTL sat solver is the more promising route. In 
principle a functional interface to the BDD package could be created via 
Maude 
builtin operators but that is a nontrivial amount of work and is not 
something 
I'm likely to implement in the near future.

Steven