import os
import pyboolector
from pyboolector import Boolector, BoolectorException

if __name__ == "__main__":
    b = Boolector()
    print ("Boolector version " + b.Version())
    print ("Boolector id " + b.GitId())
    print ()
    print (b.Copyright())

    # Try pushing a context without enabling incremental usage,
    # raises Exception
    try:
        print("Expect exception to be raised (incremental usage not enabled).")
        b.Push()
    except BoolectorException as e:
        print("Caught exception: " + str(e))

    # Try popping a context without first having pushed a context,
    # raises Exception
    try:
        b.Set_opt(pyboolector.BTOR_OPT_INCREMENTAL, True)
        print("Expect exception to be raised (no context pushed).")
        b.Pop()
    except BoolectorException as e:
        print("Caught exception: " + str(e))

### Creating Boolector nodes

    # Sorts
    _boolsort = b.BoolSort()
    # Try creating a bit-vector sort of size 0,
    # raises Exception
    try:
        print("Expect exception to be raised (bit-vector size of 0).")
        _bvsort = b.BitVecSort(0)
    except BoolectorException as e:
        print("Caught exception: " + str(e))
    _bvsort   = b.BitVecSort(128)
    _arrsort  = b.ArraySort(_bvsort, _bvsort)
    _funsort  = b.FunSort([_boolsort, _boolsort, _bvsort, _bvsort], _boolsort)

    # Constants
    _const = b.Const("10010101")
    _zero  = b.Const(0, 128)
    _ones  = b.Const(-1, 129)
    _true  = b.Const(True)
    _false = b.Const(False)
    _one   = b.Const(1, 128)
    _uint  = b.Const(77, 128)
    _int   = b.Const(-77, 128)

    # Variables
    _var   = b.Var(_bvsort, "var_symbol")
    # Try getting the assignment of _var without a call to Sat(),
    # raises Exception
    try:
        print("Expect exception to be raised (no previous call to Sat()).")
        print("{} {}".format(_var.symbol, _var.assignment))
    except BoolectorException as e:
        print("Caught exception: " + str(e))

    _param = b.Param(_bvsort, "param_symbol")  # used as function parameters
    _array = b.Array(_arrsort, "array_symbol")
    _uf    = b.UF(_funsort)

    # One's complement 
    _not0    = b.Not(_const)
    _not1    = ~_const

    # Two's complement
    _neg0    = b.Neg(_zero)
    _neg1    = -_zero

    # Reduction operations on bit vectors
    _redor   = b.Redor(_ones)
    _redxor  = b.Redxor(_one)
    _redand  = b.Redand(_uint)

    # Slicing of bit vectors
    _slice0  = b.Slice(_param, 8, 0)
    _slice1  = _param[8:0]
    _slice3  = _param[:]   # copy
    _slice2  = _param[8:]  # lower is 0
    _slice4  = _param[:0]  # upper is _param.width - 1
    _slice5  = _param[8]   # extract bit at position 8, equiv. to _param[8:8]
    _slice5  = _param[8:8] # equiv. to _param[8]

    # Unsigned/signed extension
    _uext    = b.Uext(_true, 127)
    _sext    = b.Sext(_false, 127)

    _inc     = b.Inc(_not0)
    _dec     = b.Dec(_not1)
   
    _implies0 = b.Implies(_redor, _redxor)
    _implies1 = b.Implies(False, _redor)
    _implies2 = b.Implies(True, _redxor)

    _iff0     = b.Iff(True, _redxor)
    _iff1     = b.Iff(_redor, _redxor)
    _iff2     = b.Iff(False, _redxor)

    _xor0     = b.Xor(_uext, _sext)
    _xor1     = _uext ^ _sext
    _xor2     = b.Xor(0xff, _sext)
    _xor3     = 0xff ^ _sext

    _and0     = b.And(_inc, _dec)
    _and1     = b.And(128, _dec)
    _and2     = b.And(_dec, 0xaa)
    _and3     = _dec & 0xaa

    _nand0    = b.Nand(_inc, _dec)
    _nand1    = b.Nand(128, _dec)
    _nand2    = b.Nand(_dec, 0xaa)
    _nand3    = ~(_dec & 0xaa)

    _or0      = b.Or(_inc, _dec)
    _or1      = b.Or(128, _dec)
    _or2      = b.Or(_dec, 0xaa)
    _or3      = _dec | 0xaa

    _nor0     = b.Nor(_inc, _dec)
    _nor1     = b.Nor(128, _dec)
    _nor2     = b.Nor(_dec, 0xaa)
    _nor3     = ~(_dec | 0xaa)

    _eq0      = b.Eq(_inc, _dec)
    _eq1      = b.Eq(128, _dec)
    _eq2      = b.Eq(_dec, 0xaa)
    _eq3      = _dec == 0xaa

    _neq0     = b.Ne(_inc, _dec)
    _neq1     = b.Ne(128, _dec)
    _neq2     = b.Ne(_dec, 0xaa)
    _neq3     = _dec != 0xaa

    _add0     = b.Add(_inc, _dec)
    _add1     = b.Add(128, _dec)
    _add2     = b.Add(_dec, 0xaa)
    _add3     = _dec + 0xaa

    _uaddo0   = b.Uaddo(_inc, _dec)
    _uaddo1   = b.Uaddo(128, _dec)
    _uaddo2   = b.Uaddo(_dec, 0xaa)

    _saddo0   = b.Saddo(_inc, _dec)
    _saddo1   = b.Saddo(128, _dec)
    _saddo2   = b.Saddo(_dec, 0xaa)

    _mul0     = b.Mul(_inc, _dec)
    _mul1     = b.Mul(128, _dec)
    _mul2     = b.Mul(_dec, 0xaa)
    _mul3     = _dec * 0xaa

    _umulo0   = b.Umulo(_inc, _dec)
    _umulo1   = b.Umulo(128, _dec)
    _umulo2   = b.Umulo(_dec, 0xaa)

    _smulo0   = b.Smulo(_inc, _dec)
    _smulo1   = b.Smulo(128, _dec)
    _smulo2   = b.Smulo(_dec, 0xaa)

    _ult0     = b.Ult(_inc, _dec)
    _ult1     = b.Ult(128, _dec)
    _ult2     = b.Ult(_dec, 0xaa)
    _ult3     = _dec < 0xaa

    _slt0     = b.Slt(_inc, _dec)
    _slt1     = b.Slt(128, _dec)
    _slt2     = b.Slt(_dec, 0xaa)

    _ulte0    = b.Ulte(_inc, _dec)
    _ulte1    = b.Ulte(128, _dec)
    _ulte2    = b.Ulte(_dec, 0xaa)
    _ulte3    = _dec <= 0xaa

    _slte0    = b.Slte(_inc, _dec)
    _slte1    = b.Slte(128, _dec)
    _slte2    = b.Slte(_dec, 0xaa)

    _ugt0     = b.Ugt(_inc, _dec)
    _ugt1     = b.Ugt(128, _dec)
    _ugt2     = b.Ugt(_dec, 0xaa)
    _ugt3     = _dec > 0xaa

    _sgt0     = b.Sgt(_inc, _dec)
    _sgt1     = b.Sgt(128, _dec)
    _sgt2     = b.Sgt(_dec, 0xaa)

    _ugte0    = b.Ugte(_inc, _dec)
    _ugte1    = b.Ugte(128, _dec)
    _ugte2    = b.Ugte(_dec, 0xaa)
    _ugte3    = _dec >= 0xaa

    _sgte0    = b.Sgte(_inc, _dec)
    _sgte1    = b.Sgte(128, _dec)
    _sgte2    = b.Sgte(_dec, 0xaa)

    _sll0     = b.Sll(_dec, 5)
    _sll1     = b.Sll(_dec, 0b100)
    _sll2     = _dec << 5

    _srl0     = b.Srl(_dec, 5)
    _srl1     = b.Srl(_dec, 0b100)
    _srl2     = _dec >> 5

    _sra0     = b.Sra(_dec, 5)
    _sra1     = b.Sra(_dec, 0b100)

    _rol0     = b.Rol(_dec, 5)
    _rol1     = b.Rol(_dec, 0b100)

    _ror0     = b.Ror(_dec, 5)
    _ror1     = b.Ror(_dec, 0b100)

    _sub0     = b.Sub(_inc, _dec)
    _sub1     = b.Sub(128, _dec)
    _sub2     = b.Sub(_dec, 0xaa)
    _sub3     = _dec - 0xaa

    _ssubo0   = b.Ssubo(_inc, _dec)
    _ssubo1   = b.Ssubo(128, _dec)
    _ssubo2   = b.Ssubo(_dec, 0xaa)

    _udiv0    = b.Udiv(_inc, _dec)
    _udiv1    = b.Udiv(128, _dec)
    _udiv2    = b.Udiv(_dec, 0xaa)
    _udiv3    = _dec / 0xaa

    _urem0    = b.Urem(_inc, _dec)
    _urem1    = b.Urem(128, _dec)
    _urem2    = b.Urem(_dec, 0xaa)
    _urem3    = _dec % 0xaa

    _sdiv0    = b.Sdiv(-_inc, _dec)
    _sdiv1    = b.Sdiv(128, -_dec)
    _sdiv2    = b.Sdiv(_dec, -0xaa)

    _srem0    = b.Srem(-_inc, _dec)
    _srem1    = b.Srem(128, -_dec)
    _srem2    = b.Srem(_dec, -0xaa)

    _sdivo0   = b.Sdivo(-_inc, _dec)
    _sdivo1   = b.Sdivo(128, -_dec)
    _sdivo2   = b.Sdivo(_dec, -0xaa)

    _smod0    = b.Smod(-_inc, _dec)
    _smod1    = b.Smod(128, -_dec)
    _smod2    = b.Smod(_dec, -0xaa)

    # Concatenation of bit vectors
    _concat   = b.Concat(_dec, _inc)
    _repeat   = b.Repeat(_concat, 1)
    _repeat   = b.Repeat(_repeat, 5)


    # Reads on arrays
    _read0    = b.Read(_array, _var)
    _read1    = b.Read(_array, 12)
    _read2    = _array[_var]
    _read3    = _array[0x1a]

    # Writes on arrays
    _write0   = b.Write(_array, _var, _var)
    _write1   = b.Write(_array, 10, 0b00001)

    # If-Then-Else on bit vectors
    _cond0    = b.Cond(_read0[0], _read0, _read1)
    _cond1    = b.Cond(False, _read0, _read1)
    _cond2    = b.Cond(True, 1, _read1)

    # If-Then-Else on arrays
    _cond3    = b.Cond(0, _write0, _write1)

    # Function
    p0        = b.Param(_bvsort)
    p1        = b.Param(_bvsort)
    _fun      = b.Fun([p0, p1], b.Cond(p0 < p1, p0, p1))

    # Function applications
    _apply0   = b.Apply([_var, _var], _fun)
    _apply1   = b.Apply([1, 2], _fun)
    _apply2   = _fun(1, 2)
    _apply3   = b.Apply([_true, _false, _var, _var], _uf)
    _apply4   = b.Apply([1, True, 3, 42], _uf)
    _apply5   = b.Apply([1, False, 3, 42], _uf)
    _apply6   = _uf(1, False, 3, 42)

