Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/bv/
H A Dtheory_bv_rewrite_rules.h144 ExtractMultLeadingBit, enumerator
298 case ExtractMultLeadingBit : out << "ExtractMultLeadingBit"; return out;
535 RewriteRule<ExtractMultLeadingBit> rule88;
H A Dtheory_bv_rewriter.cpp238 RewriteRule<ExtractMultLeadingBit> in RewriteExtract()
H A Dtheory_bv_rewrite_rules_simplification.h1280 bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) { in applies()
1316 Node RewriteRule<ExtractMultLeadingBit>::apply(TNode node) { in apply()