Skip to content

Commit

Permalink
Merge pull request #606 from conjure-cp/streamlining
Browse files Browse the repository at this point in the history
Streamlining
  • Loading branch information
ozgurakgun committed Nov 9, 2023
2 parents 4b1ac0a + b6161f6 commit a378f2f
Show file tree
Hide file tree
Showing 23 changed files with 1,567 additions and 10 deletions.
1 change: 1 addition & 0 deletions conjure-cp.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -157,6 +157,7 @@ Library
, Conjure.Process.LettingsForComplexInDoms
, Conjure.Process.Boost
, Conjure.Process.Sanity
, Conjure.Process.Streamlining
, Conjure.Process.Unnameds
, Conjure.Process.ValidateConstantForDomain

Expand Down
14 changes: 14 additions & 0 deletions docs/conjure-help.html
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,8 @@
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--choices=FILE</td><td style='padding-left:2ex;'>Choices to use for -al, either an eprime file (created by --log-choices), or a json file.</td></tr>
<tr><td colspan='3'>General:</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--limit-time=INT</td><td style='padding-left:2ex;'>Limit in seconds of real time.</td></tr>
<tr><td colspan='3'>Streamlining:</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--generate-streamliners=ITEM</td><td style='padding-left:2ex;'>A comma separated list of integers.<br />If provided, the streamlining constraints that correspond to the given integers will be generated.<br />Run "conjure streamlining ESSENCE_FILE" to generate a list of all applicable streamliners.</td></tr>
<tr><td colspan='3'>&nbsp;</tr>
<tr><td colspan='3'>conjure translate-parameter [OPTIONS]</td></tr>
<tr><td colspan='3' style='padding-left:2ex;'>Refinement of Essence parameter files for a particular Essence' model.<br />The model needs to be generated by Conjure.</td></tr>
Expand Down Expand Up @@ -136,6 +138,8 @@
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--savilerow-options=ITEM</td><td style='padding-left:2ex;'>Options passed to Savile Row.</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--solver-options=ITEM</td><td style='padding-left:2ex;'>Options passed to the backend solver.</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--solver=ITEM</td><td style='padding-left:2ex;'>Backend solver. Possible values:<br /> - minion (CP solver)<br /> - gecode (CP solver)<br /> - chuffed (CP solver)<br /> - or-tools (CP solver)<br /> - glucose (SAT solver)<br /> - glucose-syrup (SAT solver)<br /> - lingeling/plingeling/treengeling (SAT solver)<br /> - cadical (SAT solver)<br /> - kissat (SAT solver)<br /> - minisat (SAT solver)<br /> - bc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)<br /> - nbc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)<br /> - open-wbo (MaxSAT solver, only works with optimisation problems)<br /> - coin-or (MIP solver, implemented via MiniZinc)<br /> - cplex (MIP solver, implemented via MiniZinc)<br /> - boolector (SMT solver, supported logics: bv)<br /> - yices (SMT solver, supported logics: bv, lia, idl)<br /> - z3 (SMT solver, supported logics: bv, lia, nia, idl)<br />Default: minion<br /><br />Default logic for SMT solvers is bitvector (bv).<br />Append a dash and the name of a logic to the solver name to choose a different logic. For example yices-idl.</td></tr>
<tr><td colspan='3'>Streamlining:</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--generate-streamliners=ITEM</td><td style='padding-left:2ex;'>A comma separated list of integers.<br />If provided, the streamlining constraints that correspond to the given integers will be generated.<br />Run "conjure streamlining ESSENCE_FILE" to generate a list of all applicable streamliners.</td></tr>
<tr><td colspan='3'>&nbsp;</tr>
<tr><td colspan='3'>conjure ide [OPTIONS] ESSENCE_FILE</td></tr>
<tr><td colspan='3' style='padding-left:2ex;'>IDE support features for Conjure.<br />Not intended for direct use.</td></tr>
Expand Down Expand Up @@ -239,6 +243,16 @@
<tr><td colspan='3'>General:</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--limit-time=INT</td><td style='padding-left:2ex;'>Time limit in seconds (real time).</td></tr>
<tr><td colspan='3'>&nbsp;</tr>
<tr><td colspan='3'>conjure streamlining [OPTIONS] ESSENCE_FILE</td></tr>
<tr><td colspan='3' style='padding-left:2ex;'>Generate streamlined Essence models.</td></tr>
<tr><td colspan='3'>&nbsp;</tr>
<tr><td colspan='3'>Logging &amp; Output:</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--log-level=LOGLEVEL</td><td style='padding-left:2ex;'>Log level.</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--output-format=FORMAT</td><td style='padding-left:2ex;'>Conjure's output can be in multiple formats.<br /> plain : The default<br /> binary: A binary encoding of the Essence output.<br /> It can be read back in by Conjure.<br /> json : A json encoding of the Essence output.<br /> It can be used by other tools integrating with Conjure<br /> in order to avoid having to parse textual Essence.</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--line-width=INT</td><td style='padding-left:2ex;'>Line width to use during pretty printing.<br />Default: 120</td></tr>
<tr><td colspan='3'>General:</td></tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--limit-time=INT</td><td style='padding-left:2ex;'>Time limit in seconds (real time).</td></tr>
<tr><td colspan='3'>&nbsp;</tr>
<tr><td colspan='3'>conjure lsp [OPTIONS]</td></tr>
<tr><td colspan='3'>&nbsp;</tr>
<tr><td style='padding-left:2ex;'>&nbsp;<td style='padding-left:1ex; white-space:nowrap;'>--loglevel=LOGLEVEL</td><td style='padding-left:2ex;'>&nbsp;</tr>
Expand Down
29 changes: 29 additions & 0 deletions docs/conjure-help.txt
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,12 @@
--log-choices), or a json file.
General:
--limit-time=INT Limit in seconds of real time.
Streamlining:
--generate-streamliners=ITEM A comma separated list of integers.
If provided, the streamlining constraints that correspond to the given
integers will be generated.
Run "conjure streamlining ESSENCE_FILE" to generate a list of all
applicable streamliners.