### Node attributes and methods

    # Get symbol
    s = _var.symbol
    s = _apply4.symbol

    # Set symbol
    _var.symbol = "new_symbol"

    # Get bit width
    w = _apply4.width
    w = _fun.width

    # Get bit width of array index
    w = _array.index_width

    # Get arity of functions
    a = _fun.arity
    a = _uf.arity

    # Get bit vector representation of constants as string
    bits = _const.bits

    # Dump nodes to stdout or files (default format is BTOR)
    _apply4.Dump()
    # Dump to file 'dump.btor'
    _apply4.Dump(outfile="dump.btor")
    _apply4.Dump("smt2")
    # Dump to file 'dump.smt2'
#    _apply4.Dump("smt2", "dump.smt2")

### Boolector methods

    # Available options
    b.Options()
    # Print available options
    print("Available Boolector options:")
    print("\n".join(["  " + str(o) for o in b.Options()]))

    # Set options
    b.Set_opt(pyboolector.BTOR_OPT_INCREMENTAL, 1)
    b.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, 1)

    # Get options
    o = b.Get_opt(pyboolector.BTOR_OPT_MODEL_GEN)
#    print(o.lng)  # long option name
#    print(o.shrt) # short option name
#    print(o.desc) # description
#    print(o.min)  # min value
#    print(o.max)  # max value
#    print(o.dflt) # default value
#    print(o.val)  # current value

    # Set SAT solver (can only be done before the first Sat() call)
    # Lingeling is the default SAT solver
    #b.Set_sat_solver("MiniSAT")

    # Assert formulas
    b.Assert(_cond0[1])
    b.Assert(_apply5 != _apply3)

    # Assume formulas
    b.Assume(_cond1[1])

    # Run simplification separately
    res = b.Simplify()

    # Clone boolector instance 'b'
    bb = b.Clone()

    # Check sat
    res = b.Sat()
    # Check sat with limits
