Source code for nltk.inference.mace

# Natural Language Toolkit: Interface to the Mace4 Model Builder
#
# Author: Dan Garrette <dhgarrette@gmail.com>
#         Ewan Klein <ewan@inf.ed.ac.uk>

# URL: <http://nltk.org/>
# For license information, see LICENSE.TXT

"""
A model builder that makes use of the external 'Mace4' package.
"""
from __future__ import print_function

import os
import tempfile

from nltk.sem.logic import is_indvar
from nltk.sem import Valuation, Expression

from nltk.inference.api import ModelBuilder, BaseModelBuilderCommand
from nltk.inference.prover9 import Prover9CommandParent, Prover9Parent


[docs]class MaceCommand(Prover9CommandParent, BaseModelBuilderCommand): """ 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. """ _interpformat_bin = None def __init__(self, goal=None, assumptions=None, max_models=500, model_builder=None): """ :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) @property def valuation(mbc): return mbc.model('valuation') def _convert2val(self, valuation_str): """ 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) @staticmethod 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 @staticmethod 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 = int(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) @staticmethod 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 = value // 26 return (letter + str(num) if num > 0 else letter) def _decorate_model(self, valuation_str, format): """ 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) def _transform_output(self, 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") def _call_interpformat(self, input_str, args=[], verbose=False): """ 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)
[docs]class Mace(Prover9Parent, ModelBuilder): _mace4_bin = None def __init__(self, end_size=500): self._end_size = end_size """The maximum model size that Mace will try before simply returning false. (Use -1 for no maximum.)""" def _build_model(self, goal=None, assumptions=None, verbose=False): """ 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) def _call_mace4(self, input_str, args=[], verbose=False): """ 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)
[docs]def spacer(num=30): print('-' * num)
[docs]def decode_result(found): """ 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]
[docs]def test_model_found(arguments): """ Try some proofs and exhibit the results. """ for (goal, assumptions) in arguments: g = Expression.fromstring(goal) alist = [lp.parse(a) for a in assumptions] m = MaceCommand(g, assumptions=alist, max_models=50) found = m.build_model() for a in alist: print(' %s' % a) print('|- %s: %s\n' % (g, decode_result(found)))
[docs]def test_build_model(arguments): """ Try to build a ``nltk.sem.Valuation``. """ g = Expression.fromstring('all x.man(x)') alist = [Expression.fromstring(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')
[docs]def test_transform_output(argument_pair): """ Transform the model into various Mace4 ``interpformat`` formats. """ g = Expression.fromstring(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))
[docs]def test_make_relation_set(): 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')]))
arguments = [ ('mortal(Socrates)', ['all x.(man(x) -> mortal(x))', 'man(Socrates)']), ('(not mortal(Socrates))', ['all x.(man(x) -> mortal(x))', 'man(Socrates)']) ]
[docs]def demo(): test_model_found(arguments) test_build_model(arguments) test_transform_output(arguments[1])
if __name__ == '__main__': demo()