Home
last modified time | relevance | path

Searched refs:concatFlatten (Results 1 – 4 of 4) sorted by relevance

/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dbitvector_proof_rules.h410 virtual Theorem concatFlatten(const Expr& e) = 0;
H A Dbitvector_theorem_producer.h458 Theorem concatFlatten(const Expr& e);
H A Dtheory_bitvector.cpp977 res = d_rules->concatFlatten(e); in rewriteBV()
1047 Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee)); in rewriteBV()
1131 Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee)); in rewriteBV()
H A Dbitvector_theorem_producer.cpp3217 BitvectorTheoremProducer::concatFlatten(const Expr& e) { in concatFlatten() function in BitvectorTheoremProducer