Skip to content

Commit

Permalink
Add structural constraints as where statements for givens, so Conjure…
Browse files Browse the repository at this point in the history
… can complain about invalid instance data (ref #446)
  • Loading branch information
ozgurakgun committed Nov 22, 2022
1 parent f11a093 commit 65c3a8c
Show file tree
Hide file tree
Showing 6 changed files with 13 additions and 2 deletions.
3 changes: 1 addition & 2 deletions src/Conjure/UI/Model.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1776,13 +1776,12 @@ rule_ChooseRepr config = Rule "choose-repr" (const theRule) where
addStructurals :: (MonadLog m, MonadFailDoc m, NameGen m, EnumerateDomain m)
=> Model -> m Model
addStructurals
| forg == Given = return
| usedBefore = return
| otherwise = \ m -> do
structurals <- mkStructurals
return $ if null structurals
then m
else m { mStatements = mStatements m ++ [SuchThat structurals] }
else m { mStatements = mStatements m ++ [SuchThat structurals | forg == Find] ++ [Where structurals | forg == Given] }

channels =
[ make opEq this that
Expand Down
1 change: 1 addition & 0 deletions tests/custom/issues/446/inst.param
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
letting s be sequence(1,2,3,4,5)
1 change: 1 addition & 0 deletions tests/custom/issues/446/model.essence
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
given s: sequence (size 5, surjective) of int(1..10)
3 changes: 3 additions & 0 deletions tests/custom/issues/446/run.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
rm -rf conjure-output
conjure solve model.essence inst.param
rm -rf conjure-output *.solution
3 changes: 3 additions & 0 deletions tests/custom/issues/446/stderr.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Error:
Invalid instance, a where statement evaluated to false.
(It can be an implicit where statement added by Conjure.)
4 changes: 4 additions & 0 deletions tests/custom/issues/446/stdout.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Generating models for model.essence
Generated models: model000001.eprime
Saved under: conjure-output
Savile Row: model000001.eprime inst.param

0 comments on commit 65c3a8c

Please sign in to comment.