<commit_before>module FunctionEncoding

open FSharp.Data
open DataLoading
open Microsoft.Z3.FSharp.Common
open Microsoft.Z3.FSharp.Bool
open Microsoft.Z3.FSharp.BitVec

let toBool b = if b then True else False

let rec private delete x = function
  | [] -> []
  | h :: t when x = h -> t
  | h :: t -> h :: delete x t

let private numGenes = let statesFilename = System.Environment.GetCommandLineArgs().[1]
                       (CsvFile.Load(statesFilename).Headers |> Option.get |> Seq.length) - 1

let private numNonTransitionEnforcedStates = let nonTransitionEnforcedStatesFilename = System.Environment.GetCommandLineArgs().[5]
                                             readLines nonTransitionEnforcedStatesFilename |> Array.length

let [<Literal>] AND = 0
let [<Literal>] OR = 1
let NOTHING = numGenes + 2

let makeCircuitVar = let numBits = (uint32 << ceil <| System.Math.Log(float numGenes, 2.0)) + 1u
                     fun name -> BitVec (name, numBits)
                     
let makeEnforcedVar = let numBits = (uint32 << ceil <| System.Math.Log(float numNonTransitionEnforcedStates, 2.0)) + 1u
                      fun name -> BitVec (name, numBits)

let private variableDomains lowerBound upperBound var =
    (var >=. lowerBound) &&. (var <=. upperBound)

let private parentsOfNothingArentGates (a : BitVec []) (r : BitVec []) =
    let f c1 c2 p = ((c1 =. NOTHING) ||. (c2 =. NOTHING)) =>. ((p <>. AND) &&. (p <>. OR))

    let aParents = And [| Implies ((a.[1] =. NOTHING) ||. (a.[2] =. NOTHING),  And [| a.[0] <>. AND; a.[0] <>. OR; a.[0] <>. NOTHING |])
                          f a.[3] a.[4] a.[1]
                          f a.[5] a.[6] a.[2] |]

    let rParents = And [| f r.[1] r.[2] r.[0]
                          f r.[3] r.[4] r.[1]
                          f r.[5] r.[6] r.[2] |]
                              
    aParents &&. rParents

let private parentsOfRestAreGates (a : BitVec []) (r : BitVec []) =
    let f c1 c2 p = ((c1 <>. NOTHING) ||. (c2 <>. NOTHING)) =>.  ((p =. AND) ||. (p =. OR))

    let aParents = And [| f a.[1] a.[2] a.[0]
                          f a.[3] a.[4] a.[1]
                          f a.[5] a.[6] a.[2] |]

    let rParents = And [| f r.[1] r.[2] r.[0]
                          f r.[3] r.[4] r.[1]
                          f r.[5] r.[6] r.[2] |]

    aParents &&. rParents

let private variablesDoNotAppearMoreThanOnce symVars =
    let isVar (v : BitVec) = And [| v <>. NOTHING; v <>. AND; v <>. OR |]
    let notEqual v vars = List.map ((<>.) v) vars |> Array.ofList |> And
    let doesNotAppearMoreThanOnce (v : BitVec) = 
        (isVar v) =>. (notEqual v (delete v symVars))
    List.map doesNotAppearMoreThanOnce symVars |> Array.ofList |> And

let private enforceSiblingLexigraphicalOrdering (v1 : BitVec) (v2 : BitVec) =
    v1 <=. v2

let private enforceLexigraphicalOrderingBetweenBranches (p1 : BitVec) (p2 : BitVec) (c1 : BitVec) (c2 : BitVec) =
    (p1 =. p2) =>. (c1 <=. c2)

let private enforceLexigraphicalOrderingNaryGate (vars : BitVec []) =
    (vars.[0] =. vars.[1]) =>. (vars.[2] <=. vars.[3])

let activatorVars = set [ for i in 1..7 do yield "a" + string i ]
let repressorVars = set [ for i in 1..7 do yield "r" + string i ]
let circuitVars = activatorVars + repressorVars

let private fixMaxInputs v max =<commit_msg>Fixed bug: length of bitvector determined from length of wrong file<commit_after>module FunctionEncoding