conjure translate-parameter [OPTIONS]
Refinement of Essence parameter files for a particular Essence' model.
Expand Down Expand Up @@ -283,6 +289,12 @@
Default logic for SMT solvers is bitvector (bv).
Append a dash and the name of a logic to the solver name to choose a
different logic. For example yices-idl.
Streamlining:
--generate-streamliners=ITEM A comma separated list of integers.
If provided, the streamlining constraints that correspond to the given
integers will be generated.
Run "conjure streamlining ESSENCE_FILE" to generate a list of all
applicable streamliners.

conjure ide [OPTIONS] ESSENCE_FILE
IDE support features for Conjure.
Expand Down Expand Up @@ -461,6 +473,23 @@
General:
--limit-time=INT Time limit in seconds (real time).

conjure streamlining [OPTIONS] ESSENCE_FILE
Generate streamlined Essence models.

Logging & Output:
--log-level=LOGLEVEL Log level.
--output-format=FORMAT Conjure's output can be in multiple formats.
plain : The default
binary: A binary encoding of the Essence output.
It can be read back in by Conjure.
json : A json encoding of the Essence output.
It can be used by other tools integrating with Conjure
in order to avoid having to parse textual Essence.
--line-width=INT Line width to use during pretty printing.
Default: 120
General:
--limit-time=INT Time limit in seconds (real time).

conjure lsp [OPTIONS]

--loglevel=LOGLEVEL
Expand Down
3 changes: 2 additions & 1 deletion src/Conjure/Language/Domain.hs
Original file line number Diff line number Diff line change
Expand Up @@ -636,7 +636,8 @@ data BinaryRelationAttr
| BinRelAttr_WeakOrder
| BinRelAttr_PreOrder
| BinRelAttr_StrictPartialOrder
deriving (Eq, Ord, Show, Data, Typeable, Generic)
deriving (Eq, Ord, Show, Data, Typeable, Generic, Bounded, Enum)

instance Serialize BinaryRelationAttr
instance Hashable BinaryRelationAttr
instance ToJSON BinaryRelationAttr where toJSON = genericToJSON jsonOptions
Expand Down
2 changes: 1 addition & 1 deletion src/Conjure/Prelude.hs
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ import GHC.Integer as X ( Integer )
import GHC.Float as X ( sqrt, (**) )
import GHC.Exts as X ( Double )
import GHC.Real as X ( Fractional(..), Integral(..), fromIntegral, (^), Real(..), round, odd, even )
import GHC.Enum as X ( Enum(..) )
import GHC.Enum as X ( Enum(..), Bounded(..) )
import Data.Char as X ( Char, toLower, isSpace )
import Data.String as X ( String, IsString(..) )

Expand Down
1 change: 1 addition & 0 deletions src/Conjure/Process/Enumerate.hs
Original file line number Diff line number Diff line change
Expand Up @@ -174,6 +174,7 @@ enumerateDomain d = liftIO' $ withSystemTempDirectory ("conjure-enumerateDomain-
, lineWidth = 120
, responses = ""
, responsesRepresentation = ""
, generateStreamliners = ""
}
-- catching the (SR timeout) error, and raising a user error
catch solve $ \ (e :: SomeException) -> userErr1 $ vcat
Expand Down

0 comments on commit a378f2f

Please sign in to comment.