MarabouCore

Maraboupy bindings to the C++ Marabou via pybind11

class maraboupy.MarabouCore.PiecewiseLinearFunctionType

Bases: pybind11_builtins.pybind11_object

Members:

ReLU

Max

Disjunction

AbsoluteValue

property name

handle) -> str

Type

(self

maraboupy.MarabouCore.addAbsConstraint(inputQuery: InputQuery, b: int, f: int) → None

Add an Abs constraint to the InputQuery

Parameters

• inputQuery (InputQuery) – Marabou input query to be solved

• b (int) – Input variable

• f (int) – Output variable

maraboupy.MarabouCore.addDisjunctionConstraint(inputQuery: InputQuery, disjuncts: List[List[Equation]]) → None

Add a disjunction constraint to the InputQuery

Parameters

• inputQuery (InputQuery) – Marabou input query to be solved

• disjuncts (list of pairs) – A list of disjuncts. Each disjunct is represented by a pair: a list of bounds, and a list of (in)equalities.

maraboupy.MarabouCore.addMaxConstraint(inputQuery: InputQuery, elements: Set[int], v: int) → None

Add a Max constraint to the InputQuery

Parameters

• inputQuery (InputQuery) – Marabou input query to be solved

• elements (set of int) – Input variables to max constraint

• v (int) – Output variable from max constraint

maraboupy.MarabouCore.addReluConstraint(inputQuery: InputQuery, var1: int, var2: int) → None

Add a Relu constraint to the InputQuery

Parameters

• inputQuery (InputQuery) – Marabou input query to be solved

• var1 (int) – Input variable to Relu constraint

• var2 (int) – Output variable to Relu constraint

maraboupy.MarabouCore.addSignConstraint(inputQuery: InputQuery, var1: int, var2: int) → None

Add a Sign constraint to the InputQuery

Parameters

• inputQuery (InputQuery) – Marabou input query to be solved

• var1 (int) – Input variable to Sign constraint

• var2 (int) – Output variable to Sign constraint

maraboupy.MarabouCore.createInputQuery(arg0: InputQuery, arg1: str, arg2: str) → bool

Create input query from network and property file

maraboupy.MarabouCore.loadQuery(filename: str) → InputQuery

Loads and returns a serialized InputQuery from the given filename

Parameters

filename (str) – Name of file to load into an InputQuery

Returns

InputQuery

maraboupy.MarabouCore.saveQuery(inputQuery: InputQuery, filename: str) → None

Serializes the inputQuery in the given filename

Parameters

• inputQuery (InputQuery) – Marabou input query to be saved

• filename (str) – Name of file to save query

maraboupy.MarabouCore.solve(inputQuery: InputQuery, options: MarabouOptions, redirect: str = '') → Tuple[Dict[int, float], Statistics]

Takes in a description of the InputQuery and returns the solution

Parameters

• inputQuery (InputQuery) – Marabou input query to be solved

• (class (options) – ~maraboupy.MarabouCore.Options): Object defining the options used for Marabou

• redirect (str, optional) – Filepath to direct standard output, defaults to “”

Returns

tuple containing:

• vals (Dict[int, float]): Empty dictionary if UNSAT, otherwise a dictionary of SATisfying values for variables

• stats (Statistics): A Statistics object to how Marabou performed

Return type

(tuple)

class maraboupy.MarabouCore.InputQuery

Bases: pybind11_builtins.pybind11_object

addEquation(self: maraboupy.MarabouCore.InputQuery, arg0: Equation) → None

dump(self: maraboupy.MarabouCore.InputQuery) → None

getLowerBound(self: maraboupy.MarabouCore.InputQuery, arg0: int) → float

getNumInputVariables(self: maraboupy.MarabouCore.InputQuery) → int

getNumOutputVariables(self: maraboupy.MarabouCore.InputQuery) → int

getNumberOfVariables(self: maraboupy.MarabouCore.InputQuery) → int

getSolutionValue(self: maraboupy.MarabouCore.InputQuery, arg0: int) → float

getUpperBound(self: maraboupy.MarabouCore.InputQuery, arg0: int) → float

inputVariableByIndex(self: maraboupy.MarabouCore.InputQuery, arg0: int) → int

markInputVariable(self: maraboupy.MarabouCore.InputQuery, arg0: int, arg1: int) → None

markOutputVariable(self: maraboupy.MarabouCore.InputQuery, arg0: int, arg1: int) → None

outputVariableByIndex(self: maraboupy.MarabouCore.InputQuery, arg0: int) → int

setLowerBound(self: maraboupy.MarabouCore.InputQuery, arg0: int, arg1: float) → None

setNumberOfVariables(self: maraboupy.MarabouCore.InputQuery, arg0: int) → None

setUpperBound(self: maraboupy.MarabouCore.InputQuery, arg0: int, arg1: float) → None

class maraboupy.MarabouCore.Options

Bases: pybind11_builtins.pybind11_object

class maraboupy.MarabouCore.Equation

Bases: pybind11_builtins.pybind11_object

class EquationType

Bases: pybind11_builtins.pybind11_object

Members:

GE

LE

EQ

property name

handle) -> str

Type

(self

addAddend(self: maraboupy.MarabouCore.Equation, arg0: float, arg1: int) → None

setScalar(self: maraboupy.MarabouCore.Equation, arg0: float) → None

class maraboupy.MarabouCore.Statistics

Bases: pybind11_builtins.pybind11_object

getMaxDegradation(self: maraboupy.MarabouCore.Statistics) → float

getMaxStackDepth(self: maraboupy.MarabouCore.Statistics) → int

getNumConstraintFixingSteps(self: maraboupy.MarabouCore.Statistics) → int

getNumMainLoopIterations(self: maraboupy.MarabouCore.Statistics) → int

getNumPops(self: maraboupy.MarabouCore.Statistics) → int

getNumPrecisionRestorations(self: maraboupy.MarabouCore.Statistics) → int

getNumSimplexPivotSelectionsIgnoredForStability(self: maraboupy.MarabouCore.Statistics) → int

getNumSimplexUnstablePivots(self: maraboupy.MarabouCore.Statistics) → int

getNumSplits(self: maraboupy.MarabouCore.Statistics) → int

getNumTableauPivots(self: maraboupy.MarabouCore.Statistics) → int

getNumVisitedTreeStates(self: maraboupy.MarabouCore.Statistics) → int

getTimeSimplexStepsMicro(self: maraboupy.MarabouCore.Statistics) → int

getTotalTime(self: maraboupy.MarabouCore.Statistics) → int

hasTimedOut(self: maraboupy.MarabouCore.Statistics) → bool