open FSharp.Data
open DataLoading
open Microsoft.Z3.FSharp.Common
open Microsoft.Z3.FSharp.Bool
open Microsoft.Z3.FSharp.BitVec

let toBool b = if b then True else False

let rec private delete x = function
  | [] -> []
  | h :: t when x = h -> t
  | h :: t -> h :: delete x t

let private numGenes = let statesFilename = System.Environment.GetCommandLineArgs().[1]
                       (CsvFile.Load(statesFilename).Headers |> Option.get |> Seq.length) - 1

let private numNonTransitionEnforcedStates = let nonTransitionEnforcedStatesFilename = System.Environment.GetCommandLineArgs().[6]
                                             readLines nonTransitionEnforcedStatesFilename |> Array.length

let [<Literal>] AND = 0
let [<Literal>] OR = 1
let NOTHING = numGenes + 2

let makeCircuitVar = let numBits = (uint32 << ceil <| System.Math.Log(float numGenes, 2.0)) + 1u
                     fun name -> BitVec (name, numBits)

let makeEnforcedVar = let numBits = (uint32 << ceil <| System.Math.Log(float numNonTransitionEnforcedStates, 2.0)) + 1u
                      fun name -> BitVec (name, numBits)

let private variableDomains lowerBound upperBound var =
    (var >=. lowerBound) &&. (var <=. upperBound)

let private parentsOfNothingArentGates (a : BitVec []) (r : BitVec []) =
    let f c1 c2 p = ((c1 =. NOTHING) ||. (c2 =. NOTHING)) =>. ((p <>. AND) &&. (p <>. OR))

    let aParents = And [| Implies ((a.[1] =. NOTHING) ||. (a.[2] =. NOTHING),  And [| a.[0] <>. AND; a.[0] <>. OR; a.[0] <>. NOTHING |])
                          f a.[3] a.[4] a.[1]
                          f a.[5] a.[6] a.[2] |]

    let rParents = And [| f r.[1] r.[2] r.[0]
                          f r.[3] r.[4] r.[1]
                          f r.[5] r.[6] r.[2] |]
                              
    aParents &&. rParents

let private parentsOfRestAreGates (a : BitVec []) (r : BitVec []) =
    let f c1 c2 p = ((c1 <>. NOTHING) ||. (c2 <>. NOTHING)) =>.  ((p =. AND) ||. (p =. OR))

    let aParents = And [| f a.[1] a.[2] a.[0]
                          f a.[3] a.[4] a.[1]
                          f a.[5] a.[6] a.[2] |]

    let rParents = And [| f r.[1] r.[2] r.[0]
                          f r.[3] r.[4] r.[1]
                          f r.[5] r.[6] r.[2] |]

    aParents &&. rParents

let private variablesDoNotAppearMoreThanOnce symVars =
    let isVar (v : BitVec) = And [| v <>. NOTHING; v <>. AND; v <>. OR |]
    let notEqual v vars = List.map ((<>.) v) vars |> Array.ofList |> And
    let doesNotAppearMoreThanOnce (v : BitVec) = 
        (isVar v) =>. (notEqual v (delete v symVars))
    List.map doesNotAppearMoreThanOnce symVars |> Array.ofList |> And

let private enforceSiblingLexigraphicalOrdering (v1 : BitVec) (v2 : BitVec) =
    v1 <=. v2

let private enforceLexigraphicalOrderingBetweenBranches (p1 : BitVec) (p2 : BitVec) (c1 : BitVec) (c2 : BitVec) =
    (p1 =. p2) =>. (c1 <=. c2)

let private enforceLexigraphicalOrderingNaryGate (vars : BitVec []) =
    (vars.[0] =. vars.[1]) =>. (vars.[2] <=. vars.[3])

let activatorVars = set [ for i in 1..7 do yield "a" + string i ]
let repressorVars = set [ for i in 1..7 do yield "r" + string i ]

let private fixMaxInputs v max =
{'fraction_non_alphanumeric': 0.15937641894959892, 'fraction_numerical': 0.02573028606023914, 'mean_word_length': 2.1496663489037178, 'pattern_counts': {'":': 0, '<': 49, '<?xml version=': 0, '>': 65, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7230163', 'n_tokens_mistral': 2386, 'n_tokens_neox': 2319, 'n_words': 662}