Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add python bindings for configurations #125

Open
wants to merge 15 commits into
base: vara-dev
Choose a base branch
from
Open

Add python bindings for configurations #125

wants to merge 15 commits into from

Conversation

danjujan
Copy link
Contributor

No description provided.

@codecov-commenter
Copy link

codecov-commenter commented Sep 15, 2023

Codecov Report

Attention: 2 lines in your changes are missing coverage. Please review.

Comparison is base (5231e12) 89.74% compared to head (e638b9d) 89.73%.

Additional details and impacted files
@@             Coverage Diff              @@
##           vara-dev     #125      +/-   ##
============================================
- Coverage     89.74%   89.73%   -0.02%     
============================================
  Files            73       73              
  Lines          6991     7001      +10     
============================================
+ Hits           6274     6282       +8     
- Misses          717      719       +2     
Files Coverage Δ
include/vara/Solver/Error.h 100.00% <ø> (ø)
include/vara/Solver/Z3Solver.h 100.00% <ø> (ø)
unittests/Solver/ConfigurationFactory.cpp 100.00% <100.00%> (ø)
unittests/Solver/Z3Tests.cpp 100.00% <100.00%> (ø)
lib/Solver/Z3Solver.cpp 78.96% <88.23%> (-0.80%) ⬇️

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@danjujan danjujan requested a review from vulder September 15, 2023 13:36
Copy link
Contributor

@vulder vulder left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Except for the comment below, LGTM

Comment on lines +50 to +51
if os.path.exists('/lib/x86_64-linux-gnu/libz3.so'):
cmake_args.append('-DVARA_FEATURE_BUILD_Z3_SOLVER=False')
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if this is a good way to determine if we should build the solver.

  1. the path is a system specific
  2. we might want to build the solver from scratch even for those system, as we depend on a very specific version of z3. (The debian 11 can cause problems)

Maybe we should keep building the solver as the default and give the user a option to disable that? Or, if it works for you, only you use the local one.

danjujan and others added 10 commits October 6, 2023 17:22
For some reason, this caused other configs to appear multiple times during enumeration.
This caused 2 issues:
- either first config was skipped or getCurrentConfig would always point to the next configuration
- getAllValidConfigurations or getNumberValidConfigurations produce incorrect results if called after any call to getNextConfiguration()
The last point is an issue with the Solver API and this is a quick-fix for the Z3Solver implementation that returns an error in that case.
This implementation is quite hacky and requires a redesign of the Solver API to be fixed properly.
Comment on lines +76 to +77
auto FM = feature::loadFeatureModel(
getTestResource("test_msmr.xml"));

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[clang-format] reported by reviewdog 🐶

Suggested change
auto FM = feature::loadFeatureModel(
getTestResource("test_msmr.xml"));
auto FM = feature::loadFeatureModel(getTestResource("test_msmr.xml"));

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants