added option to disable auto config of smt solver

src/Main.hs

@@ -478,17 +478,17 @@ refineTerminalMarkingsUniqueConsensusProperty net traps siphons inequalities c@(
         r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkUnmarkedTrapSat net m0 m1 m2 x1 x2
         case r1 of
             Nothing -> do
-                return (Just c, traps, siphons, inequalities)
---                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkGeneralizedSiphonConstraintsSat net m0 m1 m2 x1 x2
---                case r2 of
---                    Nothing -> do
+                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.checkGeneralizedSiphonConstraintsSat net m0 m1 m2 x1 x2
+                case r2 of
+                    Nothing -> do
+                        return (Just c, traps, siphons, inequalities)
 --                        r3 <- checkSat $ Solver.TerminalMarkingsUniqueConsensus.checkGeneralizedCoTrapSat net m0 m1 m2 x1 x2
 --                        case r3 of
 --                            Nothing -> return (Just c, traps, siphons, inequalities)
 --                            Just inequality ->
 --                                checkTerminalMarkingsUniqueConsensusProperty' net traps siphons (inequality:inequalities)
---                    Just siphon ->
---                        checkTerminalMarkingsUniqueConsensusProperty' net traps (siphon:siphons) inequalities
+                    Just siphon ->
+                        checkTerminalMarkingsUniqueConsensusProperty' net traps (siphon:siphons) inequalities
             Just trap ->
                 checkTerminalMarkingsUniqueConsensusProperty' net (trap:traps) siphons inequalities
 

src/Options.hs

@@ -48,6 +48,7 @@ data Options = Options { inputFormat :: InputFormat
                        , optRefinementType :: Maybe RefinementType
                        , optMinimizeRefinement :: Int
                        , optAuto :: Bool
+                       , optSMTAuto :: Bool
                        , optInvariant :: Bool
                        , optBoolConst :: Bool
                        , optOutput :: Maybe String
@@ -67,6 +68,7 @@ startOptions = Options { inputFormat = PNET
                        , optRefinementType = Just SComponentWithCutRefinement
                        , optMinimizeRefinement = 0
                        , optAuto = False
+                       , optSMTAuto = True
                        , optInvariant = False
                        , optBoolConst = False
                        , optOutput = Nothing
@@ -273,6 +275,10 @@ options =
         (NoArg (\opt -> Right opt { optAuto = True }))
         "Automatically find best refinement, minimization and simplification method"
 
+        , Option "" ["smt-disable-auto-config"]
+        (NoArg (\opt -> Right opt { optSMTAuto = False }))
+        "Disable automatic configuration of the SMT solver"
+
         , Option "v" ["verbose"]
         (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
         "Increase verbosity (may be specified more than once)"

src/Solver.hs

@@ -30,12 +30,18 @@ symConstraints vars constraint = do
         syms <- mapM exists vars
         return $ constraint $ val $ M.fromList $ vars `zip` syms
 
+getSolverConfig :: Bool -> Bool -> SMTConfig
+getSolverConfig verbose auto =
+        let tweaks = if auto then [] else ["(set-option :auto_config false)"]
+        in  z3{ verbose=verbose, solverTweaks=tweaks }
+
 checkSat :: (SatModel a, SymWord a, Show a, Show b) =>
         ConstraintProblem a b -> OptIO (Maybe b)
 checkSat (problemName, resultName, vars, constraint, interpretation) = do
         verbosePut 2 $ "Checking SAT of " ++ problemName
         verbosity <- opt optVerbosity
-        result <- liftIO (satWith z3{verbose=verbosity >= 4}
+        autoConf <- opt optSMTAuto
+        result <- liftIO (satWith (getSolverConfig (verbosity >= 4) autoConf)
                     (symConstraints vars constraint))
         case rebuildModel vars (getModel result) of
             Nothing -> do