<commit_before>-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Core.Symbolic
-- Copyright   :  (c) <NAME>
-- License     :  BSD3
-- Maintainer  :  <EMAIL>
-- Stability   :  experimental
--
-- Symbolic values
-----------------------------------------------------------------------------

{-# LANGUAGE    GeneralizedNewtypeDeriving #-}
{-# LANGUAGE    TypeSynonymInstances       #-}
{-# LANGUAGE    TypeOperators              #-}
{-# LANGUAGE    MultiParamTypeClasses      #-}
{-# LANGUAGE    ScopedTypeVariables        #-}
{-# LANGUAGE    FlexibleInstances          #-}
{-# LANGUAGE    PatternGuards              #-}
{-# LANGUAGE    NamedFieldPuns             #-}
{-# LANGUAGE    DeriveDataTypeable         #-}
{-# LANGUAGE    DeriveFunctor              #-}
{-# LANGUAGE    CPP                        #-}
{-# OPTIONS_GHC -fno-warn-orphans          #-}

module Data.SBV.Core.Symbolic
  ( NodeId(..)
  , SW(..), swKind, trueSW, falseSW
  , Op(..), PBOp(..), FPOp(..)
  , Quantifier(..), needsExistentials
  , RoundingMode(..)
  , SBVType(..), newUninterpreted, addAxiom
  , SVal(..)
  , svMkSymVar
  , ArrayContext(..), ArrayInfo
  , svToSW, svToSymSW, forceSWArg
  , SBVExpr(..), newExpr, isCodeGenMode
  , Cached, cache, uncache
  , ArrayIndex, uncacheAI
  , NamedSymVar
  , getSValPathCondition, extendSValPathCondition
  , getTableIndex
  , SBVPgm(..), Symbolic, runSymbolic, runSymbolicWithState, runSymbolic', State, withNewIncState, IncState(..)
  , inProofMode, inNonInteractiveProofMode, switchToInteractiveMode, getProofMode, SBVRunMode(..), Result(..)
  , Logic(..), SMTLibLogic(..), registerKind, registerLabel
  , addAssertion, addSValConstraint, internalConstraint, internalVariable
  , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension
  , SolverCapabilities(..)
  , extractSymbolicSimulationState
  , OptimizeStyle(..), Objective(..), Penalty(..), objectiveName, addSValOptGoal
  , Tactic(..), addSValTactic, isParallelCaseAnywhere
  , Query(..), QueryContext(..), QueryState(..), query, runQuery
  , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine, getSBranchRunConfig
  , outputSVal
  , mkSValUserSort
  , SArr(..), readSArr, resetSArr, writeSArr, mergeSArr, newSArr, eqSArr
  ) where
<commit_msg>Export State constructors<commit_after>-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Core.Symbolic
-- Copyright   :  (c) <NAME>
-- License     :  BSD3
-- Maintainer  :  <EMAIL>
-- Stability   :  experimental
--
-- Symbolic values
-----------------------------------------------------------------------------

{-# LANGUAGE    GeneralizedNewtypeDeriving #-}
{-# LANGUAGE    TypeSynonymInstances       #-}
{-# LANGUAGE    TypeOperators              #-}
{-# LANGUAGE    MultiParamTypeClasses      #-}
{-# LANGUAGE    ScopedTypeVariables        #-}
{-# LANGUAGE    FlexibleInstances          #-}
{-# LANGUAGE    PatternGuards              #-}
{-# LANGUAGE    NamedFieldPuns             #-}
{-# LANGUAGE    DeriveDataTypeable         #-}
{-# LANGUAGE    DeriveFunctor              #-}
{-# LANGUAGE    CPP                        #-}
{-# OPTIONS_GHC -fno-warn-orphans          #-}

module Data.SBV.Core.Symbolic
  ( NodeId(..)
  , SW(..), swKind, trueSW, falseSW
  , Op(..), PBOp(..), FPOp(..)
  , Quantifier(..), needsExistentials
  , RoundingMode(..)
  , SBVType(..), newUninterpreted, addAxiom
  , SVal(..)
  , svMkSymVar
  , ArrayContext(..), ArrayInfo
  , svToSW, svToSymSW, forceSWArg
  , SBVExpr(..), newExpr, isCodeGenMode
  , Cached, cache, uncache
  , ArrayIndex, uncacheAI
  , NamedSymVar
  , getSValPathCondition, extendSValPathCondition
  , getTableIndex
  , SBVPgm(..), Symbolic, runSymbolic, runSymbolicWithState, runSymbolic', State(..), withNewIncState, IncState(..)
  , inProofMode, inNonInteractiveProofMode, switchToInteractiveMode, getProofMode, SBVRunMode(..), Result(..)
  , Logic(..), SMTLibLogic(..), registerKind, registerLabel
  , addAssertion, addSValConstraint, internalConstraint, internalVariable
  , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension
  , SolverCapabilities(..)
  , extractSymbolicSimulationState
  , OptimizeStyle(..), Objective(..), Penalty(..), objectiveName, addSValOptGoal
  , Tactic(..), addSValTactic, isParallelCaseAnywhere
  , Query(..), QueryContext(..), QueryState(..), query, runQuery
  , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine, getSBranchRunConfig
  , outputSVal
  , mkSValUserSort
  , SArr(..), readSArr, resetSArr, writeSArr, mergeSArr, newSArr, eqSArr
  ) where

{'fraction_non_alphanumeric': 0.21223791185280275, 'fraction_numerical': 0.0004278990158322636, 'mean_word_length': 2.299223712067749, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, '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': '1275544', 'n_tokens_mistral': 1598, 'n_tokens_neox': 1595, 'n_words': 264}