module greed.solver.solver

class Solver

This class represents a solver. Every solver must implement this interface.

method And

And(*terms)

Return an SMT And with the given terms.

Args:

• terms: The terms to AND

method Array

Array(symbol, index_sort, value_sort)

Return an SMT Array.

Args:

• symbol: The symbol of the array
• index_sort: The index sort of the array
• value_sort: The value sort of the array

method Array_Select

Array_Select(arr, index)

Return an SMT Array_Select with the given terms.

Args:

• arr: The array to select from
• index: The index to select from

method Array_Store

Array_Store(arr, index, elem)

Return an SMT Array_Store with the given terms.

Args:

• arr: The array to store to
• index: The index to store to
• elem: The element to store

method BVS

BVS(symbol, width)

Return a bitvector symbol of the given width.

Args:

• symbol: The name of the symbol
• width: The width of the symbol

method BVSort

BVSort(width)

Return a bitvector sort of the given width.

Args:

• width: The width of the bitvector

method BVV

BVV(value, width)

Return a bitvector value of the given width.

Args:

• value: The value of the bitvector
• width: The width of the bitvector

method BV_Add

BV_Add(a, b)

Return a bitvector addition of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_And

BV_And(a, b)

Return a bitvector bitwise and of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_Concat

BV_Concat(terms)

Return a bitvector concatenation of the given bitvectors.

Args:

• terms: The bitvectors to concatenate

method BV_Extract

BV_Extract(start, end, bv)

Return a bitvector extract of the given bitvector.

Args:

• start: The start of the extract
• end: The end of the extract
• bv: The bitvector to extract from

method BV_Mul

BV_Mul(a, b)

Return a bitvector multiplication of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_Not

BV_Not(a)

Return a bitvector not of the given bitvector.

Args:

• a: The bitvector to not

method BV_Or

BV_Or(a, b)

Return a bitvector bitwise or of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_SDiv

BV_SDiv(a, b)

Return a bitvector signed division of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_SGE

BV_SGE(a, b)

Return a bitvector signed greater or equal than of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_SGT

BV_SGT(a, b)

Return a bitvector signed greater than of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_SLE

BV_SLE(a, b)

Return a bitvector signed less or equal than of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_SLT

BV_SLT(a, b)

Return a bitvector signed less than of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_SMod

BV_SMod(a, b)

Return a bitvector signed modulo of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_SRem

BV_SRem(a, b)

Return a bitvector signed remainder of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_Sar

BV_Sar(a, b)

Return a bitvector arithmetic shift right of the given bitvector.

Args:

• a: The bitvector to shift
• b: The shift amount

method BV_Shl

BV_Shl(a, b)

Return a bitvector shift left of the given bitvector.

Args:

• a: The bitvector to shift
• b: The shift amount

method BV_Shr

BV_Shr(a, b)

Return a bitvector shift right of the given bitvector.

Args:

• a: The bitvector to shift
• b: The shift amount

method BV_Sign_Extend

BV_Sign_Extend(a, b)

Return a bitvector sign extension of the given bitvector.

Args:

• a: The bitvector to extend
• b: The width of the extension

method BV_Sub

BV_Sub(a, b)

Return a bitvector subtraction of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_UDiv

BV_UDiv(a, b)

Return a bitvector unsigned division of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_UGE

BV_UGE(a, b)

Return a bitvector unsigned greater or equal than of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_UGT

BV_UGT(a, b)

Return a bitvector unsigned greater than of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_ULE

BV_ULE(a, b)

Return a bitvector unsigned less or equal than of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_ULT

BV_ULT(a, b)

Return a bitvector unsigned less than of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_URem

BV_URem(a, b)

Return a bitvector unsigned remainder of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_Xor

BV_Xor(a, b)

Return a bitvector bitwise xor of the given bitvectors.

Args:

• a: The first bitvector
• b: The second bitvector

method BV_Zero_Extend

BV_Zero_Extend(a, b)

Return a bitvector zero extension of the given bitvector.

Args:

• a: The bitvector to extend
• b: The width of the extension

method Equal

Equal(a, b)

Return an SMT Equal with the given terms.

Args:

• a: The first term
• b: The second term

method If

If(cond, value_if_true, value_if_false)

Return an SMT If.

Args:

• cond: The condition formula
• value_if_true: The value if the condition is True
• value_if_false: The value if the condition is False

method Not

Not(a)

Return an SMT Not with the given term.

Args:

• a: The term to NOT

method NotEqual

NotEqual(a, b)

Return an SMT NotEqual with the given terms.

Args:

• a: The first term
• b: The second term

method Or

Or(*terms)

Return an SMT Or with the given terms.

Args:

• terms: The terms to OR

method add_assertion

add_assertion(formula)

Add a formula to the solver.

Args:

• formula: The formula to add

method add_assertions

add_assertions(formulas)

Add a list of formulas to the solver.

Args:

• formulas: The list of formulas to add

method are_formulas_sat

are_formulas_sat(terms)

Return True if the given formulas are satisfiable.

Args:

• terms: The list of formulas to check

method bv_unsigned_value

bv_unsigned_value(bv)

Return the unsigned value of the given bitvector.

Args:

• bv: The bitvector to evaluate

method copy

copy()

Implement the cloning of the solver when forking.

method eval

eval(term)

Evaluate the given term.

Args:

• term: The term to evaluate

method get_bv_by_name

get_bv_by_name(bv)

Return the bitvector with the given name.

Args:

• bv: The name of the bitvector

method is_concrete

is_concrete(bv)

Return True if the given bitvector is concrete.

Args:

• bv: The bitvector to check

method is_formula_false

is_formula_false(formula)

Return True if the given formula is always False.

Args:

• formula: The formula to check

method is_formula_sat

is_formula_sat(formula)

Return True if the given formula is satisfiable.

Args:

• formula: The formula to check

method is_formula_true

is_formula_true(formula)

Return True if the given formula is always True.

Args:

• formula: The formula to check

method is_formula_unsat

is_formula_unsat(formula)

Return True if the given formula is unsatisfiable.

Args:

• formula: The formula to check

method is_sat

is_sat()

Return True if the solver is in a satisfiable state.

method is_unsat

is_unsat()

Return True if the solver is in an unsatisfiable state.

method pop

pop()

Pop the current context from the solver.

method push

push()

Push a new context on the solver.

method solver_timeout

solver_timeout(func)

This file was automatically generated via lazydocs.