Choosing backend solver

[ozgurakgun]

Functionality to let user select a backend solver.

[ozgurakgun]

Backend solver:

• CP solvers
  • minion
  • chuffed
  • gecode
• SAT solvers
  • cadical
  • kissat
  • minisat
  • glucose
  • glucose-syrup
  • lingeling
  • plingeling
  • treengeling
• AllSAT solvers (implies --number-of-solutions=all)
  • bc_minisat_all
  • nbc_minisat_all
• MaxSAT solvers (only works for optimisation problems)
  • open-wbo
• MIP solvers
  • coin-or (@ozgurakgun - make sure this builds)
  • cplex (disabled, requires a license)
• SMT solvers
  • boolector (supported logics: bv)
  • yices (supported logics: bv, lia, idl)
  • z3 (supported logics: bv, lia, nia, idl)

Note: Append a dash and the name of a logic to the solver name to choose a different logic. For example yices-idl.

Easy option:

• SMT solvers
  • boolector with BV
  • yices with BV
  • yices with LIA
  • yices with IDL
  • z3 with BV
  • z3 with LIA
  • z3 with NIA
  • z3 with IDL