Coverage for nltk.inference.mace : 23%
Hot-keys on this page
r m x p toggle line displays
j k next/prev highlighted chunk
0 (zero) top of page
1 (one) first highlighted chunk
|
# Natural Language Toolkit: Interface to the Mace4 Model Builder # # Author: Dan Garrette <dhgarrette@gmail.com> # Ewan Klein <ewan@inf.ed.ac.uk>
# URL: <http://www.nltk.org/> # For license information, see LICENSE.TXT
A model builder that makes use of the external 'Mace4' package. """
""" A ``MaceCommand`` specific to the ``Mace`` model builder. It contains a print_assumptions() method that is used to print the list of assumptions in multiple formats. """
""" :param goal: Input expression to prove :type goal: sem.Expression :param assumptions: Input expressions to use as assumptions in the proof. :type assumptions: list(sem.Expression) :param max_models: The maximum number of models that Mace will try before simply returning false. (Use 0 for no maximum.) :type max_models: int """ if model_builder is not None: assert isinstance(model_builder, Mace) else: model_builder = Mace(max_models)
BaseModelBuilderCommand.__init__(self, model_builder, goal, assumptions)
def valuation(mbc): return mbc.model('valuation')
""" Transform the output file into an NLTK-style Valuation.
:return: A model if one is generated; None otherwise. :rtype: sem.Valuation """ valuation_standard_format = self._transform_output(valuation_str, 'standard')
val = [] for line in valuation_standard_format.splitlines(False): l = line.strip()
if l.startswith('interpretation'): # find the number of entities in the model num_entities = int(l[l.index('(')+1:l.index(',')].strip())
elif l.startswith('function') and l.find('_') == -1: # replace the integer identifier with a corresponding alphabetic character name = l[l.index('(')+1:l.index(',')].strip() if is_indvar(name): name = name.upper() value = int(l[l.index('[')+1:l.index(']')].strip()) val.append((name, MaceCommand._make_model_var(value)))
elif l.startswith('relation'): l = l[l.index('(')+1:] if '(' in l: #relation is not nullary name = l[:l.index('(')].strip() values = [int(v.strip()) for v in l[l.index('[')+1:l.index(']')].split(',')] val.append((name, MaceCommand._make_relation_set(num_entities, values))) else: #relation is nullary name = l[:l.index(',')].strip() value = int(l[l.index('[')+1:l.index(']')].strip()) val.append((name, value == 1))
return Valuation(val)
def _make_relation_set(num_entities, values): """ Convert a Mace4-style relation table into a dictionary.
:param num_entities: the number of entities in the model; determines the row length in the table. :type num_entities: int :param values: a list of 1's and 0's that represent whether a relation holds in a Mace4 model. :type values: list of int """ r = set() for position in [pos for (pos,v) in enumerate(values) if v == 1]: r.add(tuple(MaceCommand._make_relation_tuple(position, values, num_entities))) return r
def _make_relation_tuple(position, values, num_entities): if len(values) == 1: return [] else: sublist_size = len(values) / num_entities sublist_start = position / sublist_size sublist_position = position % sublist_size
sublist = values[sublist_start*sublist_size:(sublist_start+1)*sublist_size] return [MaceCommand._make_model_var(sublist_start)] + \ MaceCommand._make_relation_tuple(sublist_position, sublist, num_entities)
def _make_model_var(value): """ Pick an alphabetic character as identifier for an entity in the model.
:param value: where to index into the list of characters :type value: int """ letter = ['a','b','c','d','e','f','g','h','i','j','k','l','m','n', 'o','p','q','r','s','t','u','v','w','x','y','z'][value] num = int(value) / 26 if num > 0: return letter + str(num) else: return letter
""" Print out a Mace4 model using any Mace4 ``interpformat`` format. See http://www.cs.unm.edu/~mccune/mace4/manual/ for details.
:param valuation_str: str with the model builder's output :param format: str indicating the format for displaying models. Defaults to 'standard' format. :return: str """ if not format: return valuation_str elif format == 'valuation': return self._convert2val(valuation_str) else: return self._transform_output(valuation_str, format)
""" Transform the output file into any Mace4 ``interpformat`` format.
:param format: Output format for displaying models. :type format: str """ if format in ['standard', 'standard2', 'portable', 'tabular', 'raw', 'cooked', 'xml', 'tex']: return self._call_interpformat(valuation_str, [format])[0] else: raise LookupError("The specified format does not exist")
""" Call the ``interpformat`` binary with the given input.
:param input_str: A string whose contents are used as stdin. :param args: A list of command-line arguments. :return: A tuple (stdout, returncode) :see: ``config_prover9`` """ if self._interpformat_bin is None: self._interpformat_bin = self._modelbuilder._find_binary( 'interpformat', verbose)
return self._modelbuilder._call(input_str, self._interpformat_bin, args, verbose)
self._end_size = end_size """The maximum model size that Mace will try before simply returning false. (Use -1 for no maximum.)"""
""" Use Mace4 to build a first order model.
:return: ``True`` if a model was found (i.e. Mace returns value of 0), else ``False`` """ if not assumptions: assumptions = []
stdout, returncode = self._call_mace4(self.prover9_input(goal, assumptions), verbose=verbose) return (returncode == 0, stdout)
""" Call the ``mace4`` binary with the given input.
:param input_str: A string whose contents are used as stdin. :param args: A list of command-line arguments. :return: A tuple (stdout, returncode) :see: ``config_prover9`` """ if self._mace4_bin is None: self._mace4_bin = self._find_binary('mace4', verbose)
updated_input_str = '' if self._end_size > 0: updated_input_str += 'assign(end_size, %d).\n\n' % self._end_size updated_input_str += input_str
return self._call(updated_input_str, self._mace4_bin, args, verbose)
print('-' * num)
""" Decode the result of model_found()
:param found: The output of model_found() :type found: bool """ return {True: 'Countermodel found', False: 'No countermodel found', None: 'None'}[found]
""" Try some proofs and exhibit the results. """ lp = LogicParser() for (goal, assumptions) in arguments: g = lp.parse(goal) alist = [lp.parse(a) for a in assumptions] m = MaceCommand(g, assumptions=alist, end_size=50) found = m.build_model() for a in alist: print(' %s' % a) print('|- %s: %s\n' % (g, decode_result(found)))
""" Try to build a ``nltk.sem.Valuation``. """ lp = LogicParser() g = lp.parse('all x.man(x)') alist = [lp.parse(a) for a in ['man(John)', 'man(Socrates)', 'man(Bill)', 'some x.(-(x = John) & man(x) & sees(John,x))', 'some x.(-(x = Bill) & man(x))', 'all x.some y.(man(x) -> gives(Socrates,x,y))']]
m = MaceCommand(g, assumptions=alist) m.build_model() spacer() print("Assumptions and Goal") spacer() for a in alist: print(' %s' % a) print('|- %s: %s\n' % (g, decode_result(m.build_model()))) spacer() #print m.model('standard') #print m.model('cooked') print("Valuation") spacer() print(m.valuation, '\n')
""" Transform the model into various Mace4 ``interpformat`` formats. """ lp = LogicParser() g = lp.parse(argument_pair[0]) alist = [lp.parse(a) for a in argument_pair[1]] m = MaceCommand(g, assumptions=alist) m.build_model() for a in alist: print(' %s' % a) print('|- %s: %s\n' % (g, m.build_model())) for format in ['standard', 'portable', 'xml', 'cooked']: spacer() print("Using '%s' format" % format) spacer() print(m.model(format=format))
print(MaceCommand._make_relation_set(num_entities=3, values=[1,0,1]) == set([('c',), ('a',)])) print(MaceCommand._make_relation_set(num_entities=3, values=[0,0,0,0,0,0,1,0,0]) == set([('c', 'a')])) print(MaceCommand._make_relation_set(num_entities=2, values=[0,0,1,0,0,0,1,0]) == set([('a', 'b', 'a'), ('b', 'b', 'a')]))
('mortal(Socrates)', ['all x.(man(x) -> mortal(x))', 'man(Socrates)']), ('(not mortal(Socrates))', ['all x.(man(x) -> mortal(x))', 'man(Socrates)']) ]
test_model_found(arguments) test_build_model(arguments) test_transform_output(arguments[1])
demo() |