Skip to content

Commit

Permalink
Add absolute values and convert to Minion
Browse files Browse the repository at this point in the history
Add support for absolute values, in particular:

* Parsing from JSON.
* The `Abs` expression variant.
* The `FlatAbsEq` Minion constraint.
* Flattening and conversion to Minion.

As part of this change, a division domain bug is fixed. In our domain
calculation we use truncating division, the default Rust integer
division operator. However, the semantics of Essence Prime specify floor
division.

Truncating division has the effect of rounding towards 0.

Truncating division does `-5 / 2 =-2` and `5/2 = 2`. However, we want
`-5/2 = -3` and `5/2 = 2`.

This caused the domains of variables containing negative divisions to
sometimes be one too high. For abs-03, this caused Oxide to give
different solutions than Conjure.
  • Loading branch information
niklasdewally committed Jan 10, 2025
1 parent 3f12c25 commit eaf65ad
Show file tree
Hide file tree
Showing 38 changed files with 2,332 additions and 5 deletions.
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
use_native_parser=false
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
Model before rewriting:

find x: int(-2..3)

such that

(|x| = 1)

--

(|x| = 1),
~~> introduce_abseq ([("Minion", 4400)])
AbsEq(1,x)

--

Final model:

find x: int(-2..3)

such that

AbsEq(1,x)

Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
language ESSENCE' 1.0

find x : int(-2..3)

such that
|x| = 1
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
[
{
"x": -1
},
{
"x": 1
}
]
Original file line number Diff line number Diff line change
@@ -0,0 +1,66 @@
{
"constraints": [
{
"Eq": [
{
"clean": false,
"etype": null
},
{
"Abs": [
{
"clean": false,
"etype": null
},
{
"Atomic": [
{
"clean": false,
"etype": null
},
{
"Reference": {
"UserName": "x"
}
}
]
}
]
},
{
"Atomic": [
{
"clean": false,
"etype": null
},
{
"Literal": {
"Int": 1
}
}
]
}
]
}
],
"next_var": 0,
"variables": [
[
{
"UserName": "x"
},
{
"domain": {
"IntDomain": [
{
"Bounded": [
-2,
3
]
}
]
}
}
]
]
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
{
"constraints": [
{
"FlatAbsEq": [
{
"clean": false,
"etype": null
},
{
"Literal": {
"Int": 1
}
},
{
"Reference": {
"UserName": "x"
}
}
]
}
],
"next_var": 0,
"variables": [
[
{
"UserName": "x"
},
{
"domain": {
"IntDomain": [
{
"Bounded": [
-2,
3
]
}
]
}
}
]
]
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
run_solver=true
use_native_parser=false
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
Model before rewriting:

find x: int(-5..5)
find y: int(-5..5)

such that

(Sum([|x|, |y|]) = 10)

--

Sum([|x|, |y|]),
~~> flatten_vecop ([("Minion", 4200)])
Sum([__0, __1])
new variables:
__0: int(0..5)
__1: int(0..5)
new constraints:
__0 =aux |x|
__1 =aux |y|
--

__0 =aux |x|,
~~> introduce_abseq ([("Minion", 4400)])
AbsEq(__0,x)

--

__1 =aux |y|,
~~> introduce_abseq ([("Minion", 4400)])
AbsEq(__1,y)

--

(Sum([__0, __1]) = 10),
~~> sum_eq_to_inequalities ([("Minion", 4100)])
And([(Sum([__0, __1]) <= 10), (Sum([__0, __1]) >= 10)])

--

(Sum([__0, __1]) <= 10),
~~> introduce_sumleq ([("Minion", 4400)])
SumLeq([__0, __1], 10)

--

(Sum([__0, __1]) >= 10),
~~> introduce_sumgeq ([("Minion", 4400)])
SumGeq([__0, __1], 10)

--

Final model:

find x: int(-5..5)
find y: int(-5..5)
find __0: int(0..5)
find __1: int(0..5)

such that

And([SumLeq([__0, __1], 10), SumGeq([__0, __1], 10)]),
AbsEq(__0,x),
AbsEq(__1,y)

Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
language ESSENCE' 1.0

find x,y: int(-5..5)

such that |x| + |y| = 10
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
[
{
"__0": 5,
"__1": 5,
"x": -5,
"y": -5
},
{
"__0": 5,
"__1": 5,
"x": -5,
"y": 5
},
{
"__0": 5,
"__1": 5,
"x": 5,
"y": -5
},
{
"__0": 5,
"__1": 5,
"x": 5,
"y": 5
}
]
Original file line number Diff line number Diff line change
@@ -0,0 +1,114 @@
{
"constraints": [
{
"Eq": [
{
"clean": false,
"etype": null
},
{
"Sum": [
{
"clean": false,
"etype": null
},
[
{
"Abs": [
{
"clean": false,
"etype": null
},
{
"Atomic": [
{
"clean": false,
"etype": null
},
{
"Reference": {
"UserName": "x"
}
}
]
}
]
},
{
"Abs": [
{
"clean": false,
"etype": null
},
{
"Atomic": [
{
"clean": false,
"etype": null
},
{
"Reference": {
"UserName": "y"
}
}
]
}
]
}
]
]
},
{
"Atomic": [
{
"clean": false,
"etype": null
},
{
"Literal": {
"Int": 10
}
}
]
}
]
}
],
"next_var": 0,
"variables": [
[
{
"UserName": "x"
},
{
"domain": {
"IntDomain": [
{
"Bounded": [
-5,
5
]
}
]
}
}
],
[
{
"UserName": "y"
},
{
"domain": {
"IntDomain": [
{
"Bounded": [
-5,
5
]
}
]
}
}
]
]
}
Loading

0 comments on commit eaf65ad

Please sign in to comment.