Z3Solver.cpp - OpenGrok cross reference for /llvm-project/llvm/lib/Support/Z3Solver.cpp

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,