conjure-cp / conjure Goto Github PK

Conjure: The Automated Constraint Modelling Tool

License: Other

Makefile 0.27% Shell 5.00% Haskell 93.93% Ruby 0.28% HTML 0.02% Python 0.05% Dockerfile 0.20% Vim Snippet 0.02% Vim Script 0.22%

combinatorial-optimization constraint-programming constraints modelling sat

conjure's People

Contributors

Stargazers

Watchers

conjure's Issues

msetIntersect2.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of msetIntersect2.essence in savilerow causes:

Failed when parsing rest of structure following line:3 column 7
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:188)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/19

Bad Constraint Name

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using setIn.essence

./scripts/run/conjure-all.sh files/testdata/specs/setIn.essence

running 0002.essence.out though savilerow and solving with minion causes the following error

    $ savilerow -in-eprime files/testdata/specs/setIn/0002.essence.out 
Created output file /Users/bilalh/CS/conjure/files/testdata/specs/setIn/0002.essence.out.minion
Minion exited with error code:1 and message:
Error in input!
Bad Constraint Name or reached end of file: 'x_Occurrence_00003**EOF**
'
Error occurred on line 17
Parser gave up around:
x_Occurrence_00003**EOF**
-------------------------^

No solutions. Possible causes: Infeasible instance, Minion time-out.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/13

|x| - sss.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

running
files/testdata/specs/sss.essence

produces

Error in phase: Repr
    ErrFatal Type error in:  operator.twoBars.reference := x
    language Essence 2.0

    find x: set of set of set of int(0..9)
    such that |x| = 2

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/42

msetIn.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of msetIn.essence in savilerow causes:

ERROR: 'And' contains something other than a relation:x_Occurrence[v__2]
ERROR: Failed type checking after substituting in lettings.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/16

prob133 - Fatal (typeOf) Undefined reference:

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

./scripts/run/conjure-all-parallel.sh files/EssenceCatalog/prob133.essence

[missing:processStatement] not handled in processStatement topLevel.declaration.given.name.reference := U
                                                           topLevel.declaration.given.typeEnum := []
conjure-repr: There were errors.
    ErrFatal (typeOf) Undefined reference: U
                 Current bindings: &t, U', K, B, v, s
    language ESSENCE 1.2.0

    given U new type enum
    given s: function (total) U --> int(1..)
    given v: function (total) U --> int(1..)
    given B: int(1..)
    given K: int(1..)
    find U': set of U
    such that sum u in U' . s(u) <= B
    such that sum u in U' . v(u) >= K

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/11

nested set literals not refined

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

essence allows nested sets in letting statements such as letting y be {{1,2,3},{1,2,3}} but essence' does not. At moment the these nested sets are not converted hence they do not work in savilerow. Attached is set-of-sets_literal.essence which is an example of nested sets in a letting statement

It is also very slow taking about 15 minutes to run conjure-all on it

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/24

Set of matrixes

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

running the following

language ESSENCE 2.0

letting y be {[2,3,4}}
find x : set (size 1) of matrix indexed by [int(1..3)] of int(2..4)

such that
   forAll i in x . i = y

results in

conjure-all: There were errors.
    ErrFatal "files/testdata/specs/set-matrix.essence" (line 3, column 21):
unexpected }

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/41

lambda.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of testdata/specs/lambda.essence in SavileRow causes:

Successfully parsed 'letting ... be'.
Failed when parsing rest of structure following line:3 column 12
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:26)

Conjure does not change the input file at all

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/31

savilerow Failed when parsing rest of structure

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Crashed when running savilerow with 0001.essence created by

scripts/run/conjure-all-parallel.sh 1.essence

error

Successfully parsed 'such that'.
Failed when parsing rest of structure following line:5 column 9
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:188)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/8

structural-tuple.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Running testsdata/specs/structural-tuple.essence results in

Error in phase: Repr
    ErrFatal (typeOf) Undefined reference: i
                 Current bindings: x
    language Essence 1.3

    find x: set (size 4) of (int(0..9), int(0..9))
    such that forAll (i, j) in x . i = j

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/43

prob010.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Running conjure-all on EssenceCatalog/prob010.essence

