conjure-cp / conjure Goto Github PK
View Code? Open in Web Editor NEWConjure: The Automated Constraint Modelling Tool
License: Other
Conjure: The Automated Constraint Modelling Tool
License: Other
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.
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)
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)
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
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
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 := []
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.
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?
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.
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
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)
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)
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)
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
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
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)
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
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)
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
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)
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.
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)
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
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)
Originally reported by: Özgür Akgün (Bitbucket: ozgurakgun, GitHub: ozgurakgun)
forall should be defined as having
do we really need all three?
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
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)
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.
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 }
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
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)
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)]]]]]]]
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
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))
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)
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)
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
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
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 := []
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.
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.
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
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.