You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
104 lines
2.7 KiB
104 lines
2.7 KiB
#!python3
|
|
|
|
from pysat.formula import CNF
|
|
from pysat.solvers import Glucose4
|
|
|
|
import pathlib as pl
|
|
import random
|
|
import bz2
|
|
import sys
|
|
import argparse
|
|
|
|
|
|
def main():
|
|
args = parse_args()
|
|
|
|
instances = get_instance_paths(pl.Path(args.instance_dir))
|
|
|
|
global CORE_DIR
|
|
CORE_DIR = pl.Path(args.cores_dir)
|
|
|
|
global EXTENDED_DIR
|
|
EXTENDED_DIR = pl.Path(args.extensions_dir)
|
|
|
|
print(CORE_DIR)
|
|
|
|
for instance in instances:
|
|
run(instance, args.nr_per_instance)
|
|
|
|
def parse_args():
|
|
parser = argparse.ArgumentParser()
|
|
parser.add_argument( "-i"
|
|
,"--instance_dir"
|
|
,type=str
|
|
,default="./instances"
|
|
,help="directory containing the instances")
|
|
parser.add_argument( "-c"
|
|
,"--cores_dir"
|
|
,type=str
|
|
,default="./cores"
|
|
,help="directory containing the cores")
|
|
parser.add_argument( "-e"
|
|
,"--extensions_dir"
|
|
,type=str
|
|
,default="./extensions"
|
|
,help="directory containing the core extensions")
|
|
parser.add_argument( "-n"
|
|
,"--nr_per_instance"
|
|
,type=int
|
|
,default=1
|
|
,help="number of extensions per instance")
|
|
|
|
return parser.parse_args()
|
|
|
|
def get_instance_paths(instances_dir):
|
|
instances = []
|
|
|
|
for p in instances_dir.iterdir():
|
|
if str(p).endswith(".cnf.bz2"):
|
|
instances.append(p)
|
|
|
|
return instances
|
|
|
|
def run(instance, calls_per_instance):
|
|
ipath = pl.Path(instance)
|
|
iname = ipath.stem[:-4]
|
|
|
|
f = CNF(str(ipath))
|
|
|
|
for i in range(calls_per_instance):
|
|
cores = parse_cores(iname)
|
|
|
|
print(iname)
|
|
print(len(f.clauses), len(cores))
|
|
print("{0:.3g}".format(len(cores) * 100 / len(f.clauses)))
|
|
|
|
print()
|
|
|
|
def parse_cores(instance):
|
|
cores = []
|
|
|
|
with bz2.open(CORE_DIR / (instance + ".cores.bz2"), "tr") as cores_file:
|
|
cores = list(map(lambda l: l.strip(), cores_file.readlines()))
|
|
|
|
cores = list(map(lambda l: l.split(","), cores))
|
|
|
|
for i in range(len(cores)):
|
|
cores[i] = list(map(int, cores[i]))
|
|
cores[i] = list(map(lambda lit: -1 * lit, cores[i]))
|
|
|
|
return cores
|
|
|
|
def next_file_path(name):
|
|
counter = 0
|
|
|
|
ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
|
|
|
|
while ext_file_path.exists():
|
|
counter += 1
|
|
ext_file_path = EXTENDED_DIR / ("{}_{:04}.cnf.bz2".format(name, counter))
|
|
|
|
return ext_file_path, counter
|
|
|
|
if __name__ == "__main__":
|
|
main()
|