Metadata-Version: 2.2
Name: d4Solver
Version: 0.1.0
Summary: Python bindings for the D4 model counter and compiler
Author-Email: Logical Team <contact@univ-artois.fr>
Classifier: Programming Language :: C++
Classifier: Programming Language :: Python :: 3
Classifier: License :: OSI Approved :: MIT License
Requires-Python: >=3.9
Description-Content-Type: text/markdown

# py-d4

Python bindings for the **D4** compiler and model counter, supporting option structures, CNF files, custom clause vectors, logic circuits, weighted model counting, and d-DNNF queries. Built with `nanobind` and `scikit-build-core`.

---

## 🚀 Users Guide

### 1. Installation

Install the package directly from your GitLab PyPI package registry (typically configured in your CI or local `.pip/pip.conf`):

```bash
pip install d4Solver --extra-index-url https://gitlab.univ-artois.fr/api/v4/projects/<PROJECT_ID>/packages/pypi/simple
```

### 2. Usage Examples

#### 2.1 Basic Model Counting

You can instantiate a `Solver` using a CNF filepath or raw Python clause structures (list of lists/tuples of literals, 1-based indexing):

```python
import py_d4

# 1. Option A: Load from a DIMACS CNF file
solver = py_d4.Solver("path/to/formula.cnf")

# 2. Option B: Pass raw Python clauses and total variable count
# Formula: (x1 or x2) and (not x2 or x3)
clauses = [
    [1, 2],
    [-2, 3]
]
nb_vars = 3
solver = py_d4.Solver(clauses, nb_vars)

# Run model counting
count_res = solver.count()
print(f"Number of models: {count_res.getResult()}")     # Large integer as string (GMP support)
print(f"As Python integer: {count_res.getIntResult()}")  # Safe python int
```

#### 2.2 Compilation to d-DNNF

`py-d4` can compile CNF formulas and circuits into Decision Diagram / Deterministic Decomposable Negation Normal Form (d-DNNF):

```python
import py_d4

clauses = [[1, 2], [-2, 3]]
solver = py_d4.Solver(clauses, 3)

# Compile
compile_res = solver.compile()

# Access compiled graph statistics
print(f"Nodes in d-DNNF: {compile_res.getNbNodes()}")
print(f"Edges in d-DNNF: {compile_res.getNbEdges()}")

# Get the compiled NNF circuit string (in standard d-DNNF format)
nnf_str = compile_res.getNNFString()
print("NNF String:\n", nnf_str)
```

#### 2.3 Querying the Compiled d-DNNF

Once compiled, you can run multiple queries (SAT checks or model counting) under different literal assumptions:

```python
# Check if the formula is satisfiable (no assumptions)
is_sat = compile_res.isSAT([])  # True/False

# Check satisfiability assuming x1 is True (1) and x2 is False (-2)
is_sat_under_assumptions = compile_res.isSAT([1, -2])

# Count models under literal assumptions
# E.g., model count assuming x1 is True
count_under_x1 = compile_res.count([1])
print(f"Models satisfying x1: {count_under_x1}")
```

#### 2.4 Weighted Model Counting (WMC)

You can assign weights to literals for exact weighted model counting:

```python
import py_d4

# Formula: (x1 or x2)
solver = py_d4.Solver([[1, 2]], nb_vars=2)

# Define weights for literals (keys are 1-based literals, values are string representations)
weights = {
    1: "0.3",
    -1: "0.7",
    2: "0.4",
    -2: "0.6"
}
# Set weights (WeightType can be FLOAT or GMP)
solver.setWeights(weights, py_d4.WeightType.FLOAT)

# Compute WMC directly
count_res = solver.count()
print("WMC Result:", float(count_res.getResult()))  # Output: 0.58

# Or compile and query WMC under assumptions
compile_res = solver.compile()
print("WMC under x1=True:", float(compile_res.count([1])))  # Output: 0.3
```

#### 2.5 Logic Gates / Circuit Compilation

Instead of CNF, you can initialize the solver with logic gates to compile or count structured circuits:

```python
import py_d4

# Create a gate representing: x3 = x1 AND (not x2)
gate = py_d4.Gate()
gate.gateType = py_d4.GateType.AND
gate.inputs = [1, -2]
gate.output = 3

# Instantiate solver from gate specifications
solver = py_d4.Solver([gate], nb_vars=3)
print("Models for circuit:", solver.count().getIntResult())
```

#### 2.6 Solver Configuration & Options

Fine-tune the behavior of D4 by mutating native C++ option structures. Documentation and description of settings are exposed natively as Python docstrings:

```python
import py_d4

# Instantiate default options
opt = py_d4.OptionDpllStyleMethod()

# 1. Read Option Descriptions (C++ docstrings exposed to Python)
print(py_d4.OptionDpllStyleMethod.exploitModel.__doc__)
# Output: "If we exploit model during search"

# 2. Modify properties directly (with type safety)
opt.precision = 30
opt.exploitModel = False
opt.optionSolver.solverName = 0  # 0: glucose, 1: minisat

# 3. Modify nested option group settings
opt.optionBranchingHeuristic.freqDecay = 98

# 4. Pass options to the Solver
solver = py_d4.Solver("formula.cnf", opt)

# 5. Serialize options to/from standard Python Dictionaries
config_dict = py_d4.dump_options_to_dict(opt)
opt_restored = py_d4.load_options_from_dict(config_dict)

# 6. Serialize options to/from raw JSON Strings (via native C++ bindings)
json_str = py_d4._py_d4.dump_options_to_json(opt)
opt_restored_json = py_d4._py_d4.load_options_from_json(json_str)
```

---

## 🛠️ Developers Guide

### 1. Requirements

Before building locally, ensure the following system-level dependencies are installed on your host:
- C++20 compatible compiler (e.g. GCC >= 10, Clang >= 10)
- CMake (>= 3.15)
- GMP development headers (`libgmp-dev` / `gmp-devel`)
- Zlib development headers (`zlib1g-dev` / `zlib-devel`)

### 2. Local Build Pipeline

To compile the C++ extension module and deploy it directly inside your local Python package tree, run:

```bash
# 1. Provide your GitLab access token to clone the D4 dependency
export GITLAB_TOKEN_LOGICAL="your_gitlab_token"

# 2. Configure, generate bindings, compile, and deploy shared library
./build.sh
```

Alternatively, you can install the package in editable mode via pip:
```bash
pip install -e .
```

### 3. Re-Generating Bindings

If D4 option headers change, you can automatically parse the new C++ classes and inline constructor descriptions to rebuild the `nanobind` bindings:

```bash
python3 scripts/generate_bindings.py /path/to/local/d4
```
*(If `/path/to/local/d4` is omitted, the script automatically searches the CMake FetchContent directory).*

### 4. Running Tests

To execute the test suite and verify the integrity of the wrapper:

```bash
LD_PRELOAD=$(gcc -print-file-name=libstdc++.so.6) PYTHONPATH=. python3 tests/test_options.py
```

### 5. GitLab CI/CD Pipeline

The project includes an automated multi-stage `.gitlab-ci.yml` pipeline:
- **Build Stage**: Uses `cibuildwheel` to compile optimized, standalone Linux wheels for Python 3.8 to 3.13. It automatically routes the group-level `GITLAB_TOKEN_LOGICAL` CI variable to authenticate both the `py-d4` and internal `d4`/`optree` sub-project checkouts.
- **Deploy Stage**: Triggered on pushing Git tags. Automatically publishes the generated wheel packages directly to the GitLab project PyPI package registry using `twine`.
