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.

Sign up for GitHub

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

Jump to bottom

Turn on reduction for noodlification #107

Merged
merged 1 commit into from
Dec 26, 2023
Merged

Turn on reduction for noodlification #107

merged 1 commit into from
Dec 26, 2023

Conversation

jurajsic
Copy link
Member

@jurajsic jurajsic commented Nov 6, 2023

This PR fixes a bug where noodlification did not reduce (nor trim) automata in resulting nooodles.

Needs to be benchmarked, it is possible that simulation might slow it down, or that we should just turn on trimming.

@jurajsic jurajsic requested review from vhavlena and Adda0 November 6, 2023 12:59
@jurajsic jurajsic linked an issue Nov 6, 2023 that may be closed by this pull request
Automata in noodles are not reduced #106
Closed
@jurajsic jurajsic mentioned this pull request Nov 6, 2023
Closed
@vhavlena
Copy link
Collaborator

vhavlena commented Nov 6, 2023

Maybe the simulation reduction will be too expensive. We could add option "trim" to do just the trimming. But we will see after the results.

Adda0
Adda0 approved these changes Nov 7, 2023
View reviewed changes
Copy link
Collaborator

@Adda0 Adda0 left a comment

Choose a reason for hiding this comment

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

I would not merge until the results show that there is no significant slowdown. If there is, I would go with the suggested trim instead and merge only the trim.

@vhavlena
Copy link
Collaborator

vhavlena commented Dec 7, 2023

I suggest first to finish and merge the PR #104 and then try the effect of the noodle reduction.

@vhavlena
Copy link
Collaborator

The results (z3-noodler-feada45-a57f582 is the PR version, z3-noodler-1482571-a57f582 is the pyex-opt version -- NOT devel)
image

# of formulae: 82972
###################################################################################
####                                   Table 1                                 ####
###################################################################################
| method                     |    max |     mean |   median |   std. dev |   TO+MO+ERR |   unknowns |
|----------------------------|--------|----------|----------|------------|-------------|------------|
| z3-noodler-feada45-a57f582 | 116.1  | 0.494545 |     0.02 |    3.67665 |        2198 |       2011 |
| cvc5-1.0.8                 | 119.36 | 0.515113 |     0.02 |    5.2351  |        1723 |          2 |
| z3-4.12.2                  | 119.29 | 1.49018  |     0.04 |    8.17615 |        2623 |        123 |
| z3-noodler-1482571-a57f582 | 115.42 | 0.463528 |     0.02 |    3.42857 |        2465 |       2098 |
  • the version z3-noodler-1482571-a57f582 lacks some optimisations currently in devel (hard equations, replace_re, lex ordering), the improvement of this PR is not caused only by the noodle reduction. Ignore woorpje.
  • it seems there is some positive effect (e.g., on kaluza we have 80 TOs less now)

@vhavlena
Copy link
Collaborator

Should I merge the PR?

@Adda0
Copy link
Collaborator

Adda0 commented Dec 23, 2023

I would merge the PR.

@jurajsic jurajsic merged commit 076cd49 into devel Dec 26, 2023
@jurajsic jurajsic deleted the noodle_reduce branch December 26, 2023 08:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Adda0 Adda0 Adda0 approved these changes

@vhavlena vhavlena vhavlena approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Automata in noodles are not reduced
3 participants
@jurajsic @vhavlena @Adda0