Skip to content

Commit

Permalink
Merge branch 'develop' into qrisp-sat-solver
Browse files Browse the repository at this point in the history
  • Loading branch information
tubadzin committed Jan 13, 2025
2 parents 1c14cbe + 815c167 commit bd3e549
Show file tree
Hide file tree
Showing 31 changed files with 481 additions and 72 deletions.
1 change: 1 addition & 0 deletions Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,7 @@ ENV PATH="${PATH}:/opt/java/bin"

# Install the toolbox server and its solver scripts
COPY solvers solvers
COPY demonstrators demonstrators
RUN scripts/ci-setup-solvers.sh
COPY --from=builder /app/build/libs/toolbox-server-*.jar toolbox-server.jar

Expand Down
2 changes: 1 addition & 1 deletion build.gradle
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ plugins {
}

group = 'edu.kit.provideq'
version = '0.3.0'
version = '0.4.0'
sourceCompatibility = '17'

repositories {
Expand Down
10 changes: 10 additions & 0 deletions src/main/java/edu/kit/provideq/toolbox/Bound.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
package edu.kit.provideq.toolbox;

/**
* Represents a bound value with its type.
*
* @param value the estimated value
* @param boundType the type of the bound
*/
public record Bound(float value, BoundType boundType) {
}
15 changes: 15 additions & 0 deletions src/main/java/edu/kit/provideq/toolbox/BoundType.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
package edu.kit.provideq.toolbox;

/**
* Represents the bound type of bounds.
*/
public enum BoundType {
/**
* An upper bound.
*/
UPPER,
/**
* A lower bound.
*/
LOWER
}
10 changes: 10 additions & 0 deletions src/main/java/edu/kit/provideq/toolbox/BoundWithInfo.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
package edu.kit.provideq.toolbox;

/**
* Represents a bound estimation for the solution of a problem.
*
* @param bound the value
* @param executionTime the time it took to estimate the value
*/
public record BoundWithInfo(Bound bound, long executionTime) {
}
13 changes: 13 additions & 0 deletions src/main/java/edu/kit/provideq/toolbox/api/BoundDto.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
package edu.kit.provideq.toolbox.api;

import edu.kit.provideq.toolbox.BoundType;
import edu.kit.provideq.toolbox.BoundWithInfo;

public record BoundDto(float bound, BoundType boundType, long executionTime) {
public BoundDto(BoundWithInfo boundWithInfo) {
this(
boundWithInfo.bound().value(),
boundWithInfo.bound().boundType(),
boundWithInfo.executionTime());
}
}
114 changes: 114 additions & 0 deletions src/main/java/edu/kit/provideq/toolbox/api/EstimationRouter.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
package edu.kit.provideq.toolbox.api;

import static org.springdoc.core.fn.builders.apiresponse.Builder.responseBuilder;
import static org.springdoc.core.fn.builders.content.Builder.contentBuilder;
import static org.springdoc.core.fn.builders.parameter.Builder.parameterBuilder;
import static org.springdoc.core.fn.builders.schema.Builder.schemaBuilder;
import static org.springdoc.webflux.core.fn.SpringdocRouteBuilder.route;
import static org.springframework.http.MediaType.APPLICATION_JSON;
import static org.springframework.http.MediaType.APPLICATION_JSON_VALUE;
import static org.springframework.web.reactive.function.server.RequestPredicates.accept;
import static org.springframework.web.reactive.function.server.ServerResponse.ok;

import edu.kit.provideq.toolbox.meta.Problem;
import edu.kit.provideq.toolbox.meta.ProblemManager;
import edu.kit.provideq.toolbox.meta.ProblemManagerProvider;
import edu.kit.provideq.toolbox.meta.ProblemType;
import io.swagger.v3.oas.annotations.enums.ParameterIn;
import java.util.NoSuchElementException;
import java.util.UUID;
import org.springdoc.core.fn.builders.operation.Builder;
import org.springframework.beans.factory.annotation.Autowired;
import org.springframework.context.annotation.Bean;
import org.springframework.context.annotation.Configuration;
import org.springframework.core.ParameterizedTypeReference;
import org.springframework.http.HttpStatus;
import org.springframework.web.reactive.config.EnableWebFlux;
import org.springframework.web.reactive.function.server.RouterFunction;
import org.springframework.web.reactive.function.server.ServerRequest;
import org.springframework.web.reactive.function.server.ServerResponse;
import org.springframework.web.server.ResponseStatusException;
import reactor.core.publisher.Mono;

/**
* This router handles requests regarding {@link Problem} instance solution bound estimations.
* The /bound endpoint is only available for problem types that have an estimator.
*/
@Configuration
@EnableWebFlux
public class EstimationRouter {
public static final String PROBLEM_ID_PARAM_NAME = "problemId";
private ProblemManagerProvider managerProvider;

@Bean
RouterFunction<ServerResponse> getEstimationRoutes() {
return managerProvider.getProblemManagers().stream()
.filter(manager -> manager.getType().getEstimator().isPresent())
.map(this::defineGetRoute)
.reduce(RouterFunction::and)
.orElse(null);
}

/**
* Estimate Operation: GET /problems/TYPE/{problemId}/bound.
*/
private RouterFunction<ServerResponse> defineGetRoute(ProblemManager<?, ?> manager) {
return route().GET(
getEstimationRouteForProblemType(manager.getType()),
accept(APPLICATION_JSON),
req -> handleGet(manager, req),
ops -> handleGetDocumentation(manager, ops)
).build();
}

private <InputT, ResultT> Mono<ServerResponse> handleGet(
ProblemManager<InputT, ResultT> manager,
ServerRequest req
) {
var problemId = req.pathVariable(PROBLEM_ID_PARAM_NAME);
var problem = RouterUtility.findProblemOrThrow(manager, problemId);

Mono<BoundDto> bound;
try {
problem.estimateBound();
bound = Mono.just(new BoundDto(problem.getBound().orElseThrow()));
} catch (IllegalStateException | NoSuchElementException e) {
throw new ResponseStatusException(HttpStatus.BAD_REQUEST, e.getMessage());
}

return ok().body(bound, new ParameterizedTypeReference<>() {
});
}

private void handleGetDocumentation(
ProblemManager<?, ?> manager,
Builder ops
) {
ProblemType<?, ?> problemType = manager.getType();
ops
.operationId(getEstimationRouteForProblemType(problemType))
.tag(problemType.getId())
.description("Estimates the solution bound for the problem with the given ID.")
.parameter(parameterBuilder().in(ParameterIn.PATH).name(PROBLEM_ID_PARAM_NAME))
.response(responseBuilder()
.responseCode(String.valueOf(HttpStatus.OK.value()))
.content(getOkResponseContent())
);
}

private static org.springdoc.core.fn.builders.content.Builder getOkResponseContent() {
return contentBuilder()
.mediaType(APPLICATION_JSON_VALUE)
.schema(schemaBuilder().implementation(BoundDto.class));
}

private String getEstimationRouteForProblemType(ProblemType<?, ?> type) {
return "/problems/%s/{%s}/bound".formatted(type.getId(), PROBLEM_ID_PARAM_NAME);
}

@Autowired
void setManagerProvider(ProblemManagerProvider managerProvider) {
this.managerProvider = managerProvider;
}

}
8 changes: 8 additions & 0 deletions src/main/java/edu/kit/provideq/toolbox/api/ProblemDto.java
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package edu.kit.provideq.toolbox.api;

import edu.kit.provideq.toolbox.BoundWithInfo;
import edu.kit.provideq.toolbox.Solution;
import edu.kit.provideq.toolbox.meta.Problem;
import edu.kit.provideq.toolbox.meta.ProblemSolver;
Expand All @@ -16,6 +17,7 @@ public class ProblemDto<InputT, ResultT> {
private String typeId;
private InputT input;
private Solution<ResultT> solution;
private BoundWithInfo bound;
private ProblemState state;
private String solverId;
private List<SolverSetting> solverSettings;
Expand All @@ -38,6 +40,7 @@ public static <InputT, ResultT> ProblemDto<InputT, ResultT> fromProblem(
dto.typeId = problem.getType().getId();
dto.input = problem.getInput().orElse(null);
dto.solution = problem.getSolution();
dto.bound = problem.getBound().orElse(null);
dto.state = problem.getState();
dto.solverId = problem.getSolver()
.map(ProblemSolver::getId)
Expand Down Expand Up @@ -67,6 +70,10 @@ public Solution<ResultT> getSolution() {
return solution;
}

public BoundWithInfo getBound() {
return bound;
}

public ProblemState getState() {
return state;
}
Expand Down Expand Up @@ -100,6 +107,7 @@ public String toString() {
+ ", solverId=" + solverId
+ ", input=" + input
+ ", solution=" + solution
+ ", value=" + bound
+ ", solverSettings=" + solverSettings
+ ", subProblems=" + subProblems
+ '}';
Expand Down
118 changes: 118 additions & 0 deletions src/main/java/edu/kit/provideq/toolbox/api/ProblemExampleRouter.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,118 @@
package edu.kit.provideq.toolbox.api;

import static org.springdoc.core.fn.builders.apiresponse.Builder.responseBuilder;
import static org.springdoc.core.fn.builders.arrayschema.Builder.arraySchemaBuilder;
import static org.springdoc.core.fn.builders.content.Builder.contentBuilder;
import static org.springdoc.core.fn.builders.exampleobject.Builder.exampleOjectBuilder;
import static org.springdoc.core.fn.builders.schema.Builder.schemaBuilder;
import static org.springdoc.webflux.core.fn.SpringdocRouteBuilder.route;
import static org.springframework.http.MediaType.APPLICATION_JSON;
import static org.springframework.web.reactive.function.server.RequestPredicates.accept;
import static org.springframework.web.reactive.function.server.ServerResponse.ok;

import com.fasterxml.jackson.core.JsonProcessingException;
import com.fasterxml.jackson.databind.ObjectMapper;
import edu.kit.provideq.toolbox.exception.MissingExampleException;
import edu.kit.provideq.toolbox.meta.Problem;
import edu.kit.provideq.toolbox.meta.ProblemManager;
import edu.kit.provideq.toolbox.meta.ProblemManagerProvider;
import edu.kit.provideq.toolbox.meta.ProblemType;
import java.util.List;
import java.util.Optional;
import org.springdoc.core.fn.builders.operation.Builder;
import org.springframework.beans.factory.annotation.Autowired;
import org.springframework.context.annotation.Bean;
import org.springframework.context.annotation.Configuration;
import org.springframework.core.ParameterizedTypeReference;
import org.springframework.http.HttpStatus;
import org.springframework.web.reactive.config.EnableWebFlux;
import org.springframework.web.reactive.function.server.RouterFunction;
import org.springframework.web.reactive.function.server.ServerResponse;
import reactor.core.publisher.Mono;

/**
* This router provides example problems for each problem type.
*/
@Configuration
@EnableWebFlux
public class ProblemExampleRouter {
private ProblemManagerProvider managerProvider;

@Bean
RouterFunction<ServerResponse> getProblemExampleRoutes() {
var managers = this.managerProvider.getProblemManagers();
return managers.stream().map(this::defineReadRoute)
.reduce(RouterFunction::and)
.orElseThrow();
}

/**
* GET /problems/TYPE/example.
*/
private RouterFunction<ServerResponse> defineReadRoute(ProblemManager<?, ?> manager) {
return route().GET(
getPath(manager.getType()),
accept(APPLICATION_JSON),
req -> handleRead(manager),
ops -> configureReadDocs(manager, ops)
).build();
}

private <InputT, ResultT> Mono<ServerResponse> handleRead(
ProblemManager<InputT, ResultT> manager
) {
var exampleProblems = getExampleInput(manager);

return ok().body(Mono.just(exampleProblems), new ParameterizedTypeReference<>() {
});
}

private static <InputT, ResultT> List<InputT> getExampleInput(
ProblemManager<InputT, ResultT> manager
) {
return manager.getExampleInstances()
.stream()
.map(Problem::getInput)
.filter(Optional::isPresent)
.map(Optional::get)
.toList();
}

private static void configureReadDocs(ProblemManager<?, ?> manager, Builder ops) {
var type = manager.getType();

String requestString;
try {
requestString = new ObjectMapper().writeValueAsString(getExampleInput(manager));
} catch (JsonProcessingException exception) {
throw new MissingExampleException(manager.getType(), exception);
}

ops
.operationId(getPath(manager.getType()))
.description("This endpoint can be used to view example problems for '"
+ type.getId() + "'.")
.tag(type.getId())
.response(responseBuilder()
.responseCode(String.valueOf(HttpStatus.OK.value()))
.content(contentBuilder()
.array(arraySchemaBuilder()
.schema(schemaBuilder().implementation(String.class))
)
.example(exampleOjectBuilder()
.value(requestString)
)
)
.content(contentBuilder()));
}

private static String getPath(ProblemType<?, ?> type) {
return "/problems/%s/examples".formatted(type.getId());
}

@Autowired
void setManagerProvider(ProblemManagerProvider managerProvider) {
this.managerProvider = managerProvider;
}

}
Loading

0 comments on commit bd3e549

Please sign in to comment.