<commit_before>-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Provers.CVC4
-- Copyright   :  (c) <NAME>
-- License     :  BSD3
-- Maintainer  :  <EMAIL>
-- Stability   :  experimental
--
-- The connection to the CVC4 SMT solver
-----------------------------------------------------------------------------

{-# LANGUAGE ScopedTypeVariables #-}

module Data.SBV.Provers.CVC4(cvc4) where

import Data.Maybe (isNothing)

import Data.SBV.Core.Data
import Data.SBV.SMT.SMT

-- | The description of the CVC4 SMT solver
-- The default executable is @\"cvc4\"@, which must be in your path. You can use the @SBV_CVC4@ environment variable to point to the executable on your system.
-- The default options are @\"--lang smt\"@. You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options.
cvc4 :: SMTSolver
cvc4 = SMTSolver {
           name         = CVC4
         , executable   = "cvc4"
         , options      = ["--lang", "smt"]
         , engine       = standardEngine "SBV_CVC4" "SBV_CVC4_OPTIONS" modConfig addTimeOut standardModel
         , capabilities = SolverCapabilities {
                                capSolverName              = "CVC4"
                              , mbDefaultLogic             = const (Just "ALL_SUPPORTED")  -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary
                              , supportsDefineFun          = True
                              , supportsProduceModels      = True
                              , supportsQuantifiers        = True
                              , supportsUninterpretedSorts = True
                              , supportsUnboundedInts      = True
                              , supportsReals              = True  -- Not quite the same capability as Z3; but works more or less..
                              , supportsFloats             = False
                              , supportsDoubles            = False
                              , supportsOptimization       = False
                              , supportsPseudoBooleans     = False
                              , supportsUnsatCores         = False
                              , supportsCustomQueries      = True
                              }
         }
 where addTimeOut o i | i < 0 = error $ "CVC4: Timeout value must be non-negative, received: " ++ show i
                      | True  = o ++ ["--tlimit=" ++ show i ++ "000"]  -- SBV takes seconds, CVC4 wants milli-seconds

       -- If custom queries are present, CVC4 requires an explicit command-line argument
       modConfig :: SMTConfig -> SMTConfig
       modConfig cfg
        | isNothing (customQuery cfg) = cfg
        | True                        = cfg {solver = (solver cfg) {options = newOpts}}
        where newOpts = options (solver cfg) ++ ["--interactive"]<commit_msg>Fix cvc4 incremental call options<commit_after>-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Provers.CVC4
-- Copyright   :  (c) <NAME>
-- License     :  BSD3
-- Maintainer  :  <EMAIL>
-- Stability   :  experimental
--
-- The connection to the CVC4 SMT solver
-----------------------------------------------------------------------------

{-# LANGUAGE ScopedTypeVariables #-}

module Data.SBV.Provers.CVC4(cvc4) where

import Data.Maybe (isNothing)

import Data.SBV.Core.Data
import Data.SBV.SMT.SMT

-- | The description of the CVC4 SMT solver
-- The default executable is @\"cvc4\"@, which must be in your path. You can use the @SBV_CVC4@ environment variable to point to the executable on your system.
-- The default options are @\"--lang smt\"@. You can use the @SBV_CVC4_OPTIONS@ environment variable to override the options.
cvc4 :: SMTSolver
cvc4 = SMTSolver {
           name         = CVC4
         , executable   = "cvc4"
         , options      = ["--lang", "smt"]
         , engine       = standardEngine "SBV_CVC4" "SBV_CVC4_OPTIONS" modConfig addTimeOut standardModel
         , capabilities = SolverCapabilities {
                                capSolverName              = "CVC4"
                              , mbDefaultLogic             = const (Just "ALL_SUPPORTED")  -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary
                              , supportsDefineFun          = True
                              , supportsProduceModels      = True
                              , supportsQuantifiers        = True
                              , supportsUninterpretedSorts = True
                              , supportsUnboundedInts      = True
                              , supportsReals              = True  -- Not quite the same capability as Z3; but works more or less..
                              , supportsFloats             = False
                              , supportsDoubles            = False
                              , supportsOptimization       = False
                              , supportsPseudoBooleans     = False
                              , supportsUnsatCores         = False
                              , supportsCustomQueries      = True
                              }
         }
 where addTimeOut o i | i < 0 = error $ "CVC4: Timeout value must be non-negative, received: " ++ show i
                      | True  = o ++ ["--tlimit=" ++ show i ++ "000"]  -- SBV takes seconds, CVC4 wants milli-seconds

       -- If custom queries are present, CVC4 requires an explicit command-line argument
       modConfig :: SMTConfig -> SMTConfig
       modConfig cfg
        | isNothing (customQuery cfg) = cfg
        | True                        = cfg {solver = (solver cfg) {options = newOpts}}
        where newOpts = options (solver cfg) ++ ["--incremental", "--interactive", "--no-interactive-prompt"]
{'fraction_non_alphanumeric': 0.13128205128205128, 'fraction_numerical': 0.008717948717948718, 'mean_word_length': 1.2599459250675937, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3591248', 'n_tokens_mistral': 1484, 'n_tokens_neox': 1452, 'n_words': 445}