Searched refs:BVZEROEXTEND (Results 1 – 7 of 7) sorted by relevance
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/ |
H A D | bvsimple.cvc | 25 ( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND 28 ( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND
|
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/ |
H A D | cvc3.userdoc.01.cvc | 22 QUERY BVZEROEXTEND(0bin1,3) = 0bin0001;
|
/dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/ |
H A D | theory_bitvector.cpp | 1332 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 D | bitvector_theorem_producer.cpp | 6085 CHECK_SOUND(BVZEROEXTEND == e.getOpKind(), in zeroExtendRule()
|
/dports/math/cvc3/cvc3-2.4.1/src/include/ |
H A D | theory_bitvector.h | 50 BVZEROEXTEND, enumerator
|
/dports/math/cvc3/cvc3-2.4.1/doc/ |
H A D | userdoc.dox | 999 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 D | Cvc.g | 198 BVZEROEXTEND_TOK = 'BVZEROEXTEND'; 1993 // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits
|