Error in phase: Refn
    ErrFatal Cannot determine the type of: topLevel.letting.name.reference := Golfers
                                           topLevel.letting.typeUnnamed.binOp.operator := *
                                           topLevel.letting.typeUnnamed.binOp.left.reference := g
                                           topLevel.letting.typeUnnamed.binOp.right.reference := s
    language ESSENCE 1.2.0

    given w: int(1..)
    given g: int(1..)
    given s: int(1..)
    letting Golfers be new type of size g * s
    find sched: mset (size w) of partition (regular, size g) from Golfers
    find sched_Explicit:
            matrix indexed by [int(1..w)] of partition (regular, size g) from Golfers
    such that
        forAll week1 in sched#Explicit
            . (forAll week2 in sched#Explicit
                   . week1 != week2
                     ->
                     (forAll group1 in parts(week1) , group2 in parts(week2)
                          . |group1 intersect group2| < 2))

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/33

holey-matrix.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Running conjure-all on specs/holey-matrix.essence does not produce any .epime files!

in the .rts file it shows the following error

conjure-all: There were errors.
    ErrFatal not handled in processStatement topLevel.declaration.dim.name.reference := x
                                             topLevel.declaration.dim.domain.domain.matrix.index.domain.int.ranges := []
                                             topLevel.declaration.dim.domain.domain.matrix.inner.domain.matrix.index.domain.int.ranges := []
                                             topLevel.declaration.dim.domain.domain.matrix.inner.domain.matrix.inner.domain.int.ranges := []

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/30

prob024 savilerow Failed when parsing rest of structure

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Crashed when running savilerow with 0002.essence created by

EssenceCatalog/prob024.essence

error

Successfully parsed 'find ... :'.
Failed when parsing rest of structure following line:7 column 9
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:188)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/9

xmatch question

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

When using xMatch on b5.essence

language ESSENCE 2.0

letting sol be [0,1]
find x : int(0..9)

such that
    x != 1

I can get the such that part by using

let Spec _ statements = spec
let res = [ (x) | x@[xMatch|  [Tagged a b] := topLevel.suchThat|] <- statements ]

and the declaration by using

let res = [ (x) | x@[xMatch|  [Tagged a b] := topLevel.declaration|] <- statements ]

why does

let res = [ (x) | x@[xMatch|  [Tagged a b] := topLevel.letting|] <- statements ]

return no results

b5.essence haskell representation

#!haskell
Spec ("ESSENCE",[2,0]) [Tagged "topLevel" [Tagged "letting" [Tagged "name"
[Tagged "reference" [Prim (S "sol")]],Tagged "expr" [Tagged "value" [Tagged
"matrix" [Tagged "values" [Tagged "value" [Tagged "literal" [Prim (I
0)]],Tagged "value" [Tagged "literal" [Prim (I 1)]]]]]]]],Tagged "topLevel"
[Tagged "declaration" [Tagged "find" [Tagged "name" [Tagged "reference" [Prim
(S "x")]],Tagged "domain" [Tagged "domain" [Tagged "int" [Tagged "ranges"
[Tagged "range" [Tagged "fromTo" [Tagged "value" [Tagged "literal" [Prim (I
0)]],Tagged "value" [Tagged "literal" [Prim (I 9)]]]]]]]]]]],Tagged "topLevel"
[Tagged "suchThat" [Tagged "binOp" [Tagged "operator" [Prim (S "!=")],Tagged
"left" [Tagged "reference" [Prim (S "x")]],Tagged "right" [Tagged "value"
[Tagged "literal" [Prim (I 1)]]]]]]]

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/15

prob024.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Running SavileRow on 0001.eprime from EssenceCatalog/prob024.essence

Failed when parsing rest of structure following line:15 column 9
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readPartExpression(EPrimeReader.java:850)
    at savilerow.eprimeparser.EPrimeReader.readExpression(EPrimeReader.java:770)
    at savilerow.eprimeparser.EPrimeReader.readConstraints(EPrimeReader.java:739)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:60)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:26)

on 0002.eprime

Successfully read quantifier up to '.'
Failed when parsing rest of structure following line:10 column 9
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readPartExpression(EPrimeReader.java:850)
    at savilerow.eprimeparser.EPrimeReader.readExpression(EPrimeReader.java:770)
    at savilerow.eprimeparser.EPrimeReader.readConstraints(EPrimeReader.java:739)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:60)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:26)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/34

Output in a separate file the rules applied for each generated file.

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Output in a separate file the rules applied for each generated file.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/10

parse error b2.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

conjure-all.sh on testdata/specs/b2.essence
savilerow on 001.essence.out

