Lines Matching refs:Solver

525   std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && {  in solve()
529       return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations);  in solve()
534         return std::make_pair(Solver::Result::TimedOut(), 0);  in solve()
563           return std::make_pair(Solver::Result::Unsatisfiable(), MaxIterations);  in solve()
620     return std::make_pair(Solver::Result::Satisfiable(buildSolution()),  in solve()
626   llvm::DenseMap<Atom, Solver::Result::Assignment> buildSolution() {  in buildSolution()
627     llvm::DenseMap<Atom, Solver::Result::Assignment> Solution;  in buildSolution()
634               ? Solver::Result::Assignment::AssignedFalse  in buildSolution()
635               : Solver::Result::Assignment::AssignedTrue;  in buildSolution()
786 Solver::Result
789     return Solver::Result::Satisfiable({{}});  in solve()