Lines Matching refs:SMTExprRef
288 void addConstraint(const SMTExprRef &Exp) const override { in addConstraint()
301 SMTExprRef newExprRef(const SMTExpr &Exp) { in newExprRef()
315 SMTSortRef getSort(const SMTExprRef &Exp) override { in getSort()
336 SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { in mkBVNeg()
341 SMTExprRef mkBVNot(const SMTExprRef &Exp) override { in mkBVNot()
346 SMTExprRef mkNot(const SMTExprRef &Exp) override { in mkNot()
351 SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAdd()
357 SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSub()
363 SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVMul()
369 SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSRem()
375 SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVURem()
381 SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSDiv()
387 SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUDiv()
393 SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVShl()
399 SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAshr()
405 SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVLshr()
411 SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVXor()
417 SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVOr()
423 SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVAnd()
429 SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUlt()
435 SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSlt()
441 SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUgt()
447 SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSgt()
453 SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUle()
459 SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSle()
465 SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVUge()
471 SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVSge()
477 SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkAnd()
482 SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkOr()
487 SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkEqual()
493 SMTExprRef mkFPNeg(const SMTExprRef &Exp) override { in mkFPNeg()
498 SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override { in mkFPIsInfinite()
503 SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override { in mkFPIsNaN()
508 SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override { in mkFPIsNormal()
513 SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override { in mkFPIsZero()
518 SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPMul()
519 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkFPMul()
526 SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPDiv()
527 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkFPDiv()
534 SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPRem()
540 SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPAdd()
541 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkFPAdd()
548 SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPSub()
549 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkFPSub()
556 SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPLt()
562 SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPGt()
568 SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPLe()
574 SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPGe()
580 SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkFPEqual()
586 SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, in mkIte()
587 const SMTExprRef &F) override { in mkIte()
593 SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override { in mkBVSignExt()
598 SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override { in mkBVZeroExt()
603 SMTExprRef mkBVExtract(unsigned High, unsigned Low, in mkBVExtract()
604 const SMTExprRef &Exp) override { in mkBVExtract()
611 SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, in mkBVAddNoOverflow()
620 SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, in mkBVAddNoUnderflow()
621 const SMTExprRef &RHS) override { in mkBVAddNoUnderflow()
629 SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, in mkBVSubNoOverflow()
630 const SMTExprRef &RHS) override { in mkBVSubNoOverflow()
638 SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, in mkBVSubNoUnderflow()
647 SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, in mkBVSDivNoOverflow()
648 const SMTExprRef &RHS) override { in mkBVSDivNoOverflow()
656 SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override { in mkBVNegNoOverflow()
663 SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, in mkBVMulNoOverflow()
672 SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, in mkBVMulNoUnderflow()
673 const SMTExprRef &RHS) override { in mkBVMulNoUnderflow()
679 SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override { in mkBVConcat()
685 SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override { in mkFPtoFP()
686 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkFPtoFP()
693 SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override { in mkSBVtoFP()
694 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkSBVtoFP()
701 SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override { in mkUBVtoFP()
702 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkUBVtoFP()
709 SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override { in mkFPtoSBV()
710 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkFPtoSBV()
716 SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override { in mkFPtoUBV()
717 SMTExprRef RoundingMode = getFloatRoundingMode(); in mkFPtoUBV()
723 SMTExprRef mkBoolean(const bool b) override { in mkBoolean()
728 SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override { in mkBitvector()
750 SMTExprRef mkFloat(const llvm::APFloat Float) override { in mkFloat()
755 SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth()); in mkFloat()
761 SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override { in mkSymbol()
768 llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, in getBitvector()
777 bool getBoolean(const SMTExprRef &Exp) override { in getBoolean()
781 SMTExprRef getFloatRoundingMode() override { in getFloatRoundingMode()
786 bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST, in toAPFloat()
807 bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST, in toAPSInt()
845 bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override { in getInterpretation()
852 SMTExprRef Assign = newExprRef( in getInterpretation()
859 bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override { in getInterpretation()
866 SMTExprRef Assign = newExprRef( in getInterpretation()