Searched refs:bvOne (Results 1 – 8 of 8) sorted by relevance
| /dports/security/klee/klee-2.2/lib/Solver/ |
| H A D | STPBuilder.h | 78 ExprHandle bvOne(unsigned width);
|
| H A D | Z3Builder.h | 109 Z3ASTHandle bvOne(unsigned width);
|
| H A D | STPBuilder.cpp | 119 ExprHandle STPBuilder::bvOne(unsigned width) { in bvOne() function in STPBuilder
150 return vc_eqExpr(vc, bvExtract(expr, bit, bit), bvOne(1)); in bvBoolExtract()
601 return vc_iteExpr(vc, src, bvOne(*width_out), bvZero(*width_out)); in constructActual()
|
| H A D | Z3Builder.cpp | 137 Z3ASTHandle Z3Builder::bvOne(unsigned width) { return bvZExtConst(width, 1); } in bvOne() function in klee::Z3Builder
181 return Z3ASTHandle(Z3_mk_eq(ctx, bvExtract(expr, bit, bit), bvOne(1)), ctx); in bvBoolExtract()
564 return iteExpr(src, bvOne(*width_out), bvZero(*width_out)); in constructActual()
|
| H A D | MetaSMTBuilder.h | 81 typename SolverContext::result_type bvOne(unsigned width) { in bvOne() function
283 metaSMT::logic::equal(extract(bit, bit, expr), bvOne(1)))); in bvBoolExtract()
736 res = evaluate(_solver, metaSMT::logic::Ite(child, bvOne(ce_width), in constructActual()
|
| /dports/math/cvc3/cvc3-2.4.1/src/include/ |
| H A D | theory_bitvector.h | 162 const Expr& bvOne() const { return d_bvOne; } in bvOne() function
|
| /dports/math/cvc3/cvc3-2.4.1/src/theory_bitvector/ |
| H A D | bitvector_theorem_producer.h | 52 const Expr& bvOne() const { return d_bvOne; } in bvOne() function
|
| H A D | bitvector_theorem_producer.cpp | 496 const Expr MSB0isOne = MSB0.eqExpr(bvOne()); in signBVLTRule()
498 const Expr MSB1isOne = MSB1.eqExpr(bvOne()); in signBVLTRule()
943 return newRWTheorem(lhs, negative? bvZero() : bvOne(), thm.getAssumptionsRef(), pf); in bitExtractToExtract()
4288 return newTheorem(e.eqExpr(bvZero()) || e.eqExpr(bvOne()), Assumptions::emptyAssump(), pf); in typePredBit()
4316 kids.push_back(bit.eqExpr(bvZero()) || bit.eqExpr(bvOne())); in expandTypePred()
4320 res = (e.eqExpr(bvZero()) || e.eqExpr(bvOne())); in expandTypePred()
|