Skip to content

Add "--num-cores" option and pass through to clingo. #138

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
rpgoldman wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Add "--num-cores" option and pass through to clingo. #138

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 14 additions & 11 deletions popper/bkcons.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand All @@ -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', [])])
Expand Down Expand Up @@ -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', [])])

Expand Down Expand Up @@ -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 = []
Expand Down
13 changes: 13 additions & 0 deletions popper/gen2.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
34 changes: 32 additions & 2 deletions popper/gen3.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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).
Expand Down
54 changes: 53 additions & 1 deletion popper/generate.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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
Expand Down
14 changes: 11 additions & 3 deletions popper/util.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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
Expand All @@ -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', [], """
Expand Down Expand Up @@ -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)
Expand Down