Bases: Solver
A solver that uses clingo.
clingo is an ASP
system to ground and solve logic programs, it is
part of the Potsdam Answer Set Solving Collection (Potassco; potassco.org/).
>>> from typedlogic.integrations.frameworks.pydantic import FactBaseModel
>>> class AncestorOf(FactBaseModel):
... ancestor: str
... descendant: str
>>> from typedlogic import SentenceGroup, PredicateDefinition
>>> solver = ClingoSolver()
>>> solver.add_predicate_definition(PredicateDefinition(predicate="AncestorOf", arguments={'ancestor': str, 'descendant': str}))
>>> solver.add_fact(AncestorOf(ancestor='p1', descendant='p1a'))
>>> solver.add_fact(AncestorOf(ancestor='p1a', descendant='p1aa'))
>>> aa = SentenceGroup(name="transitivity-of-ancestor-of")
>>> solver.add_sentence_group(aa)
>>> soln = solver.check()
This solver does not implement the open-world assumption.
>>> from typedlogic.profiles import OpenWorld
>>> solver.profile.impl(OpenWorld)
False
This solver supports MultipleModelSemantics:
>>> from typedlogic.profiles import MultipleModelSemantics
>>> solver.profile.impl(MultipleModelSemantics)
True
This means that when you call solver.models(), you will get all models that satisfy the program.
See the tutorial for examples of this.
Source code in src/typedlogic/integrations/solvers/clingo/clingo_solver.py
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131 | @dataclass
class ClingoSolver(Solver):
"""
A solver that uses clingo.
[clingo](https://potassco.org/clingo/) is an [ASP](https://en.wikipedia.org/wiki/Answer_set_programming)
system to ground and solve logic programs, it is
part of the Potsdam Answer Set Solving Collection (Potassco; [potassco.org/](https://potassco.org/)).
>>> from typedlogic.integrations.frameworks.pydantic import FactBaseModel
>>> class AncestorOf(FactBaseModel):
... ancestor: str
... descendant: str
>>> from typedlogic import SentenceGroup, PredicateDefinition
>>> solver = ClingoSolver()
>>> solver.add_predicate_definition(PredicateDefinition(predicate="AncestorOf", arguments={'ancestor': str, 'descendant': str}))
>>> solver.add_fact(AncestorOf(ancestor='p1', descendant='p1a'))
>>> solver.add_fact(AncestorOf(ancestor='p1a', descendant='p1aa'))
>>> aa = SentenceGroup(name="transitivity-of-ancestor-of")
>>> solver.add_sentence_group(aa)
>>> soln = solver.check()
This solver does not implement the open-world assumption.
>>> from typedlogic.profiles import OpenWorld
>>> solver.profile.impl(OpenWorld)
False
This solver supports MultipleModelSemantics:
>>> from typedlogic.profiles import MultipleModelSemantics
>>> solver.profile.impl(MultipleModelSemantics)
True
This means that when you call `solver.models()`, you will get all models that satisfy the program.
See the tutorial for examples of this.
"""
exec_name: str = field(default="clingo")
profile: ClassVar[Profile] = MixedProfile(AnswerSetProgramming(), AllowsComparisonTerms(), MultipleModelSemantics())
ctl: Optional[Control] = None
def _clauses(self) -> Iterator[str]:
negation_symbol = "not" if self.assume_closed_world else "-"
prolog_config = PrologConfig(
disjunctive_datalog=True,
double_quote_strings=True,
negation_symbol=negation_symbol,
allow_nesting=False,
double_quote_floats=True,
)
for sentence in self.base_theory.sentences + self.base_theory.ground_terms:
if not isinstance(sentence, Sentence):
raise ValueError(f"Expected Sentence, got {sentence}")
rules = []
try:
for rule in to_horn_rules(sentence, allow_disjunctions_in_head=True, allow_goal_clauses=True):
rules.append(rule)
# yield as_prolog(rule, config=prolog_config)
except NotInProfileError as e:
logger.info(f"Skipping sentence {sentence} due to {e}")
for rule in rules:
try:
yield as_prolog(rule, config=prolog_config)
except NotInProfileError as e:
logger.info(f"Skipping sentence {sentence} due to {e}")
def models(self) -> Iterator[Model]:
ctl = Control(["0"])
predicate_name_map = {pd.predicate.lower(): pd.predicate for pd in self.base_theory.predicate_definitions}
for clause in self._clauses():
ctl.add(clause)
# Ground the program
ctl.ground([("base", [])])
# Solve the program
with ctl.solve(yield_=True) as handle:
for clingo_model in handle:
facts = []
for atom in clingo_model.symbols(shown=True):
p = predicate_name_map.get(atom.name, atom.name)
def _v(sym: clingo.Symbol) -> Any:
if sym.type == SymbolType.String:
return str(sym.string)
if sym.type == SymbolType.Number:
return sym.number
return sym
term = Term(p, *[_v(a) for a in atom.arguments])
if not atom.positive:
term = ~term
facts.append(term)
model = Model(ground_terms=facts)
yield model
def check(self) -> Solution:
models = list(self.models())
sat = len(models) > 0
return Solution(satisfiable=sat)
def dump(self) -> str:
s = ""
for clause in self._clauses():
s += f"{clause}\n"
return s
|
