Lines Matching refs:LHS
248 static bool areEquivalent(const llvm::fltSemantics &LHS, in areEquivalent() argument
250 return (llvm::APFloat::semanticsPrecision(LHS) == in areEquivalent()
252 (llvm::APFloat::semanticsMinExponent(LHS) == in areEquivalent()
254 (llvm::APFloat::semanticsMaxExponent(LHS) == in areEquivalent()
256 (llvm::APFloat::semanticsSizeInBits(LHS) == in areEquivalent()
351 SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAdd() argument
353 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, in mkBVAdd()
357 SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSub() argument
359 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, in mkBVSub()
363 SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVMul() argument
365 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST, in mkBVMul()
369 SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSRem() argument
371 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST, in mkBVSRem()
375 SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVURem() argument
377 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST, in mkBVURem()
381 SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSDiv() argument
383 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST, in mkBVSDiv()
387 SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUDiv() argument
389 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST, in mkBVUDiv()
393 SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVShl() argument
395 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST, in mkBVShl()
399 SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAshr() argument
401 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST, in mkBVAshr()
405 SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVLshr() argument
407 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST, in mkBVLshr()
411 SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVXor() argument
413 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST, in mkBVXor()
417 SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVOr() argument
419 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST, in mkBVOr()
423 SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAnd() argument
425 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST, in mkBVAnd()
429 SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUlt() argument
431 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST, in mkBVUlt()
435 SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSlt() argument
437 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST, in mkBVSlt()
441 SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUgt() argument
443 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST, in mkBVUgt()
447 SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSgt() argument
449 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST, in mkBVSgt()
453 SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUle() argument
455 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST, in mkBVUle()
459 SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSle() argument
461 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST, in mkBVSle()
465 SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUge() argument
467 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST, in mkBVUge()
471 SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSge() argument
473 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST, in mkBVSge()
477 SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkAnd() argument
478 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; in mkAnd()
482 SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkOr() argument
483 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST}; in mkOr()
487 SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkEqual() argument
489 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST, in mkEqual()
518 SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPMul() argument
523 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPMul()
526 SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPDiv() argument
531 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPDiv()
534 SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPRem() argument
536 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST, in mkFPRem()
540 SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPAdd() argument
545 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPAdd()
548 SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPSub() argument
553 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST))); in mkFPSub()
556 SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPLt() argument
558 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST, in mkFPLt()
562 SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPGt() argument
564 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST, in mkFPGt()
568 SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPLe() argument
570 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST, in mkFPLe()
574 SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPGe() argument
576 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST, in mkFPGe()
580 SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPEqual() argument
582 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST, in mkFPEqual()
611 SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, in mkBVAddNoOverflow() argument
614 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVAddNoOverflow()
620 SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, in mkBVAddNoUnderflow() argument
623 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVAddNoUnderflow()
629 SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, in mkBVSubNoOverflow() argument
632 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSubNoOverflow()
638 SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, in mkBVSubNoUnderflow() argument
641 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSubNoUnderflow()
647 SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, in mkBVSDivNoOverflow() argument
650 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSDivNoOverflow()
663 SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, in mkBVMulNoOverflow() argument
666 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVMulNoOverflow()
672 SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, in mkBVMulNoUnderflow() argument
675 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVMulNoUnderflow()
679 SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVConcat() argument
681 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST, in mkBVConcat()