diff --git a/popper/bkcons.py b/popper/bkcons.py index 31c05cc2..7d51b4f0 100644 --- a/popper/bkcons.py +++ b/popper/bkcons.py @@ -713,13 +713,10 @@ def deduce_bk_cons(settings, tester): encoding.append(f'type({p},{types}).') - - encoding = '\n'.join(encoding) - # print(encoding) - # with open('bkcons-encoding.pl', 'w') as f: - # f.write(encoding) - # exit() - solver = clingo.Control(['-Wnone']) + encoding = '\n'.join(encoding_list) + solve_arg = [] if settings.num_cores == 1 \ + else [f"--parallel-mode={settings.num_cores}"] + solver = clingo.Control(['-Wnone'] + solve_arg) solver.add('base', [], encoding) solver.ground([('base', [])]) out = set() @@ -745,11 +742,13 @@ def deduce_recalls(settings): counts = {} counts_all = {} + solve_arg = [] if settings.num_cores == 1 \ + else [f"--parallel-mode={settings.num_cores}"] try: with open(settings.bk_file) as f: bk = f.read() - solver = clingo.Control(['-Wnone']) + solver = clingo.Control(['-Wnone'] + solve_arg) with suppress_stdout_stderr(): solver.add('base', [], bk) solver.ground([('base', [])]) @@ -842,7 +841,9 @@ def deduce_type_cons(settings): with open(settings.bk_file) as f: bk = f.read() - solver = clingo.Control(['-Wnone']) + solve_arg = [] if settings.num_cores == 1 \ + else [f"--parallel-mode={settings.num_cores}"] + solver = clingo.Control(['-Wnone'] + solve_arg) solver.add('base', [], bk) solver.ground([('base', [])]) @@ -1008,8 +1009,10 @@ def deduce_non_singletons(settings): # with open('TOTAL', 'w') as f: # f.write(encoding) - solver = clingo.Control(['-Wnone']) - solver.add('base', [], encoding) + solve_arg = [] if settings.num_cores == 1 \ + else [f"--parallel-mode={settings.num_cores}"] + solver = clingo.Control(['-Wnone'] + solve_arg) + solver.add('base', [], encoding_str) solver.ground([('base', [])]) cons = [] diff --git a/popper/gen2.py b/popper/gen2.py index a536f866..f6544e95 100644 --- a/popper/gen2.py +++ b/popper/gen2.py @@ -38,6 +38,19 @@ def __init__(self, settings, bkcons=[]): self.handle = None self.pruned_sizes = set() + solver = self.init_solver(encoding) + self.solver = solver + + def init_solver(self, encoding) -> clingo.Control: + solve_arg = [] if self.settings.num_cores == 1 \ + else [f"--parallel-mode={self.settings.num_cores}"] + solver = clingo.Control(['--heuristic=Domain', '-Wnone'] + solve_arg) + solver.configuration.solve.models = 0 + solver.add('base', [], encoding) + solver.ground([('base', [])]) + return solver + + def build_encoding(self, bkcons, settings): encoding = [] alan = resources.files(__package__).joinpath("lp/alan.pl").read_text() encoding.append(alan) diff --git a/popper/gen3.py b/popper/gen3.py index ab39be3a..88495228 100644 --- a/popper/gen3.py +++ b/popper/gen3.py @@ -53,6 +53,37 @@ def __init__(self, settings, bkcons=[]): self.new_seen_rules = set() self.new_ground_cons = set() + encoding = self.build_encoding(bkcons, settings) + + # with open('ENCODING-GEN.pl', 'w') as f: + # f.write(encoding) + + solver = self.init_solver(encoding) + self.solver = solver + + def init_solver(self, encoding) -> clingo.Control: + solve_arg = [] if self.settings.num_cores == 1 \ + else [f"--parallel-mode={self.settings.num_cores}"] + if self.settings.single_solve: + solver = clingo.Control(['--heuristic=Domain', '-Wnone'] + solve_arg) + else: + solver = clingo.Control(['-Wnone'] + solve_arg) + NUM_OF_LITERALS = """ + %%% External atom for number of literals in the program %%%%% + #external size_in_literals(n). + :- + size_in_literals(n), + #sum{K+1,Clause : body_size(Clause,K)} != n. + """ + solver.add('number_of_literals', ['n'], NUM_OF_LITERALS) + assert isinstance(solver.configuration.solve, + clingo.configuration.Configuration) + solver.configuration.solve.models = 0 + solver.add('base', [], encoding) + solver.ground([('base', [])]) + return solver + + def build_encoding(self, bkcons, settings): encoding = [] alan = resources.files(__package__).joinpath("lp/alan-old.pl").read_text() encoding.append(alan) @@ -103,8 +134,7 @@ def __init__(self, settings, bkcons=[]): encoding.append(f'custom_max_size({settings.max_literals}).') if settings.pi_enabled: - encoding.append(f'#show head_literal/4.') - + encoding.append('#show head_literal/4.') if settings.noisy: encoding.append(""" program_bounds(0..K):- max_size(K). diff --git a/popper/generate.py b/popper/generate.py index d99e8319..eff11775 100644 --- a/popper/generate.py +++ b/popper/generate.py @@ -102,6 +102,54 @@ def __init__(self, settings, bkcons=[]): # TODO: dunno self.new_ground_cons = set() + encoding = self.build_encoding(bkcons, settings) + + # with open('ENCODING-GEN.pl', 'w') as f: + # f.write(encoding) + + solver = self.init_solver(encoding) + self.solver = solver + + def init_solver(self, encoding): + solve_arg = [] if self.settings.num_cores == 1 \ + else [f"--parallel-mode={self.settings.num_cores}"] + if self.settings.single_solve: + solver = clingo.Control(['--heuristic=Domain', '-Wnone'] + solve_arg) + else: + solver = clingo.Control(['-Wnone'] + solve_arg) + NUM_OF_LITERALS = """ + %%% External atom for number of literals in the program %%%%% + #external size_in_literals(n). + :- + size_in_literals(n), + #sum{K+1,Clause : body_size(Clause,K)} != n. + """ + solver.add('number_of_literals', ['n'], NUM_OF_LITERALS) + + if self.settings.no_bias: + NUM_OF_VARS = """ + %%% External atom for number of variables in the program %%%%% + #external size_in_vars(v). + :- + size_in_vars(v), + #max{V : clause_var(_,V)} != v - 1. + """ + solver.add('number_of_vars', ['v'], NUM_OF_VARS) + + NUM_OF_RULES = """ + %%% External atom for number of rules in the program %%%%% + #external size_in_rules(r). + :- + size_in_rules(r), + #max{R : clause(R)} != r - 1. + """ + solver.add('number_of_rules', ['r'], NUM_OF_RULES) + solver.configuration.solve.models = 0 + solver.add('base', [], encoding) + solver.ground([('base', [])]) + return solver + + def build_encoding(self, bkcons, settings): encoding = [] alan = resources.files(__package__).joinpath("lp/alan-old.pl").read_text() # alan = resources.files(__package__).joinpath("lp/alan.pl").read_text() @@ -1061,7 +1109,11 @@ def find_bindings(self, body, all_vars): # print('ASDASDA') # solver = clingo.Control() - solver = clingo.Control(['-Wnone']) + # solver = clingo.Control(['-Wnone']) + if self.settings.num_cores == 1: + solver = clingo.Control(['-Wnone']) + else: + solver = clingo.Control(['-Wnone', f"--parallel-mode={self.settings.num_cores}"]) # solver = clingo.Control(["-t4"]) # ask for all models solver.configuration.solve.models = 0 diff --git a/popper/util.py b/popper/util.py index 742f049f..06cf8516 100644 --- a/popper/util.py +++ b/popper/util.py @@ -222,7 +222,7 @@ def flatten(xs): return [item for sublist in xs for item in sublist] class Settings: - def __init__(self, cmd_line=False, info=True, debug=False, show_stats=True, max_literals=MAX_LITERALS, timeout=TIMEOUT, quiet=False, eval_timeout=EVAL_TIMEOUT, max_examples=MAX_EXAMPLES, max_body=None, max_rules=None, max_vars=None, functional_test=False, kbpath=False, ex_file=False, bk_file=False, bias_file=False, showcons=False, no_bias=False, order_space=False, noisy=False, batch_size=BATCH_SIZE, solver='rc2', anytime_solver=None, anytime_timeout=ANYTIME_TIMEOUT): + def __init__(self, cmd_line=False, info=True, debug=False, show_stats=True, max_literals=MAX_LITERALS, timeout=TIMEOUT, quiet=False, eval_timeout=EVAL_TIMEOUT, max_examples=MAX_EXAMPLES, max_body=None, max_rules=None, max_vars=None, functional_test=False, kbpath=False, ex_file=False, bk_file=False, bias_file=False, showcons=False, no_bias=False, order_space=False, noisy=False, batch_size=BATCH_SIZE, solver='rc2', anytime_solver=None, anytime_timeout=ANYTIME_TIMEOUT,num_cores=1): if cmd_line: args = parse_args() @@ -302,6 +302,7 @@ def format(self, record): self.no_bias = no_bias self.order_space = order_space self.noisy = noisy + self.num_cores = num_cores if noisy: self.batch_size = 20000 @@ -317,7 +318,10 @@ def format(self, record): self.solution = None self.best_prog_score = None - solver = clingo.Control(['-Wnone']) + if num_cores == 1: + solver = clingo.Control(['-Wnone']) + else: + solver = clingo.Control(['-Wnone', f"--parallel-mode={num_cores}"]) with open(self.bias_file) as f: solver.add('bias', [], f.read()) solver.add('bias', [], """ @@ -624,7 +628,11 @@ def load_types(settings): #defined clause_var/2. #defined var_type/3.""" # solver = clingo.Control() - solver = clingo.Control(['-Wnone']) + # solver = clingo.Control(['-Wnone']) + if settings.num_cores == 1: + solver = clingo.Control(['-Wnone']) + else: + solver = clingo.Control(['-Wnone', f"--parallel-mode={settings.num_cores}"]) with open(settings.bias_file) as f: solver.add('bias', [], f.read()) solver.add('bias', [], enc)