Index

A

add_clause() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.WCNF method) (optilog.solvers.sat.pyisat.PyiSAT method) add_clauses() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.WCNF method) (optilog.solvers.sat.pyisat.PyiSAT method) add_comment() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.WCNF method)

add_filter() (optilog.running.ParsingInfo method) add_var() (optilog.formulas.VarManager method) append_quant_set() (optilog.formulas.QCNF method) at_least_k() (optilog.encoders.pb.Encoder static method) at_least_one() (optilog.encoders.pb.Encoder static method) at_most_k() (optilog.encoders.pb.Encoder static method) at_most_one() (optilog.encoders.pb.Encoder static method) available_solvers() (optilog.blackbox.SatexBlackBox static method)

B

BlackBoxRedirection (class in optilog.blackbox)

Bool (class in optilog.tuning)

C

card_encodings() (optilog.encoders.pb.Encoder static method) (optilog.encoders.pb.IncrementalEncoder static method) Categorical (class in optilog.tuning) CfgCall (class in optilog.tuning) CfgCls (class in optilog.tuning) CfgObj (class in optilog.tuning) Choice (class in optilog.tuning) clauses (optilog.formulas.CNF attribute) (optilog.formulas.QCNF property) clear_interrupt() (optilog.solvers.sat.pyisat.PyiSAT method)

clone() (optilog.solvers.sat.pyisat.PyiSAT method) CNF (class in optilog.formulas) CNFException (class in optilog.formulas) copy() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.VarManager method) (optilog.formulas.WCNF method) core() (optilog.solvers.sat.pyisat.PyiSAT method) cost() (optilog.formulas.WCNF method) CPUTime (optilog.blackbox.SystemBlackBox attribute)

D

Default (optilog.blackbox.BlackBoxRedirection attribute)

Dict (class in optilog.tuning) DockerEnforcer (class in optilog.blackbox)

E

E_STATE (C++ enum) E_STATE::SAT (C++ enumerator) E_STATE::UNKNOWN (C++ enumerator) E_STATE::UNSAT (C++ enumerator) enable_static_heuristic() (optilog.solvers.sat.pyisat.PyiSAT method) Encoder (class in optilog.encoders.pb) exactly_k() (optilog.encoders.pb.Encoder static method)

exactly_one() (optilog.encoders.pb.Encoder static method) ExecutionConstraints (class in optilog.blackbox) extend() (optilog.encoders.pb.IncrementalEncoder method) extend_vars() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.VarManager method) (optilog.formulas.WCNF method)

F

feasible() (optilog.formulas.WCNF method)

format_config() (optilog.blackbox.SystemBlackBox method) from_template() (optilog.running.ParsingInfo static method)

G

generate_scenario() (optilog.running.RunningScenario method) (optilog.tuning.configurators.GGAScenario method) (optilog.tuning.configurators.SMACScenario method) get() (optilog.blackbox.SatexBlackBox method) (optilog.blackbox.SystemBlackBox method) (optilog.solvers.sat.pyisat.PyiSAT method) get_amo_encodings() (optilog.encoders.pb.IncrementalEncoder static method) get_command() (optilog.tuning.configurators.GGAScenario static method) (optilog.tuning.configurators.SMACScenario static method) get_config() (optilog.blackbox.SatexBlackBox class method) (optilog.blackbox.SystemBlackBox class method) (optilog.solvers.sat.pyisat.PyiSAT static method) (optilog.tuning.configurators.utils.GGAParser method)

get_configs() (optilog.tuning.configurators.utils.GGAParser method) (optilog.tuning.configurators.utils.SMACParser method) get_incremental_pb_encodings() (optilog.encoders.pb.Encoder static method) get_init_clauses() (optilog.encoders.pb.IncrementalEncoder method) get_lit() (optilog.formulas.VarManager method) get_polarity() (optilog.solvers.sat.pyisat.PyiSAT method) get_trail() (optilog.solvers.sat.pyisat.PyiSAT method) GGAParser (class in optilog.tuning.configurators.utils) GGAScenario (class in optilog.tuning.configurators)

H

hard_clauses (optilog.formulas.WCNF attribute) header() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.WCNF method)

I

IncrementalEncoder (class in optilog.encoders.pb) init() (optilog.encoders.pb.IncrementalEncoder static method) Instance (optilog.blackbox.SystemBlackBox attribute) Int (class in optilog.tuning) interrupt() (optilog.solvers.sat.pyisat.PyiSAT method) is_full_model() (optilog.solvers.sat.pyisat.PyiSAT method) is_sat (optilog.blackbox.SatexBlackBox property) iSAT (C++ class) iSAT::addClause (C++ function) iSAT::clearInterrupt (C++ function) iSAT::clone (C++ function) iSAT::core (C++ function) iSAT::enableStaticHeuristic (C++ function) iSAT::get (C++ function) iSAT::getActivities (C++ function) iSAT::getLearntClauses (C++ function) iSAT::getMaxVar (C++ function) iSAT::getModel (C++ function) iSAT::getNumClauses (C++ function) iSAT::getNumConflicts (C++ function) iSAT::getPolarity (C++ function)

iSAT::getTrail (C++ function) iSAT::getUnits (C++ function) iSAT::getValue (C++ function) iSAT::getVersion (C++ function) iSAT::interrupt (C++ function) iSAT::isFullModel (C++ function) iSAT::newVar (C++ function) iSAT::propagate (C++ function) iSAT::set (C++ function), [1], [2], [3] iSAT::setConflictsBudget (C++ function) iSAT::setDecisionVariable (C++ function) iSAT::setIncremental (C++ function) iSAT::setPropagationBudget (C++ function) iSAT::setStaticHeuristic (C++ function) iSAT::setVarPolarity (C++ function) iSAT::solve (C++ function) iSAT::solveHardLimited (C++ function) iSAT::solveLimit (C++ function) iSAT::traceProof (C++ function) iSAT::unsatState (C++ function) iSAT::unsetVarPolarity (C++ function)

