algorithm.hpp File Reference

#include "ast.hpp"
#include <map>

Go to the source code of this file.

Namespaces
namespace	lala

Functions
template<class Allocator , class ExtendedSig >
CUDA NI bool	lala::is_v_op_constant (const TFormula< Allocator, ExtendedSig > &f, Sig sig)
template<class Allocator , class ExtendedSig >
CUDA NI bool	lala::is_v_op_z (const TFormula< Allocator, ExtendedSig > &f, Sig sig)
template<class Allocator , class ExtendedSig >
CUDA NI bool	lala::is_var_equality (const TFormula< Allocator, ExtendedSig > &f)
template<class Allocator >
CUDA NI TFormula< Allocator >	lala::make_v_op_z (LVar< Allocator > v, Sig sig, logic_int z, AType aty=UNTYPED, const Allocator &allocator=Allocator())
template<class Allocator >
CUDA NI TFormula< Allocator >	lala::make_v_op_z (AVar v, Sig sig, logic_int z, AType aty=UNTYPED, const Allocator &allocator=Allocator())
template<class Allocator >
CUDA Sig	lala::geq_of_constant (const TFormula< Allocator > &f)
template<class Allocator >
CUDA Sig	lala::leq_of_constant (const TFormula< Allocator > &f)
template<typename Allocator , typename ExtendedSig >
CUDA const TFormula< Allocator, ExtendedSig > &	lala::var_in (const TFormula< Allocator, ExtendedSig > &f)
template<class F >
CUDA NI int	lala::num_vars (const F &f)
template<class F >
CUDA size_t	lala::num_quantified_vars (const F &f)
template<class F >
CUDA size_t	lala::num_quantified_vars (const F &f, AType aty)
template<class F >
CUDA size_t	lala::num_constraints (const F &f)
template<class F >
CUDA size_t	lala::num_tnf_constraints (const F &f)
template<class F >
CUDA NI AType	lala::type_of_conjunction (const typename F::Sequence &seq)
template<class F >
CUDA NI battery::tuple< F, F >	lala::extract_ty (const F &f, AType ty)
template<class F >
CUDA NI std::optional< F >	lala::negate (const F &f)
template<class F >
CUDA NI std::optional< F >	lala::de_morgan_law (Sig sig_neg, const F &f)
template<class F >
CUDA NI std::optional< F >	lala::negate_eq (const F &f)
CUDA Sig	lala::negate_arithmetic_comparison (Sig sig)
template<class F >
CUDA NI bool	lala::is_arithmetic_comparison (const F &f)
template<class F >
CUDA NI bool	lala::is_set_comparison (const F &f)
template<class F >
CUDA NI bool	lala::is_comparison (const F &f)
CUDA NI Sig	lala::converse_comparison (Sig sig)
template<class F , class Env >
CUDA NI void	lala::map_avar_to_lvar (F &f, const Env &env, bool erase_type=false)
template<class F >
CUDA NI F	lala::eval (const F &f)
template<class F , class Alloc = battery::standard_allocator>
CUDA NI F	lala::normalize (const F &f, battery::vector< F, Alloc > &extra)
template<class F >
CUDA NI F	lala::normalize (const F &f)
template<class F >
CUDA F	lala::decompose_in_constraint (const F &f, const typename F::allocator_type &alloc=typename F::allocator_type())
template<class F >
CUDA F	lala::decompose_arith_neq_constraint (const F &f, const typename F::allocator_type &alloc=typename F::allocator_type())
template<class F >
std::optional< F >	lala::decompose_set_constraints (const F &f, std::map< std::string, std::vector< std::string > > &set2bool_vars)
template<class F >
std::optional< LVar< typename F::allocator_type > >	lala::find_maximize_var (const F &f)
template<class F >
std::optional< typename F::Existential >	lala::find_existential_of (const F &f, const LVar< typename F::allocator_type > &var)