Lipen

import org.junit.jupiter.api.Test

fun <T> combine(sequences: List<Sequence<T>>): Sequence<List<T>> = sequence {
    if (sequences.isEmpty()) return@sequence

    if (sequences.size == 1) {
        for (x in sequences[0]) {
            yield(listOf(x))
        }
        return@sequence

Lipen

import mmap
import tqdm

def parse_binary_drat_mmap(path):
    with open(path, "rb") as f:
        with mmap.mmap(f.fileno(), 0, access=mmap.ACCESS_READ) as mm:
            state = 0
            # state = 0 -- reading the mode: b'a' or b'd'
            # state = 1 -- reading the clause
            mode = None  # "a" or "d", for user

Lipen

#!/usr/bin/env python
# coding: utf-8

def quicksort(A, p=0, r=None):
    if r is None:
        r = len(A) - 1
    if p < r:
        q = partition(A, p, r)
        quicksort(A,p,q-1)
        quicksort(A,q+1,r)

Lipen

%%% Graph Coloring

%% Constants.
int: V;
int: E = length(edges1d) div 2;
int: k;

set of int: NODES = 1..V;
set of int: EDGES = 1..E;
set of int: COLORS = 1..k;

Lipen

Lipen

; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2
(set-logic ALL)

(synth-fun f ((x Bool) (y Bool) (z Bool)) Bool
    ((Start Bool)) (
    (Start Bool (
        x y z
        (not Start)
        (and Start Start)

Lipen

from pysat.examples.rc2 import RC2
from pysat.formula import WCNF, IDPool

vpool = IDPool(start_from=1)


def cover(v):
    return vpool.id(f'cover@{v}')

Lipen

from pysat.formula import CNF, IDPool
from pysat.solvers import Minisat22 as Solver
from enum import Enum

NodeType = Enum("NodeType", "VAR AND OR NOT")


class BFSynthesizer:
    def __init__(self, n: int, tt: str, P: int):
        assert len(tt) == 2 ** n, "Incorrect truth table size"

Lipen

package examples.einstein

import com.github.lipen.satlib.op.exactlyOne
import com.github.lipen.satlib.op.imply
import com.github.lipen.satlib.op.implyOr
import com.github.lipen.satlib.solver.MiniSatSolver
import com.github.lipen.satlib.solver.Solver
import com.github.lipen.satlib.solver.newDomainVarArray
import com.github.lipen.satlib.utils.DomainVarArray
import com.github.lipen.satlib.utils.convert

Lipen

from pysat.formula import CNF, IDPool
from pysat.solvers import Minisat22

n, k = map(int, input().split())
cnf = CNF()
vpool = IDPool(start_from=1)


def bit(i):
    return vpool.id(f'v@{i}')