expansions: draft
This commit is contained in:
parent
0fdd3c31f4
commit
b9f461c025
6 changed files with 495 additions and 0 deletions
25
tests/core/expand.cc
Normal file
25
tests/core/expand.cc
Normal file
|
|
@ -0,0 +1,25 @@
|
|||
#include "config.h"
|
||||
|
||||
#include <spot/tl/expansions.hh>
|
||||
#include <spot/tl/parse.hh>
|
||||
#include <spot/twa/formula2bdd.hh>
|
||||
#include <iostream>
|
||||
|
||||
int main(int argc, char** argv)
|
||||
{
|
||||
if (argc != 2)
|
||||
return 1;
|
||||
|
||||
spot::formula f = spot::parse_infix_sere(argv[1]).f;
|
||||
auto d = spot::make_bdd_dict();
|
||||
|
||||
auto m = spot::expansion(f, d, nullptr);
|
||||
|
||||
for (const auto& [bdd_l, form] : m)
|
||||
std::cout << '[' << bdd_to_formula(bdd_l, d) << ']' << ": " << form << std::endl;
|
||||
std::cout << "formula: " << expansion_to_formula(m, d) << std::endl;
|
||||
|
||||
d->unregister_all_my_variables(nullptr);
|
||||
|
||||
return 0;
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue