spot::ltlf_one_step_unsat_rewrite_with_cache Class Reference

Cached version of the one-step unsatisfiability rewriting for LTLf formulas. More...

#include <spot/tl/ltlf.hh>

Collaboration diagram for spot::ltlf_one_step_unsat_rewrite_with_cache:

Public Member Functions
	ltlf_one_step_unsat_rewrite_with_cache ()
	Build the cache.
	~ltlf_one_step_unsat_rewrite_with_cache ()
	Destroy the cache.
formula	rewrite (formula f)
	Rewrite an LTLf formula.

Detailed Description

Cached version of the one-step unsatisfiability rewriting for LTLf formulas.

Constructor & Destructor Documentation

ltlf_one_step_unsat_rewrite_with_cache()

spot::ltlf_one_step_unsat_rewrite_with_cache::ltlf_one_step_unsat_rewrite_with_cache

(

)

Build the cache.

~ltlf_one_step_unsat_rewrite_with_cache()

spot::ltlf_one_step_unsat_rewrite_with_cache::~ltlf_one_step_unsat_rewrite_with_cache

(

)

Destroy the cache.

Member Function Documentation

rewrite()

formula spot::ltlf_one_step_unsat_rewrite_with_cache::rewrite

(

formula

f

)

Rewrite an LTLf formula.

---

The documentation for this class was generated from the following file:

• spot/tl/ltlf.hh