fix for support for eta constraints in spec file#152
Open
zurabksmlp wants to merge 6 commits into
Open
Conversation
fbrausse
reviewed
Jun 1, 2026
fbrausse
left a comment
fbrausse
left a comment
Collaborator
There was a problem hiding this comment.
In general looks good to me, except for typos and I have a question about the introduction of named parameters.
mdmitry1
requested changes
Jun 1, 2026
Collaborator
There was a problem hiding this comment.
There are some new diffs. Most of the due to missing print statement.
However, for several tests diffs are in the results
-
New diffs report
smlp_eta_spec_handling_fix_diffs.log -
All Results
eta_spec_handling_fix_code.tar.gz -
Reproduction - wheel for
Ubuntu 24.04
wheel.tar.gz -
Got the same results with wheel built by GitHub actions
=== 1. Run 26743307966 [eta_spec_handling_fix]: Build ===
attempt 3 [by: mdmitry1] [started: 2026-06-01 13:22:46 IDT] [finished: 2026-06-01 13:37:10 IDT]:
smlptech-1.2.1rc11.dev5+g446399f54-cp311-cp311-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl
Note: the two first build attempts failed due to GitHub actions issue - failures are unrelated to this PR.
…d also a number of missing master files
Collaborator
|
After the latest commit 972c4a4 there is a crash. Wheel for reproduction: ReproductionBelow changes fix this crash diff --git a/src/smlp_py/smlp_flows.py b/src/smlp_py/smlp_flows.py
index a1480b3..a0d2bc0 100644
--- a/src/smlp_py/smlp_flows.py
+++ b/src/smlp_py/smlp_flows.py
@@ -87,6 +87,7 @@ class SmlpFlows:
self.specInst.set_logger(self.logger)
self.frontierInst.set_logger(self.logger)
self.optInst.set_logger(self.logger)
+ self.verifyInst.set_logger(self.logger)
self.queryInst.set_logger(self.logger)
self.refineInst.set_logger(self.logger)
self.correlInst.set_logger(self.logger)
diff --git a/src/smlp_py/smlp_verify.py b/src/smlp_py/smlp_verify.py
index cba0990..205b633 100644
--- a/src/smlp_py/smlp_verify.py
+++ b/src/smlp_py/smlp_verify.py
@@ -63,11 +63,11 @@ class SmlpVerify:
solver_instance.add(self._smlpTermsInst.smlp_not(asrt_form))
res = solver_instance.check()
- if self._modelTermsInst.solver_status_is_unsat(res): #isinstance(res, core.unsat):
+ if self._modelTermsInst.solver_status_unsat(res): #isinstance(res, core.unsat):
status = 'UNSAT' if asrt_name == self._VACUITY_ASSERTION_NAME else 'PASS'
self._verify_logger.info('Completed with result: {}'.format(status)) #UNSAT 'PASS'
asrt_res_dict = {'status':'PASS', 'asrt':None, 'model':None}
- elif self._modelTermsInst.solver_status_is_sat(res): #isinstance(res, core.sat):
+ elif self._modelTermsInst.solver_status_sat(res): #isinstance(res, core.sat):
status = 'SAT' if asrt_name == self._VACUITY_ASSERTION_NAME else 'FAIL'
self._verify_logger.info('Completed with result: {}'.format(status)) #SAT 'FAIL (SAT)'
witness_vals_dict = self._smlpTermsInst.witness_term_to_const(self._modelTermsInst.get_solver_model(res),
@@ -76,7 +76,7 @@ class SmlpVerify:
asrt_ce_val = eval(asrt_expr, {}, witness_vals_dict)
assert not asrt_ce_val
asrt_res_dict = {'status':'FAIL', 'asrt': asrt_ce_val, 'model':witness_vals_dict}
- elif self._modelTermsInst.solver_status_is_unknwn(res): #isinstance(res, core.unknown):
+ elif self._modelTermsInst.solver_status_unknown(res): #isinstance(res, core.unknown):
self._verify_logger.info('Completed with result: {}'.format('UNKNOWN'))
# TODO !!!: add reason for UNKNOWN or report that reason as 'status' field
asrt_res_dict = {'status':'UNKNOWN', 'asrt':None, 'model':None}However, now one of the output files is missing: @zurabksmlp, please review |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixed handing of eta constraints defined in spec file. Eta constraints in command line worked as expected.
Changes are inn files:
src/smlp_py/smlp_flows.py
src/smlp_py/smlp_spec.py
The change is relevant to the following tests -- these test use spec file with an eta constraint:
-- Master files for tests 90-92,94,113-116 are not really affected in the sense that only the .txt log files changed but not the results
-- Master files tests 93,95,96,98,108,228 are affected -- results changed -- in particular, assertion counter examples and/or trace files -- and results are as expected. For test 108 some of the missing master files (not main ones) were also added.
-- Master files tests 142,146,165–177,188–195,199,200 -- these master files do not exist and we cannot compare.
-- Master files for test 123 -- input data is missing for this test and changes cannot be compared
Test 229 also refers to spec file with eta constraint but this eta constraint has no effect (this test is a sanity check).