Lines Matching defs:LHS

253 static bool areEquivalent(const llvm::fltSemantics &LHS,
255 return (llvm::APFloat::semanticsPrecision(LHS) ==
257 (llvm::APFloat::semanticsMinExponent(LHS) ==
259 (llvm::APFloat::semanticsMaxExponent(LHS) ==
261 (llvm::APFloat::semanticsSizeInBits(LHS) ==
363 SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
365 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
369 SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
371 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
375 SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
377 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
381 SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
383 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
387 SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
389 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
393 SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
395 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
399 SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
401 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
405 SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
407 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
411 SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
413 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
417 SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
419 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
423 SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
425 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
429 SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
431 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
435 SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
437 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
441 SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
443 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
447 SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
449 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
453 SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
455 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
459 SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
461 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
465 SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
467 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
471 SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
473 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
477 SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
479 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
483 SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
485 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
489 SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
490 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
494 SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
495 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
499 SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
501 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
530 SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
535 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
538 SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
543 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
546 SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
548 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
552 SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
557 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
560 SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
565 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
568 SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
570 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
574 SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
576 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
580 SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
582 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
586 SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
588 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
592 SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
594 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
623 SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
626 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
632 SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS,
635 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
641 SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS,
644 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
650 SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
653 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
659 SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS,
662 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
675 SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
678 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
684 SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS,
687 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
691 SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
693 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,