From 38c52f661609b7a4df34aba8efe80b389e298d30 Mon Sep 17 00:00:00 2001 From: Vu Date: Fri, 7 May 2021 09:43:49 -0500 Subject: [PATCH 01/13] modified htd path in config.json --- .gitignore | 1 + config.json | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) create mode 100644 .gitignore diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..bee8a64 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +__pycache__ diff --git a/config.json b/config.json index d91a86f..a42a5a0 100644 --- a/config.json +++ b/config.json @@ -3,8 +3,8 @@ "dsn": { "host": "localhost", "port": 5432, - "database": "logicsem", - "user": "logicsem", + "database": "logicsem", + "user": "logicsem", "password": "XXX", "application_name": "dpdb" }, @@ -19,7 +19,7 @@ "application_name": "dpdb-admin" }, "htd": { - "path": "../htd/bin/htd_main", + "path": "../htd/build/bin/htd_main", "parameters": [ "--child-limit","5" ] From 269a1e197504bcfbbcdd004f87617cec210c6dba Mon Sep 17 00:00:00 2001 From: Vu Date: Sat, 8 May 2021 20:45:54 -0500 Subject: [PATCH 02/13] formatted whitespace --- config.json | 12 ++++++------ nesthdb.py | 3 +-- 2 files changed, 7 insertions(+), 8 deletions(-) mode change 100644 => 100755 nesthdb.py diff --git a/config.json b/config.json index a42a5a0..44c0b09 100644 --- a/config.json +++ b/config.json @@ -11,12 +11,12 @@ "max_connections": 100 }, "db_admin": { - "host": "localhost", - "port": 5432, - "database": "logicsem", - "user": "postgres", - "password": "XXX", - "application_name": "dpdb-admin" + "host": "localhost", + "port": 5432, + "database": "logicsem", + "user": "postgres", + "password": "XXX", + "application_name": "dpdb-admin" }, "htd": { "path": "../htd/build/bin/htd_main", diff --git a/nesthdb.py b/nesthdb.py old mode 100644 new mode 100755 index c4b8ea0..34702f0 --- a/nesthdb.py +++ b/nesthdb.py @@ -218,7 +218,7 @@ def call_solver(self,type): logger.info(f"Solver {type} result: {result}") return result - + def solve_classic(self): if interrupted: return -1 @@ -382,4 +382,3 @@ def signal_handler(sig, frame): if __name__ == "__main__": main() - From 5dec376c742dee450936aa09614342b51dbfef2d Mon Sep 17 00:00:00 2001 From: Vu Date: Sat, 8 May 2021 20:53:27 -0500 Subject: [PATCH 03/13] merged config.json with Dropbox version (https://tinyurl.com/nesthdb) --- config.json | 56 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) diff --git a/config.json b/config.json index 44c0b09..d33a27f 100644 --- a/config.json +++ b/config.json @@ -26,5 +26,61 @@ }, "dpdb": { "max_worker_threads": 24 + }, + "problem_specific": { + "nestpmc": { + "max_solver_threads": 12, + "inner_vars_threshold": 40, + "max_worker_threads": 12 + } + }, + "nesthdb": { + "threshold_hybrid" : 1000, + "threshold_abstract" : 8, + "max_recursion_depth" : 1, + "sat_solver": { + "path": "/programs/picosat-965", + "seed_arg": "-s" + }, + "sharpsat_solver": { + "path": "/miniC2D-1.0.0", + "args": "-C -c", + "output_parser": { + "class": "RegExReader", + "args": { + "pattern": "Counting... (\\d+) models" + }, + "result":"result" + } + }, + "pmc_solver": { + "path": "/projMC-wrapper-1.0", + "seed_arg": "-s", + "output_parser": { + "class": "RegExReader", + "args": { + "pattern": "s (\\d+)\\n" + }, + "result":"result" + } + }, + "preprocessor": { + "path": "/pmc-1.0", + "args": "-vivification -eliminateLit -litImplied -iterate=10" + }, + "asp": { + "encodings": [ + { + "file": "./guess_min_degree.lp", + "size": 95, + "timeout": 10 + }, + { + "file": "./guess_increase2.lp", + "size": 64, + "timeout" : 35 + } + ] + } } } From fe47ef1d265c416a44c6cbc8541d6d07195d6717 Mon Sep 17 00:00:00 2001 From: Vu Date: Sat, 8 May 2021 21:38:59 -0500 Subject: [PATCH 04/13] modified paths to picosat and pmc --- config.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/config.json b/config.json index d33a27f..5ac10ad 100644 --- a/config.json +++ b/config.json @@ -39,7 +39,7 @@ "threshold_abstract" : 8, "max_recursion_depth" : 1, "sat_solver": { - "path": "/programs/picosat-965", + "path": "../picosat/picosat", "seed_arg": "-s" }, "sharpsat_solver": { @@ -65,7 +65,7 @@ } }, "preprocessor": { - "path": "/pmc-1.0", + "path": "./bin/pmc", "args": "-vivification -eliminateLit -litImplied -iterate=10" }, "asp": { From b8a29d258d7a9cb4d52fc83bc092c30b29c0e96e Mon Sep 17 00:00:00 2001 From: Vu Date: Sat, 8 May 2021 21:58:34 -0500 Subject: [PATCH 05/13] corrected guess_increase2.lp to guess_increase.lp in config --- config.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/config.json b/config.json index 5ac10ad..64b89ad 100644 --- a/config.json +++ b/config.json @@ -76,7 +76,7 @@ "timeout": 10 }, { - "file": "./guess_increase2.lp", + "file": "./guess_increase.lp", "size": 64, "timeout" : 35 } From 7e2904f7ff717224ea7c67995977577aa44c16ce Mon Sep 17 00:00:00 2001 From: Vu Date: Sat, 8 May 2021 22:00:49 -0500 Subject: [PATCH 06/13] deleted `"max_solver_threads": 24` in "dpdb" to avoid conflict with `"max_solver_threads": 12` in "problem_specific" modified: config.json --- config.json | 1 - 1 file changed, 1 deletion(-) diff --git a/config.json b/config.json index 64b89ad..ec87767 100644 --- a/config.json +++ b/config.json @@ -25,7 +25,6 @@ ] }, "dpdb": { - "max_worker_threads": 24 }, "problem_specific": { "nestpmc": { From ba66c0f99306074c9c396f2a000105b5b90177e7 Mon Sep 17 00:00:00 2001 From: Vu Date: Sat, 8 May 2021 22:37:50 -0500 Subject: [PATCH 07/13] added projMC-wrapper.py (slight modification from https://tinyurl.com/nesthdb) --- config.json | 2 +- projMC-wrapper.py | 48 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 1 deletion(-) create mode 100755 projMC-wrapper.py diff --git a/config.json b/config.json index ec87767..e4bc4c6 100644 --- a/config.json +++ b/config.json @@ -53,7 +53,7 @@ } }, "pmc_solver": { - "path": "/projMC-wrapper-1.0", + "path": "./projMC-wrapper.py", "seed_arg": "-s", "output_parser": { "class": "RegExReader", diff --git a/projMC-wrapper.py b/projMC-wrapper.py new file mode 100755 index 0000000..76773a4 --- /dev/null +++ b/projMC-wrapper.py @@ -0,0 +1,48 @@ +#!/usr/bin/python2 +#Wrapper for projMC to enable projMC to use the common input format +import sys +import os.path +import random +import tempfile +import subprocess + +fo = tempfile.NamedTemporaryFile()#delete=False) +fp = tempfile.NamedTemporaryFile()#delete=False) + +fi = 1 +rarg = 2020 +if len(sys.argv) > 3: + #rarg = int(sys.argv[2]) + rarg = random.randrange(13423423471) #int(sys.argv[2]) + #random.seed(int(sys.argv[2])) + fi = 3 + +f = sys.stdin if len(sys.argv) == fi else file(sys.argv[fi], "rb") +proj = [] +for r in f: + fo.write(r) + #print("c {}".format(r)), + if r.startswith("c ind"): + var = r.split(" ")[2:-1] + proj += var + +#print proj +fp.write("{0}\n".format(",".join(proj))) +fp.flush() +fp.seek(0) +fp.flush() + +fo.flush() +fo.seek(0) +fo.flush() + +if len(sys.argv) > fi: + f.close() + +print("c ./bin/projMC {} -fpv={} -rnd-seed{}", fo.name, fp.name, rarg) +pmc = subprocess.Popen(["./bin/projMC", "-rnd-init", "-rnd-seed={}".format(rarg), fo.name, "-fpv={0}".format(fp.name)], stdout=sys.stdout, stderr=sys.stderr) +pmc.wait() + +fo.close() +fp.close() +sys.exit(pmc.returncode) From 1f24f158a042cce83a6b14a72748bff5387a5d77 Mon Sep 17 00:00:00 2001 From: Vu Date: Sat, 8 May 2021 22:54:44 -0500 Subject: [PATCH 08/13] ignored bin/ --- .gitignore | 2 ++ config.json | 4 ++-- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index bee8a64..8b17f55 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ +bin/ + __pycache__ diff --git a/config.json b/config.json index e4bc4c6..0fb8b88 100644 --- a/config.json +++ b/config.json @@ -19,7 +19,7 @@ "application_name": "dpdb-admin" }, "htd": { - "path": "../htd/build/bin/htd_main", + "path": "./bin/htd_main", "parameters": [ "--child-limit","5" ] @@ -38,7 +38,7 @@ "threshold_abstract" : 8, "max_recursion_depth" : 1, "sat_solver": { - "path": "../picosat/picosat", + "path": "./bin/picosat", "seed_arg": "-s" }, "sharpsat_solver": { From d47fb33473a608a4967f50c8815a57a356df2b0c Mon Sep 17 00:00:00 2001 From: Vu Date: Sat, 8 May 2021 23:10:05 -0500 Subject: [PATCH 09/13] shebang --- nesthdb.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/nesthdb.py b/nesthdb.py index 34702f0..71988f4 100755 --- a/nesthdb.py +++ b/nesthdb.py @@ -1,4 +1,4 @@ -#!/usr/bin/python3 +#!/usr/bin/env python3 # -*- coding: future_fstrings -*- import importlib import logging From 336cec9f97f963e3f6db522d203b38e4f2e8f4e2 Mon Sep 17 00:00:00 2001 From: Vu Date: Wed, 12 May 2021 19:08:38 -0500 Subject: [PATCH 10/13] added helper.py to absolutize paths in config json files --- helper.py | 25 +++++++++++++++++++++++++ nesthdb.py | 3 +++ 2 files changed, 28 insertions(+) create mode 100644 helper.py diff --git a/helper.py b/helper.py new file mode 100644 index 0000000..181aa2a --- /dev/null +++ b/helper.py @@ -0,0 +1,25 @@ +#!/usr/bin/env python3 + +import os + +def absolutizePath(relPath): # paths in config may be relative to root of repository + return os.path.abspath(os.path.join(os.path.dirname(__file__), relPath)) + +def absolutizePaths(object): # returns new config in which all paths are absolute + if isinstance(object, str): # base case + return object + else: + assert isinstance(object, dict), object # config + absCfg = {} # new config with absolute paths, to be returned + for (key, value) in object.items(): + assert isinstance(key, str), key + if key in {"path", "file"}: + assert isinstance(value, str), value + absCfg[key] = absolutizePath(value) + elif isinstance(value, dict): + absCfg[key] = absolutizePaths(value) + elif isinstance(value, list): # possibly `list` of `str` + absCfg[key] = [absolutizePaths(member) for member in value] + else: # base case + absCfg[key] = value + return absCfg diff --git a/nesthdb.py b/nesthdb.py index 71988f4..cabfdc0 100755 --- a/nesthdb.py +++ b/nesthdb.py @@ -7,6 +7,8 @@ from collections import defaultdict +import helper # file ./helper.py + from common import * from dpdb.abstraction import MinorGraph, ClingoControl from dpdb.db import BlockingThreadedConnectionPool, DBAdmin, DEBUG_SQL, setup_debug_sql @@ -356,6 +358,7 @@ def main(): arg_parser.add_argument("--no-cache", dest="no_cache", help="Disable cache", action="store_true") args = parse_args(arg_parser) cfg = read_cfg(args.config) + cfg = helper.absolutizePaths(cfg) # relative paths would fail if executed from different dir fname = args.file formula = Formula.from_file(fname) From 96008f4defe69fbd19aa71714081edce4a84f029 Mon Sep 17 00:00:00 2001 From: Vu Date: Wed, 12 May 2021 19:51:11 -0500 Subject: [PATCH 11/13] changed: python2 to python3, `file` to `open`, binary mode to text mode modified: projMC-wrapper.py --- projMC-wrapper.py | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/projMC-wrapper.py b/projMC-wrapper.py index 76773a4..781b4cd 100755 --- a/projMC-wrapper.py +++ b/projMC-wrapper.py @@ -1,4 +1,4 @@ -#!/usr/bin/python2 +#!/usr/bin/env python3 #Wrapper for projMC to enable projMC to use the common input format import sys import os.path @@ -6,8 +6,10 @@ import tempfile import subprocess -fo = tempfile.NamedTemporaryFile()#delete=False) -fp = tempfile.NamedTemporaryFile()#delete=False) +import helper # file ./helper.py + +fo = tempfile.NamedTemporaryFile(mode='w') +fp = tempfile.NamedTemporaryFile(mode='w') fi = 1 rarg = 2020 @@ -17,7 +19,7 @@ #random.seed(int(sys.argv[2])) fi = 3 -f = sys.stdin if len(sys.argv) == fi else file(sys.argv[fi], "rb") +f = sys.stdin if len(sys.argv) == fi else open(sys.argv[fi], "r") proj = [] for r in f: fo.write(r) @@ -40,7 +42,7 @@ f.close() print("c ./bin/projMC {} -fpv={} -rnd-seed{}", fo.name, fp.name, rarg) -pmc = subprocess.Popen(["./bin/projMC", "-rnd-init", "-rnd-seed={}".format(rarg), fo.name, "-fpv={0}".format(fp.name)], stdout=sys.stdout, stderr=sys.stderr) +pmc = subprocess.Popen([f"{helper.absolutizePath('./bin/projMC')}", "-rnd-init", "-rnd-seed={}".format(rarg), fo.name, "-fpv={0}".format(fp.name)], stdout=sys.stdout, stderr=sys.stderr) pmc.wait() fo.close() From 876475656b1aaa67c156f99675612c67fe28e0b7 Mon Sep 17 00:00:00 2001 From: Vu Date: Thu, 13 May 2021 00:27:01 -0500 Subject: [PATCH 12/13] enabled stdout info with: logger.addHandler(logging.StreamHandler(sys.stdout)) modified: nesthdb.py --- nesthdb.py | 1 + 1 file changed, 1 insertion(+) diff --git a/nesthdb.py b/nesthdb.py index cabfdc0..a3b90b0 100755 --- a/nesthdb.py +++ b/nesthdb.py @@ -18,6 +18,7 @@ from dpdb.writer import FileWriter, StreamWriter, denormalize_cnf, normalize_cnf logger = logging.getLogger("nestHDB") +logger.addHandler(logging.StreamHandler(sys.stdout)) #setup_logging("DEBUG") #setup_logging() setup_debug_sql() From e1948f4edc887a8a7230ab0b73b3b08a5d99a012 Mon Sep 17 00:00:00 2001 From: Vu Date: Fri, 13 Aug 2021 17:44:53 -0500 Subject: [PATCH 13/13] Deleted occurences of line: "# -*- coding: future_fstrings -*-" --- common.py | 8 ++++---- dpdb/abstraction.py | 12 +++++------- dpdb/db.py | 5 ++--- dpdb/problem.py | 6 ++---- dpdb/problems/nestpmc.py | 3 +-- dpdb/problems/pmc.py | 3 +-- dpdb/problems/pmcext.py | 3 +-- dpdb/problems/sat.py | 3 +-- dpdb/problems/sat_util.py | 1 - dpdb/problems/sharpsat.py | 4 +--- dpdb/problems/sharpsatext.py | 3 +-- dpdb/problems/vertexcover.py | 6 ++---- nesthdb.py | 2 +- 13 files changed, 22 insertions(+), 37 deletions(-) diff --git a/common.py b/common.py index f257444..024eff7 100755 --- a/common.py +++ b/common.py @@ -1,5 +1,5 @@ #!/usr/bin/python3 -# -*- coding: future_fstrings -*- + import argparse import logging import subprocess @@ -84,7 +84,7 @@ def setup_arg_parser(usage): parser = argparse.ArgumentParser(usage="%(prog)s [general options] -f input-file problem-type [problem specific-options]", formatter_class=MyFormatter) parser.add_argument("-f", "--file", dest="file", help="Input file for the problem to solve", required=True) - + # general options gen_opts = parser.add_argument_group("general options", "General options") gen_opts.add_argument("-t", dest="type", help="type of the cluster run", default="") @@ -110,7 +110,7 @@ def parse_args(parser): logging.basicConfig(format='[%(levelname)s] %(name)s: %(message)s', level=log_level) return args - + """ _LOG_LEVEL_STRINGS = ["DEBUG_SQL", "DEBUG", "INFO", "WARNING", "ERROR", "CRITICAL"] @@ -155,7 +155,7 @@ class MyFormatter(argparse.ArgumentDefaultsHelpFormatter,argparse.RawDescription p.add_argument(arg,**kwargs) parser.add_argument("-f", "--file", dest="file", help="Input file for the problem to solve", required=True) - + # general options gen_opts = parser.add_argument_group("general options", "General options") gen_opts.add_argument("-t", dest="type", help="type of the cluster run", default="") diff --git a/dpdb/abstraction.py b/dpdb/abstraction.py index c58ef5d..5a31e55 100644 --- a/dpdb/abstraction.py +++ b/dpdb/abstraction.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import clingo import importlib import logging @@ -150,13 +149,13 @@ def choose_subset(self, select_subset, encodingFile, timeout=30, usc=False, solv c = clingoctl aset = [sys.maxsize, False, [], None, []] - + def __on_model(model): #if len(model.cost) == 0: # return - + logger.debug("better answer set found: %s %s %s", model, model.cost, model.optimality_proven) - + aset[1] |= model.optimality_proven opt = model.cost[0] if len(model.cost) > 0 else 0 if opt <= aset[0]: @@ -173,7 +172,7 @@ def __on_model(model): # FIXME: use mutable string prog = encodingContent - + if clingoctl is None: c = clingo.Control() @@ -190,7 +189,7 @@ def __on_model(model): for p in self._nodes: prog += "p({0}).\n".format(p) - # subset (buckets) of proj to select upon + # subset (buckets) of proj to select upon #for b in range(1, select_subset + 1, 1): prog += "b({0}).\n".format(select_subset) #print(prog) @@ -391,4 +390,3 @@ def normalize(self): self.normalized_nodes = normalized_nodes self.normalized_adj = normalized_adj self.normalized_edges = normalized_edges - diff --git a/dpdb/db.py b/dpdb/db.py index 3170526..7d6893a 100644 --- a/dpdb/db.py +++ b/dpdb/db.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import logging import select import re @@ -37,7 +36,7 @@ def from_pool(cls, pool): instance = cls() instance._pool = pool instance._conn = pool.getconn() - return instance + return instance # we need this wrapper because conn object is required def __debug_query__ (self, query, params = []): @@ -86,7 +85,7 @@ def exec_and_fetch(self,q,p = []): return cur.fetchone() except pg.errors.AdminShutdown: logger.warning("Connection closed by admin") - + def exec_and_fetch_all(self,q,p = []): try: self.__debug_query__(q,p) diff --git a/dpdb/problem.py b/dpdb/problem.py index 7adb1d6..40edb85 100644 --- a/dpdb/problem.py +++ b/dpdb/problem.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import logging import os import signal @@ -255,7 +254,7 @@ def init_problem(): [self.name,self.type,self.td.num_bags,self.td.tree_width,self.td.num_orig_vertices,self.td.root.id],"id")[0] self.set_id(problem_id) logger.info("Created problem with ID %d", self.id) - + def drop_tables(): logger.debug("Dropping tables") self.db.drop_table("td_bag") @@ -310,7 +309,7 @@ def create_tables_for_node(n, workers = {}): db.create_view(f"td_node_{n.id}_v", ass_view) if "parallel_setup" in self.kwargs and self.kwargs["parallel_setup"]: db.close() - + def insert_data(): logger.debug("Inserting problem data") self.db.ignore_next_praefix(3) @@ -436,4 +435,3 @@ def solve_node(self, node, db): row_cnt = db.last_rowcount db.update("td_node_status",["end_time","rows"],["statement_timestamp()",str(row_cnt)],[f"node = {node.id}"]) db.commit() - diff --git a/dpdb/problems/nestpmc.py b/dpdb/problems/nestpmc.py index ffb4868..225ff98 100644 --- a/dpdb/problems/nestpmc.py +++ b/dpdb/problems/nestpmc.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import logging import subprocess from collections import defaultdict @@ -45,7 +44,7 @@ def __init__(self, name, pool, max_solver_threads=12, inner_vars_threshold=0, st def td_node_column_def(self,var): return td_node_column_def(var) - + def td_node_extra_columns(self): return [("model_count","NUMERIC")] diff --git a/dpdb/problems/pmc.py b/dpdb/problems/pmc.py index 3f73268..97498ee 100644 --- a/dpdb/problems/pmc.py +++ b/dpdb/problems/pmc.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import logging from collections import defaultdict @@ -15,7 +14,7 @@ def __init__(self, name, pool, store_formula=False, **kwargs): def td_node_column_def(self,var): return td_node_column_def(var) - + def filter(self,node): return filter(self.var_clause_dict, node) diff --git a/dpdb/problems/pmcext.py b/dpdb/problems/pmcext.py index 2268b92..6944d53 100644 --- a/dpdb/problems/pmcext.py +++ b/dpdb/problems/pmcext.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import logging import subprocess from collections import defaultdict @@ -27,7 +26,7 @@ def __init__(self, name, pool, max_solver_threads=12, store_formula=False, **kwa def td_node_column_def(self,var): return td_node_column_def(var) - + def td_node_extra_columns(self): return [("model_count","NUMERIC")] diff --git a/dpdb/problems/sat.py b/dpdb/problems/sat.py index 0fd4afa..8007d78 100644 --- a/dpdb/problems/sat.py +++ b/dpdb/problems/sat.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import logging from collections import defaultdict @@ -16,7 +15,7 @@ def __init__(self, name, pool, store_formula=False, **kwargs): def td_node_column_def(self,var): return td_node_column_def(var) - + def filter(self,node): return filter(self.var_clause_dict, node) diff --git a/dpdb/problems/sat_util.py b/dpdb/problems/sat_util.py index 770b2a9..8871e05 100644 --- a/dpdb/problems/sat_util.py +++ b/dpdb/problems/sat_util.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- from dpdb.problem import * from collections import defaultdict diff --git a/dpdb/problems/sharpsat.py b/dpdb/problems/sharpsat.py index ff710f5..4fcf060 100644 --- a/dpdb/problems/sharpsat.py +++ b/dpdb/problems/sharpsat.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import logging from collections import defaultdict @@ -19,7 +18,7 @@ def td_node_column_def(self,var): def td_node_extra_columns(self): return [("model_count","NUMERIC")] - + def candidate_extra_cols(self,node): return ["{} AS model_count".format( " * ".join(set([var2cnt(node,v) for v in node.vertices] + @@ -91,4 +90,3 @@ def node2cnt(node): ) } ) - diff --git a/dpdb/problems/sharpsatext.py b/dpdb/problems/sharpsatext.py index c2c4752..47239cb 100644 --- a/dpdb/problems/sharpsatext.py +++ b/dpdb/problems/sharpsatext.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import clingo import logging import subprocess @@ -31,7 +30,7 @@ def __init__(self, name, pool, max_solver_threads=12, store_formula=False, **kwa def td_node_column_def(self,var): return td_node_column_def(var) - + def td_node_extra_columns(self): return [("model_count","NUMERIC")] diff --git a/dpdb/problems/vertexcover.py b/dpdb/problems/vertexcover.py index 052c2cb..e6093af 100644 --- a/dpdb/problems/vertexcover.py +++ b/dpdb/problems/vertexcover.py @@ -1,4 +1,3 @@ -# -*- coding: future_fstrings -*- import logging from dpdb.reader import TdReader, TwReader, EdgeReader @@ -17,7 +16,7 @@ def td_node_column_def(self,var): def td_node_extra_columns(self): return [("size","INTEGER")] - + def candidate_extra_cols(self,node): introduce = [var2size(node,v) for v in node.vertices if node.needs_introduce(v)] join = [node2size(n) for n in node.children] @@ -32,7 +31,7 @@ def candidate_extra_cols(self,node): if len(join) > 1: children = [vc for c in node.children for vc in c.vertices if vc in node.vertices] duplicates = ["case when {} then 1 else 0 end * {}".format( - var2tab_col(node,var,False),len(node.vertex_children(var))-1) + var2tab_col(node,var,False),len(node.vertex_children(var))-1) for var in set(children) if len(node.vertex_children(var)) > 1] # subtract vertices counted multiple times if duplicates: @@ -116,4 +115,3 @@ def node2size(node): ) } ) - diff --git a/nesthdb.py b/nesthdb.py index a3b90b0..f71b52c 100755 --- a/nesthdb.py +++ b/nesthdb.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -# -*- coding: future_fstrings -*- + import importlib import logging import sys