natural language toolkit interface to the mace4 model builder dan garrette dhgarrettegmail com ewan klein ewaninf ed ac uk url https 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 printassumptions 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 listsem expression param maxmodels the maximum number of models that mace will try before simply returning false use 0 for no maximum type maxmodels int transform the output file into an nltkstyle valuation return a model if one is generated none otherwise rtype sem valuation find the number of entities in the model replace the integer identifier with a corresponding alphabetic character relation is not nullary relation is nullary convert a mace4style relation table into a dictionary param numentities the number of entities in the model determines the row length in the table type numentities 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 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 print out a mace4 model using any mace4 interpformat format see https www cs unm edumccunemace4manual for details param valuationstr str with the model builder s output param format str indicating the format for displaying models defaults to standard format return str transform the output file into any mace4 interpformat format param format output format for displaying models type format str call the interpformat binary with the given input param inputstr a string whose contents are used as stdin param args a list of commandline arguments return a tuple stdout returncode see configprover9 the maximum model size that mace will try before simply returning false use 1 for no maximum def buildmodelself goalnone assumptionsnone verbosefalse if not assumptions assumptions stdout returncode self callmace4 self prover9inputgoal assumptions verboseverbose return returncode 0 stdout def callmace4self inputstr args verbosefalse if self mace4bin is none self mace4bin self findbinarymace4 verbose updatedinputstr if self endsize 0 updatedinputstr assignendsize d nn self endsize updatedinputstr inputstr return self callupdatedinputstr self mace4bin args verbose def spacernum30 print num def decoderesultfound return true countermodel found false no countermodel found none none found def testmodelfoundarguments for goal assumptions in arguments g expression fromstringgoal alist lp parsea for a in assumptions m macecommandg assumptionsalist maxmodels50 found m buildmodel for a in alist print s a printf g decoderesultfoundn def testbuildmodelarguments g expression fromstringall x manx alist expression fromstringa for a in manjohn mansocrates manbill some x x john manx seesjohn x some x x bill manx all x some y manx givessocrates x y m macecommandg assumptionsalist m buildmodel spacer printassumptions and goal spacer for a in alist print s a printf g decoderesultm buildmodeln spacer printm model standard printm model cooked printvaluation spacer printm valuation n def testtransformoutputargumentpair g expression fromstringargumentpair0 alist lp parsea for a in argumentpair1 m macecommandg assumptionsalist m buildmodel for a in alist print s a printf g m buildmodeln for format in standard portable xml cooked spacer printusing s format format spacer printm modelformatformat def testmakerelationset print macecommand makerelationsetnumentities3 values1 0 1 c a print macecommand makerelationset numentities3 values0 0 0 0 0 0 1 0 0 c a print macecommand makerelationsetnumentities2 values0 0 1 0 0 0 1 0 a b a b b a arguments mortalsocrates all x manx mortalx mansocrates not mortalsocrates all x manx mortalx mansocrates def demo testmodelfoundarguments testbuildmodelarguments testtransformoutputarguments1 if name main demo natural language toolkit interface to the mace4 model builder dan garrette dhgarrette gmail com ewan klein ewan inf ed ac uk url https 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 transform the output file into an nltk style valuation return a model if one is generated none otherwise rtype sem valuation find the number of entities in the model replace the integer identifier with a corresponding alphabetic character relation is not nullary relation is nullary 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 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 print out a mace4 model using any mace4 interpformat format see https 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 transform the output file into any mace4 interpformat format param format output format for displaying models type format str 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 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 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 decode the result of model_found param found the output of model_found type found bool try some proofs and exhibit the results try to build a nltk sem valuation print m model standard print m model cooked transform the model into various mace4 interpformat formats
import os
import tempfile

from nltk.inference.api import BaseModelBuilderCommand, ModelBuilder
from nltk.inference.prover9 import Prover9CommandParent, Prover9Parent
from nltk.sem import Expression, Valuation
from nltk.sem.logic import is_indvar


class MaceCommand(Prover9CommandParent, BaseModelBuilderCommand):
    

    _interpformat_bin = None

    def __init__(self, goal=None, assumptions=None, max_models=500, model_builder=None):
        
        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):
        
        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"):
                
                num_entities = int(l[l.index("(") + 1 : l.index(",")].strip())

            elif l.startswith("function") and l.find("_") == -1:
                
                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:
                    
                    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:
                    
                    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):
        
        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):
        
        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):
        
        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):
        
        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):
        
        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
        )


class Mace(Prover9Parent, ModelBuilder):
    _mace4_bin = None

    def __init__(self, end_size=500):
        self._end_size = end_size
        

    def _build_model(self, goal=None, assumptions=None, verbose=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):
        
        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)


def spacer(num=30):
    print("-" * num)


def decode_result(found):
    
    return {True: "Countermodel found", False: "No countermodel found", None: "None"}[
        found
    ]


def test_model_found(arguments):
    
    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(f"|- {g}: {decode_result(found)}\n")


def test_build_model(arguments):
    
    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(f"|- {g}: {decode_result(m.build_model())}\n")
    spacer()
    
    
    print("Valuation")
    spacer()
    print(m.valuation, "\n")


def test_transform_output(argument_pair):
    
    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(f"|- {g}: {m.build_model()}\n")
    for format in ["standard", "portable", "xml", "cooked"]:
        spacer()
        print("Using '%s' format" % format)
        spacer()
        print(m.model(format=format))


def test_make_relation_set():
    print(
        MaceCommand._make_relation_set(num_entities=3, values=[1, 0, 1])
        == {("c",), ("a",)}
    )
    print(
        MaceCommand._make_relation_set(
            num_entities=3, values=[0, 0, 0, 0, 0, 0, 1, 0, 0]
        )
        == {("c", "a")}
    )
    print(
        MaceCommand._make_relation_set(num_entities=2, values=[0, 0, 1, 0, 0, 0, 1, 0])
        == {("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)"]),
]


def demo():
    test_model_found(arguments)
    test_build_model(arguments)
    test_transform_output(arguments[1])


if __name__ == "__main__":
    demo()