symbolic: Use new Crucible goal-proving helpers

[langston-barrett]

Soon, Crucible will have a new API for dispatching proof obligations. Uses of that API could replace the following code in macaw-symbolic:

macaw/symbolic/src/Data/Macaw/Symbolic/Testing.hs

Lines 318 to 352 in 6457541

	proveOneGoal
	:: ( CB.IsSymInterface sym
	, sym ~ WE.ExprBuilder t st fs
	)
	=> WS.SolverAdapter st
	-> sym
	-> CB.Assumptions sym
	-> WL.LabeledPred (WI.Pred sym) CS.SimError
	-> IO ()
	proveOneGoal goalSolver sym asmps lp = do
	assumptions <- CB.assumptionsPred sym asmps
	goal <- WI.notPred sym (lp L.^. WL.labeledPred)
	WS.solver_adapter_check_sat goalSolver sym WS.defaultLogData [assumptions, goal] $ \satRes ->
	case satRes of
	WSR.Unsat {} -> return ()
	WSR.Sat {} -> error ("Failed to prove goal: " ++ show (lp L.^. WL.labeledPredMsg))
	WSR.Unknown {} -> error ("Failed to prove goal: " ++ show (lp L.^. WL.labeledPredMsg))
	return ()
	proveGoals
	:: ( CB.IsSymInterface sym, sym ~ WE.ExprBuilder t st fs )
	=> WS.SolverAdapter st
	-> sym
	-> Maybe (CB.Goals (CB.Assumptions sym) (CB.Assertion sym))
	-> IO ()
	proveGoals goalSolver sym = mapM_ (go mempty)
	where
	go asmps gs =
	case gs of
	CB.Assuming as gs1 -> go (asmps <> as) gs1
	CB.Prove lp -> proveOneGoal goalSolver sym asmps lp
	CB.ProveConj g1 g2 -> do
	go asmps g1
	go asmps g2
	return ()