Add option to switch between Z3 and CVC4 (df541473) · Commits · i7 / peregrine

src/Options.hs

+16 −1

Original line number	Diff line number	Diff line
		{-# LANGUAGE TupleSections #-}

		module Options
		(InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),
		(InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),BackendSolver(..),
		PropertyOption(..),Options(..),startOptions,options,parseArgs,
		usageInformation)
		where
		@@ -20,6 +20,9 @@ instance Show InputFormat where
		instance Show OutputFormat where
		show OutDOT = "DOT"

		data BackendSolver = Z3
		\| CVC4

		data RefinementType = TrapRefinement
		\| SiphonRefinement
		\| UTrapRefinement
		@@ -37,6 +40,7 @@ data Options = Options { inputFormat :: InputFormat
		, optVerbosity :: Int
		, optShowHelp :: Bool
		, optShowVersion :: Bool
		, optSolver :: BackendSolver
		, optProperties :: PropertyOption
		, optRefinementType :: RefinementOption
		, optMinimizeRefinement :: Int
		@@ -52,6 +56,7 @@ startOptions = Options { inputFormat = InPP
		, optVerbosity = 1
		, optShowHelp = False
		, optShowVersion = False
		, optSolver = Options.Z3
		, optProperties = PropDefault
		, optRefinementType = RefDefault
		, optMinimizeRefinement = 0
		@@ -88,6 +93,16 @@ options =
		(NoArg (\opt -> Right opt { optInvariant = True }))
		"Generate an invariant"

		, Option "" ["solver"]
		(ReqArg (\arg opt ->
		case arg of
		"z3" -> Right opt { optSolver = Options.Z3 }
		"cvc4" -> Right opt { optSolver = Options.CVC4 }
		_ -> Left ("invalid argument for refinement method: " ++ arg)
		)
		"SOLVER")
		("Use backend solver SOLVER (z3, cvc4)")

		, Option "r" ["refinement"]
		(ReqArg (\arg opt ->
		let addRef ref =

+10 −3

Original line number	Diff line number	Diff line
		@@ -32,15 +32,22 @@ symConstraints vars exVars allVars constraint = do
		allSyms <- mapM forall allVars
		return $ constraint $ val $ M.fromList $ (vars `zip` syms) ++ (exVars `zip` exSyms) ++ (allVars `zip` allSyms)

		getSolverConfig :: Bool -> SMTConfig
		getSolverConfig verbose = z3{ verbose=verbose }
		getSolverConfig :: BackendSolver -> Bool -> SMTConfig
		getSolverConfig Options.Z3 verbose = z3 { verbose=verbose }
		getSolverConfig Options.CVC4 verbose =
		cvc4 {
		verbose=verbose,
		solverSetOptions = [],
		solver = (solver cvc4) { Data.SBV.options = const ["--lang", "smt", "--incremental", "--no-interactive-prompt"] }
		}

		checkSat :: (SatModel a, SymWord a, Show a, Show b) =>
		ConstraintProblem a b -> OptIO (Maybe b)
		checkSat (problemName, resultName, vars, exVars, allVars, constraint, interpretation) = do
		verbosePut 2 $ "Checking SAT of " ++ problemName
		verbosity <- opt optVerbosity
		result <- liftIO (satWith (getSolverConfig (verbosity >= 4))
		solver <- opt optSolver
		result <- liftIO (satWith (getSolverConfig solver (verbosity >= 4))
		(symConstraints vars exVars allVars constraint))
		case rebuildModel vars (getModelAssignment result) of
		Nothing -> do