<commit_before>----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.SMT.SMTLib2
-- Copyright   :  (c) <NAME>
-- License     :  BSD3
-- Maintainer  :  <EMAIL>
-- Stability   :  experimental
-- Portability :  portable
--
-- Conversion of symbolic programs to SMTLib format, Using v2 of the standard
-----------------------------------------------------------------------------
{-# LANGUAGE PatternGuards #-}

module Data.SBV.SMT.SMTLib2(cvt, addNonEqConstraints) where

import qualified Data.Foldable as F (toList)
import qualified Data.Map      as M
import Data.List (intercalate)
import Numeric (showHex)

import Data.SBV.BitVectors.Data

addNonEqConstraints :: [[(String, CW)]] -> SMTLibPgm -> String
addNonEqConstraints nonEqConstraints (SMTLibPgm _ (aliasTable, pre, post)) = intercalate "\n" $
     pre
  ++ [ "; --- refuted-models ---" ]
  ++ concatMap nonEqs (map (map intName) nonEqConstraints)
  ++ post
 where intName (s, c)
          | Just sw <- s `lookup` aliasTable = (show sw, c)
          | True                             = (s, c)

nonEqs :: [(String, CW)] -> [String]
nonEqs []     =  []
nonEqs [sc]   =  ["(assert " ++ nonEq sc ++ ")"]
nonEqs (sc:r) =  ["(assert (or " ++ nonEq sc]
              ++ map (("           " ++) . nonEq) r
              ++ ["        ))"]

nonEq :: (String, CW) -> String
nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))"

tbd :: String -> a
tbd m = error $ "SBV.SMTLib2: Not-yet-supported: " ++ m ++ ". Please report."

cvt :: Bool                                        -- ^ is this a sat problem?
    -> [String]                                    -- ^ extra comments to place on top
    -> [(Quantifier, NamedSymVar)]                 -- ^ inputs and aliasing names
    -> [(SW, CW)]                                  -- ^ constants
    -> [((Int, (Bool, Int), (Bool, Int)), [SW])]   -- ^ auto-generated tables
    -> [(Int, ArrayInfo)]                          -- ^ user specified arrays
    -> [(String, SBVType)]                         -- ^ uninterpreted functions/constants
    -> [(String, [String])]                        -- ^ user given axioms
    -> Pgm                                         -- ^ assignments
    -> SW                                          -- ^ output variable
    -> ([String], [String])
cvt isSat comments qinps consts tbls arrs uis axs asgnsSeq out
  | not (null uis)
  = tbd "uninterpreted functions"
  | not (null axs)
  = tbd "axioms"
  | not (null tbls)
  = tbd "look-up tables"
  | not (null arrs)
  = tbd "user defined arrays"
  | True
  = (pre, extractModel)
  where pre  =  [ "; Automatically generated by SBV. Do not edit." ]
             ++ map ("; " ++) comments
             ++ [ "(set-option :produce-models true)"
                , "(set-logic UFBV)"
                , "; --- literal constants ---"
                ]
             ++ concatMap declConst consts
             ++ [ "; --- skolem constants ---" ]
             ++ [ "(declare-fun " ++ show s ++ " " ++ smtFunType ss s ++ ")" | Right (s, ss) <- skolemInps]
             ++ [ "; --- formula ---" ]
             ++ [ "(assert (forall (" ++ intercalate "\n                 " ["(" ++ show s ++ " " ++ smtType s ++ ")" | Left s <- skolemInps] ++ ")" ]
             ++ map (("            " ++) . mkLet) asgns
             ++ [ "                 " ++ assertOut ++ replicate (2 + length asgns) ')' ]
        assertOut
           | isSat = "(= " ++ show out ++ " #b1)"
           | True  = "(= " ++ show out ++ " #b0)"
        extractModel = "(check-sat)" : [extract s ss | Right (s, ss) <- skolemInps]
          where extract s [] = "(get-value (" ++ show s ++ "))"
                extract s ss = "(eval (" ++ show s ++ concat [" #x0000" | _ <- ss] ++ "))"
        skolemInps = skolemize (if isSat then qinps else map flipQ qinps)
          where flipQ (ALL, x) = (EX, x)
                flipQ (EX, x)  = (ALL, x)
        skolemMap = M.fromList [(s, ss) | Right (s, ss) <- skolemInps, not (null ss)]
        asgns = F.toList asgnsSeq
        mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp skolemMap e ++ "))" 
        declConst (s, c) = [ "(declare-fun " ++ show s ++ " " ++ smtFunType [] s ++ ")"
                           , "(assert (= " ++ show s ++ " " ++ cvtCW c ++ "))"<commit_msg>SMTLib2: skip the for all if there are no universals<commit_after>----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.SMT.SMTLib2
-- Copyright   :  (c) <NAME>
-- License     :  BSD3
-- Maintainer  :  <EMAIL>
-- Stability   :  experimental
-- Portability :  portable
--
-- Conversion of symbolic programs to SMTLib format, Using v2 of the standard
-----------------------------------------------------------------------------
{-# LANGUAGE PatternGuards #-}

module Data.SBV.SMT.SMTLib2(cvt, addNonEqConstraints) where

import qualified Data.Foldable as F (toList)
import qualified Data.Map      as M
import Data.List (intercalate)
import Numeric (showHex)

import Data.SBV.BitVectors.Data

addNonEqConstraints :: [[(String, CW)]] -> SMTLibPgm -> String
addNonEqConstraints nonEqConstraints (SMTLibPgm _ (aliasTable, pre, post)) = intercalate "\n" $
     pre
  ++ [ "; --- refuted-models ---" ]
  ++ concatMap nonEqs (map (map intName) nonEqConstraints)
  ++ post
 where intName (s, c)
          | Just sw <- s `lookup` aliasTable = (show sw, c)
          | True                             = (s, c)

nonEqs :: [(String, CW)] -> [String]
nonEqs []     =  []
nonEqs [sc]   =  ["(assert " ++ nonEq sc ++ ")"]
nonEqs (sc:r) =  ["(assert (or " ++ nonEq sc]
              ++ map (("           " ++) . nonEq) r
              ++ ["        ))"]

nonEq :: (String, CW) -> String
nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))"

