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

Model Strengthening #379

Merged
merged 138 commits into from Oct 10, 2017

Conversation

Projects
None yet
2 participants
@Druid-of-Luhn
Contributor

Druid-of-Luhn commented Aug 10, 2017

Adding domain attributes; adding, modifying and removing constraints; changing types.

Adds the new model-strengthening command to Conjure.

The fasterIteration rule requires ferret's symmetry_detect executable to be on the $PATH. It will be ignored if not present.

Compilation warns about variables v and d (from essence Template Haskell) being unused in doubleDistinctIter, but they are in fact used later on.

Billy Brown added some commits Jun 6, 2017

Billy Brown
Ignoring editor temporary files
Ignoring vim's temporary files with the pattern .*.swp
Billy Brown
Addition of Conjure.UI.StrengthenVariables module
Added the Conjure.UI.StrengthenVariables module which at the
moment does nothing. Its function is called on Essence code,
so it is ready to be implemented.
Billy Brown
Adding functions to fetch references to a variable
Adding functions that fetch references to a variable:
 - the variable's definition or declaration
 - constraints involving the variable
 - other declarations involving the variable

Implemented finding a variable's definition or declaration.
Billy Brown
Moved StrengthenVariables to correct place
Moved the variable strengthening code to the correct place in
Process and added it as a command-line option for acting purely
on the essence class.
Billy Brown
Adding function to work with function attributes
Added a function to work with function attributes, which does
nothing at the moment other than print the domain. The function
can notify the caller of whether or not it modified the domain,
which is passed to the top level to decide when to stop making
passes.
Billy Brown
Small function attribute change added
As a test, making function attributes (total, bijective) if it is
surjective and its domain is equal to its codomain. This is a
proof of concept for attribute computing and rewriting.
Billy Brown
Refactored framework for strengthening variables
Refactored the framework for strengthening variables so that the
functions only deal with single statements and the model for
context.

The Modified data type is now used better and with better functions
to correctly propagate modification of values.
Billy Brown
Removed use of Modified to simplify code
Removed the use of Modified from StrengthenVariables and now
comparing Models when deciding whether to loop again or not.
This simplifies the code and allows it to be made monadic so
that helper functions which themselves are monadic can be used.
Billy Brown
StrengthenVariables now monadic with MonadFail
All functions in StrengthenVariables are now monadic, in the sense
that they return a `m a` where m is at least a MonadFail.
Billy Brown
Comparing function domains by size
Comparing function domains by size when determining whether they
should be transformed from surjective to total and bijective.

If the domainSizeOf calculation results in an error, it is logged
for development purposes but otherwise ignored for transformation.
Billy Brown
Added rule for in/bijective -> total
Added rules to make partial injective and bijective functions
total.
Billy Brown
Finding variables with integer domains
Finding variables with integer domains so that they can have them
reduced by analysing their relations to other variables in the
`such that` part of the model.
Billy Brown
Fetching the list of expressions referencing a var
Fetching the list of expressions in the such that section of the
model by recursing down the expression tree and writing up the
expressions that contain a reference to the variable.
Billy Brown
Converting expressions to arithmetic relations
Using the method described by Finlay Marno in his dissertation for
domain reduction, which requires expressions to be converted to
arithmetic relations.
Billy Brown
Simplified use of Writer
Simplified the use of Writer to extract the expressions that refer
to a variable. Now using execWriter and no longer using two
functions for varInExpr.
Billy Brown
Simplified function and added comments
Simplified the `findCallingExpressions` function and added more
explanatory comments to the `varInExp` function.
Billy Brown
Changing ArithRelation tree with variable on right
Rewriting the ArithRelation tree of an expression to place the
variable of interest alone on the right of the equality, which
allows the left side to be used in constraining the domain.
Billy Brown
Can get domain of ArithRef in ArithRelation tree
ArithRef has been changed to hold the reference expression,
instead of only the name, so that domainOf can be used on it
when performing domain arithmetic for possible reduction.
Billy Brown
Removed rule for injective/bijective to total
Removed the rule that marked injective or bijective functions as
total.
Billy Brown
Bijective functions may be marked total
Bijective functions for which the domain and codomain are of equal
size are now also marked as being total.
Billy Brown
Combining domains into constrained domains
Combining two domains into more constrained domains, by using min
and max expressions when both bounds are set, or by taking a bound
when one is set but not the other. Single domain ranges ignore the
other domain, even if it is another single value. Non-overlapping
domains are not found and should be an error.
Billy Brown
Finished (incorrect) arithmetic domain reductions
Finished a first effort at arithmetic domain reduction which on
the surface appears to correctly follow the theory, but still
appears to be incorrect.
Billy Brown
Combining and ignoring in OpMin/OpMax
Combining values in OpMin and OpMax in the same matrix, instead of
creating deeply (in fact infinitely due to repeated
transformations) nested min and max expressions.

