| allocator_type typedef | lala::TFormula< Allocator, ExtendedSig > | |
| B | lala::TFormula< Allocator, ExtendedSig > | static |
| b() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| b() | lala::TFormula< Allocator, ExtendedSig > | inline |
| data() | lala::TFormula< Allocator, ExtendedSig > | inline |
| data() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| E | lala::TFormula< Allocator, ExtendedSig > | static |
| ESeq | lala::TFormula< Allocator, ExtendedSig > | static |
| eseq() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| eseq(size_t i) const | lala::TFormula< Allocator, ExtendedSig > | inline |
| eseq() | lala::TFormula< Allocator, ExtendedSig > | inline |
| eseq(size_t i) | lala::TFormula< Allocator, ExtendedSig > | inline |
| esig() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| esig() | lala::TFormula< Allocator, ExtendedSig > | inline |
| Existential typedef | lala::TFormula< Allocator, ExtendedSig > | |
| exists() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| Formula typedef | lala::TFormula< Allocator, ExtendedSig > | |
| index() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| inplace_map(Fun fun) | lala::TFormula< Allocator, ExtendedSig > | inline |
| is(size_t kind) const | lala::TFormula< Allocator, ExtendedSig > | inline |
| is_binary() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| is_constant() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| is_false() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| is_logical() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| is_true() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| is_unary() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| is_untyped() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| is_variable() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| LogicSet typedef | lala::TFormula< Allocator, ExtendedSig > | |
| LV | lala::TFormula< Allocator, ExtendedSig > | static |
| lv() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| make_avar(AVar v) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_avar(AType ty, int vid) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_binary(TFormula lhs, Sig sig, TFormula rhs, AType atype=UNTYPED, const Allocator &allocator=Allocator(), bool flatten=true) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_bool(logic_bool b, AType atype=UNTYPED) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_exists(AType ty, LVar< Allocator > lvar, Sort< Allocator > ctype) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_false() | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_lvar(AType ty, LVar< Allocator > lvar) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_nary(Sig sig, Sequence children, AType atype=UNTYPED, bool flatten=true) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_nary(ExtendedSig esig, Sequence children, AType atype=UNTYPED) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_real(double lb, double ub, AType atype=UNTYPED) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_real(logic_real r, AType atype=UNTYPED) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_set(LogicSet set, AType atype=UNTYPED) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_true() | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_unary(Sig sig, TFormula child, AType atype=UNTYPED, const Allocator &allocator=Allocator()) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| make_z(logic_int i, AType atype=UNTYPED) | lala::TFormula< Allocator, ExtendedSig > | inlinestatic |
| map(Fun fun) | lala::TFormula< Allocator, ExtendedSig > | inline |
| map_atype(AType aty) const | lala::TFormula< Allocator, ExtendedSig > | inline |
| map_sig(Sig sig) const | lala::TFormula< Allocator, ExtendedSig > | inline |
| operator=(const this_type &rhs) | lala::TFormula< Allocator, ExtendedSig > | inline |
| operator=(this_type &&rhs) | lala::TFormula< Allocator, ExtendedSig > | inline |
| print(bool print_atype=true) const | lala::TFormula< Allocator, ExtendedSig > | inline |
| R | lala::TFormula< Allocator, ExtendedSig > | static |
| r() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| r() | lala::TFormula< Allocator, ExtendedSig > | inline |
| S | lala::TFormula< Allocator, ExtendedSig > | static |
| s() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| s() | lala::TFormula< Allocator, ExtendedSig > | inline |
| Seq | lala::TFormula< Allocator, ExtendedSig > | static |
| seq() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| seq(size_t i) const | lala::TFormula< Allocator, ExtendedSig > | inline |
| seq() | lala::TFormula< Allocator, ExtendedSig > | inline |
| seq(size_t i) | lala::TFormula< Allocator, ExtendedSig > | inline |
| Sequence typedef | lala::TFormula< Allocator, ExtendedSig > | |
| sig() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| sig() | lala::TFormula< Allocator, ExtendedSig > | inline |
| sort() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| swap(this_type &other) | lala::TFormula< Allocator, ExtendedSig > | inline |
| TFormula class | lala::TFormula< Allocator, ExtendedSig > | friend |
| TFormula() | lala::TFormula< Allocator, ExtendedSig > | inline |
| TFormula(Formula &&formula) | lala::TFormula< Allocator, ExtendedSig > | inline |
| TFormula(AType uid, Formula &&formula) | lala::TFormula< Allocator, ExtendedSig > | inline |
| TFormula(const this_type &other) | lala::TFormula< Allocator, ExtendedSig > | inline |
| TFormula(this_type &&other) | lala::TFormula< Allocator, ExtendedSig > | inline |
| TFormula(const TFormula< Alloc2, ExtendedSig2 > &other, const Allocator &allocator=Allocator()) | lala::TFormula< Allocator, ExtendedSig > | inline |
| this_type typedef | lala::TFormula< Allocator, ExtendedSig > | |
| to_z() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| type() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| type_as(AType ty) | lala::TFormula< Allocator, ExtendedSig > | inline |
| V | lala::TFormula< Allocator, ExtendedSig > | static |
| v() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| v() | lala::TFormula< Allocator, ExtendedSig > | inline |
| Z | lala::TFormula< Allocator, ExtendedSig > | static |
| z() const | lala::TFormula< Allocator, ExtendedSig > | inline |
| z() | lala::TFormula< Allocator, ExtendedSig > | inline |
1.12.0