#    res = b.Sat(100, 10000)
#    res = b.Sat(lod_limit=100, sat_limit=10000)
    if res == b.SAT: print("result: SAT")
    else           : print("result: UNSAT")

    # Get model or query assignments for nodes
    if res == b.SAT:
        print("Model:")
        # Get model and print to stdout
        b.Print_model()
        # Get model and print to file 'model.out'
#        b.Print_model("model.out")

         # Query assignments
#        print("Query assignments:")
#        print("{} {}".format(_var.symbol, _var.assignment))
#        print("{} {}".format(_array.symbol, _array.assignment))
#        print("{} {}".format(_uf.symbol, _uf.assignment))

    # Get matching node of _cond0 in clone 'bb'
    _cond0_matched = bb.Match(_cond0)
    # Assume
    bb.Assume(~_cond0_matched[1])
    bb.Assume(_cond0_matched[2])
    # Check sat
    res = bb.Sat()
    if res == bb.SAT: print("result: SAT")
    else            : print("result: UNSAT")

    if res == b.UNSAT:
        # Check if assumptions are failed
        bb.Failed(~_cond0_matched[1])
        bb.Failed(_cond0_matched[2])

    os.remove("dump.btor")

### Quantifiers
    bbb = Boolector()
    bbb.Set_opt(pyboolector.BTOR_OPT_MODEL_GEN, 1)
    _bvsort   = bbb.BitVecSort(128)
    x        = bbb.Param(_bvsort)
    y        = bbb.Param(_bvsort)
    z        = bbb.Param(_bvsort)
    _exists   = bbb.Exists([x], x > z)
    _forall   = bbb.Forall([y, z], _exists)
    bbb.Assert(_forall)
    res       = bbb.Sat()
    if res == bbb.SAT: print("result: SAT")
    else             : print("result: UNSAT")

### Option interaction
    bbbb = Boolector()
    desired_output_format = pyboolector.BTOR_OUTPUT_FORMAT_AIGER_ASCII
    bbbb.Set_opt(
        pyboolector.BTOR_OPT_OUTPUT_FORMAT, desired_output_format
    )
    assert (
        bbbb.Get_opt(pyboolector.BTOR_OPT_OUTPUT_FORMAT).val
        == desired_output_format
    )
    assert (
        bbbb.Get_opt(pyboolector.BTOR_OPT_OUTPUT_FORMAT).val
        != pyboolector.BTOR_OUTPUT_FORMAT_SMT2
    )