Commit 1c8f5fe1 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Small refactoring in the solver sat function

parent dd79a707
...@@ -11,9 +11,6 @@ import Solver.StateEquation ...@@ -11,9 +11,6 @@ import Solver.StateEquation
import Solver.TransitionInvariant import Solver.TransitionInvariant
import Solver.TrapConstraints import Solver.TrapConstraints
-- TODO: check type of property and only do trap refinement for safety
-- properties
checkSafetyProperty :: PetriNet -> Formula -> [[String]] -> IO Bool checkSafetyProperty :: PetriNet -> Formula -> [[String]] -> IO Bool
checkSafetyProperty net f traps = do checkSafetyProperty net f traps = do
r <- checkSat $ checkStateEquationSat net f traps r <- checkSat $ checkStateEquationSat net f traps
......
...@@ -26,5 +26,5 @@ checkSat :: (SatModel a, SymWord a) => ...@@ -26,5 +26,5 @@ checkSat :: (SatModel a, SymWord a) =>
([String], M.Map String (SBV a) -> SBool) -> ([String], M.Map String (SBV a) -> SBool) ->
IO (Maybe (M.Map String a)) IO (Maybe (M.Map String a))
checkSat (vars, constraint) = do checkSat (vars, constraint) = do
result <- sat $ symConstraints vars constraint result <- satWith z3{verbose=False} $ symConstraints vars constraint
return $ rebuildModel vars $ getModel result return $ rebuildModel vars $ getModel result
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment