Commit 38d5a278 authored by Marek Chalupa's avatar Marek Chalupa
Browse files

improve hard solving

parent 1f2b3f2e

slowbeast/solvers/solver.py

+33 −13
Original line number Diff line number Diff line
@@ -283,9 +283,29 @@ def _sort_subs(subs): 




def try_solve_incrementally(assumptions, exprs, em, to1=3000, to2=1000):

    # check if we can evaluate some expression syntactically

    for a in assumptions:

        exprs = [em.substitute(e, (a, em.getTrue())) for e in exprs]

    # filter out expressions that are 'true'

    exprs = [e for e in exprs if not (e.is_concrete() and bool(e.value()))]



    solver = IncrementalSolver()

    solver.add(*assumptions)

    if assumptions:

        # First try to rewrite the formula into simpler form

        expr1 = em.conjunction(*exprs).rewrite_polynomials(assumptions)

        # try to subsume the implied expressions

        # assert solver.is_sat() is True # otherwise we'll subsume everything

        exprs = [e for e in exprs if solver.try_is_sat(500, em.Not(e)) is not False]

        r = solver.try_is_sat(1000, *exprs)

        if r is not None:

            return r

    else:

        # this will allow us to rewrite expressions

        assumptions = exprs



    # Now try to rewrite the formula into a simpler form

    expr1 = em.conjunction(*exprs)

    if not expr1.is_concrete():

        expr1 = expr1.rewrite_polynomials(assumptions)

    A = []

    for i in range(len(assumptions)):

        a = assumptions[i]
@@ -293,12 +313,12 @@ def try_solve_incrementally(assumptions, exprs, em, to1=3000, to2=1000): 
            a.rewrite_polynomials([x for n, x in enumerate(assumptions) if n != i])

        )

    assumptions = A

        r = IncrementalSolver().try_is_sat(to1, *assumptions, expr1)

    solver = IncrementalSolver()

    solver.add(*assumptions)

    r = solver.try_is_sat(to1, expr1)

    if r is not None:

        return r

    expr = em.conjunction(*assumptions, expr1)

    else:

        expr = em.conjunction(*assumptions, *exprs)



    ###

    # Now try abstractions
@@ -308,7 +328,7 @@ def try_solve_incrementally(assumptions, exprs, em, to1=3000, to2=1000): 
        solver = IncrementalSolver()

        solver.add(rexpr.rewrite_and_simplify())

        for placeholder, e in _sort_subs(subs):

            if solver.is_sat() is False:

            if solver.try_is_sat(to2) is False:

                return False

            solver.add(em.Eq(e, placeholder))

        # solve the un-abstracted expression

slowbeast/symexe/executionstate.py

+13 −4
Original line number Diff line number Diff line
@@ -99,12 +99,10 @@ class SEState(ExecutionState): 
        if r is not None:

            return r



        conj = self.expr_manager().conjunction

        expr = conj(*e)

        r = try_solve_incrementally(self.constraints(), e, self.expr_manager())

        if r is not None:

            return r

        return self._solver.is_sat(expr)

        return self._solver.is_sat(self.expr_manager().conjunction(*e))



    def try_is_sat(self, timeout, *e):

        return self._solver.try_is_sat(timeout, *e)
@@ -114,7 +112,18 @@ class SEState(ExecutionState): 
        Solve the PC and return True if it is sat. Handy in the cases

        when the state is constructed manually.

        """

        return self.is_sat(*self.constraints())

        C = self.constraints()

        if not C:

            return True

        r = self._solver.try_is_sat(1000, *C)

        if r is not None:

            return r



        em = self.expr_manager()

        r = try_solve_incrementally([], C, em)

        if r is not None:

            return r

        return self._solver.is_sat(em.conjunction(*C))



    def concretize(self, *e):

        return self._solver.concretize(self.constraints(), *e)