Parsed comma.
Failed when parsing rest of structure following line:5 column 61
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:188)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/14

Spec with no constraints

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

language Essence 2.0

find x : set (minSize 1) of set (minSize 1) of int(1..1)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/36

Make identity in quantified expressions explicit

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

forall should be defined as having

(a, b -> a /\ b) as the glueOp
(a, b -> a => b) as the skipOp
true as the identity

do we really need all three?

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/2

Implicit wheres

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

Essence has implicit where statements. Following is the list of implicit wheres that we can think of. This list can possibly grow:

letting id be new type of size e:int
where: e >= 1

Similar, but not an "implicit where": given players new type enum
If there are repeated strings we expect the parser/type checking to spot this.

matrix indexed by [w1(l1..u1),…,wn(ln..un)]
where: li <= ui for all 1 <= i <= n
_We're getting rid of this as per Ozgur's example of refining a possibly
empty set._

annotations (size e:int), (maxSize e:int), (minSize e:int),
(partSize e:int)
where: e >= 0

function variable constructors (see p19).
function(e1 -> e1', …, en -> en')
where: alldiff(ei) - not quite because we allow duplicate mappings. So:
forall i, j:int(1..n) . i != j -> (ei' = ej' -> ei != ej)

partition(e1, …, en) (see p18,19)
where: forall i, j:int(1..n) . i != j -> (ei intersection ej = empty set)

????
given players new type enum
given a: players, b: players
find aBoyNamedSue: players(a..b)
where: a < b

p12 maxOccur a, minOccur b
where: a >= 0, b >= 0

p14, partition annotations:
numParts n (n should be greater than or equal to 0)
partSize m (m should be greater than or equal to 0)

NB We explicitly say that elements of a set constructed this way are not required to be distinct. Similarly for relations. Duplicate mappings for functions are ignored.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/4

matrix-of-set.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of matrix-of-set.essence in SavileRow causes:

Successfully parsed 'matrix indexed by ... of'.
Failed when parsing rest of structure following line:3 column 40
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:188)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/21

nesting.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

When using any of the .eprime files of specs/nesting.essence in savilerow
errors occur

***  files/testdata/specs/nesting/0002.eprime  ***
Successfully parsed 'matrix indexed by ... of'.
Failed when parsing rest of structure following line:5 column 46
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:26)

nesting.log contains the error for each .eprime file

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/25

set-of-sets.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of set-of-sets.essence in SavileRow causes:

Successfully read quantifier up to '.'
Failed when parsing rest of structure following line:17 column 9
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:26)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/23

enum1.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of testdata/specs/enum1.essence in SavileRow causes:

Successfully parsed 'letting ... be'.
Failed when parsing rest of structure following line:3 column 12
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:26)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/27

domains literals are not refined

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

The domain literals involving union are not refined

(b6.essence in testdata/specs/)

language ESSENCE 2.0
find y : set (maxSize 2) of int({8,3} union {2,7})

such that
    {2,7, 8} subset y

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/26

from alan 24

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

#!
    Bilalh $ ./run-all-out.sh EssenceCatalog/fromAlan/prob024.essence
