Home
last modified time | relevance | path

Searched refs:BvIteMergeElseElse (Results 1 – 3 of 3) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/bv/
H A Dtheory_bv_rewrite_rules.h114 BvIteMergeElseElse, enumerator
261 case BvIteMergeElseElse : out << "BvIteMergeElseElse"; return out;
583 RewriteRule<BvIteMergeElseElse> rule138;
H A Dtheory_bv_rewriter.cpp186 RewriteRule<BvIteMergeElseElse>>::apply(node); in RewriteITEBv()
H A Dtheory_bv_rewrite_rules_simplification.h230 inline bool RewriteRule<BvIteMergeElseElse>::applies(TNode node) in applies()
238 inline Node RewriteRule<BvIteMergeElseElse>::apply(TNode node) in apply()