module greed.solver.yices2

class YicesTerm

method __init__

__init__(yices_id, operator=None, children=None, name=None, value=None)

property value

method dump

dump(pp=False)

method pp

pp()

class YicesTermBool

method __init__

__init__(yices_id, operator=None, children=None, name=None, value=None)

property value

method dump

dump(pp=False)

method pp

pp()

class YicesTermBV

method __init__

__init__(yices_id, operator=None, children=None, name=None, value=None)

property bitsize

property value

method dump

dump(pp=False)

method pp

pp()

class YicesTermArray

method __init__

__init__(yices_id, operator=None, children=None, name=None, value=None)

property value

method dump

dump(pp=False)

method pp

pp()

class YicesType

method __init__

__init__(yices_id, name)

class YicesTypeBV

method __init__

__init__(yices_id, name)

class YicesTypeArray

method __init__

__init__(yices_id, name)

class Yices2

Backend for Yices2

For the list of options see here. https://github.com/SRI-CSL/yices2/blob/bc50bebdc3aabb161328bbfc234a10da6dd3d5c4/doc/sphinx/source/context-operations.rst

self.solver.enable_option("var-elim") self.solver.enable_option("arith-elim") self.solver.enable_option("flatten") self.solver.enable_option("assert-ite-bounds") self.solver.enable_option("eager-arith-lemmas") self.solver.enable_option("keep-ite") self.solver.enable_option("bvarith-elim") self.solver.enable_option("break-symmetries")

cfg.set_config("arith-solver", 'simplex')

method __init__

__init__()

method And

And(*terms: YicesTermBool) → YicesTermBool

method Array

Array(symbol, index_sort: YicesTypeBV, value_sort: YicesTypeBV) → YicesTermArray

method Array_Select

Array_Select(arr: YicesTermArray, index: YicesTermBV) → YicesTermBV

method Array_Store

Array_Store(
    arr: YicesTermArray,
    index: YicesTermBV,
    elem: YicesTermBV
) → YicesTermArray

method BVS

BVS(symbol: str, width: int) → YicesTermBV

method BVSort

BVSort(width: int) → YicesTypeBV

method BVV

BVV(value: int, width: int) → YicesTermBV

method BV_Add

BV_Add(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_And

BV_And(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_Concat

BV_Concat(terms: List[YicesTermBV]) → YicesTermBV

method BV_Extract

BV_Extract(start: int, end: int, bv: YicesTermBV) → YicesTermBV

method BV_Mul

BV_Mul(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_Not

BV_Not(a: YicesTermBV) → YicesTermBV

method BV_Or

BV_Or(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_SDiv

BV_SDiv(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_SGE

BV_SGE(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method BV_SGT

BV_SGT(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method BV_SLE

BV_SLE(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method BV_SLT

BV_SLT(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method BV_SMod

BV_SMod(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_SRem

BV_SRem(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_Sar

BV_Sar(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_Shl

BV_Shl(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_Shr

BV_Shr(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_Sign_Extend

BV_Sign_Extend(a: YicesTermBV, b: int) → YicesTermBV

method BV_Sub

BV_Sub(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_UDiv

BV_UDiv(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_UGE

BV_UGE(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method BV_UGT

BV_UGT(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method BV_ULE

BV_ULE(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method BV_ULT

BV_ULT(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method BV_URem

BV_URem(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_Xor

BV_Xor(a: YicesTermBV, b: YicesTermBV) → YicesTermBV

method BV_Zero_Extend

BV_Zero_Extend(a: YicesTermBV, b: int) → YicesTermBV

method Equal

Equal(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method If

If(
    cond: YicesTermBool,
    value_if_true: YicesTerm,
    value_if_false: YicesTerm
) → YicesTerm

method Not

Not(a: YicesTermBool) → YicesTermBool

method NotEqual

NotEqual(a: YicesTermBV, b: YicesTermBV) → YicesTermBool

method Or

Or(*terms: YicesTermBool) → YicesTermBool

method add_assertion

add_assertion(formula: YicesTermBool)

method add_assertions

add_assertions(formulas: List[YicesTermBool])

method bv_unsigned_value

bv_unsigned_value(bv: YicesTermBV) → int

method copy

copy()

method eval

eval(term: YicesTerm, raw=False)

method get_bv_by_name

get_bv_by_name(symbol)

method is_concrete

is_concrete(bv: YicesTermBV) → bool

method is_formula_false

is_formula_false(formula: YicesTermBool) → bool

method is_formula_true

is_formula_true(formula: YicesTermBool) → bool

method pop

pop()

method push

push()

This file was automatically generated via lazydocs.