Lines Matching defs:RHS

254                           const llvm::fltSemantics &RHS) {
256           llvm::APFloat::semanticsPrecision(RHS)) &&
258           llvm::APFloat::semanticsMinExponent(RHS)) &&
260           llvm::APFloat::semanticsMaxExponent(RHS)) &&
262           llvm::APFloat::semanticsSizeInBits(RHS));
363   SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
366                                     toZ3Expr(*RHS).AST)));
369   SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
372                                     toZ3Expr(*RHS).AST)));
375   SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
378                                     toZ3Expr(*RHS).AST)));
381   SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
384                                      toZ3Expr(*RHS).AST)));
387   SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
390                                      toZ3Expr(*RHS).AST)));
393   SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
396                                      toZ3Expr(*RHS).AST)));
399   SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
402                                      toZ3Expr(*RHS).AST)));
405   SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
408                                     toZ3Expr(*RHS).AST)));
411   SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
414                                      toZ3Expr(*RHS).AST)));
417   SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
420                                      toZ3Expr(*RHS).AST)));
423   SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
426                                     toZ3Expr(*RHS).AST)));
429   SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
432                                    toZ3Expr(*RHS).AST)));
435   SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
438                                     toZ3Expr(*RHS).AST)));
441   SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
444                                     toZ3Expr(*RHS).AST)));
447   SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
450                                     toZ3Expr(*RHS).AST)));
453   SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
456                                     toZ3Expr(*RHS).AST)));
459   SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
462                                     toZ3Expr(*RHS).AST)));
465   SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
468                                     toZ3Expr(*RHS).AST)));
471   SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
474                                     toZ3Expr(*RHS).AST)));
477   SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
480                                     toZ3Expr(*RHS).AST)));
483   SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
486                                     toZ3Expr(*RHS).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 {
502                                  toZ3Expr(*RHS).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 {
549                                       toZ3Expr(*RHS).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 {
571                                      toZ3Expr(*RHS).AST)));
574   SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
577                                      toZ3Expr(*RHS).AST)));
580   SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
583                                       toZ3Expr(*RHS).AST)));
586   SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
589                                       toZ3Expr(*RHS).AST)));
592   SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
595                                      toZ3Expr(*RHS).AST)));
623   SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
627                                          toZ3Expr(*RHS).AST, isSigned)));
633                                 const SMTExprRef &RHS) override {
636                                           toZ3Expr(*RHS).AST)));
642                                const SMTExprRef &RHS) override {
645                                          toZ3Expr(*RHS).AST)));
650   SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
654                                           toZ3Expr(*RHS).AST, isSigned)));
660                                 const SMTExprRef &RHS) override {
663                                           toZ3Expr(*RHS).AST)));
675   SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
679                                          toZ3Expr(*RHS).AST, isSigned)));
685                                 const SMTExprRef &RHS) override {
688                                           toZ3Expr(*RHS).AST)));
691   SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
694                                      toZ3Expr(*RHS).AST)));