Skip to content

Commit c17299b

Browse files
GermanMTGermanMT
committed
chore: change smt collection name
1 parent a04b29f commit c17299b

File tree

3 files changed

+58
-58
lines changed

3 files changed

+58
-58
lines changed

‎app/controllers/smt_operation_controller.py‎

Lines changed: 35 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -53,15 +53,15 @@ async def valid_graph(
5353
json_encoder: JSONEncoder = Depends(get_json_encoder),
5454
) -> JSONResponse:
5555
graph_data = await requirement_file_service.read_data_for_smt_transform(valid_graph_request.requirement_file_id, valid_graph_request.max_depth)
56-
smt_text_id = f"{valid_graph_request.requirement_file_id}:{valid_graph_request.max_depth}"
56+
smt_id = f"{valid_graph_request.requirement_file_id}:{valid_graph_request.max_depth}"
5757
if graph_data["name"] is not None:
5858
smt_model = SMTModel(graph_data, valid_graph_request.node_type.value, "mean")
59-
smt_text = await smt_service.read_smt_text(smt_text_id)
60-
if smt_text is not None and smt_text["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
61-
smt_model.convert(smt_text["text"])
59+
smt = await smt_service.read_smt(smt_id)
60+
if smt is not None and smt["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
61+
smt_model.convert(smt["text"])
6262
else:
6363
model_text = smt_model.transform()
64-
await smt_service.replace_smt_text(smt_text_id, model_text)
64+
await smt_service.replace_smt(smt_id, model_text)
6565
result = ValidGraphOperation.execute(smt_model)
6666
return JSONResponse(
6767
status_code=status.HTTP_200_OK,
@@ -102,15 +102,15 @@ async def minimize_impact(
102102
json_encoder: JSONEncoder = Depends(get_json_encoder),
103103
) -> JSONResponse:
104104
graph_data = await requirement_file_service.read_data_for_smt_transform(min_max_impact_request.requirement_file_id, min_max_impact_request.max_depth)
105-
smt_text_id = f"{min_max_impact_request.requirement_file_id}:{min_max_impact_request.max_depth}"
105+
smt_id = f"{min_max_impact_request.requirement_file_id}:{min_max_impact_request.max_depth}"
106106
if graph_data["name"] is not None:
107107
smt_model = SMTModel(graph_data, min_max_impact_request.node_type.value, min_max_impact_request.aggregator)
108-
smt_text = await smt_service.read_smt_text(smt_text_id)
109-
if smt_text is not None and smt_text["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
110-
smt_model.convert(smt_text["text"])
108+
smt = await smt_service.read_smt(smt_id)
109+
if smt is not None and smt["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
110+
smt_model.convert(smt["text"])
111111
else:
112112
model_text = smt_model.transform()
113-
await smt_service.replace_smt_text(smt_text_id, model_text)
113+
await smt_service.replace_smt(smt_id, model_text)
114114
result = await MinimizeImpactOperation.execute(smt_model, min_max_impact_request.limit)
115115
return JSONResponse(
116116
status_code=status.HTTP_200_OK,
@@ -151,15 +151,15 @@ async def maximize_impact(
151151
json_encoder: JSONEncoder = Depends(get_json_encoder),
152152
) -> JSONResponse:
153153
graph_data = await requirement_file_service.read_data_for_smt_transform(min_max_impact_request.requirement_file_id, min_max_impact_request.max_depth)
154-
smt_text_id = f"{min_max_impact_request.requirement_file_id}:{min_max_impact_request.max_depth}"
154+
smt_id = f"{min_max_impact_request.requirement_file_id}:{min_max_impact_request.max_depth}"
155155
if graph_data["name"] is not None:
156156
smt_model = SMTModel(graph_data, min_max_impact_request.node_type.value, min_max_impact_request.aggregator)
157-
smt_text = await smt_service.read_smt_text(smt_text_id)
158-
if smt_text is not None and smt_text["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
159-
smt_model.convert(smt_text["text"])
157+
smt = await smt_service.read_smt(smt_id)
158+
if smt is not None and smt["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
159+
smt_model.convert(smt["text"])
160160
else:
161161
model_text = smt_model.transform()
162-
await smt_service.replace_smt_text(smt_text_id, model_text)
162+
await smt_service.replace_smt(smt_id, model_text)
163163
result = await MaximizeImpactOperation.execute(smt_model, min_max_impact_request.limit)
164164
return JSONResponse(
165165
status_code=status.HTTP_200_OK,
@@ -200,15 +200,15 @@ async def filter_configs(
200200
json_encoder: JSONEncoder = Depends(get_json_encoder),
201201
) -> JSONResponse:
202202
graph_data = await requirement_file_service.read_data_for_smt_transform(filter_configs_request.requirement_file_id, filter_configs_request.max_depth)
203-
smt_text_id = f"{filter_configs_request.requirement_file_id}:{filter_configs_request.max_depth}"
203+
smt_id = f"{filter_configs_request.requirement_file_id}:{filter_configs_request.max_depth}"
204204
if graph_data["name"] is not None:
205205
smt_model = SMTModel(graph_data, filter_configs_request.node_type.value, filter_configs_request.aggregator)
206-
smt_text = await smt_service.read_smt_text(smt_text_id)
207-
if smt_text is not None and smt_text["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
208-
smt_model.convert(smt_text["text"])
206+
smt = await smt_service.read_smt(smt_id)
207+
if smt is not None and smt["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
208+
smt_model.convert(smt["text"])
209209
else:
210210
model_text = smt_model.transform()
211-
await smt_service.replace_smt_text(smt_text_id, model_text)
211+
await smt_service.replace_smt(smt_id, model_text)
212212
result = await FilterConfigsOperation.execute(
213213
smt_model,
214214
filter_configs_request.max_threshold,
@@ -254,15 +254,15 @@ async def valid_config(
254254
json_encoder: JSONEncoder = Depends(get_json_encoder),
255255
) -> JSONResponse:
256256
graph_data = await requirement_file_service.read_data_for_smt_transform(valid_config_request.requirement_file_id, valid_config_request.max_depth)
257-
smt_text_id = f"{valid_config_request.requirement_file_id}:{valid_config_request.max_depth}"
257+
smt_id = f"{valid_config_request.requirement_file_id}:{valid_config_request.max_depth}"
258258
if graph_data["name"] is not None:
259259
smt_model = SMTModel(graph_data, valid_config_request.node_type.value, valid_config_request.aggregator)
260-
smt_text = await smt_service.read_smt_text(smt_text_id)
261-
if smt_text is not None and smt_text["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
262-
smt_model.convert(smt_text["text"])
260+
smt = await smt_service.read_smt(smt_id)
261+
if smt is not None and smt["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
262+
smt_model.convert(smt["text"])
263263
else:
264264
model_text = smt_model.transform()
265-
await smt_service.replace_smt_text(smt_text_id, model_text)
265+
await smt_service.replace_smt(smt_id, model_text)
266266
config = await version_service.read_serial_numbers_by_releases(valid_config_request.node_type.value, valid_config_request.config)
267267
result = ValidConfigOperation.execute(smt_model, config)
268268
return JSONResponse(
@@ -305,15 +305,15 @@ async def complete_config(
305305
json_encoder: JSONEncoder = Depends(get_json_encoder),
306306
) -> JSONResponse:
307307
graph_data = await requirement_file_service.read_data_for_smt_transform(complete_config_request.requirement_file_id, complete_config_request.max_depth)
308-
smt_text_id = f"{complete_config_request.requirement_file_id}:{complete_config_request.max_depth}"
308+
smt_id = f"{complete_config_request.requirement_file_id}:{complete_config_request.max_depth}"
309309
if graph_data["name"] is not None:
310310
smt_model = SMTModel(graph_data, complete_config_request.node_type.value, complete_config_request.aggregator)
311-
smt_text = await smt_service.read_smt_text(smt_text_id)
312-
if smt_text is not None and smt_text["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
313-
smt_model.convert(smt_text["text"])
311+
smt = await smt_service.read_smt(smt_id)
312+
if smt is not None and smt["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
313+
smt_model.convert(smt["text"])
314314
else:
315315
model_text = smt_model.transform()
316-
await smt_service.replace_smt_text(smt_text_id, model_text)
316+
await smt_service.replace_smt(smt_id, model_text)
317317
config = await version_service.read_serial_numbers_by_releases(complete_config_request.node_type.value, complete_config_request.config)
318318
result = await CompleteConfigOperation.execute(smt_model, config)
319319
return JSONResponse(
@@ -355,15 +355,15 @@ async def config_by_impact(
355355
json_encoder: JSONEncoder = Depends(get_json_encoder),
356356
) -> JSONResponse:
357357
graph_data = await requirement_file_service.read_data_for_smt_transform(config_by_impact_request.requirement_file_id, config_by_impact_request.max_depth)
358-
smt_text_id = f"{config_by_impact_request.requirement_file_id}:{config_by_impact_request.max_depth}"
358+
smt_id = f"{config_by_impact_request.requirement_file_id}:{config_by_impact_request.max_depth}"
359359
if graph_data["name"] is not None:
360360
smt_model = SMTModel(graph_data, config_by_impact_request.node_type.value, config_by_impact_request.aggregator)
361-
smt_text = await smt_service.read_smt_text(smt_text_id)
362-
if smt_text is not None and smt_text["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
363-
smt_model.convert(smt_text["text"])
361+
smt = await smt_service.read_smt(smt_id)
362+
if smt is not None and smt["moment"].replace(tzinfo=UTC) > graph_data["moment"].replace(tzinfo=UTC):
363+
smt_model.convert(smt["text"])
364364
else:
365365
model_text = smt_model.transform()
366-
await smt_service.replace_smt_text(smt_text_id, model_text)
366+
await smt_service.replace_smt(smt_id, model_text)
367367
result = await ConfigByImpactOperation.execute(smt_model, config_by_impact_request.impact)
368368
return JSONResponse(
369369
status_code=status.HTTP_200_OK,

‎app/services/smt_service.py‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,12 @@ class SMTService:
88
def __init__(self, db: DatabaseManager):
99
self.smts_collection = db.get_smts_collection()
1010

11-
async def replace_smt_text(self, smt_text_id: str, text: str) -> None:
11+
async def replace_smt(self, smt_id: str, text: str) -> None:
1212
await self.smts_collection.replace_one(
13-
{"smt_text_id": smt_text_id},
14-
{"smt_text_id": smt_text_id, "text": text, "moment": datetime.now()},
13+
{"smt_id": smt_id},
14+
{"smt_id": smt_id, "text": text, "moment": datetime.now()},
1515
upsert=True,
1616
)
1717

18-
async def read_smt_text(self, smt_text_id: str) -> dict[str, Any]:
19-
return await self.smts_collection.find_one({"smt_text_id": smt_text_id})
18+
async def read_smt(self, smt_id: str) -> dict[str, Any]:
19+
return await self.smts_collection.find_one({"smt_id": smt_id})

‎tests/unit/services/test_smt_service.py‎

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -16,44 +16,44 @@ def mock_db(self):
1616
return db, collection
1717

1818
@pytest.mark.asyncio
19-
async def test_replace_smt_text(self, mock_db):
19+
async def test_replace_smt(self, mock_db):
2020
db, collection = mock_db
2121
service = SMTService(db)
2222

2323
smt_id = "smt-123"
2424
text_content = "(assert (> x 5))"
2525

26-
await service.replace_smt_text(smt_id, text_content)
26+
await service.replace_smt(smt_id, text_content)
2727

2828
collection.replace_one.assert_called_once()
2929
call_args = collection.replace_one.call_args
3030

31-
assert call_args[0][0] == {"smt_text_id": smt_id}
31+
assert call_args[0][0] == {"smt_id": smt_id}
3232

3333
doc = call_args[0][1]
34-
assert doc["smt_text_id"] == smt_id
34+
assert doc["smt_id"] == smt_id
3535
assert doc["text"] == text_content
3636
assert "moment" in doc
3737
assert isinstance(doc["moment"], datetime)
3838

3939
assert call_args[1]["upsert"] is True
4040

4141
@pytest.mark.asyncio
42-
async def test_replace_smt_text_empty(self, mock_db):
42+
async def test_replace_smt_empty(self, mock_db):
4343
db, collection = mock_db
4444
service = SMTService(db)
4545

4646
smt_id = "smt-empty"
4747
text_content = ""
4848

49-
await service.replace_smt_text(smt_id, text_content)
49+
await service.replace_smt(smt_id, text_content)
5050

5151
call_args = collection.replace_one.call_args
5252
doc = call_args[0][1]
5353
assert doc["text"] == ""
5454

5555
@pytest.mark.asyncio
56-
async def test_replace_smt_text_complex_formula(self, mock_db):
56+
async def test_replace_smt_complex_formula(self, mock_db):
5757
db, collection = mock_db
5858
service = SMTService(db)
5959

@@ -66,54 +66,54 @@ async def test_replace_smt_text_complex_formula(self, mock_db):
6666
(check-sat)
6767
(get-model)"""
6868

69-
await service.replace_smt_text(smt_id, text_content)
69+
await service.replace_smt(smt_id, text_content)
7070

7171
call_args = collection.replace_one.call_args
7272
doc = call_args[0][1]
7373
assert doc["text"] == text_content
7474
assert "(check-sat)" in doc["text"]
7575

7676
@pytest.mark.asyncio
77-
async def test_read_smt_text(self, mock_db):
77+
async def test_read_smt(self, mock_db):
7878
db, collection = mock_db
7979
service = SMTService(db)
8080

8181
smt_id = "smt-read-123"
8282
expected_doc = {
83-
"smt_text_id": smt_id,
83+
"smt_id": smt_id,
8484
"text": "(assert (= x 42))",
8585
"moment": datetime.now(),
8686
}
8787

8888
collection.find_one.return_value = expected_doc
8989

90-
result = await service.read_smt_text(smt_id)
90+
result = await service.read_smt(smt_id)
9191

92-
collection.find_one.assert_called_once_with({"smt_text_id": smt_id})
92+
collection.find_one.assert_called_once_with({"smt_id": smt_id})
9393

9494
assert result == expected_doc
9595

9696
@pytest.mark.asyncio
97-
async def test_read_smt_text_not_found(self, mock_db):
97+
async def test_read_smt_not_found(self, mock_db):
9898
db, collection = mock_db
9999
service = SMTService(db)
100100

101101
smt_id = "non-existent-smt"
102102
collection.find_one.return_value = None
103103

104-
result = await service.read_smt_text(smt_id)
104+
result = await service.read_smt(smt_id)
105105

106106
assert result is None
107-
collection.find_one.assert_called_once_with({"smt_text_id": smt_id})
107+
collection.find_one.assert_called_once_with({"smt_id": smt_id})
108108

109109
@pytest.mark.asyncio
110-
async def test_read_smt_text_with_metadata(self, mock_db):
110+
async def test_read_smt_with_metadata(self, mock_db):
111111
db, collection = mock_db
112112
service = SMTService(db)
113113

114114
smt_id = "smt-with-meta"
115115
expected_doc = {
116-
"smt_text_id": smt_id,
116+
"smt_id": smt_id,
117117
"text": "(declare-const version String)",
118118
"moment": datetime(2025, 10, 27, 10, 30, 0),
119119
"solver": "z3",
@@ -122,7 +122,7 @@ async def test_read_smt_text_with_metadata(self, mock_db):
122122

123123
collection.find_one.return_value = expected_doc
124124

125-
result = await service.read_smt_text(smt_id)
125+
result = await service.read_smt(smt_id)
126126

127127
assert result["text"] == "(declare-const version String)"
128128
assert result["solver"] == "z3"

0 commit comments

Comments
 (0)