Home
last modified time | relevance | path

Searched refs:BVZEROEXTEND (Results 1 – 7 of 7) sorted by relevance

/dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/
H A Dbvsimple.cvc25 ( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND
28 ( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/
H A Dcvc3.userdoc.01.cvc22 QUERY BVZEROEXTEND(0bin1,3) = 0bin0001;
/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/
H A Dtheory_bitvector.cpp1332 case BVZEROEXTEND: in rewriteBV()
1745 getEM()->newKind(BVZEROEXTEND,"_BVZEROEXTEND"); in TheoryBitvector()
1791 kinds.push_back(BVZEROEXTEND); in TheoryBitvector()
3108 case BVZEROEXTEND: { in computeType()
3149 case BVZEROEXTEND: in computeType()
3726 case BVZEROEXTEND: in print()
3953 case BVZEROEXTEND: { in print()
4040 case BVZEROEXTEND: { in print()
4299 case BVZEROEXTEND: in parseExprOp()
5379 e.getOpKind() == BVZEROEXTEND), in getBVIndex()
H A Dbitvector_theorem_producer.cpp6085 CHECK_SOUND(BVZEROEXTEND == e.getOpKind(), in zeroExtendRule()
/dports/math/cvc3/cvc3-2.4.1/src/include/
H A Dtheory_bitvector.h50 BVZEROEXTEND, enumerator
/dports/math/cvc3/cvc3-2.4.1/doc/
H A Duserdoc.dox999 Zero extension BVZEROEXTEND(_,k) BVZEROEXTEND(0bin1,3) (= 0bin0001)
1030 one mixfix zero extension operator \f$\mathrm{BVZEROEXTEND}(\_, k)\f$ for each \f$k >= 1\f$,
/dports/math/cvc4/CVC4-1.7/src/parser/cvc/
H A DCvc.g198 BVZEROEXTEND_TOK = 'BVZEROEXTEND';
1993 // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits