diff --git a/.gitignore b/.gitignore index c616bfc..44464ca 100644 --- a/.gitignore +++ b/.gitignore @@ -4,4 +4,7 @@ /src/tempfile.jl /Manifest.toml /docs/build/ -/test/data/* \ No newline at end of file +/test/data/* +src/espresso.linux +src/abc +src/boom.exe diff --git a/src/minimize.jl b/src/minimize.jl index f7d4ee9..a1d087f 100644 --- a/src/minimize.jl +++ b/src/minimize.jl @@ -1,4 +1,5 @@ """ +by https://jackhack96.github.io/logic-synthesis/espresso.html. espresso_minimize( syntaxtree::SoleLogics.Formula, silent::Bool = true, @@ -81,3 +82,509 @@ function espresso_minimize( conditionstype = use_scalar_range_conditions ? SoleData.RangeScalarCondition : SoleData.ScalarCondition return PLA._pla_to_formula(minimized_pla, silent, pla_args...; conditionstype, pla_kwargs...) end + +""" +by https://github.com/berkeley-abc/abc +abc_minimize( + syntaxtree::SoleLogics.Formula, + silent::Bool = true, + args...; + abcbinary = nothing, + otherflags = [], + use_scalar_range_conditions = false, + kwargs... +) +""" +function abc_minimize( + syntaxtree::SoleLogics.Formula, + silent::Bool = true, + args...; + fast = true, + abcbinary = nothing, + otherflags = [], + use_scalar_range_conditions = false, + kwargs... +) + if isnothing(abcbinary) + # Determine the path of the abc binary relative to the location of this file + # Consider downloading abc from https://github.com/berkeley-abc/abc. + abcbinary = joinpath(@__DIR__, "abc") + if !isfile(abcbinary) + error("abc binary not found at $abcbinary, provide path with abcbinary argument") + end + end + + # Funzione interna per rimuovere spazi da stringhe + removewhitespaces(s::AbstractString) = replace(s, r"\s+" => "") + + # Converte formula in PLA string + dc_set = false + pla_string, pla_args, pla_kwargs = PLA._formula_to_pla(syntaxtree, dc_set, silent; use_scalar_range_conditions=use_scalar_range_conditions) + + silent || println("Input PLA:\n$pla_string\n") + + # Validazione e correzione del formato PLA + function validate_and_fix_pla(pla_content::String) + lines = split(pla_content, '\n') + filtered_lines = filter(line -> !isempty(strip(line)), lines) + filtered_lines = map(line -> replace(line, "≥" => ">="), filtered_lines) + + # Trova le righe di intestazione + i_line_idx = findfirst(line -> startswith(line, ".i "), filtered_lines) + o_line_idx = findfirst(line -> startswith(line, ".o "), filtered_lines) + ilb_line_idx = findfirst(line -> startswith(line, ".ilb "), filtered_lines) + olb_line_idx = findfirst(line -> startswith(line, ".olb "), filtered_lines) + + if isnothing(i_line_idx) || isnothing(o_line_idx) + error("PLA format invalid: missing .i or .o lines") + end + + # Estrai il numero di input/output + i_count = parse(Int, split(filtered_lines[i_line_idx])[2]) + o_count = parse(Int, split(filtered_lines[o_line_idx])[2]) + + # Conta le variabili effettive dai label se esistono + actual_inputs = 0 + if !isnothing(ilb_line_idx) + ilb_parts = split(filtered_lines[ilb_line_idx])[2:end] + actual_inputs = length(ilb_parts) + else + # Se non ci sono label, conta dalle righe di prodotto + product_lines = filter(line -> occursin(r"^[01\-]+ ", line), filtered_lines) + if !isempty(product_lines) + first_product = split(product_lines[1])[1] + actual_inputs = length(first_product) + end + end + + # Correggi il mismatch se necessario + if actual_inputs > 0 && actual_inputs != i_count + silent || println("Fixing input count mismatch: declared=$i_count, actual=$actual_inputs") + filtered_lines[i_line_idx] = ".i $actual_inputs" + end + + + return join(filtered_lines, '\n') + end + + # Valida e correggi il PLA + corrected_pla = validate_and_fix_pla(String(pla_string)) + silent || println("corrected pls: \n",corrected_pla) + # File temporanei input e output + inputfile = tempname() * ".pla" + outputfile = tempname() * ".pla" + + try + # Scrivi PLA corretto su file input + open(inputfile, "w") do f + write(f, corrected_pla) + end + + silent || println("Corrected PLA written to: $inputfile") + + # Comando abc + if fast + abc_commands = [ + "read $inputfile", + "strash", + "dc2", + "collapse", + "write $outputfile" + + #"read $inputfile", + #"strash", # diretto in AIG + #"refactor -z", # flag -z per velocità + #"rewrite -z", + #"balance", + #"collapse", + #"write $outputfile" # mantieni AIG ottimizzato + ] + else + abc_commands = [ + "read $inputfile", + "sop", + "strash", + "dc2", + "collapse", + "strash", + "dc2", + "collapse", + "sop", + "write $outputfile" + ] + end + + abc_cmd_str = join(abc_commands, "; ") + abc_cmd = `$abcbinary -c $abc_cmd_str` + + silent || println("Running ABC command: $abc_cmd") + + # Esegui comando con cattura output/errori + result = try + run(abc_cmd) + true + catch e + silent || println("ABC command failed: $e") + false + end + + if !result || !isfile(outputfile) + silent || println("ABC failed or output file not created, returning original formula") + return syntaxtree + end + + # Leggi output minimizzato + minimized_pla_raw = read(outputfile, String) + minimized_pla_raw = replace(minimized_pla_raw, ">=" => "≥") + + silent || println("good minimze the king: ",minimized_pla_raw) + + if isempty(strip(minimized_pla_raw)) + silent || println("Empty ABC output, returning original formula") + return syntaxtree + end + + silent || println("Raw minimized PLA output:\n$minimized_pla_raw\n") + + # Pulizia output + function clean_abc_output(raw_pla::String) + lines = split(raw_pla, '\n') + pla_lines = filter(line -> !isempty(strip(line)) && + (startswith(line, '.') || occursin(r"^[01\-]+ ", line)), lines) + return join(pla_lines, '\n') + end + + minimized_pla = clean_abc_output(minimized_pla_raw) + + println("Cleaned minimized PLA:\n$minimized_pla\n") + + conditionstype = use_scalar_range_conditions ? SoleData.RangeScalarCondition : SoleData.ScalarCondition + + # Converti PLA minimizzato in formula + try + form = PLA._pla_to_formula(minimized_pla, silent, pla_args...; conditionstype, pla_kwargs...) + println("formula returned: ",form) + return form + catch e + silent || println("Failed to convert minimized PLA back to formula: $e") + silent || println("Returning original formula") + return syntaxtree + end + + finally + # Elimina file temporanei + rm(inputfile; force=true) + rm(outputfile; force=true) + end +end + +#= + function espressoTexas_minimize( + syntaxtree::SoleLogics.Formula, + silent::Bool = true, + args...; + espressobinary = nothing, + otherflags = [], + use_scalar_range_conditions = false, + kwargs... + ) + if isnothing(espressobinary) + # Determine the path of the abc binary relative to the location of this file + # Consider downloading abc from https://github.com/berkeley-abc/abc. + espressobinary = joinpath(@__DIR__, "espresso.linux") + if !isfile(espressobinary) + error("abc binary not found at $espressobinary, provide path with espressobinary argument") + end + end + + # Funzione interna per rimuovere spazi da stringhe + removewhitespaces(s::AbstractString) = replace(s, r"\s+" => "") + + # Converte formula in PLA string + dc_set = false + pla_string, pla_args, pla_kwargs = PLA._formula_to_pla(syntaxtree, dc_set, silent; use_scalar_range_conditions=use_scalar_range_conditions) + + silent || println("Input PLA:\n$pla_string\n") + + # Validazione e correzione del formato PLA + function validate_and_fix_pla(pla_content::String) + lines = split(pla_content, '\n') + filtered_lines = filter(line -> !isempty(strip(line)), lines) + + # Trova le righe di intestazione + i_line_idx = findfirst(line -> startswith(line, ".i "), filtered_lines) + o_line_idx = findfirst(line -> startswith(line, ".o "), filtered_lines) + ilb_line_idx = findfirst(line -> startswith(line, ".ilb "), filtered_lines) + olb_line_idx = findfirst(line -> startswith(line, ".olb "), filtered_lines) + + if isnothing(i_line_idx) || isnothing(o_line_idx) + error("PLA format invalid: missing .i or .o lines") + end + + # Estrai il numero di input/output + i_count = parse(Int, split(filtered_lines[i_line_idx])[2]) + o_count = parse(Int, split(filtered_lines[o_line_idx])[2]) + + # Conta le variabili effettive dai label se esistono + actual_inputs = 0 + if !isnothing(ilb_line_idx) + ilb_parts = split(filtered_lines[ilb_line_idx])[2:end] + actual_inputs = length(ilb_parts) + else + # Se non ci sono label, conta dalle righe di prodotto + product_lines = filter(line -> occursin(r"^[01\-]+ ", line), filtered_lines) + if !isempty(product_lines) + first_product = split(product_lines[1])[1] + actual_inputs = length(first_product) + end + end + + # Correggi il mismatch se necessario + if actual_inputs > 0 && actual_inputs != i_count + silent || println("Fixing input count mismatch: declared=$i_count, actual=$actual_inputs") + filtered_lines[i_line_idx] = ".i $actual_inputs" + end + + + return join(filtered_lines, '\n') + end + + # Valida e correggi il PLA + corrected_pla = validate_and_fix_pla(String(pla_string)) + silent || println("corrected pls: \n",corrected_pla) + # File temporanei input e output + inputfile = tempname() * ".pla" + outputfile = tempname() * ".pla" + + try + # Scrivi PLA corretto su file input + open(inputfile, "w") do f + write(f, corrected_pla) + end + + silent || println("Corrected PLA written to: $inputfile") + + espresso_cmd = `$espressobinary $inputfile` + + silent || println("Running ESPRESSO command: $espresso_cmd") + + # Esegui comando con cattura output/errori + result = try + run(espresso_cmd) + true + catch e + silent || println("ESPRESSO command failed: $e") + false + end + + if !result || !isfile(outputfile) + silent || println("ESPRESSO failed or output file not created, returning original formula") + return syntaxtree + end + + # Leggi output minimizzato + minimized_pla_raw = read(outputfile, String) + minimized_pla_raw = replace(minimized_pla_raw, ">=" => "≥") + + silent || println("good minimized the king: ",minimized_pla_raw) + + if isempty(strip(minimized_pla_raw)) + silent || println("Empty ESPRESSO output, returning original formula") + return syntaxtree + end + + silent || println("Raw minimized PLA output:\n$minimized_pla_raw\n") + + # Pulizia output + function clean_ESPRESSO_output(raw_pla::String) + lines = split(raw_pla, '\n') + pla_lines = filter(line -> !isempty(strip(line)) && + (startswith(line, '.') || occursin(r"^[01\-]+ ", line)), lines) + return join(pla_lines, '\n') + end + + minimized_pla = clean_ESPRESSO_output(minimized_pla_raw) + + silent || println("Cleaned minimized PLA:\n$minimized_pla\n") + + conditionstype = use_scalar_range_conditions ? SoleData.RangeScalarCondition : SoleData.ScalarCondition + + # Converti PLA minimizzato in formula + try + return PLA._pla_to_formula(minimized_pla, silent, pla_args...; conditionstype, pla_kwargs...) + catch e + silent || println("Failed to convert minimized PLA back to formula: $e") + silent || println("Returning original formula") + return syntaxtree + end + + finally + # Elimina file temporanei + rm(inputfile; force=true) + rm(outputfile; force=true) + end + end +=# + +function mktemp_pla() + (f, io) = mktemp() + close(io) + newf = f * ".pla" + cp(f, newf; force=true) + rm(f; force=true) + (newf, open(newf, "w")) +end + + +function boom_minimize(f::LeftmostLinearForm, single::Bool, name::String = "", silent::Bool = true; kwargs...) + #print(dump(f)) + pla_string, pla_args, pla_kwargs = PLA._formula_to_pla(f, false, silent; necessary_type=true, kwargs...) + + (infile, infile_io) = mktemp_pla() + (outfile, outfile_io) = mktemp_pla() + close(outfile_io) + + try + write(infile_io, pla_string) + close(infile_io) + + boom_exe = joinpath(@__DIR__, "boom.exe") + sh_cmd = `sh -c "wine $boom_exe $infile > $outfile"` + run(sh_cmd) + + minimized_output = read(outfile, String) + + # Remove .type line that causes parser issues + minimized_output = replace(minimized_output, r"\.type.*\n" => "") + + # ===== PLA FORMAT NORMALIZATION ===== + # Convert "000000 1" format to "0000001" for compatibility with _pla_to_formula parser + lines = split(minimized_output, '\n') + normalized_lines = String[] + + for line in lines + line = strip(line) + + # If line contains binary pattern + space + output, normalize it + if match(r"^[01-]+\s+[01]$", line) !== nothing + parts = split(line) + binary_part = parts[1] + output_part = parts[2] + # Combine into space-free format + normalized_line = binary_part * output_part + push!(normalized_lines, normalized_line) + else + # Keep line as is + push!(normalized_lines, line) + end + end + + minimized_output = join(normalized_lines, '\n') + + # ===== MAIN CORRECTION ===== + # Extract variable labels from original PLA + original_lines = split(pla_string, '\n') + original_ilb = "" + original_ob = "" + + for line in original_lines + line = strip(line) + if startswith(line, ".ilb ") + original_ilb = line + elseif startswith(line, ".ob ") + original_ob = line + end + end + + # Handle special case where BOOM minimizes everything to "always true" + lines = split(minimized_output, '\n') + processed_lines = String[] + + # Add original labels if missing + ilb_added = false + ob_added = false + + for line in lines + line = strip(line) + + # Add .ilb after .i if not present + if startswith(line, ".i ") && !ilb_added && !isempty(original_ilb) + push!(processed_lines, line) + push!(processed_lines, original_ilb) + ilb_added = true + continue + end + + # Add .ob after .o if not present + if startswith(line, ".o ") && !ob_added && !isempty(original_ob) + push!(processed_lines, line) + push!(processed_lines, original_ob) + ob_added = true + continue + end + + # Handle tautology case (all don't-care followed by output) + if match(r"^-+\s*(\d+)\s*$", line) !== nothing + # BOOM minimized everything to "always true" (tautology) + # Replace with simple rule without don't care + m = match(r"^-+\s*(\d+)\s*$", line) + output = m.captures[1] + + # Extract number of input variables from original PLA + i_count = 0 + for orig_line in original_lines + if startswith(strip(orig_line), ".i ") + i_count = parse(Int, split(strip(orig_line))[2]) + break + end + end + + # Create rule with all 0s (or first valid combination) + zeros_pattern = repeat("0", i_count) + push!(processed_lines, "$zeros_pattern$output") + + elseif occursin("-", line) && match(r"^[01-]+\s*\d+", line) !== nothing + # Keep don't care rules for now, but could expand all combinations + push!(processed_lines, line) + else + push!(processed_lines, line) + end + end + + # Update .p count if necessary + rule_count = count(x -> match(r"^[01-]+\d+", x) !== nothing, processed_lines) + if rule_count > 0 + processed_lines = map(processed_lines) do line + if startswith(line, ".p ") + ".p $rule_count" + else + line + end + end + end + + minimized_output = join(processed_lines, '\n') + + println("=== Original PLA ===") + println(pla_string) + println("=== BOOM PLA Content (Corrected) ===") + println(minimized_output) + println("=== Debug Info ===") + println("pla_args: ", pla_args) + println("pla_kwargs: ", pla_kwargs) + println("original_ilb: ", original_ilb) + println("original_ob: ", original_ob) + println("==========================") + + # Pass original arguments to maintain variable labels + result = PLA._pla_to_formula(minimized_output, silent, pla_args...; pla_kwargs..., featvaltype=Float64) + println("=== Resulting Formula ===") + println(result) + println("==========================") + return result + + finally + isfile(infile) && rm(infile; force=true) + isfile(outfile) && rm(outfile; force=true) + end +end diff --git a/src/scalar-pla.jl b/src/scalar-pla.jl index 978badc..16ec2de 100644 --- a/src/scalar-pla.jl +++ b/src/scalar-pla.jl @@ -29,8 +29,49 @@ _removewhitespaces = x->replace(x, (' ' => "")) # Function to encode a disjunct into a PLA row +""" + encode_disjunct(disjunct::LeftmostConjunctiveForm, features::AbstractVector, conditions::AbstractVector, includes, excludes, feat_condindxss) -> Vector{String} + + Encode a logical disjunct into a Programmable Logic Array (PLA) row representation. + + This function converts a logical disjunct (a conjunction of literals) into a PLA row format, + where each position corresponds to a condition and can be set to "1" (true), "0" (false), + or "-" (don't care). + + # Arguments + - `disjunct::LeftmostConjunctiveForm`: The logical disjunct to encode, containing literals + - `features::AbstractVector`: Vector of features used in the logical formula + - `conditions::AbstractVector`: Vector of all possible conditions + - `includes`: Matrix-like structure defining inclusion relationships between conditions + - `excludes`: Matrix-like structure defining exclusion relationships between conditions + - `feat_condindxss`: Mapping from features to their corresponding condition indices + + # Returns + - `Vector{String}`: PLA row representation where each element is "1", "0", or "-" + + # Details + The function processes each literal in the disjunct: + - For positive literals, sets "1" for included conditions and "0" for excluded ones + - For negative literals, inverts the logic (sets "0" for included, "1" for excluded) + - Handles dual conditions when they exist by applying inverted logic + - Detects and warns about logical conflicts when contradictory values are assigned + - Preserves more restrictive values (NEG over POS) when conflicts occur + + # Examples + ```julia + # Assuming appropriate data structures are set up + pla_row = encode_disjunct(my_disjunct, features, conditions, includes, excludes, feat_condindxss) + # Returns something like: ["1", "0", "-", "1", "0"] + ``` + + # Notes + - The function assumes that either the main condition or its dual exists in the conditions vector + - Warnings are issued when logical conflicts are detected during encoding + - The resulting PLA row uses "-" for don't-care positions that are not constrained by any literal +""" function encode_disjunct(disjunct::LeftmostConjunctiveForm, features::AbstractVector, conditions::AbstractVector, includes, excludes, feat_condindxss) pla_row = fill("-", length(conditions)) + # For each atom in the disjunct, add zeros or ones to relevants for lit in SoleLogics.grandchildren(disjunct) # @show syntaxstring(lit) @@ -46,33 +87,150 @@ function encode_disjunct(disjunct::LeftmostConjunctiveForm, features::AbstractVe # @show feat_icond, feat_idualcond @assert !(isnothing(feat_icond) && isnothing(feat_idualcond)) - # if ispos - # @show excludes[i_feat] - # if !isnothing(feat_icond) - # @views pla_row[feat_condindxs][map(ic->includes[i_feat][feat_icond,ic], eachindex(feat_condindxs))] .= "1" - # @views pla_row[feat_condindxs][map(ic->excludes[i_feat][feat_icond,ic], eachindex(feat_condindxs))] .= "0" - # end - # else - # # if !isnothing(feat_idualcond) - # # @views pla_row[feat_condindxs][map(ic->includes[i_feat][feat_idualcond,ic], eachindex(feat_condindxs))] .= "0" - # # @views pla_row[feat_condindxs][map(ic->excludes[i_feat][feat_idualcond,ic], eachindex(feat_condindxs))] .= "1" - # # end - # end POS, NEG = ispos ? ("1", "0") : ("0", "1") + + # Manage the main condition if !isnothing(feat_icond) - @views pla_row[feat_condindxs][map(((ic,c),)->includes[i_feat][feat_icond,ic], enumerate(feat_condindxs))] .= POS - @views pla_row[feat_condindxs][map(((ic,c),)->excludes[i_feat][feat_icond,ic], enumerate(feat_condindxs))] .= NEG + # For each condition this includes, set POS if not already NEG + for (ic, c) in enumerate(feat_condindxs) + if includes[i_feat][feat_icond, ic] + if pla_row[c] == "-" # Only if it has not already been set + pla_row[c] = POS + elseif pla_row[c] == NEG && POS == "1" + # Conflict: We already have a NEG but we should put POS + # This indicates a logical problem in the formula + @warn "Logic conflict detected at position $(c): was $(NEG), should be $(POS)" + # Keep NEG (more restrictive) + end + end + end + + # For any condition that this excludes, set NEG + for (ic, c) in enumerate(feat_condindxs) + if excludes[i_feat][feat_icond, ic] + if pla_row[c] == "-" + pla_row[c] = NEG + elseif pla_row[c] == POS && NEG == "0" + # Conflict: We already have a POS but we should put NEG + @warn "Logic conflict detected at position $(c): was $(POS), should be $(NEG)" + # Set NEG (more restrictive) + pla_row[c] = NEG + end + end + end end + + # Handle dual condition if exists if !isnothing(feat_idualcond) - @views pla_row[feat_condindxs][map(((ic,c),)->includes[i_feat][feat_idualcond,ic], enumerate(feat_condindxs))] .= NEG - @views pla_row[feat_condindxs][map(((ic,c),)->excludes[i_feat][feat_idualcond,ic], enumerate(feat_condindxs))] .= POS + # For dual condition, invert POS and NEG + for (ic, c) in enumerate(feat_condindxs) + if includes[i_feat][feat_idualcond, ic] + if pla_row[c] == "-" + pla_row[c] = NEG + elseif pla_row[c] == POS && NEG == "0" + @warn "Logic conflict detected at position $(c): was $(POS), should be $(NEG)" + pla_row[c] = NEG + end + end + end + + for (ic, c) in enumerate(feat_condindxs) + if excludes[i_feat][feat_idualcond, ic] + if pla_row[c] == "-" + pla_row[c] = POS + elseif pla_row[c] == NEG && POS == "1" + @warn "Logic conflict detected at position $(c): was $(NEG), should be $(POS)" + # Keep NEG + end + end + end end end - # println(pla_row) + return pla_row end # Function to parse and process the formula into PLA +""" + _formula_to_pla(formula::SoleLogics.Formula, dc_set=false, silent=true, args...; encoding=:univariate, use_scalar_range_conditions=false, kwargs...) -> (String, Tuple, NamedTuple) + + Convert a logical formula into Programmable Logic Array (PLA) format representation. + + This function transforms a logical formula into a PLA format suitable for digital logic synthesis + and hardware implementation. The conversion process involves normalizing the formula to Disjunctive + Normal Form (DNF), extracting conditions and features, and encoding the logic into a structured + PLA representation. + + # Arguments + - `formula::SoleLogics.Formula`: The input logical formula to convert + - `dc_set::Bool=false`: Whether to include don't-care set in the output (currently unused) + - `silent::Bool=true`: If `false`, prints intermediate steps and debugging information + - `args...`: Additional positional arguments passed to underlying functions + + # Keyword Arguments + - `encoding::Symbol=:univariate`: Encoding method for variables (`:univariate` or `:multivariate`) + - `use_scalar_range_conditions::Bool=false`: Whether to use scalar range conditions in the conversion + - `kwargs...`: Additional keyword arguments passed to DNF conversion and scalar simplification + + # Returns + A tuple containing: + - `String`: The complete PLA format string ready for use with logic synthesis tools + - `Tuple`: A tuple containing `(nothing, conditions)` where conditions is the vector of extracted conditions + - `NamedTuple`: Configuration parameters used in the conversion including encoding method and other options + + # Details + The conversion process follows these main steps: + + 1. **Formula Normalization**: Converts the input formula to DNF using specified profiles and atom flipping rules + 2. **Scalar Simplification**: Applies scalar simplification techniques based on the configuration + 3. **Condition Extraction**: Identifies unique conditions and features from the normalized formula + 4. **Condition Processing**: Optionally applies scalar tiling and removes dual conditions + 5. **Relationship Analysis**: Computes inclusion and exclusion relationships between conditions + 6. **PLA Header Generation**: Creates appropriate headers based on encoding method: + - `:univariate`: Standard binary encoding with `.i`, `.o`, `.ilb` directives + - `:multivariate`: Multi-valued variable encoding with `.mv`, `.label` directives + 7. **Row Encoding**: Converts each disjunct to PLA rows using the `encode_disjunct` function + 8. **Output Assembly**: Combines headers, onset rows, and termination markers into final PLA format + + # Encoding Methods + - **`:univariate`**: Each condition becomes a binary input variable (standard PLA format) + - **`:multivariate`**: Groups conditions by feature, supporting multi-valued variables (experimental) + + # PLA Format Output + The generated PLA string includes: + - Variable declarations (`.i`, `.o` for univariate; `.mv` for multivariate) + - Input/output labels (`.ilb`, `.ob`, `.label`) + - Product term count (`.p`) + - Logic onset rows (condition patterns with output values) + - End marker (`.e`) + + # Examples + ```julia + # Basic conversion with default settings + pla_string, conditions, config = _formula_to_pla(my_formula) + + # Verbose conversion with multivariate encoding + pla_string, conditions, config = _formula_to_pla( + my_formula, + false, + false; # silent=false for debugging output + encoding=:multivariate, + use_scalar_range_conditions=true + ) + ``` + + # Notes + - The `:multivariate` encoding is experimental and may not be fully tested + - Scalar range conditions provide additional optimization opportunities but may increase complexity + - The function assumes the input formula can be successfully converted to DNF + - Conditions are automatically sorted and processed to remove redundancy + - The resulting PLA format is compatible with standard logic synthesis tools + + # See Also + - `encode_disjunct`: Function used internally to encode individual disjuncts + - `SoleLogics.dnf`: DNF conversion functionality + - `SoleData.scalar_simplification`: Scalar simplification methods +""" function _formula_to_pla( formula::SoleLogics.Formula, dc_set = false, @@ -223,44 +381,6 @@ function _formula_to_pla( # # Generate DC-set rows for each disjunct pla_dcset_rows = [] - # TODO remove - # @assert !(dc_set && encoding == :multivariate) - # if dc_set - # for feat in features - # feat_condindxs = findall(c->feature(c) == feat, conditions) - # # feat_condindxs = collect(eachindex(conditions)) - # # cond_mask = map((c)->feature(c) == feat, conditions) - # includes = [SoleData.includes(conditions[cond_i], conditions[cond_j]) for cond_i in feat_condindxs, cond_j in feat_condindxs] - # excludes = [SoleData.excludes(conditions[cond_i], conditions[cond_j]) for cond_i in feat_condindxs, cond_j in feat_condindxs] - # for (i,cond_i) in enumerate(feat_condindxs) - # for (j,cond_j) in enumerate(feat_condindxs) - # if includes[i, j] - # println("$(syntaxstring(conditions[cond_i])) -> $(syntaxstring(conditions[cond_j]))") - # end - # if excludes[j, i] - # println("$(syntaxstring(conditions[cond_i])) -> !$(syntaxstring(conditions[cond_j]))") - # end - # end - # end - # print(includes) - # print(excludes) - # for (i,cond_i) in enumerate(feat_condindxs) - # row = fill("-", length(conditions)) - # row[cond_i] = "1" - # for (j,cond_j) in enumerate(feat_condindxs) - # if includes[j, i] - # row[cond_j] = "1" - # elseif excludes[j, i] - # row[cond_j] = NEG - # end - # end - # push!(pla_dcset_rows, "$(join(row, "")) -") # Append "-" for the DC-set output - # end - # end - # println(pla_dcset_rows) - # # readline() - # end - # Combine PLA components pla_content = [ join(pla_header, "\n"), @@ -277,6 +397,119 @@ function _formula_to_pla( ) end +""" + _pla_to_formula(pla::AbstractString, silent=true, ilb_str=nothing, conditions=nothing; conditionstype=SoleData.ScalarCondition, featuretype=SoleData.VariableValue, featvaltype=nothing, kwargs...) -> SoleLogics.Formula + + Convert a Programmable Logic Array (PLA) format string back into a logical formula representation. + + This function performs the inverse operation of `_formula_to_pla`, parsing a PLA format string + and reconstructing the corresponding logical formula in Disjunctive Normal Form (DNF). It handles + both univariate (binary) and multivariate PLA formats, processing input variables, output + specifications, and logic rows to rebuild the original logical structure. + + # Arguments + - `pla::AbstractString`: The PLA format string to parse and convert + - `silent::Bool=true`: If `false`, prints debugging information during parsing + - `ilb_str::Union{String,Nothing}=nothing`: Expected input labels string for validation (optional) + - `conditions::Union{AbstractVector,Nothing}=nothing`: Pre-existing conditions to map against (optional) + + # Keyword Arguments + - `conditionstype::Type=SoleData.ScalarCondition`: Type constructor for creating new conditions + - `featuretype::Type=SoleData.VariableValue`: Type for feature representation + - `featvaltype::Union{Type,Nothing}=nothing`: Type for feature values (optional) + - `kwargs...`: Additional arguments passed to condition parsing functions + + # Returns + - `SoleLogics.Formula`: The reconstructed logical formula in DNF, or `⊤` (true) if no valid rows exist + + # Details + The conversion process follows these main steps: + + 1. **PLA Parsing**: Processes the input string line by line, extracting: + - Variable declarations (`.i`, `.o`, `.mv`) + - Input/output labels (`.ilb`, `.ob`, `.label`) + - Logic rows and don't-care specifications + - Multi-valued variable metadata + + 2. **Variable Mapping**: Maps PLA input variables to logical conditions: + - Uses provided `conditions` mapping if available + - Creates new conditions using `conditionstype` constructor + - Handles both binary and multi-valued variables + + 3. **Row Processing**: Converts each PLA row into logical conjuncts: + - `'1'` values become positive literals + - `'0'` values become negative literals + - `'-'` values are ignored (don't-care) + - Only processes ON-set rows (output = '1') + + 4. **Formula Reconstruction**: Combines processed rows: + - Each row becomes a conjunctive clause (AND of literals) + - All clauses are combined disjunctively (OR of conjunctions) + - Applies scalar simplification to optimize the result + + # PLA Format Support + The function supports standard PLA directives: + - `.i N`: Number of input variables (univariate format) + - `.o N`: Number of output variables (must be 1) + - `.mv N B S1 S2...`: Multi-valued variable declaration (experimental) + - `.ilb labels`: Input variable labels + - `.ob label`: Output variable label + - `.label var=N labels`: Multi-valued variable labels + - `.p N`: Number of product terms (ignored) + - `.e`: End marker + + # Examples + ```julia + # Basic PLA to formula conversion + pla_string = \""" + .i 3 + .o 1 + .ilb x y z + .ob output + 11- 1 + -01 1 + .e + \""" + formula = _pla_to_formula(pla_string) + + # Conversion with pre-defined conditions + formula = _pla_to_formula(pla_string, true, nothing, my_conditions) + + # Verbose conversion with custom types + formula = _pla_to_formula( + pla_string, + false; # silent=false for debugging + conditionstype=MyConditionType, + featuretype=MyFeatureType + ) + ``` + + # Multi-valued Variable Support + For PLA files with multi-valued variables (`.mv` directive): + - Binary variables are processed first + - Multi-valued variables are grouped and processed separately + - Variable labels are extracted from `.label` directives + - Each multi-valued variable contributes one selected literal per row + + # Error Handling + The function validates: + - PLA format correctness and known directive support + - Consistency between provided and parsed input labels + - Single output variable requirement + - Valid truth values in logic rows + + # Notes + - Multi-valued variable support is experimental and may not be fully tested + - The function assumes well-formed PLA input with valid syntax + - Only ON-set rows (output='1') are processed; OFF-set and don't-care rows are ignored + - Scalar simplification is applied to optimize the reconstructed formula + - Returns `⊤` (tautology) if no valid logic rows are found + + # See Also + - `_formula_to_pla`: Inverse function for converting formulas to PLA format + - `SoleData.scalar_simplification`: Formula optimization functionality + - `parsecondition`: Condition parsing utilities +""" function _pla_to_formula( pla::AbstractString, silent = true, @@ -448,4 +681,4 @@ end # function formula_to_emacs(expr::SyntaxTree) end -end +end \ No newline at end of file