If an expression being added to the min or the max expression is
already contained within it, then it is not added, as there is no
need to compare it to itself.
Billy Brown
Added comment identifying source of error
Added a FIXME comment identifying the source of an error in the
transferBranchRL when the right side is a non-commutative
operation.
Billy Brown
Fixed arithmetic relation tree transformations
Fixed the arithmetic relation tree transformations when applying a
subtraction or a division to both sides to isolate the variable in
question. Unfortunately the theory that is applied does not appear
to be correct.
Billy Brown
Simplified special case handling in tree transform
Simplified the handling of subtraction and division special cases
when transforming the tree to bring the variable of interest onto
the right side.

Also extracted 'where' functions from liftEqual to the top level.
Billy Brown
Fixed arithmetic domain reduction
Fixed the implementation of arithmetic domain reduction by
correctly matching the behaviour of upper and lower bounds
calculations in the cases of subtraction and division.

Billy Brown added some commits Aug 8, 2017

Billy Brown
Removed references to removed rules
Removed references in comments to rules that will no longer be
implemented.
Billy Brown
Changing mset to set if maxOccur = 1
Changing the type of a multiset to a set if its maxOccur attribute
is 1. Constraints involving the variable are updated to use the
toMSet function on occurrences of the set.
Billy Brown
@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Aug 10, 2017

Collaborator

Thanks @Druid-of-Luhn -- I want to look into the code a bit more before merging, but this looks very nicely structured so my job there will be easy.

Did you try running any of the tests? We will see what travis thinks soon, but I will also run the whole test suite (with --limit-time 0, to run all tests, travis doesn't do that) before merging.

Well done!

Collaborator

ozgurakgun commented Aug 10, 2017

Thanks @Druid-of-Luhn -- I want to look into the code a bit more before merging, but this looks very nicely structured so my job there will be easy.

Did you try running any of the tests? We will see what travis thinks soon, but I will also run the whole test suite (with --limit-time 0, to run all tests, travis doesn't do that) before merging.

Well done!

@Druid-of-Luhn

This comment has been minimized.

Show comment
Hide comment
@Druid-of-Luhn

Druid-of-Luhn Aug 10, 2017

Contributor

I'll have a go at running the tests, in case something fails and I can fix it quite easily.

Contributor

Druid-of-Luhn commented Aug 10, 2017

I'll have a go at running the tests, in case something fails and I can fix it quite easily.

@Druid-of-Luhn

This comment has been minimized.

Show comment
Hide comment
@Druid-of-Luhn

Druid-of-Luhn Aug 10, 2017

Contributor

One of the tests failed (GHC 8.0.2, help text files differ or something) but the others errored during compilation:

Conflicting definitions for 'v'
    Bound at: src/Conjure/Process/ModelStrengthening.hs:818:23-62
              src/Conjure/Process/ModelStrengthening.hs:818:23-62
    In a case alternative
        [essence| forAll &x, &y in &v, &x' != &y' . &_ |]

From running tests locally:

35 out of 2166 tests failed (538.07s)

Last two are issues/370/02 and help-text.

Contributor

Druid-of-Luhn commented Aug 10, 2017

One of the tests failed (GHC 8.0.2, help text files differ or something) but the others errored during compilation:

Conflicting definitions for 'v'
    Bound at: src/Conjure/Process/ModelStrengthening.hs:818:23-62
              src/Conjure/Process/ModelStrengthening.hs:818:23-62
    In a case alternative
        [essence| forAll &x, &y in &v, &x' != &y' . &_ |]

From running tests locally:

35 out of 2166 tests failed (538.07s)

Last two are issues/370/02 and help-text.

@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Aug 10, 2017

Collaborator

Oh, I see what it is!

Passing -ddump-splices to GHC (modify the cabal file) makes GHC print the generates splice for that TH pattern. It is the following.

src/Conjure/Process/ModelStrengthening.hs:818:23-62: Splicing pattern
    Language.Haskell.TH.Quote.quotePat
      essence " forAll &x, &y in &v, &x' != &y' . &_ "
  ======>
    Op (MkOpAnd (OpAnd (Comprehension _
                                      ((ghc-prim-0.5.1.0:GHC.Types.:) (Generator (GenInExpr x v))
                                                                      ((ghc-prim-0.5.1.0:GHC.Types.:) (Generator (GenInExpr y
                                                                                                                            v))
                                                                                                      ((ghc-prim-0.5.1.0:GHC.Types.:) (Condition (Op (MkOpNeq (OpNeq x'
                                                                                                                                                                     y'))))
                                                                                                                                      ghc-prim-0.5.1.0:GHC.Types.[]))))))

src/Conjure/Process/ModelStrengthening.hs:818:23: error:
    • Conflicting definitions for ‘v’
      Bound at: src/Conjure/Process/ModelStrengthening.hs:818:23-62
                src/Conjure/Process/ModelStrengthening.hs:818:23-62
    • In a case alternative
    |
818 |              [essence| forAll &x, &y in &v, &x' != &y' . &_ |] | x' `refersTo` x && y' `refersTo` y
    |                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

See the repeated v's. The parser expands forAll &x, &y in &v to forAll &x . forAll &y in &v

Collaborator

ozgurakgun commented Aug 10, 2017

Oh, I see what it is!

Passing -ddump-splices to GHC (modify the cabal file) makes GHC print the generates splice for that TH pattern. It is the following.

src/Conjure/Process/ModelStrengthening.hs:818:23-62: Splicing pattern
    Language.Haskell.TH.Quote.quotePat
      essence " forAll &x, &y in &v, &x' != &y' . &_ "
  ======>
    Op (MkOpAnd (OpAnd (Comprehension _
                                      ((ghc-prim-0.5.1.0:GHC.Types.:) (Generator (GenInExpr x v))
                                                                      ((ghc-prim-0.5.1.0:GHC.Types.:) (Generator (GenInExpr y
                                                                                                                            v))
                                                                                                      ((ghc-prim-0.5.1.0:GHC.Types.:) (Condition (Op (MkOpNeq (OpNeq x'
                                                                                                                                                                     y'))))
                                                                                                                                      ghc-prim-0.5.1.0:GHC.Types.[]))))))

src/Conjure/Process/ModelStrengthening.hs:818:23: error:
    • Conflicting definitions for ‘v’
      Bound at: src/Conjure/Process/ModelStrengthening.hs:818:23-62
                src/Conjure/Process/ModelStrengthening.hs:818:23-62
    • In a case alternative
    |
818 |              [essence| forAll &x, &y in &v, &x' != &y' . &_ |] | x' `refersTo` x && y' `refersTo` y
    |                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

See the repeated v's. The parser expands forAll &x, &y in &v to forAll &x . forAll &y in &v

@Druid-of-Luhn

This comment has been minimized.

Show comment
Hide comment
@Druid-of-Luhn

Druid-of-Luhn Aug 10, 2017

Contributor

Should I just change the pattern-match to the expanded form then, use v and v' and equate the two in a guard? Or would it be easy enough to change the TemplateHaskell expansion to do that?

Contributor

Druid-of-Luhn commented Aug 10, 2017

Should I just change the pattern-match to the expanded form then, use v and v' and equate the two in a guard? Or would it be easy enough to change the TemplateHaskell expansion to do that?

@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Aug 10, 2017

Collaborator

I think the former is better.

Collaborator

ozgurakgun commented Aug 10, 2017

I think the former is better.

Billy Brown
Fixed Template Haskell expansion bug
Fixed the bug in essence Template Haskell expansion by manually
expanding it.
@Druid-of-Luhn

This comment has been minimized.

Show comment
Hide comment
@Druid-of-Luhn

Druid-of-Luhn Aug 10, 2017

Contributor

The two tests that fail are different help texts (fixed I think, but running local tests without limit takes a while), and autogen/gen_26_3:

autogen/gen26_3:                                                                                  FAIL (6.19s)
      Conjuring
      Savile Row: model.eprime
      Validating solutions
      Checking
      Checking extra files
      Checking expected files
      Checking expected file: model.eprime
        files differ.
        1c1
        <     var3_PartitionAsSet_ExplicitR5_ExplicitVarSizeWithMarker_Marker[1],
        ---
        >     sum([toInt(q25 <= var3_PartitionAsSet_ExplicitR5_ExplicitVarSizeWithMarker_Marker[1]) | q25 : int(1..let2)]),
Contributor

Druid-of-Luhn commented Aug 10, 2017

The two tests that fail are different help texts (fixed I think, but running local tests without limit takes a while), and autogen/gen_26_3:

autogen/gen26_3:                                                                                  FAIL (6.19s)
      Conjuring
      Savile Row: model.eprime
      Validating solutions
      Checking
      Checking extra files
      Checking expected files
      Checking expected file: model.eprime
        files differ.
        1c1
        <     var3_PartitionAsSet_ExplicitR5_ExplicitVarSizeWithMarker_Marker[1],
        ---
        >     sum([toInt(q25 <= var3_PartitionAsSet_ExplicitR5_ExplicitVarSizeWithMarker_Marker[1]) | q25 : int(1..let2)]),
@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Aug 10, 2017

Collaborator

If you run dist/build/conjure-testing/conjure-testing -p help that should only test the help file thing.

If you run tests/acceptAllOutputs.sh it should accept any changed test output files as "correct". Feel free to accept if things look sensible. After "accepting", if you run the tests again the test should pass (if there are no other issues).

Collaborator

ozgurakgun commented Aug 10, 2017

If you run dist/build/conjure-testing/conjure-testing -p help that should only test the help file thing.

If you run tests/acceptAllOutputs.sh it should accept any changed test output files as "correct". Feel free to accept if things look sensible. After "accepting", if you run the tests again the test should pass (if there are no other issues).

@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Aug 10, 2017

Collaborator

I could make the updates if you give me write access to this branch by the way.

Collaborator

ozgurakgun commented Aug 10, 2017

I could make the updates if you give me write access to this branch by the way.

@Druid-of-Luhn

This comment has been minimized.

Show comment
Hide comment
@Druid-of-Luhn
Contributor

Druid-of-Luhn commented Aug 10, 2017

@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Aug 10, 2017

Collaborator

Turns out I can! I will look at the other failing tests next.

Collaborator

ozgurakgun commented Aug 10, 2017

Turns out I can! I will look at the other failing tests next.

@Druid-of-Luhn

This comment has been minimized.

Show comment
Hide comment
@Druid-of-Luhn
Contributor

Druid-of-Luhn commented Aug 10, 2017

Could it be from me uncommenting this code in DomainOf.hs? https://github.com/conjure-cp/conjure/pull/379/files#diff-8ac628a4b76860765a9c63bd83b79d1a

@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Aug 10, 2017

Collaborator

I am not sure, but I am a bit suspicious of that change. I will run all the tests over night, we'll see if anything else breaks!

Collaborator

ozgurakgun commented Aug 10, 2017

I am not sure, but I am a bit suspicious of that change. I will run all the tests over night, we'll see if anything else breaks!

@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Aug 20, 2017

Collaborator

@Druid-of-Luhn -- just for your information, this looks good and I will merge it soon. I want to make a release before merging it, and I am busy with a few other things so it will take some time.

Collaborator

ozgurakgun commented Aug 20, 2017

@Druid-of-Luhn -- just for your information, this looks good and I will merge it soon. I want to make a release before merging it, and I am busy with a few other things so it will take some time.

@ozgurakgun ozgurakgun merged commit cc18bac into conjure-cp:master Oct 10, 2017

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@ozgurakgun

This comment has been minimized.

Show comment
Hide comment
@ozgurakgun

ozgurakgun Oct 10, 2017

Collaborator

finally merged, thanks @Druid-of-Luhn!

Collaborator

ozgurakgun commented Oct 10, 2017

finally merged, thanks @Druid-of-Luhn!

@Druid-of-Luhn Druid-of-Luhn deleted the Druid-of-Luhn:type-inference branch Oct 10, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment