From 3a35696db1b025a7f924978f9fb99787dd47d0b3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?O=CC=88zgu=CC=88r=20Akgu=CC=88n?= Date: Wed, 8 Nov 2023 19:34:08 +0000 Subject: [PATCH] update expected help text --- docs/conjure-help.html | 2 +- docs/conjure-help.txt | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/conjure-help.html b/docs/conjure-help.html index ebfebad5f..9af27a831 100644 --- a/docs/conjure-help.html +++ b/docs/conjure-help.html @@ -135,7 +135,7 @@ Options for other tools:  --savilerow-options=ITEMOptions passed to Savile Row.  --solver-options=ITEMOptions passed to the backend solver. - --solver=ITEMBackend solver. Possible values:
- minion (CP solver)
- gecode (CP solver)
- chuffed (CP solver)
- glucose (SAT solver)
- glucose-syrup (SAT solver)
- lingeling/plingeling/treengeling (SAT solver)
- cadical (SAT solver)
- kissat (SAT solver)
- minisat (SAT solver)
- bc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)
- nbc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)
- open-wbo (MaxSAT solver, only works with optimisation problems)
- coin-or (MIP solver, implemented via MiniZinc)
- cplex (MIP solver, implemented via MiniZinc)
- boolector (SMT solver, supported logics: bv)
- yices (SMT solver, supported logics: bv, lia, idl)
- z3 (SMT solver, supported logics: bv, lia, nia, idl)
Default: minion

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. + --solver=ITEMBackend solver. Possible values:
- minion (CP solver)
- gecode (CP solver)
- chuffed (CP solver)
- or-tools (CP solver)
- glucose (SAT solver)
- glucose-syrup (SAT solver)
- lingeling/plingeling/treengeling (SAT solver)
- cadical (SAT solver)
- kissat (SAT solver)
- minisat (SAT solver)
- bc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)
- nbc_minisat_all (AllSAT solver, only works with --number-of-solutions=all)
- open-wbo (MaxSAT solver, only works with optimisation problems)
- coin-or (MIP solver, implemented via MiniZinc)
- cplex (MIP solver, implemented via MiniZinc)
- boolector (SMT solver, supported logics: bv)
- yices (SMT solver, supported logics: bv, lia, idl)
- z3 (SMT solver, supported logics: bv, lia, nia, idl)
Default: minion

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.   conjure ide [OPTIONS] ESSENCE_FILE IDE support features for Conjure.
Not intended for direct use. diff --git a/docs/conjure-help.txt b/docs/conjure-help.txt index 35aa27329..d71f608d8 100644 --- a/docs/conjure-help.txt +++ b/docs/conjure-help.txt @@ -262,6 +262,7 @@ - minion (CP solver) - gecode (CP solver) - chuffed (CP solver) + - or-tools (CP solver) - glucose (SAT solver) - glucose-syrup (SAT solver) - lingeling/plingeling/treengeling (SAT solver)