Commit fb806c12 authored by Marek Chalupa's avatar Marek Chalupa
Browse files

solver: do not solve reduced formulas

parent b9e5decd

slowbeast/domains/symbolic.py

+13 −11
Original line number Diff line number Diff line
@@ -768,27 +768,33 @@ if _use_z3: 
                nc = Not(chld[0] + 1 <= chld[1])

                if nc in clauses:

                    eqs.append((clause, nc, chld[0] == chld[1]))

                    continue

                nc = (chld[1] <= chld[0])

                if nc in clauses:

                    eqs.append((clause, nc, chld[0] == chld[1]))

                    continue

                nc = (chld[0] >= chld[1])

                if nc in clauses:

                    eqs.append((clause, nc, chld[0] == chld[1]))

                    continue

            if is_app_of(clause, Z3_OP_ULEQ):

                chld = clause.children()

                nc = Not(ULE(1 + chld[0], chld[1]))

                nc = Not(BVULE(1 + chld[0], chld[1]))

                if nc in clauses:

                    eqs.append((clause, nc, chld[0] == chld[1]))

                    continue

                nc = Not(ULE(chld[0] + 1, chld[1]))

                nc = Not(BVULE(chld[0] + 1, chld[1]))

                if nc in clauses:

                    eqs.append((clause, nc, chld[0] == chld[1]))

                nc = UGE(chld[0], chld[1])

                    continue

                nc = BVUGE(chld[0], chld[1])

                if nc in clauses:

                    eqs.append((clause, nc, chld[0] == chld[1]))

                nc = ULE(chld[1], chld[0])

                    continue

                nc = BVULE(chld[1], chld[0])

                if nc in clauses:

                    eqs.append((clause, nc, chld[0] == chld[1]))

                    continue

        return eqs



    def eqs_from_ineqs(expr):
@@ -838,13 +844,9 @@ if _use_z3: 
            # is underapproximation

            return expr

        else:

            red = (_reduce_eq_bitwidth(c, bw) for c in chld)

            if is_and(expr):

                return mk_and(*red)

            elif is_or(expr):

                return mk_or(*red)

            # elif is_add(expr): return Sum(*red)

            # elif is_mul(expr): return Product(*red)

            red = [_reduce_eq_bitwidth(c, bw) for c in chld]

            if is_and(expr): return mk_and(*red)

            elif is_or(expr): return mk_or(*red)

            else:

                return expr.decl()(*red)

slowbeast/solvers/solver.py

+15 −15
Original line number Diff line number Diff line
@@ -312,22 +312,22 @@ def solve_incrementally(assumptions, exprs, em, to1=3000, to2=500): 
    if expr.is_concrete():

        return bool(expr.value())



    # FIXME try reduced bitwidth with propagating back models instead of this

    solver = IncrementalSolver()

    for bw in (1, 2, 4, 8, 16):

        # FIXME: handle signed/unsinged and negations correctly in

        # reduce_arith_bitwidth and use that

        solver.add(expr.reduce_eq_bitwidth(bw).rewrite_and_simplify())

        r = solver.try_is_sat(bw*500)

        if r is False: return False

        elif r is None:

            break

        assert r is True

        # the reduced subformulas are sat. Try to check the original formula

        # with the knowledge about the reduced formulas stored in the solver

        r = solver.try_is_sat(bw*500, expr)

        if r is not None:

            return r

    # FIXME try reduced bitwidth with propagating back models instead of this

   #for bw in (1, 2, 4, 8, 16):

   #    # FIXME: handle signed/unsinged and negations correctly in

   #    # reduce_arith_bitwidth and use that

   #    solver.add(expr.reduce_eq_bitwidth(bw).rewrite_and_simplify())

   #    r = solver.try_is_sat(bw*500)

   #    if r is False: return False

   #    elif r is None:

   #        break

   #    assert r is True

   #    # the reduced subformulas are sat. Try to check the original formula

   #    # with the knowledge about the reduced formulas stored in the solver

   #    r = solver.try_is_sat(bw*500, expr)

   #    if r is not None:

   #        return r

    ###

    # Now try abstractions

    #