# penponism

**Repository Path**: marvintau/penponism

## Basic Information

- **Project Name**: penponism
- **Description**: Post-modern SAT solver
- **Primary Language**: Unknown
- **License**: Not specified
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2025-05-19
- **Last Updated**: 2026-02-27

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Penponism

A CNF/SAT tooling suite with ternary vector operations and an interactive REPL environment.

## Requirements

- Zig 0.15.2 or later

## Building

To build the library for your current platform:

```bash
zig build
```

### Cross-Compilation to Windows

Build for Windows x86_64:

```bash
zig build windows-x64
```

Build for Windows ARM64:

```bash
zig build windows-arm64
```

The Windows executables will be placed in:
- `zig-out/windows-x86_64/penponism.exe` (for x64)
- `zig-out/windows-aarch64/penponism.exe` (for ARM64)

You can also use the generic target option for any platform:

```bash
zig build -Dtarget=x86_64-windows
zig build -Dtarget=aarch64-windows
```

## Testing

To run the tests:

```bash
zig build test
```

## Usage

### Command Line Interface

Penponism provides various commands for CNF/SAT operations:

```bash
# Show statistics of a CNF file
./zig-out/bin/penponism stats <path.cnf>

# Print CNF matrix
./zig-out/bin/penponism print <path.cnf>

# Sort clauses
./zig-out/bin/penponism sort <path.cnf>

# Apply subsumption elimination
./zig-out/bin/penponism subsume <path.cnf>

# Davis-Putnam variable elimination
./zig-out/bin/penponism davput <path.cnf> <var_index>

# Davis-Putnam with disjunall optimization
./zig-out/bin/penponism davputdisjun <path.cnf> <var_index>

# Start interactive REPL
./zig-out/bin/penponism repl
```

### REPL Environment

The REPL provides an interactive scripting environment for CNF/SAT operations:

```bash
# Start REPL interactively
./zig-out/bin/penponism repl

# Or run a script file
cat examples/davis_putnam.repl | ./zig-out/bin/penponism repl
```

#### REPL Commands

**File Operations:**
- `var = read "path/to/file.cnf"` - Load a CNF file into a variable

**CNF Manipulation:**
- `pos, neg, non = splitby var var_index` - Split by variable into 3 parts (positive, negative, non-presenting)
- `result = dirres pos neg var_index` - Direct resolution (eliminates variable)
- `result = concat mat1 mat2 ...` - Concatenate multiple termats
- `result = subsume mat` - Apply subsumption elimination
- `result = disjunall mat` - Convert to disjoint normal form
- `result = sort mat` - Sort clauses

**Inspection:**
- `print var` - Print the CNF matrix
- `stats var` - Show statistics (variables, clauses)
- `vars` - List all variables in memory

**Control:**
- `help` - Show help message
- `exit` or `quit` - Exit REPL

## GUI assets

### Icon bitmaps (15×15 BMP)

The GUI uses tiny cubox-styled icons generated into `assets/icons/`:

- `prompt_in.bmp` (⊢)
- `prompt_out.bmp` (⊣)
- `op_eq.bmp` (=)
- `insert_plus.bmp` (+)
- `delete_minus.bmp` (-)

To regenerate them:

```bash
node tools/gen_icons.js
```

Alternatively (recommended), generate **font-based** glyph icons (avoids hard-coded shapes) using stb_truetype:

```bash
zig run tools/gen_icons_font.zig tools/stb_truetype_impl.c -lc -Ivendor/zgui/libs/imgui
```

#### REPL Example

```
> cnf = read "cnf/simple/bin.cnf"
Loaded cnf: 8 vars, 7 clauses

> pos, neg, non = splitby cnf 1
Split by var 1: pos=1 clauses, neg=1 clauses, non=5 clauses

> elim = dirres pos neg 1
Direct resolution: elim=1 clauses

> result = concat non elim
Concatenated: result=6 clauses

> final = subsume result
Subsumption: final=5 clauses (was 6)

> print final
(5 clauses, 8 vars)
...

> exit
```

See the `examples/` directory for more REPL script examples.

## Implementation Notes

The Zig version maintains the same functionality as the original C++ implementation:

- `TerVec` represents a ternary vector with extension and polarity bit arrays
- Operations include intersection (comm), equality checking, and bit manipulation
- The implementation uses fixed-size byte arrays for consistent memory layout

## License

[Add your license information here]