Skip to content

Commit be1b476

Browse files
rpgoldmanrpgoldman
committed
Factor out ASP solver initialization.
Create two new methods, `build_encoding` and `init_solver` that encapsulate the set up of the solver. Did this for my own purposes, but it simplifies the code, as well, and could be used later to reduce code duplication.
1 parent 70bbb85 commit be1b476

File tree

4 files changed

+122
-120
lines changed

4 files changed

+122
-120
lines changed

‎popper/abs_generate.py‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,10 @@
11
import abc
2-
from typing import FrozenSet, Tuple, TYPE_CHECKING
2+
from typing import FrozenSet, Tuple, TYPE_CHECKING, List
3+
4+
import clingo
35

46
if TYPE_CHECKING:
5-
from . util import Literal, Settings
7+
from . util import Settings
68

79
Rule = Tuple['Literal', FrozenSet['Literal']]
810
RuleBase = FrozenSet[Rule]
@@ -41,4 +43,14 @@ def parse_handles(self, new_handles):
4143
pass
4244

4345
def constrain(self, tmp_new_cons):
46+
pass
47+
48+
@abc.abstractmethod
49+
def build_encoding(self, bkcons: List, settings: "Settings") -> str:
50+
"""Build and return a string for an ASP solver, used to generate hypotheses."""
51+
pass
52+
53+
@abc.abstractmethod
54+
def init_solver(self, encoding: str) -> clingo.Control:
55+
"""Incorporate the `encoding` into a new solver (`clingo.Control`) and return it."""
4456
pass

‎popper/gen2.py‎

Lines changed: 26 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
import numbers
22
import re
33
from itertools import permutations
4-
from typing import Any, Set, Tuple
4+
from typing import Any, Set, Tuple, Optional
55

66
import clingo
77
import clingo.script
@@ -19,6 +19,7 @@ def arg_to_symbol(arg):
1919
return Number(arg)
2020
if isinstance(arg, str):
2121
return Function(arg)
22+
raise TypeError(f"Cannot translate {arg} to clingo Symbol")
2223

2324

2425
def atom_to_symbol(pred, args) -> Function:
@@ -38,6 +39,9 @@ def atom_to_symbol(pred, args) -> Function:
3839

3940
class Generator(AbstractGenerator):
4041
settings: Settings
42+
model: Optional[clingo.Model]
43+
solver: Optional[clingo.Control]
44+
handler: Optional[clingo.SolveHandle]
4145

4246
def __init__(self, settings: Settings, bkcons=[]):
4347
self.savings = 0
@@ -46,26 +50,41 @@ def __init__(self, settings: Settings, bkcons=[]):
4650
self.handle = None
4751
self.pruned_sizes = set()
4852

53+
encoding = self.build_encoding(bkcons, settings)
54+
55+
with open('/tmp/ENCODING-GEN.pro', 'w') as f:
56+
f.write(encoding)
57+
58+
solver = self.init_solver(encoding)
59+
self.solver = solver
60+
61+
self.model = None
62+
63+
def init_solver(self, encoding):
64+
if self.settings.single_solve:
65+
solver = clingo.Control(['--heuristic=Domain', '-Wnone'])
66+
solver.configuration.solve.models = 0
67+
solver.add('base', [], encoding)
68+
solver.ground([('base', [])])
69+
return solver
70+
71+
def build_encoding(self, bkcons, settings):
4972
encoding = []
5073
alan = resource_string(__name__, "lp/alan.pl").decode()
5174
encoding.append(alan)
52-
5375
with open(settings.bias_file) as f:
5476
bias_text = f.read()
5577
bias_text = re.sub(r'max_vars\(\d*\).', '', bias_text)
5678
bias_text = re.sub(r'max_body\(\d*\).', '', bias_text)
5779
bias_text = re.sub(r'max_clauses\(\d*\).', '', bias_text)
58-
5980
# AC: NEED TO COMPLETELY REFACTOR THIS CODE
60-
for p,a in settings.pointless:
81+
for p, a in settings.pointless:
6182
bias_text = re.sub(rf'body_pred\({p},\s*{a}\)\.', '', bias_text)
6283
bias_text = re.sub(rf'constant\({p},.*?\).*', '', bias_text, flags=re.MULTILINE)
63-
6484
encoding.append(bias_text)
6585
encoding.append(f'max_clauses({settings.max_rules}).')
6686
encoding.append(f'max_body({settings.max_body}).')
6787
encoding.append(f'max_vars({settings.max_vars}).')
68-
6988
# ADD VARS, DIRECTIONS, AND TYPES
7089
head_arity = len(settings.head_literal.arguments)
7190
encoding.append(f'head_vars({head_arity}, {tuple(range(head_arity))}).')
@@ -76,7 +95,6 @@ def __init__(self, settings: Settings, bkcons=[]):
7695
encoding.append(f'vars({arity}, {tuple(xs)}).')
7796
for i, x in enumerate(xs):
7897
encoding.append(f'var_pos({x}, {tuple(xs)}, {i}).')
79-
8098
type_encoding = set()
8199
if self.settings.head_types:
82100
types = tuple(self.settings.head_types)
@@ -90,38 +108,22 @@ def __init__(self, settings: Settings, bkcons=[]):
90108
for i, x in enumerate(types):
91109
type_encoding.add(f'type_pos({str_types}, {i}, {x}).')
92110
encoding.extend(type_encoding)
93-
94111
for pred, xs in self.settings.directions.items():
95112
for i, v in xs.items():
96113
if v == '+':
97114
encoding.append(f'direction_({pred}, {i}, in).')
98115
if v == '-':
99116
encoding.append(f'direction_({pred}, {i}, out).')
100-
101117
max_size = (1 + settings.max_body) * settings.max_rules
102118
if settings.max_literals < max_size:
103119
encoding.append(f'custom_max_size({settings.max_literals}).')
104-
105120
if settings.noisy:
106121
encoding.append(NOISY_ENCODING)
107-
108122
encoding.extend(bkcons)
109-
110123
if settings.single_solve:
111124
encoding.append(DEFAULT_HEURISTIC)
112-
113125
encoding = '\n'.join(encoding)
114-
115-
with open('/tmp/ENCODING-GEN.pro', 'w') as f:
116-
f.write(encoding)
117-
118-
if self.settings.single_solve:
119-
solver = clingo.Control(['--heuristic=Domain', '-Wnone'])
120-
121-
solver.configuration.solve.models = 0
122-
solver.add('base', [], encoding)
123-
solver.ground([('base', [])])
124-
self.solver = solver
126+
return encoding
125127

126128
def update_solver(self, size):
127129
# not used when learning programs without pi or recursion

‎popper/gen3.py‎

Lines changed: 31 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -55,20 +55,45 @@ def __init__(self, settings, bkcons=[]):
5555
self.new_seen_rules = set()
5656
self.new_ground_cons = set()
5757

58+
encoding = self.build_encoding(bkcons, settings)
59+
60+
# with open('ENCODING-GEN.pl', 'w') as f:
61+
# f.write(encoding)
62+
63+
solver = self.init_solver(encoding)
64+
self.solver = solver
65+
66+
def init_solver(self, encoding):
67+
if self.settings.single_solve:
68+
solver = clingo.Control(['--heuristic=Domain', '-Wnone'])
69+
else:
70+
solver = clingo.Control(['-Wnone'])
71+
NUM_OF_LITERALS = """
72+
%%% External atom for number of literals in the program %%%%%
73+
#external size_in_literals(n).
74+
:-
75+
size_in_literals(n),
76+
#sum{K+1,Clause : body_size(Clause,K)} != n.
77+
"""
78+
solver.add('number_of_literals', ['n'], NUM_OF_LITERALS)
79+
solver.configuration.solve.models = 0
80+
solver.add('base', [], encoding)
81+
solver.ground([('base', [])])
82+
return solver
83+
84+
def build_encoding(self, bkcons, settings):
5885
encoding = []
5986
alan = resource_string(__name__, "lp/alan-old.pl").decode()
6087
encoding.append(alan)
61-
6288
with open(settings.bias_file) as f:
6389
bias_text = f.read()
64-
bias_text = re.sub(r'max_vars\(\d*\).','', bias_text)
65-
bias_text = re.sub(r'max_body\(\d*\).','', bias_text)
66-
bias_text = re.sub(r'max_clauses\(\d*\).','', bias_text)
90+
bias_text = re.sub(r'max_vars\(\d*\).', '', bias_text)
91+
bias_text = re.sub(r'max_body\(\d*\).', '', bias_text)
92+
bias_text = re.sub(r'max_clauses\(\d*\).', '', bias_text)
6793
encoding.append(bias_text)
6894
encoding.append(f'max_clauses({settings.max_rules}).')
6995
encoding.append(f'max_body({settings.max_body}).')
7096
encoding.append(f'max_vars({settings.max_vars}).')
71-
7297
# ADD VARS, DIRECTIONS, AND TYPES
7398
head_arity = len(settings.head_literal.arguments)
7499
encoding.append(f'head_vars({head_arity}, {tuple(range(head_arity))}).')
@@ -80,68 +105,38 @@ def __init__(self, settings, bkcons=[]):
80105

81106
for i, x in enumerate(xs):
82107
encoding.append(f'var_pos({x}, {tuple(xs)}, {i}).')
83-
84108
# types = tuple(self.settings.head_types)
85109
# str_types = str(types).replace("'","")
86110
# for x, i in enumerate(self.settings.head_types):
87111
# encoding.append(f'type_pos({str_types}, {i}, {x}).')
88-
89112
# for pred, types in self.settings.body_types.items():
90113
# types = tuple(types)
91114
# str_types = str(types).replace("'","")
92115
# for i, x in enumerate(types):
93-
94116
# encoding.append(f'type_pos({str_types}, {i}, {x}).')
95-
96117
# for pred, xs in self.settings.directions.items():
97118
# for i, v in xs.items():
98119
# if v == '+':
99120
# encoding.append(f'direction_({pred}, {i}, in).')
100121
# if v == '-':
101122
# encoding.append(f'direction_({pred}, {i}, out).')
102-
103123
max_size = (1 + settings.max_body) * settings.max_rules
104124
if settings.max_literals < max_size:
105125
encoding.append(f'custom_max_size({settings.max_literals}).')
106-
107126
if settings.pi_enabled:
108127
encoding.append(f'#show head_literal/4.')
109-
110128
if settings.noisy:
111129
encoding.append("""
112130
program_bounds(0..K):- max_size(K).
113131
program_size_at_least(M):- size(N), program_bounds(M), M <= N.
114132
""")
115-
116133
# if settings.bkcons:
117134
encoding.extend(bkcons)
118-
119135
if settings.single_solve:
120136
if settings.order_space:
121137
encoding.append(DEFAULT_HEURISTIC)
122-
123138
encoding = '\n'.join(encoding)
124-
125-
# with open('ENCODING-GEN.pl', 'w') as f:
126-
# f.write(encoding)
127-
128-
if self.settings.single_solve:
129-
solver = clingo.Control(['--heuristic=Domain','-Wnone'])
130-
else:
131-
solver = clingo.Control(['-Wnone'])
132-
NUM_OF_LITERALS = """
133-
%%% External atom for number of literals in the program %%%%%
134-
#external size_in_literals(n).
135-
:-
136-
size_in_literals(n),
137-
#sum{K+1,Clause : body_size(Clause,K)} != n.
138-
"""
139-
solver.add('number_of_literals', ['n'], NUM_OF_LITERALS)
140-
141-
solver.configuration.solve.models = 0
142-
solver.add('base', [], encoding)
143-
solver.ground([('base', [])])
144-
self.solver = solver
139+
return encoding
145140

146141
def get_prog(self):
147142
if self.handle is None:

0 commit comments

Comments
 (0)