tbd :: String -> a
tbd m = error $ "SBV.SMTLib2: Not-yet-supported: " ++ m ++ ". Please report."

cvt :: Bool                                        -- ^ is this a sat problem?
    -> [String]                                    -- ^ extra comments to place on top
    -> [(Quantifier, NamedSymVar)]                 -- ^ inputs and aliasing names
    -> [(SW, CW)]                                  -- ^ constants
    -> [((Int, (Bool, Int), (Bool, Int)), [SW])]   -- ^ auto-generated tables
    -> [(Int, ArrayInfo)]                          -- ^ user specified arrays
    -> [(String, SBVType)]                         -- ^ uninterpreted functions/constants
    -> [(String, [String])]                        -- ^ user given axioms
    -> Pgm                                         -- ^ assignments
    -> SW                                          -- ^ output variable
    -> ([String], [String])
cvt isSat comments qinps consts tbls arrs uis axs asgnsSeq out
  | not (null uis)
  = tbd "uninterpreted functions"
  | not (null axs)
  = tbd "axioms"
  | not (null tbls)
  = tbd "look-up tables"
  | not (null arrs)
  = tbd "user defined arrays"
  | True
  = (pre, extractModel)
  where pre  =  [ "; Automatically generated by SBV. Do not edit." ]
             ++ map ("; " ++) comments
             ++ [ "(set-option :produce-models true)"
                , "(set-logic UFBV)"
                , "; --- literal constants ---"
                ]
             ++ concatMap declConst consts
             ++ [ "; --- skolem constants ---" ]
             ++ [ "(declare-fun " ++ show s ++ " " ++ smtFunType ss s ++ ")" | Right (s, ss) <- skolemInps]
             ++ [ "; --- formula ---" ]
             ++ [if null foralls
                 then "(assert "
                 else "(assert (forall (" ++ intercalate "\n                 "
                                             ["(" ++ show s ++ " " ++ smtType s ++ ")" | s <- foralls] ++ ")"]
             ++ map (letAlign . mkLet) asgns
             ++ [ letAlign assertOut ++ replicate ((if null foralls then 1 else 2) + length asgns) ')' ]
        foralls = [s | Left s <- skolemInps]
        letAlign s
          | null foralls = "   " ++ s
          | True         = "            " ++ s
        assertOut
           | isSat = "(= " ++ show out ++ " #b1)"
           | True  = "(= " ++ show out ++ " #b0)"
        extractModel = "(check-sat)" : [extract s ss | Right (s, ss) <- skolemInps]
          where extract s [] = "(get-value (" ++ show s ++ "))"
                extract s ss = "(eval (" ++ show s ++ concat [" #x0000" | _ <- ss] ++ "))"
        skolemInps = skolemize (if isSat then qinps else map flipQ qinps)
          where flipQ (ALL, x) = (EX, x)
                flipQ (EX, x)  = (ALL, x)
        skolemMap = M.fromList [(s, ss) | Right (s, ss) <- skolemInps, not (null ss)]
        asgns = F.toList asgnsSeq
        mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp skolemMap e ++ "))" 
        declConst (s, c) = [ "(declare-fun " ++ show s ++ " " ++ smtFunType [] s ++ ")"
                           , "(assert (= " ++ show s ++ " " ++ cvtCW c ++ "))"
{'fraction_non_alphanumeric': 0.19889998877539566, 'fraction_numerical': 0.002918397126501291, 'mean_word_length': 1.4324324324324325, 'pattern_counts': {'":': 0, '<': 20, '<?xml version=': 0, '>': 37, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 27, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '884942', 'n_tokens_mistral': 2815, 'n_tokens_neox': 2712, 'n_words': 758}