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

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

In project "undefined"

On Google
