reference, declaration → definition definition → references, declarations, derived classes, virtual overrides reference to multiple definitions → definitions unreferenced |
49 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); 56 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption)); 58 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); 67 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange)); 85 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); 87 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); 91 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); 124 SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty)); 126 Solver->reset(); 130 Optional<bool> isSat = Solver->check(); 135 if (!Solver->getInterpretation(Exp, Value)) 140 Solver, Exp, BO_NE, 141 Ty->isBooleanType() ? Solver->mkBoolean(Value.getBoolValue()) 142 : Solver->mkBitvector(Value, Value.getBitWidth()), 145 Solver->addConstraint(NotExp); 147 Optional<bool> isNotSat = Solver->check(); 192 Solver, Ctx, ConvertedLHS, LTy, ConvertedRHS, RTy); 266 return Solver->isFPSupported(); 292 LLVM_DUMP_METHOD void dump() const { Solver->dump(); } 318 Constraint = Solver->mkAnd(Constraint, I++->second); 321 Solver->addConstraint(Constraint); 339 Solver->reset(); 342 Optional<bool> res = Solver->check();