Commit 7748a719 authored by Marek Chalupa's avatar Marek Chalupa
Browse files

Revert "improve hard solving" 

This reverts commit 38d5a278.
It breaks things. We must do that part by part and check for
regressions.
parent 276fc210

slowbeast/solvers/solver.py

+13 −33
Original line number Diff line number Diff line
@@ -283,42 +283,22 @@ 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:

        # 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)

        # First try to rewrite the formula into simpler form

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

        A = []

        for i in range(len(assumptions)):

            a = assumptions[i]

            A.append(

                a.rewrite_polynomials([x for n, x in enumerate(assumptions) if n != i])

            )

        assumptions = A

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

        if r is not None:

            return r

        expr = em.conjunction(*assumptions, expr1)

    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]

        A.append(

            a.rewrite_polynomials([x for n, x in enumerate(assumptions) if n != i])

        )

    assumptions = A

    solver = IncrementalSolver()

    solver.add(*assumptions)

    r = solver.try_is_sat(to1, expr1)

    if r is not None:

        return r

    expr = em.conjunction(*assumptions, expr1)

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



    ###

    # Now try abstractions
@@ -328,7 +308,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.try_is_sat(to2) is False:

            if solver.is_sat() is False:

                return False

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

        # solve the un-abstracted expression

slowbeast/symexe/executionstate.py

+4 −13
Original line number Diff line number Diff line
@@ -99,10 +99,12 @@ 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(self.expr_manager().conjunction(*e))

        return self._solver.is_sat(expr)



    def try_is_sat(self, timeout, *e):

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

        when the state is constructed manually.

        """

        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))

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



    def concretize(self, *e):

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