From b2211bc43314869830de563f69c956c9bac2f9ff Mon Sep 17 00:00:00 2001 From: Steluro <282664784+Steluro@users.noreply.github.com> Date: Fri, 24 Jul 2026 14:09:45 -0400 Subject: [PATCH 1/4] ci: lighten and clean docker image --- .dockerignore | 157 ++++++++++++++++++++++++++++++++++++++++++++++++-- Dockerfile | 43 +++++++++----- 2 files changed, 181 insertions(+), 19 deletions(-) diff --git a/.dockerignore b/.dockerignore index 80aa51b..4531308 100644 --- a/.dockerignore +++ b/.dockerignore @@ -1,7 +1,152 @@ -*.org -*.tex -*.pdf -json/ -sam/ +# ----------------------------------------------------------------------------- +# Python +# ----------------------------------------------------------------------------- __pycache__/ -_minted-main/ +*.py[cod] +*$py.class +*.pyo +*.pyd + +# C extensions +*.so + +# ----------------------------------------------------------------------------- +# Virtual environments +# ----------------------------------------------------------------------------- +.venv/ +venv/ +env/ +ENV/ + +# ----------------------------------------------------------------------------- +# Build / packaging +# ----------------------------------------------------------------------------- +build/ +dist/ +downloads/ +develop-eggs/ +eggs/ +.eggs/ +lib/ +lib64/ +parts/ +sdist/ +var/ +wheels/ +share/python-wheels/ +*.egg-info/ +*.egg +pip-wheel-metadata/ + +# ----------------------------------------------------------------------------- +# Installer logs +# ----------------------------------------------------------------------------- +pip-log.txt +pip-delete-this-directory.txt + +# ----------------------------------------------------------------------------- +# Testing / coverage +# ----------------------------------------------------------------------------- +.tox/ +.nox/ +.pytest_cache/ +.coverage +.coverage.* +.cache/ +coverage.xml +*.cover +*.py,cover +htmlcov/ + +# ----------------------------------------------------------------------------- +# Type checkers +# ----------------------------------------------------------------------------- +.mypy_cache/ +.pyre/ +.pytype/ +.dmypy.json + +# ----------------------------------------------------------------------------- +# Linting +# ----------------------------------------------------------------------------- +.ruff_cache/ +.pylint.d/ + +# ----------------------------------------------------------------------------- +# Jupyter +# ----------------------------------------------------------------------------- +.ipynb_checkpoints/ + +# ----------------------------------------------------------------------------- +# IDEs +# ----------------------------------------------------------------------------- +.vscode/ +.idea/ +*.iml + +# ----------------------------------------------------------------------------- +# Operating systems +# ----------------------------------------------------------------------------- +.DS_Store +Thumbs.db +desktop.ini + +# ----------------------------------------------------------------------------- +# Git +# ----------------------------------------------------------------------------- +.git/ +.gitignore +.gitattributes + +# ----------------------------------------------------------------------------- +# Environment files +# ----------------------------------------------------------------------------- +.env +.env.* +*.env + +# ----------------------------------------------------------------------------- +# Logs +# ----------------------------------------------------------------------------- +*.log +logs/ + +# ----------------------------------------------------------------------------- +# Temporary files +# ----------------------------------------------------------------------------- +tmp/ +temp/ +*.tmp +*.swp +*.swo +*~ + +# ----------------------------------------------------------------------------- +# Documentation +# ----------------------------------------------------------------------------- +docs/_build/ + +# ----------------------------------------------------------------------------- +# mkdocs / sphinx +# ----------------------------------------------------------------------------- +site/ + +# ----------------------------------------------------------------------------- +# Local databases +# ----------------------------------------------------------------------------- +*.sqlite +*.sqlite3 +*.db + +# ----------------------------------------------------------------------------- +# Docker +# ----------------------------------------------------------------------------- +Dockerfile* +docker-compose*.yml +docker-compose*.yaml + +# ----------------------------------------------------------------------------- +# Misc +# ----------------------------------------------------------------------------- +.cache-loader/ +.pybuilder/ \ No newline at end of file diff --git a/Dockerfile b/Dockerfile index ad7911a..7fe33ec 100644 --- a/Dockerfile +++ b/Dockerfile @@ -1,22 +1,39 @@ -FROM minizinc/minizinc +# Use the official slim Python image +FROM python:3.12-slim -WORKDIR /usr/src/app +# Prevent Python from writing .pyc files and buffer logs +ENV PYTHONDONTWRITEBYTECODE=1 \ + PYTHONUNBUFFERED=1 -RUN apt-get update && \ - apt-get upgrade -y && \ - apt-get install software-properties-common python3 python3-pip nginx -y && \ - apt-add-repository ppa:swi-prolog/stable && \ - apt-get update && \ - apt-get install swi-prolog python3.12-venv -y && \ - python3 -m venv venv +# Install required packages +RUN apt-get update \ + && apt-get install -y --no-install-recommends \ + wget \ + unzip \ + ca-certificates \ + minizinc \ + swi-prolog \ + # Clean up + && rm -rf /var/lib/apt/lists/* -ENV PATH="./venv/bin:$PATH" +# Set the working directory +WORKDIR /app +# Create a non-root user +RUN useradd --create-home --shell /bin/bash appuser + +# Install Python dependencies COPY requirements.txt . -RUN pip install --upgrade pip && \ - pip install -r requirements.txt +RUN pip install --no-cache-dir -r requirements.txt +# Copy the application (excluding ignored files in .dockerignore) COPY . . +# Give ownership to the non-root user +RUN chown -R appuser:appuser /app + +# Switch to non-root user +USER appuser + EXPOSE 5000 -CMD ["./venv/bin/gunicorn", "--bind=0.0.0.0:5000", "--workers=4", "--timeout=0", "app:app"] +CMD ["gunicorn", "--bind=0.0.0.0:5000", "--workers=4", "--timeout=0", "app:app"] From 0eef6c321c98c2814551becb7767172929b2f351 Mon Sep 17 00:00:00 2001 From: Steluro <282664784+Steluro@users.noreply.github.com> Date: Fri, 24 Jul 2026 16:06:03 -0400 Subject: [PATCH 2/4] ci: automatize requirements declaration --- requirements-dev.in | 3 ++ requirements-dev.txt | 81 ++++++++++++++++++++++++++++++++++++++++++++ requirements.in | 9 +++++ requirements.txt | 46 ++++++++++++++++++++----- 4 files changed, 130 insertions(+), 9 deletions(-) create mode 100644 requirements-dev.in create mode 100644 requirements-dev.txt create mode 100644 requirements.in diff --git a/requirements-dev.in b/requirements-dev.in new file mode 100644 index 0000000..7426104 --- /dev/null +++ b/requirements-dev.in @@ -0,0 +1,3 @@ +-r requirements.txt + +pip-tools \ No newline at end of file diff --git a/requirements-dev.txt b/requirements-dev.txt new file mode 100644 index 0000000..6eb1c52 --- /dev/null +++ b/requirements-dev.txt @@ -0,0 +1,81 @@ +# +# This file is autogenerated by pip-compile with Python 3.13 +# by the following command: +# +# pip-compile requirements-dev.in +# +arpeggio==2.0.2 + # via + # -r requirements.txt + # textx +blinker==1.9.0 + # via + # -r requirements.txt + # flask +build==1.5.0 + # via pip-tools +click==8.2.1 + # via + # -r requirements.txt + # flask + # pip-tools +flask==3.1.1 + # via + # -r requirements.txt + # flask-cors +flask-cors==5.0.0 + # via -r requirements.txt +gunicorn==23.0.0 + # via -r requirements.txt +itsdangerous==2.2.0 + # via + # -r requirements.txt + # flask +jinja2==3.1.6 + # via + # -r requirements.txt + # flask +markupsafe==3.0.2 + # via + # -r requirements.txt + # flask + # jinja2 + # werkzeug +minizinc==0.10.0 + # via -r requirements.txt +networkx==3.4.2 + # via -r requirements.txt +packaging==25.0 + # via + # -r requirements.txt + # build + # gunicorn + # wheel +pip-tools==7.6.0 + # via -r requirements-dev.in +pydantic==1.10.2 + # via -r requirements.txt +pyproject-hooks==1.2.0 + # via + # build + # pip-tools +swiplserver==1.0.2 + # via -r requirements.txt +textx==4.2.2 + # via -r requirements.txt +typing-extensions==4.14.0 + # via + # -r requirements.txt + # pydantic +werkzeug==3.1.3 + # via + # -r requirements.txt + # flask +wheel==0.47.0 + # via pip-tools +z3-solver==4.15.1.0 + # via -r requirements.txt + +# The following packages are considered to be unsafe in a requirements file: +# pip +# setuptools diff --git a/requirements.in b/requirements.in new file mode 100644 index 0000000..286c929 --- /dev/null +++ b/requirements.in @@ -0,0 +1,9 @@ +Flask +flask-cors +gunicorn +minizinc +networkx +pydantic +swiplserver +textX +z3-solver \ No newline at end of file diff --git a/requirements.txt b/requirements.txt index d16cc2b..f59b9fb 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,19 +1,47 @@ -Arpeggio==2.0.2 +# +# This file is autogenerated by pip-compile with Python 3.13 +# by the following command: +# +# pip-compile +# +arpeggio==2.0.2 + # via textx blinker==1.9.0 + # via flask click==8.2.1 -Flask==3.1.1 + # via flask +flask==3.1.1 + # via + # -r requirements.in + # flask-cors flask-cors==5.0.0 + # via -r requirements.in gunicorn==23.0.0 + # via -r requirements.in itsdangerous==2.2.0 -Jinja2==3.1.6 -MarkupSafe==3.0.2 + # via flask +jinja2==3.1.6 + # via flask +markupsafe==3.0.2 + # via + # flask + # jinja2 + # werkzeug minizinc==0.10.0 + # via -r requirements.in networkx==3.4.2 + # via -r requirements.in packaging==25.0 + # via gunicorn pydantic==1.10.2 -pyhumps==3.8.0 + # via -r requirements.in swiplserver==1.0.2 -textX==4.2.2 -typing_extensions==4.14.0 -Werkzeug==3.1.3 -z3-solver==4.15.1.0 \ No newline at end of file + # via -r requirements.in +textx==4.2.2 + # via -r requirements.in +typing-extensions==4.14.0 + # via pydantic +werkzeug==3.1.3 + # via flask +z3-solver==4.15.1.0 + # via -r requirements.in From fa05fcb108e42401059f2b34c70f9e0bf4bb65c9 Mon Sep 17 00:00:00 2001 From: Steluro <282664784+Steluro@users.noreply.github.com> Date: Fri, 24 Jul 2026 16:53:18 -0400 Subject: [PATCH 3/4] ci: add ruff linting and formatting to ci --- .../semantictranslator-main-aws-image.yml | 83 ++++++++++++------- app.py | 2 +- pyproject.toml | 22 +++++ requirements-dev.in | 3 +- requirements-dev.txt | 2 + .../backends/minizinc/backend.py | 8 +- .../backends/minizinc/compiler.py | 28 ++----- variability_solver/backends/z3/backend.py | 4 +- variability_solver/backends/z3/compiler.py | 18 ++-- variability_solver/backends/z3/executor.py | 4 +- variability_solver/frontends/clif/frontend.py | 6 +- variability_solver/frontends/clif/lowerer.py | 23 ++--- variability_solver/frontends/clif/parser.py | 38 +++++---- variability_solver/ir/constraints.py | 9 +- variability_solver/ir/model.py | 2 +- variability_solver/query.py | 8 +- variability_solver/result.py | 17 ++-- variability_solver/utils/sexpr/lexer.py | 18 ++-- variability_solver/utils/sexpr/parser.py | 7 +- variability_solver/utils/sexpr/sexpr.py | 3 + 20 files changed, 166 insertions(+), 139 deletions(-) create mode 100644 pyproject.toml diff --git a/.github/workflows/semantictranslator-main-aws-image.yml b/.github/workflows/semantictranslator-main-aws-image.yml index a28ce3b..e3845ca 100644 --- a/.github/workflows/semantictranslator-main-aws-image.yml +++ b/.github/workflows/semantictranslator-main-aws-image.yml @@ -1,43 +1,64 @@ name: semantictranslator-main-aws-image on: + pull_request: + branches: + - main + types: [opened, synchronize, reopened] push: branches: - main workflow_dispatch: jobs: + ruff: + name: Ruff Check + runs-on: "ubuntu-latest" + + steps: + - uses: actions/checkout@v4 + + - name: Install Ruff + uses: astral-sh/ruff-action@v3 + + - name: Run Ruff check + run: ruff check . + + - name: Run Ruff format + run: ruff format --check . + build: - runs-on: 'ubuntu-latest' + needs: ruff + runs-on: "ubuntu-latest" steps: - - uses: actions/checkout@v2 - - - name: Set up Docker Buildx - uses: docker/setup-buildx-action@v1 - - - name: Log in to registry - uses: docker/login-action@v1 - with: - registry: ${{vars.ACR_DOKCERHUB}} - username: ${{secrets.ACRUSERNAME_DOKCERHUB}} - password: ${{secrets.ACRUSERPASSWORD_DOKCERHUB}} - - - name: Build and push container image to registry - uses: docker/build-push-action@v3 - with: - context: . - push: true - tags: ${{vars.ACR_DOKCERHUB}}/${{secrets.ACRUSERNAME_DOKCERHUB}}/variamos_semantictranslator:main - file: ./Dockerfile - - - name: Deploy changes into the server - uses: appleboy/ssh-action@master - with: - host: ${{ secrets.AWS_HOST }} - username: ${{ secrets.AWS_USERNAME }} - key: ${{ secrets.VARIAMOS_AWS_PEM }} - script: | - echo "Executing command on remote server..." - sudo docker compose --env-file .env.aws.develop -f docker-compose-aws-develop-nginx.yml pull - sudo docker compose --env-file .env.aws.develop -f docker-compose-aws-develop-nginx.yml up -d + - uses: actions/checkout@v4 + + - name: Set up Docker Buildx + uses: docker/setup-buildx-action@v3 + + - name: Log in to registry + uses: docker/login-action@v3 + with: + registry: ${{vars.ACR_DOKCERHUB}} + username: ${{secrets.ACRUSERNAME_DOKCERHUB}} + password: ${{secrets.ACRUSERPASSWORD_DOKCERHUB}} + + - name: Build and push container image to registry + uses: docker/build-push-action@v6 + with: + context: . + push: true + tags: ${{vars.ACR_DOKCERHUB}}/${{secrets.ACRUSERNAME_DOKCERHUB}}/variamos_semantictranslator:main + file: ./Dockerfile + + - name: Deploy changes into the server + uses: appleboy/ssh-action@master + with: + host: ${{ secrets.AWS_HOST }} + username: ${{ secrets.AWS_USERNAME }} + key: ${{ secrets.VARIAMOS_AWS_PEM }} + script: | + echo "Executing command on remote server..." + sudo docker compose --env-file .env.aws.develop -f docker-compose-aws-develop-nginx.yml pull + sudo docker compose --env-file .env.aws.develop -f docker-compose-aws-develop-nginx.yml up -d diff --git a/app.py b/app.py index 475573b..9ef078f 100644 --- a/app.py +++ b/app.py @@ -43,7 +43,7 @@ def get_solvers() -> Response: "description": solver.description, } for solver in SOLVERS - ] + ] } ) diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..7ffe7cb --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,22 @@ +[tool.ruff] +line-length = 100 +target-version = "py313" + +exclude = [ + "old_request_handler/**", +] + +[tool.ruff.lint] +select = [ + "E", # pycodestyle errors + "F", # pyflakes + "I", # import sorting + "B", # bugbear + "UP", # pyupgrade +] + +ignore = [] + +[tool.ruff.format] +quote-style = "double" +indent-style = "space" \ No newline at end of file diff --git a/requirements-dev.in b/requirements-dev.in index 7426104..08ccdda 100644 --- a/requirements-dev.in +++ b/requirements-dev.in @@ -1,3 +1,4 @@ -r requirements.txt -pip-tools \ No newline at end of file +pip-tools +ruff \ No newline at end of file diff --git a/requirements-dev.txt b/requirements-dev.txt index 6eb1c52..7e2b870 100644 --- a/requirements-dev.txt +++ b/requirements-dev.txt @@ -59,6 +59,8 @@ pyproject-hooks==1.2.0 # via # build # pip-tools +ruff==0.16.0 + # via -r requirements-dev.in swiplserver==1.0.2 # via -r requirements.txt textx==4.2.2 diff --git a/variability_solver/backends/minizinc/backend.py b/variability_solver/backends/minizinc/backend.py index a187a50..05076f7 100644 --- a/variability_solver/backends/minizinc/backend.py +++ b/variability_solver/backends/minizinc/backend.py @@ -1,5 +1,5 @@ from abc import ABC, abstractmethod -from enum import Enum +from enum import StrEnum from variability_solver.backends.minizinc.executor import MinizincExecutor @@ -11,7 +11,7 @@ from .compiler import MinizincCompiler -class _Solver(str, Enum): +class _Solver(StrEnum): GECODE = "gecode" @@ -34,9 +34,7 @@ def execute(self, model: Model, query: Query, options: Options) -> Result: variable_names = MinizincCompiler().get_variable_names(model) match query.operation: case Operation.CHECK_SATISFIABILITY: - return MinizincExecutor().check_satisfiability( - self._solver, solver_model - ) + return MinizincExecutor().check_satisfiability(self._solver, solver_model) case Operation.SOLVE: return MinizincExecutor().solve( self._solver, solver_model, query.limit or 1, variable_names diff --git a/variability_solver/backends/minizinc/compiler.py b/variability_solver/backends/minizinc/compiler.py index 278cbca..a48dc64 100644 --- a/variability_solver/backends/minizinc/compiler.py +++ b/variability_solver/backends/minizinc/compiler.py @@ -70,24 +70,14 @@ def _compile_formula(self, formula: Formula) -> str: return f"(not {self._compile_formula(operand)})" case Disjunction(operands=operands): return ( - "(" - + " \\/ ".join( - self._compile_formula(operand) for operand in operands - ) - + ")" + "(" + " \\/ ".join(self._compile_formula(operand) for operand in operands) + ")" ) case Conjunction(operands=operands): return ( - "(" - + " /\\ ".join( - self._compile_formula(operand) for operand in operands - ) - + ")" + "(" + " /\\ ".join(self._compile_formula(operand) for operand in operands) + ")" ) case Implication(left=left, right=right): - return ( - f"({self._compile_formula(left)} -> {self._compile_formula(right)})" - ) + return f"({self._compile_formula(left)} -> {self._compile_formula(right)})" case Biconditional(left=left, right=right): return f"({self._compile_formula(left)} <-> {self._compile_formula(right)})" case Equality(left=left, right=right): @@ -110,21 +100,13 @@ def _compile_term(self, term: Term) -> str: case Addition(operands=operands): if len(operands) == 0: return "0" - return ( - "(" - + " + ".join(self._compile_term(operand) for operand in operands) - + ")" - ) + return "(" + " + ".join(self._compile_term(operand) for operand in operands) + ")" case Subtraction(left=left, right=right): return f"({self._compile_term(left)} - {self._compile_term(right)})" case Multiplication(operands=operands): if len(operands) == 0: return "1" - return ( - "(" - + " * ".join(self._compile_term(operand) for operand in operands) - + ")" - ) + return "(" + " * ".join(self._compile_term(operand) for operand in operands) + ")" case Division(left=left, right=right): return f"({self._compile_term(left)} / {self._compile_term(right)})" case _: diff --git a/variability_solver/backends/z3/backend.py b/variability_solver/backends/z3/backend.py index 21e20c0..b53dab0 100644 --- a/variability_solver/backends/z3/backend.py +++ b/variability_solver/backends/z3/backend.py @@ -31,6 +31,4 @@ def execute(self, model: Model, query: Query, options: Options) -> Result: limit = query.limit or 1 return Z3Executor().solve(solver, limit, variable_names) case _: - raise NotImplementedError( - f"The operation {query.operation} is not supported" - ) + raise NotImplementedError(f"The operation {query.operation} is not supported") diff --git a/variability_solver/backends/z3/compiler.py b/variability_solver/backends/z3/compiler.py index a8412b9..67cc47a 100644 --- a/variability_solver/backends/z3/compiler.py +++ b/variability_solver/backends/z3/compiler.py @@ -26,7 +26,7 @@ class Z3Compiler: def __init__(self) -> None: self.variables: dict[int, z3.ExprRef] = {} - + def get_variable_names(self, model: Model) -> dict[str, str]: return {f"var_{variable.var_id}": variable.name for variable in model.variables} @@ -83,9 +83,7 @@ def _compile_term(self, term: Term) -> z3.ExprRef: ) result = compiled_left - compiled_right case Multiplication(operands=operands): - result = z3.Product( - *[self._compile_term(operand) for operand in operands] - ) + result = z3.Product(*[self._compile_term(operand) for operand in operands]) case Division(left=left, right=right): compiled_left = self._compile_term(left) compiled_right = self._compile_term(right) @@ -108,17 +106,11 @@ def _compile_formula(self, formula: Formula) -> z3.BoolRef: case Negation(operand=operand): result = z3.Not(self._compile_formula(operand)) case Disjunction(operands=operands): - result = z3.Or( - *[self._compile_formula(operand) for operand in operands] - ) + result = z3.Or(*[self._compile_formula(operand) for operand in operands]) case Conjunction(operands=operands): - result = z3.And( - *[self._compile_formula(operand) for operand in operands] - ) + result = z3.And(*[self._compile_formula(operand) for operand in operands]) case Implication(left=left, right=right): - result = z3.Implies( - self._compile_formula(left), self._compile_formula(right) - ) + result = z3.Implies(self._compile_formula(left), self._compile_formula(right)) case Biconditional(left=left, right=right): result = self._compile_formula(left) == self._compile_formula(right) case Equality(left=left, right=right): diff --git a/variability_solver/backends/z3/executor.py b/variability_solver/backends/z3/executor.py index 73eeef0..4782ade 100644 --- a/variability_solver/backends/z3/executor.py +++ b/variability_solver/backends/z3/executor.py @@ -22,7 +22,9 @@ def solve(self, solver_model: z3.Solver, limit: int, variable_names: dict[str, s return SolveResult(solutions=[solution]) return SolveResult(solutions=[]) - def _solution_from_model(self, model: z3.ModelRef, variable_names: dict[str, str]) -> dict[str, object]: + def _solution_from_model( + self, model: z3.ModelRef, variable_names: dict[str, str] + ) -> dict[str, object]: solution = {} for d in model.decls(): value = model[d] diff --git a/variability_solver/frontends/clif/frontend.py b/variability_solver/frontends/clif/frontend.py index a77b97c..4446bb1 100644 --- a/variability_solver/frontends/clif/frontend.py +++ b/variability_solver/frontends/clif/frontend.py @@ -5,14 +5,16 @@ class CLIFFrontend(Frontend): - @property def name(self) -> str: return "CLIF" @property def description(self) -> str: - return "Common Logic Interchange Format as defined in the ISO/IEC 24707 standard for Common Logic" + return ( + "Common Logic Interchange Format" + " (as defined in the ISO/IEC 24707 standard for Common Logic)" + ) @property def file_extensions(self) -> tuple[str, ...]: diff --git a/variability_solver/frontends/clif/lowerer.py b/variability_solver/frontends/clif/lowerer.py index 4eb7b06..b7e0020 100644 --- a/variability_solver/frontends/clif/lowerer.py +++ b/variability_solver/frontends/clif/lowerer.py @@ -1,4 +1,5 @@ from __future__ import annotations + from dataclasses import dataclass, field from variability_solver.ir.constraints import ( @@ -83,7 +84,9 @@ def lower_clif(theory: clif.Theory) -> Model: raise LoweringError(f"Variable {var.name} has no sort") if var.domain is None: var.domain = FullDomain() - variables.append(Variable(var_id=var.var_id, name=var.name, sort=var.sort, domain=var.domain)) + variables.append( + Variable(var_id=var.var_id, name=var.name, sort=var.sort, domain=var.domain) + ) return Model( variables=variables, constraints=constraints, @@ -124,17 +127,21 @@ def _lower_formula(node: clif.Formula, ctx: _Context) -> Formula: case _: raise LoweringError(f"Unsupported formula: {node!r}") - - + + BINARY_PREDICATES = { # predicate: (constructor, swap_operands) "<": (LessThan, False), "<=": (LessEqual, False), ">": (LessThan, True), ">=": (LessEqual, True), - "!=": (lambda left, right: Negation(operand=Equality(left=left, right=right)), False), + "!=": ( + lambda left, right: Negation(operand=Equality(left=left, right=right)), + False, + ), } + def _lower_atom(node: clif.Atom, ctx: _Context) -> Formula: if not isinstance(node.predicate, clif.Name): raise LoweringError("Higher-order predicates are not directly translatable.") @@ -197,9 +204,7 @@ def _lower_term(node: clif.Term, ctx: _Context) -> Term: def _lower_function(node: clif.Function, ctx: _Context) -> Term: if not isinstance(node.operator, clif.Name): - raise LoweringError( - "Higher-order function operators are not directly translatable." - ) + raise LoweringError("Higher-order function operators are not directly translatable.") args = _lower_term_sequence(node.arguments, ctx) @@ -221,9 +226,7 @@ def _lower_function(node: clif.Function, ctx: _Context) -> Term: return Division(left=args[0], right=args[1]) case _: - raise LoweringError( - f"Function '{node.operator.name}' is not directly translatable." - ) + raise LoweringError(f"Function '{node.operator.name}' is not directly translatable.") def _lower_term_sequence(seq: clif.TermSequence, ctx: _Context) -> tuple[Term, ...]: diff --git a/variability_solver/frontends/clif/parser.py b/variability_solver/frontends/clif/parser.py index fc6a71b..39e3ba5 100644 --- a/variability_solver/frontends/clif/parser.py +++ b/variability_solver/frontends/clif/parser.py @@ -57,8 +57,8 @@ def _parse_formula(self, expr: SExpr) -> clif.Formula: items=[Symbol(value="="), *args], ): raise SyntacticError( - f"Equality must have exactly 2 arguments," - f"got {len(args)} at {loc}") + f"Equality must have exactly 2 arguments,got {len(args)} at {loc}" + ) # Negation case List( @@ -74,8 +74,7 @@ def _parse_formula(self, expr: SExpr) -> clif.Formula: location=_, items=[Symbol(value="not"), *args], ): - raise SyntacticError( - f"Negation must have exactly 1 argument, got {len(args)}") + raise SyntacticError(f"Negation must have exactly 1 argument, got {len(args)}") # Conjunction case List( @@ -111,8 +110,8 @@ def _parse_formula(self, expr: SExpr) -> clif.Formula: items=[Symbol(value="if"), *args], ): raise SyntacticError( - f"Implication must have exactly 2 arguments, " - f"got {len(args)} at {expr.location}") + f"Implication must have exactly 2 arguments, got {len(args)} at {expr.location}" + ) # Biconditional case List( @@ -131,7 +130,8 @@ def _parse_formula(self, expr: SExpr) -> clif.Formula: ): raise SyntacticError( f"Biconditional must have exactly 2 arguments, " - f"got {len(args)} at {expr.location}") + f"got {len(args)} at {expr.location}" + ) # Universal quantification case List( @@ -139,8 +139,7 @@ def _parse_formula(self, expr: SExpr) -> clif.Formula: items=[Symbol(value="forall"), List(items=bindings), body], ): return clif.ForAll( - bindings=[self._parse_binding(binding) - for binding in bindings], + bindings=[self._parse_binding(binding) for binding in bindings], body=self._parse_formula(body), ) @@ -151,7 +150,8 @@ def _parse_formula(self, expr: SExpr) -> clif.Formula: ): raise SyntacticError( f"Universal quantification must have exactly 2 arguments, " - f"got {len(args)} at {expr.location}") + f"got {len(args)} at {expr.location}" + ) # Existential quantification case List( @@ -159,8 +159,7 @@ def _parse_formula(self, expr: SExpr) -> clif.Formula: items=[Symbol(value="exists"), List(items=bindings), body], ): return clif.Exists( - bindings=[self._parse_binding(binding) - for binding in bindings], + bindings=[self._parse_binding(binding) for binding in bindings], body=self._parse_formula(body), ) @@ -171,7 +170,8 @@ def _parse_formula(self, expr: SExpr) -> clif.Formula: ): raise SyntacticError( f"Existential quantification must have exactly 2 arguments, " - f"got {len(args)} at {expr.location}") + f"got {len(args)} at {expr.location}" + ) # Atomic sentence case List( @@ -208,7 +208,8 @@ def _parse_term(self, expr: SExpr) -> clif.Term: raise SemanticError( f"Sequence marker '@{term.name}' " f"cannot appear as a standalone term " - f"at {expr.location}") + f"at {expr.location}" + ) return term @@ -217,7 +218,8 @@ def _parse_term(self, expr: SExpr) -> clif.Term: raise SyntacticError( "Empty list cannot be used as a term. " "Expected a valid term expression (e.g., '(predicate arg1 arg2)'). " - f"at {loc}") + f"at {loc}" + ) case List( location=_, @@ -238,8 +240,7 @@ def _parse_term(self, expr: SExpr) -> clif.Term: def _parse_term_sequence(self, exprs: list[SExpr]) -> clif.TermSequence: """Parse a sequence of terms from S-expressions.""" return clif.TermSequence( - elements=[self._parse_term_sequence_element( - expr) for expr in exprs], + elements=[self._parse_term_sequence_element(expr) for expr in exprs], ) def _parse_term_sequence_element(self, expr: SExpr) -> clif.Term | clif.SequenceMarker: @@ -279,4 +280,5 @@ def _parse_binding(self, expr: SExpr) -> clif.Binding: case _: raise SyntacticError( - f"Expected name or sequence marker as binding at {expr.location}") + f"Expected name or sequence marker as binding at {expr.location}" + ) diff --git a/variability_solver/ir/constraints.py b/variability_solver/ir/constraints.py index 9f00171..786f131 100644 --- a/variability_solver/ir/constraints.py +++ b/variability_solver/ir/constraints.py @@ -2,11 +2,11 @@ from pydantic import BaseModel - # ====================================================================== # Base classes # ====================================================================== + class Node(BaseModel, frozen=True): pass @@ -27,12 +27,14 @@ class Term(Node, frozen=True): # Atomic Formulas # ---------------------------------------------------------------------- + class AtomicFormula(Formula, frozen=True): pass # Comparisons + class Comparison(AtomicFormula, frozen=True): left: Term right: Term @@ -79,12 +81,13 @@ class Implication(CompositeFormula, frozen=True): class Biconditional(CompositeFormula, frozen=True): left: Formula right: Formula - + # ====================================================================== # Terms # ====================================================================== + class VariableRef(Term, frozen=True): var_id: int @@ -93,8 +96,10 @@ class VariableRef(Term, frozen=True): # Constants # --------------------------------------------------------------------- + class Constant(Term, frozen=True): """Represents a constant value in the constraint (ex: 5, True).""" + value: object diff --git a/variability_solver/ir/model.py b/variability_solver/ir/model.py index 42f6a19..85134db 100644 --- a/variability_solver/ir/model.py +++ b/variability_solver/ir/model.py @@ -6,4 +6,4 @@ class Model(BaseModel, frozen=True): variables: list[Variable] - constraints: list[Formula] \ No newline at end of file + constraints: list[Formula] diff --git a/variability_solver/query.py b/variability_solver/query.py index 4e6acf3..c60e673 100644 --- a/variability_solver/query.py +++ b/variability_solver/query.py @@ -1,15 +1,15 @@ -from enum import Enum +from enum import StrEnum from pydantic import BaseModel -class Operation(str, Enum): +class Operation(StrEnum): CHECK_SATISFIABILITY = "sat" SOLVE = "solve" OPTIMIZE = "optimize" -class Direction(str, Enum): +class Direction(StrEnum): MAXIMIZE = "maximize" MINIMIZE = "minimize" @@ -36,4 +36,4 @@ class Query(BaseModel, frozen=True): limit: int | None = None target: str | None = None direction: Direction | None = None - iteration_rules: list[IterationRule] | None = None \ No newline at end of file + iteration_rules: list[IterationRule] | None = None diff --git a/variability_solver/result.py b/variability_solver/result.py index c5ab1a9..3f30d02 100644 --- a/variability_solver/result.py +++ b/variability_solver/result.py @@ -10,15 +10,20 @@ class SATResult(Result, frozen=True): class SolveResult(Result, frozen=True): - solutions: list[dict[str, object]] = Field(default_factory=list) - + solutions: list[dict[str, object]] = Field(default_factory=list) + class Iteration(BaseModel, frozen=True): values: dict[str, object] result: SATResult - - + + class IterateResult(Result, frozen=True): - # example: [{"values": {"feature1": True, "feature2": False}, "result": SATResult(satisfiable=True)}, ...] + # example: [ + # { + # "values": {"feature1": True, "feature2": False}, + # "result": SATResult(satisfiable=True), + # }, + # ... + # ] iterations: list[Iteration] - \ No newline at end of file diff --git a/variability_solver/utils/sexpr/lexer.py b/variability_solver/utils/sexpr/lexer.py index e3db24f..697e021 100644 --- a/variability_solver/utils/sexpr/lexer.py +++ b/variability_solver/utils/sexpr/lexer.py @@ -12,7 +12,6 @@ class Lexer: - def __init__(self, text: str): self.text: str = text self.pos: int = 0 @@ -60,7 +59,7 @@ def _skip_layout(self) -> bool: return self._skip_whitespace() or self._skip_comment() def _read_symbol(self) -> Token: - """Read a symbol token, which is a sequence of non-whitespace, non-parenthesis characters.""" + """Read a symbol token""" location = Location(self.line, self.column) chars = [] @@ -68,11 +67,7 @@ def _read_symbol(self) -> Token: chars.append(ch) self._advance() - return Token( - TokenType.SYMBOL, - "".join(chars), - location - ) + return Token(TokenType.SYMBOL, "".join(chars), location) def _read_string(self) -> Token: """Read a string token, which is a sequence of characters enclosed in double quotes.""" @@ -87,16 +82,13 @@ def _read_string(self) -> Token: if self._current() is None: raise LexicalError( - f"Unterminated string at line {location.line}, column {location.column}") + f"Unterminated string at line {location.line}, column {location.column}" + ) self._advance() # consume closing quote # Strings are treated as symbols - return Token( - TokenType.SYMBOL, - '"' + "".join(chars) + '"', - location - ) + return Token(TokenType.SYMBOL, '"' + "".join(chars) + '"', location) def _next_token(self) -> Token: """Return the next token from the input stream.""" diff --git a/variability_solver/utils/sexpr/parser.py b/variability_solver/utils/sexpr/parser.py index 13859bd..826da17 100644 --- a/variability_solver/utils/sexpr/parser.py +++ b/variability_solver/utils/sexpr/parser.py @@ -41,9 +41,7 @@ def _expect(self, typ: TokenType) -> None: """Expect the current token to be of the given type.""" token = self._current if token.type != typ: - raise SExprParseError( - f"Expected {typ.name}, got {token.type.name} at {token.location}" - ) + raise SExprParseError(f"Expected {typ.name}, got {token.type.name} at {token.location}") def _parse_expr(self) -> SExpr: """Parse a single S-expression.""" @@ -61,8 +59,7 @@ def _parse_expr(self) -> SExpr: return self._parse_list() case _: - raise SExprParseError( - f"Unexpected token {token.type.name} at {token.location}") + raise SExprParseError(f"Unexpected token {token.type.name} at {token.location}") def _parse_list(self) -> List: """Parse a list S-expression.""" diff --git a/variability_solver/utils/sexpr/sexpr.py b/variability_solver/utils/sexpr/sexpr.py index 2d47742..1465abc 100644 --- a/variability_solver/utils/sexpr/sexpr.py +++ b/variability_solver/utils/sexpr/sexpr.py @@ -14,16 +14,19 @@ @dataclass(frozen=True) class SExpr: """Base class for all S-expression nodes.""" + location: Location @dataclass(frozen=True) class Symbol(SExpr): """Represents a symbolic identifier in an S-expression.""" + value: str @dataclass(frozen=True) class List(SExpr): """Represents a nested list structure in an S-expression.""" + items: list[SExpr] From 4afa7e2aaee9b2cd8472fe5d0677bed5c627898f Mon Sep 17 00:00:00 2001 From: Steluro <282664784+Steluro@users.noreply.github.com> Date: Fri, 24 Jul 2026 17:06:08 -0400 Subject: [PATCH 4/4] patch(ci): stop building on PR --- .github/workflows/semantictranslator-main-aws-image.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/semantictranslator-main-aws-image.yml b/.github/workflows/semantictranslator-main-aws-image.yml index e3845ca..2dc2736 100644 --- a/.github/workflows/semantictranslator-main-aws-image.yml +++ b/.github/workflows/semantictranslator-main-aws-image.yml @@ -28,6 +28,7 @@ jobs: run: ruff format --check . build: + if: github.event_name == 'push' || github.event_name == 'workflow_dispatch' needs: ruff runs-on: "ubuntu-latest"