MarabouCore

Maraboupy bindings to the C++ Marabou via pybind11

class maraboupy.MarabouCore.PiecewiseLinearFunctionType[source]

Bases: pybind11_builtins.pybind11_object

Members:

ReLU

Max

Disjunction

AbsoluteValue

property name[source]

handle) -> str

Type

(self

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

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[source]

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[source]

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[source]

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[source]

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[source]

Create input query from network and property file

maraboupy.MarabouCore.loadQuery(filename: str) → InputQuery[source]

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[source]

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][source]

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[source]

Bases: pybind11_builtins.pybind11_object

addEquation(self: maraboupy.MarabouCore.InputQuery, arg0: Equation) → None[source]
dump(self: maraboupy.MarabouCore.InputQuery) → None[source]
getLowerBound(self: maraboupy.MarabouCore.InputQuery, arg0: int) → float[source]
getNumInputVariables(self: maraboupy.MarabouCore.InputQuery) → int[source]
getNumOutputVariables(self: maraboupy.MarabouCore.InputQuery) → int[source]
getNumberOfVariables(self: maraboupy.MarabouCore.InputQuery) → int[source]
getSolutionValue(self: maraboupy.MarabouCore.InputQuery, arg0: int) → float[source]
getUpperBound(self: maraboupy.MarabouCore.InputQuery, arg0: int) → float[source]
inputVariableByIndex(self: maraboupy.MarabouCore.InputQuery, arg0: int) → int[source]
markInputVariable(self: maraboupy.MarabouCore.InputQuery, arg0: int, arg1: int) → None[source]
markOutputVariable(self: maraboupy.MarabouCore.InputQuery, arg0: int, arg1: int) → None[source]
outputVariableByIndex(self: maraboupy.MarabouCore.InputQuery, arg0: int) → int[source]
setLowerBound(self: maraboupy.MarabouCore.InputQuery, arg0: int, arg1: float) → None[source]
setNumberOfVariables(self: maraboupy.MarabouCore.InputQuery, arg0: int) → None[source]
setUpperBound(self: maraboupy.MarabouCore.InputQuery, arg0: int, arg1: float) → None[source]
class maraboupy.MarabouCore.Options[source]

Bases: pybind11_builtins.pybind11_object

class maraboupy.MarabouCore.Equation[source]

Bases: pybind11_builtins.pybind11_object

class EquationType[source]

Bases: pybind11_builtins.pybind11_object

Members:

GE

LE

EQ

property name[source]

handle) -> str

Type

(self

addAddend(self: maraboupy.MarabouCore.Equation, arg0: float, arg1: int) → None[source]
setScalar(self: maraboupy.MarabouCore.Equation, arg0: float) → None[source]
class maraboupy.MarabouCore.Statistics[source]

Bases: pybind11_builtins.pybind11_object

getMaxDegradation(self: maraboupy.MarabouCore.Statistics) → float[source]
getMaxStackDepth(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumConstraintFixingSteps(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumMainLoopIterations(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumPops(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumPrecisionRestorations(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumSimplexPivotSelectionsIgnoredForStability(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumSimplexUnstablePivots(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumSplits(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumTableauPivots(self: maraboupy.MarabouCore.Statistics) → int[source]
getNumVisitedTreeStates(self: maraboupy.MarabouCore.Statistics) → int[source]
getTimeSimplexStepsMicro(self: maraboupy.MarabouCore.Statistics) → int[source]
getTotalTime(self: maraboupy.MarabouCore.Statistics) → int[source]
hasTimedOut(self: maraboupy.MarabouCore.Statistics) → bool[source]