repr my/24.essence
[representation] find seq: function (total) Index --> Num
                 (#2) AsReln, Matrix1D
[created file] my/24.essence-repr/0001.essence
[created file] my/24.essence-repr/0002.essence
conjure-refn: There were errors.
    ErrFatal Cannot determine the type of: functionApply.actual.reference := preimage
                                           functionApply.args.reference := seq#Matrix1D
                                           functionApply.args.structural.single.reference := m
    language ESSENCE' 1.0

    given k: int(1..)
    given n: int(1..)
    letting Index be domain int(1..k * n)
    letting Num be domain int(1..n)
    find seq: function (total) Index --> Num
    find seq_Matrix1D: matrix indexed by [Index] of Num
    such that
        forAll m : Num
            . (exists s : function (total, injective) int(1..k) --> Index
                   . (forAll i : Index
                          . i in range(s) <-> i in preimage(seq#Matrix1D, m))
                     /\
                     (forAll j : int(1..k - 1) . s(j + 1) - s(j) = m))

    topLevel.declaration.given.name.reference := k
    topLevel.declaration.given.domain.domain.int.ranges.range.from.value.literal := 1
    topLevel.declaration.given.name.reference := n
    topLevel.declaration.given.domain.domain.int.ranges.range.from.value.literal := 1
    topLevel.letting.name.reference := Index
    topLevel.letting.domain.domain.int.ranges.range.fromTo.value.literal := 1
    topLevel.letting.domain.domain.int.ranges.range.fromTo.binOp.operator := *
    topLevel.letting.domain.domain.int.ranges.range.fromTo.binOp.left.reference := k
    topLevel.letting.domain.domain.int.ranges.range.fromTo.binOp.right.reference := n
    topLevel.letting.name.reference := Num
    topLevel.letting.domain.domain.int.ranges.range.fromTo.value.literal := 1
    topLevel.letting.domain.domain.int.ranges.range.fromTo.reference := n
    topLevel.declaration.find.name.reference := seq
    topLevel.declaration.find.domain.domain.function.attributes.attrCollection.attribute.name.reference := total
    topLevel.declaration.find.domain.domain.function.innerFrom.reference := Index
    topLevel.declaration.find.domain.domain.function.innerTo.reference := Num
    topLevel.declaration.find.name.reference := seq_Matrix1D
    topLevel.declaration.find.domain.domain.matrix.index.reference := Index
    topLevel.declaration.find.domain.domain.matrix.inner.reference := Num
    topLevel.suchThat.quantified.quantifier.reference := forAll
    topLevel.suchThat.quantified.quanVar.structural.single.reference := m
    topLevel.suchThat.quantified.quanOverDom.reference := Num
    topLevel.suchThat.quantified.quanOverOp := []
    topLevel.suchThat.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.quantified.quantifier.reference := exists
    topLevel.suchThat.quantified.body.quantified.quanVar.structural.single.reference := s
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.attributes.attrCollection.attribute.name.reference := total
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.attributes.attrCollection.attribute.name.reference := injective
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.innerFrom.domain.int.ranges.range.fromTo.value.literal := 1
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.innerFrom.domain.int.ranges.range.fromTo.reference := k
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.innerTo.reference := Index
    topLevel.suchThat.quantified.body.quantified.quanOverOp := []
    topLevel.suchThat.quantified.body.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.body.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.operator := /\
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quantifier.reference := forAll
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quanVar.structural.single.reference := i
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quanOverDom.reference := Index
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quanOverOp := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.operator := <->
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.left.binOp.operator := in
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.left.binOp.left.structural.single.reference := i
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.left.binOp.right.operator.range.structural.single.reference := s
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.operator := in
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.left.structural.single.reference := i
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.right.functionApply.actual.reference := preimage
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.right.functionApply.args.reference := seq#Matrix1D
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.right.functionApply.args.structural.single.reference := m
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quantifier.reference := forAll
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanVar.structural.single.reference := j
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverDom.domain.int.ranges.range.fromTo.value.literal := 1
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverDom.domain.int.ranges.range.fromTo.binOp.operator := -
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverDom.domain.int.ranges.range.fromTo.binOp.left.reference := k
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverDom.domain.int.ranges.range.fromTo.binOp.right.value.literal := 1
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverOp := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.operator := =
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.operator := -
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.left.functionApply.actual.structural.single.reference := s
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.left.functionApply.args.binOp.operator := +
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.left.functionApply.args.binOp.left.structural.single.reference := j
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.left.functionApply.args.binOp.right.value.literal := 1
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.right.functionApply.actual.structural.single.reference := s
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.right.functionApply.args.structural.single.reference := j
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.right.structural.single.reference := m
refn my/24.essence-repr/0002.essence
[applied] i in range(s)
          {rules/refns/set-in-to-quantified.rule}
              (exists v__1 in range(s) . v__1 = i)
conjure-refn: There were errors.
    ErrFatal Cannot determine the type of: functionApply.actual.reference := preimage
                                           functionApply.args.reference := seq#AsReln
                                           functionApply.args.structural.single.reference := m
    language ESSENCE' 1.0

    given k: int(1..)
    given n: int(1..)
    letting Index be domain int(1..k * n)
    letting Num be domain int(1..n)
    find seq: function (total) Index --> Num
    find seq_AsReln: relation of (Index * Num)
    such that
        forAll m : Num
            . (exists s : function (total, injective) int(1..k) --> Index
                   . (forAll i : Index
                          . i in range(s) <-> i in preimage(seq#AsReln, m))
                     /\
                     (forAll j : int(1..k - 1) . s(j + 1) - s(j) = m))
    such that
        forAll v__1 : Index
            . (sum v__2 in toSet(seq_AsReln) . v__1 = v__2[1]) = 1

    topLevel.declaration.given.name.reference := k
    topLevel.declaration.given.domain.domain.int.ranges.range.from.value.literal := 1
    topLevel.declaration.given.name.reference := n
    topLevel.declaration.given.domain.domain.int.ranges.range.from.value.literal := 1
    topLevel.letting.name.reference := Index
    topLevel.letting.domain.domain.int.ranges.range.fromTo.value.literal := 1
    topLevel.letting.domain.domain.int.ranges.range.fromTo.binOp.operator := *
    topLevel.letting.domain.domain.int.ranges.range.fromTo.binOp.left.reference := k
    topLevel.letting.domain.domain.int.ranges.range.fromTo.binOp.right.reference := n
    topLevel.letting.name.reference := Num
    topLevel.letting.domain.domain.int.ranges.range.fromTo.value.literal := 1
    topLevel.letting.domain.domain.int.ranges.range.fromTo.reference := n
    topLevel.declaration.find.name.reference := seq
    topLevel.declaration.find.domain.domain.function.attributes.attrCollection.attribute.name.reference := total
    topLevel.declaration.find.domain.domain.function.innerFrom.reference := Index
    topLevel.declaration.find.domain.domain.function.innerTo.reference := Num
    topLevel.declaration.find.name.reference := seq_AsReln
    topLevel.declaration.find.domain.domain.relation.attributes.attrCollection := []
    topLevel.declaration.find.domain.domain.relation.inners.reference := Index
    topLevel.declaration.find.domain.domain.relation.inners.reference := Num
    topLevel.suchThat.quantified.quantifier.reference := forAll
    topLevel.suchThat.quantified.quanVar.structural.single.reference := m
    topLevel.suchThat.quantified.quanOverDom.reference := Num
    topLevel.suchThat.quantified.quanOverOp := []
    topLevel.suchThat.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.quantified.quantifier.reference := exists
    topLevel.suchThat.quantified.body.quantified.quanVar.structural.single.reference := s
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.attributes.attrCollection.attribute.name.reference := total
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.attributes.attrCollection.attribute.name.reference := injective
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.innerFrom.domain.int.ranges.range.fromTo.value.literal := 1
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.innerFrom.domain.int.ranges.range.fromTo.reference := k
    topLevel.suchThat.quantified.body.quantified.quanOverDom.domain.function.innerTo.reference := Index
    topLevel.suchThat.quantified.body.quantified.quanOverOp := []
    topLevel.suchThat.quantified.body.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.body.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.operator := /\
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quantifier.reference := forAll
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quanVar.structural.single.reference := i
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quanOverDom.reference := Index
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quanOverOp := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.operator := <->
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.left.binOp.operator := in
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.left.binOp.left.structural.single.reference := i
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.left.binOp.right.operator.range.structural.single.reference := s
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.operator := in
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.left.structural.single.reference := i
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.right.functionApply.actual.reference := preimage
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.right.functionApply.args.reference := seq#AsReln
    topLevel.suchThat.quantified.body.quantified.body.binOp.left.quantified.body.binOp.right.binOp.right.functionApply.args.structural.single.reference := m
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quantifier.reference := forAll
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanVar.structural.single.reference := j
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverDom.domain.int.ranges.range.fromTo.value.literal := 1
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverDom.domain.int.ranges.range.fromTo.binOp.operator := -
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverDom.domain.int.ranges.range.fromTo.binOp.left.reference := k
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverDom.domain.int.ranges.range.fromTo.binOp.right.value.literal := 1
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverOp := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.operator := =
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.operator := -
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.left.functionApply.actual.structural.single.reference := s
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.left.functionApply.args.binOp.operator := +
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.left.functionApply.args.binOp.left.structural.single.reference := j
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.left.functionApply.args.binOp.right.value.literal := 1
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.right.functionApply.actual.structural.single.reference := s
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.left.binOp.right.functionApply.args.structural.single.reference := j
    topLevel.suchThat.quantified.body.quantified.body.binOp.right.quantified.body.binOp.right.structural.single.reference := m
    topLevel.suchThat.quantified.quantifier.reference := forAll
    topLevel.suchThat.quantified.quanVar.structural.single.reference := v__1
    topLevel.suchThat.quantified.quanOverDom.reference := Index
    topLevel.suchThat.quantified.quanOverOp := []
    topLevel.suchThat.quantified.quanOverExpr := []
    topLevel.suchThat.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.binOp.operator := =
    topLevel.suchThat.quantified.body.binOp.left.quantified.quantifier.reference := sum
    topLevel.suchThat.quantified.body.binOp.left.quantified.quanVar.structural.single.reference := v__2
    topLevel.suchThat.quantified.body.binOp.left.quantified.quanOverDom := []
    topLevel.suchThat.quantified.body.binOp.left.quantified.quanOverOp.binOp.in := []
    topLevel.suchThat.quantified.body.binOp.left.quantified.quanOverExpr.operator.toSet.reference := seq_AsReln
    topLevel.suchThat.quantified.body.binOp.left.quantified.guard.emptyGuard := []
    topLevel.suchThat.quantified.body.binOp.left.quantified.body.binOp.operator := =
    topLevel.suchThat.quantified.body.binOp.left.quantified.body.binOp.left.structural.single.reference := v__1
    topLevel.suchThat.quantified.body.binOp.left.quantified.body.binOp.right.operator.index.left.structural.single.reference := v__2
    topLevel.suchThat.quantified.body.binOp.left.quantified.body.binOp.right.operator.index.right.value.literal := 1
    topLevel.suchThat.quantified.body.binOp.right.value.literal := 1
refn my/24.essence-repr/0001.essence
[applied] i in range(s)
          {rules/refns/set-in-to-quantified.rule}
              (exists v__1 in range(s) . v__1 = i)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/7

Parsing large files is slow

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

See the attached file for an example. It takes 50 seconds to parse on my machine.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/44

enum2.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Running conjure-all on specs/enum2.essence does not produce any .epime files!

in the .rts file it shows the following error

conjure-all: There were errors.
    ErrFatal not handled in processStatement topLevel.declaration.given.name.reference := e
                                             topLevel.declaration.given.typeEnum := []

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/28

Essence evaluator

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

It is time to implement the partial evaluator for Essence. The actual implementation will just be lifted from the old codebase, so shouldn't take too long.

Also add it to repl, to see repl in action.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/1

prob007.essence never finishes

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

running prob007.essence never finishes (run for 7 hours by mistake)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/12

Eating 30GB of memory

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

Bilal claims running conjure on files/testdata/specs/set-of-sets_nested_literals2.essence creates 30GB swap files.

Will try to reproduce then report back.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/37

Earlier detection of missing rules

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

If the repr phase chooses a representation for an abstract variable, that abstract variable should be removed in the next refn phase. Because all use sites of it will be refined.

So, after refn, check if the spec contains any tagged identifiers. Like x#Occurrence.

If it does, there must be a missing rule application, better stop and report an error.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/6

eprime files taking over 7 minutes to read using readSpec

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using this code to read 001.eprime of set-of-sets_nested_literals9.essence

pair <-  pairWithContents filepath
[spec]   <- runCompEIO (readSpec pair)

take over 7 minutes (I gave up waiting). The .eprime file is over 600 lines long

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/40

stack overflow

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

In addition to the previous files I sent by email

language ESSENCE 2.0

letting y be `1`
find x : set(size 1) of set (minSize 1, maxSize 2) of set (minSize 1, maxSize 2) of int(1..1)

such that
    y subsetEq x

also causes a stack overflow

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/38

Massive space usage

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Needed to use -K100M to run and also took over 1GB of heap space to produce a single `.eprime' file

language ESSENCE 2.0

letting y be `2,3},{2`
find x : set(minSize 0, maxSize 1) of set (minSize 1, maxSize 2) of set (minSize 1, maxSize 2) of int(2..3)

such that
    y subsetEq x


 569,167,862,984 bytes allocated in the heap
 111,936,191,488 bytes copied during GC
     452,372,080 bytes maximum residency (2034 sample(s))
       6,857,352 bytes maximum slop
            1249 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     1105565 colls,   0 par   108.90s  110.37s    0.0001s    0.1623s
  Gen  1      2034 colls,     0 par   55.58s   56.64s     0.0278s    0.5691s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time  211.52s  (213.84s elapsed)
  GC      time  164.47s  (167.01s elapsed)
  EXIT    time    0.01s  (  0.09s elapsed)
  Total   time  376.00s  (380.94s elapsed)

  %GC     time      43.7%  (43.8% elapsed)

  Alloc rate    2,690,890,863 bytes per MUT second

  Productivity  56.3% of total user, 55.5% of total elapsed

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/39

mmt.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of mmt.essence in savilerow causes

Successfully parsed 'matrix indexed by ... of'.
Failed when parsing rest of structure following line:3 column 53
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readDomain(EPrimeReader.java:521)
    at savilerow.eprimeparser.EPrimeReader.readFind(EPrimeReader.java:360)
    at savilerow.eprimeparser.EPrimeReader.readDeclaration(EPrimeReader.java:218)
    at savilerow.eprimeparser.EPrimeReader.readDeclarations(EPrimeReader.java:180)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:52)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:188)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/18

Singleton tuple

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

What the syntax for a Singleton tuple

If I write letting d be (3) I get

[Tagged Tstatement
   [Tagged Tthis
      [Tagged TtopLevel
         [Tagged Tletting
            [Tagged Tname [Tagged Treference [Prim (S "d")]],
             Tagged Texpr [Tagged Tvalue [Tagged Tliteral [Prim (I 3)]]]]]]

If I do find a : tuple (int(0..9)) it is refined to

find a_tuple1: int(0..9)

and solved to be

letting a_tuple1 be 1

I tried using

[Tagged TtopLevel
   [Tagged Tletting
      [Tagged Texpr
         [Tagged Tvalue
            [Tagged Ttuple
               [Tagged Tvalues [Tagged Tvalue [Tagged Tliteral [Prim (I 1)]]]]]],
       Tagged Tname [Tagged Treference [Prim (S "a")]]]]

but this results in letting a be tuple (1).

Is this correct?

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/48

interactive mode should make use of ResolveTwoBars

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

it really should.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/3

mms.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of testdata/specs/mms.essence in SavileRow causes:

ERROR: Matrix index out of bounds: mms_Explicit[3, -3, 0]
ERROR: Index 0 is out of bounds: 3 is not between 0 and 2
ERROR: Note that matrix indices may have been shifted to start at 0 if they did not in the input file.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/32

matrix-indby-enum.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of matrix-indby-enum.essence in SavileRow causes:

Successfully parsed 'given' keyword.
Failed when parsing rest of structure following line:3 column 5
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:77)
    at savilerow.eprimeparser.EPrimeReader.readDeclaration(EPrimeReader.java:200)
    at savilerow.eprimeparser.EPrimeReader.readDeclarations(EPrimeReader.java:180)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:52)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:188)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/20

unused tuple not refined

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

running tuple2.essence shown below


language Essence 2.0

letting c be (1,2)

find a : tuple (int(0..9))
find b : tuple (int(0..9),int(3..8))

such that
    a[1] = 1,
    b[1] = 2,
    b[2] = 3,

produces


language ESSENCE' 1.0

letting c be (1, 2)
find a_tuple1: int(0..9)
find b_tuple1: int(0..9)
find b_tuple2: int(3..8)
such that
    a_tuple1 = 1,
    b_tuple1 = 2,
    b_tuple2 = 3

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/47

tuple err

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

err when running tuple.essence (shown below)

language Essence 2.0

letting c be (1,2)

find a : tuple (int(0..9))
find b : tuple (int(0..9),int(3..8))

such that
    a[1] = 1,
    b = c

err

Error in phase: Groom
    (typeOf) Undefined reference: b
        Current bindings: b_tuple2,
                          b_tuple2,
                          b_tuple1,
                          b_tuple1,
                          a_tuple1,
                          a_tuple1,
                          c,
                          c

log

[removedDecl] a
[removedDecl] b

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/46

variables from constants

Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)

for example the following:

language Essence 1.3

find x : int(0..9)

such that |{1,x}| = x

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/5

tuple of set not refined

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

The set in the below example is not refined

language Essence 2.0


find a : tuple (int(0..9))
find b : tuple (int(0..9),int(3..8),set of int(3..4) )

such that
    a[1] = 1,
    b[1] = 2,
    b[2] = 3

and create the following

language ESSENCE' 1.0

find a_tuple1: int(0..9)
find b_tuple1: int(0..9)
find b_tuple2: int(3..8)
find b_tuple3: set of int(3..4)
such that
    a_tuple1 = 1,
    b_tuple1 = 2,
    b_tuple2 = 3

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/49

Conjure much slower on n.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

using n.essence shown below

language Essence 2.0

find x : set (minSize 2) of set of int(1..4)

such that
    forAll y in x . (sum i in y . i) = 4

On the 6th on Nov this ran in just over 2 minutes and produced 11 .eprime files.

 205,158,156,432 bytes allocated in the heap
  41,567,415,240 bytes copied during GC
      30,410,240 bytes maximum residency (1309 sample(s))
         550,600 bytes maximum slop
              85 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     397618 colls,     0 par   44.53s   45.09s     0.0001s    0.0043s
  Gen  1      1309 colls,     0 par   21.51s   21.81s     0.0167s    0.0526s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time   72.61s  ( 73.48s elapsed)
  GC      time   66.03s  ( 66.91s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time  138.64s  (140.39s elapsed)

  %GC     time      47.6%  (47.7% elapsed)

  Alloc rate    2,825,420,424 bytes per MUT second

  Productivity  52.4% of total user, 51.7% of total elapsed

Running it for 7 minutes it still has not produced any .eprime files. I attached n_old.zip which contains all the previously refined .eprime files and the log

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/50

msetEq.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of msetEq.essence in savilerow causes:

ERROR: Implication contains non-relation expression:x_Occurrence[v__6]
ERROR: Failed type checking after substituting in lettings.

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/17

mset repr

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

At the moment sets and msets uses the same suffix when they are refined to a matrix.

e.g find x_Explicit

Could you add a way to tell them apart?

e.g find x_MExplicit for a mset

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/22

function1.essence Unknown tag: hist

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

running function1.essence result in the error Unknown tag: hist

conjure-all: Unknown tag: hist
  76,501,150,776 bytes allocated in the heap
  14,420,016,024 bytes copied during GC
      56,740,872 bytes maximum residency (251 sample(s))
       1,013,800 bytes maximum slop
             162 MB total memory in use (0 MB lost due to fragmentation)

                                    Tot time (elapsed)  Avg pause  Max pause
  Gen  0     148256 colls,     0 par   13.63s   13.82s     0.0001s    0.0010s
  Gen  1       251 colls,     0 par    5.83s    6.00s     0.0239s    0.0815s

  INIT    time    0.00s  (  0.00s elapsed)
  MUT     time   27.99s  ( 28.35s elapsed)
  GC      time   19.46s  ( 19.81s elapsed)
  EXIT    time    0.00s  (  0.00s elapsed)
  Total   time   47.45s  ( 48.17s elapsed)

  %GC     time      41.0%  (41.1% elapsed)

  Alloc rate    2,732,776,578 bytes per MUT second

  Productivity  59.0% of total user, 58.1% of total elapsed

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/45

Set not refined

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

in files/testdata/specs/sets_not_refined.essence one of the sets are not refined.

See 002.eprime which is attached since running conjure-all on sets_not_refined.essence take a very long time.

find x_ExplicitVarSize_tuple1: matrix indexed by [int(1..2 ** 4)] of bool
find x_ExplicitVarSize_tuple2:
        matrix indexed by [int(1..2 ** 4)] of set of int(1..4)
find x_ExplicitVarSize_tuple2_Occurrence:
        matrix indexed by [int(1..2 ** 4), int(1..4)] of bool
find x_ExplicitVarSize_tuple2_ExplicitVarSize_tuple1:
        matrix indexed by [int(1..2 ** 4), int(1..4)] of bool
find x_ExplicitVarSize_tuple2_ExplicitVarSize_tuple2:
        matrix indexed by [int(1..2 ** 4), int(1..4)] of int(1..4)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/35

forall-0.essence

Originally reported by: Bilal Hussain (Bitbucket: Bilalh, GitHub: Bilalh)

Using 0001.eprime of testdata/specs/forall-0.essence in SavileRow causes:

Successfully parsed 'letting ... be'.
Failed when parsing rest of structure following line:7 column 19
Exception in thread "main" java.lang.AssertionError
    at savilerow.eprimeparser.EPrimeTokenizer.reset(EPrimeTokenizer.java:89)
    at savilerow.eprimeparser.EPrimeReader.readModel(EPrimeReader.java:64)
    at savilerow.EPrimeTailor.main(EPrimeTailor.java:26)

Bitbucket: https://bitbucket.org/stacs_cp/conjure-old/issue/29

conjure-cp / conjure Goto Github PK

conjure's People

Contributors

Stargazers

Watchers

Forkers

conjure's Issues

Recommend Projects

Recommend Topics

Recommend Org