L

learnt_clauses() (optilog.solvers.sat.pyisat.PyiSAT method) load_cnf() (in module optilog.formulas.loaders) (optilog.solvers.sat.pyisat.PyiSAT method)

load_qcnf() (in module optilog.formulas.loaders) load_wcnf() (in module optilog.formulas.loaders) (optilog.solvers.sat.pyisat.PyiSAT method)

M

max_var() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.VarManager method) (optilog.formulas.WCNF method) (optilog.solvers.sat.pyisat.PyiSAT method)

Memory (optilog.blackbox.SystemBlackBox attribute) model (optilog.blackbox.SatexBlackBox property) model() (optilog.solvers.sat.pyisat.PyiSAT method) module optilog.formulas.loaders optilog.modelling

N

new_var() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.VarManager method) (optilog.formulas.WCNF method) (optilog.solvers.sat.pyisat.PyiSAT method) Null (optilog.blackbox.BlackBoxRedirection attribute)

num_clauses() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.WCNF method) (optilog.solvers.sat.pyisat.PyiSAT method) num_conflicts() (optilog.solvers.sat.pyisat.PyiSAT method) num_quant_levels() (optilog.formulas.QCNF method)

O

optilog.formulas.loaders module

optilog.modelling module

P

parse_scenario() (in module optilog.running) parsed (optilog.blackbox.SatexBlackBox property) (optilog.blackbox.SystemBlackBox property) ParsingInfo (class in optilog.running) pb_encodings() (optilog.encoders.pb.Encoder static method) (optilog.encoders.pb.IncrementalEncoder static method)

print_clauses_color() (in module optilog.formulas.visualization) Process (optilog.blackbox.BlackBoxRedirection attribute) propagate() (optilog.solvers.sat.pyisat.PyiSAT method) PyiSAT (class in optilog.solvers.sat.pyisat)

Q

QCNF (class in optilog.formulas)

QCNFException (class in optilog.formulas)

R

range_k1_k2() (optilog.encoders.pb.Encoder static method) Real (class in optilog.tuning) returncode (optilog.blackbox.SystemBlackBox property) run() (optilog.blackbox.SatexBlackBox method) (optilog.blackbox.SystemBlackBox method)

RunningScenario (class in optilog.running) RunningSolverType (class in optilog.running) RunSolver (class in optilog.blackbox)

S

sat (optilog.blackbox.SatexBlackBox property) SatexBlackBox (class in optilog.blackbox) satisfied() (optilog.formulas.CNF method) save_configs() (optilog.tuning.configurators.utils.GGAParser method) (optilog.tuning.configurators.utils.SMACParser method) Seed (optilog.blackbox.SystemBlackBox attribute) set() (optilog.blackbox.SatexBlackBox method) (optilog.blackbox.SystemBlackBox method) (optilog.solvers.sat.pyisat.PyiSAT method) set_conf_budget() (optilog.solvers.sat.pyisat.PyiSAT method) set_decision_var() (optilog.solvers.sat.pyisat.PyiSAT method) set_default() (optilog.blackbox.SatexBlackBox class method) (optilog.blackbox.SystemBlackBox class method) set_incremental() (optilog.solvers.sat.pyisat.PyiSAT method) set_minimum_vars() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.VarManager method) (optilog.formulas.WCNF method)

set_polarity() (optilog.solvers.sat.pyisat.PyiSAT method) set_prop_budget() (optilog.solvers.sat.pyisat.PyiSAT method) set_static_heuristic() (optilog.solvers.sat.pyisat.PyiSAT method) shuffle() (optilog.formulas.CNF method) (optilog.formulas.WCNF method) SMACParser (class in optilog.tuning.configurators.utils) SMACScenario (class in optilog.tuning.configurators) soft_clauses (optilog.formulas.WCNF attribute) solve() (optilog.solvers.sat.pyisat.PyiSAT method) solve_hard_limited() (optilog.solvers.sat.pyisat.PyiSAT method) solve_limited() (optilog.solvers.sat.pyisat.PyiSAT method) statistics() (optilog.formulas.CNF method) stderr (optilog.blackbox.SystemBlackBox property) Stdout (optilog.blackbox.BlackBoxRedirection attribute) stdout (optilog.blackbox.SystemBlackBox property) sum_soft_weights() (optilog.formulas.WCNF method) SystemBlackBox (class in optilog.blackbox)

T

top_weight() (optilog.formulas.WCNF method) trace_proof() (optilog.solvers.sat.pyisat.PyiSAT method) TuningEntrypointType (class in optilog.tuning.configurators)

TuningGlobalConfigurableType (class in optilog.tuning.configurators) TYPES (optilog.running.RunningSolverType attribute) (optilog.tuning.configurators.TuningEntrypointType attribute) (optilog.tuning.configurators.TuningGlobalConfigurableType attribute)

U

unsat_state() (optilog.solvers.sat.pyisat.PyiSAT method)

unset_polarity() (optilog.solvers.sat.pyisat.PyiSAT method)

V

value() (optilog.solvers.sat.pyisat.PyiSAT method) var_manager (optilog.formulas.CNF attribute) (optilog.formulas.QCNF attribute) (optilog.formulas.WCNF attribute)

VarManager (class in optilog.formulas)

W

WallTime (optilog.blackbox.SystemBlackBox attribute) WCNF (class in optilog.formulas) WCNFException (class in optilog.formulas) write_dimacs() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.WCNF method)

write_dimacs_file() (optilog.formulas.CNF method) (optilog.formulas.QCNF method) (optilog.formulas.WCNF method)