<commit_before># Natural Language Toolkit: Interface to the Mace4 Model Builder 
#
# Author: <NAME> <<EMAIL>>
#         <NAME> <<EMAIL>>

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

import os
import tempfile
from string import join
from nltk.sem.logic import *
from nltk.sem import Valuation
from api import ModelBuilder, BaseModelBuilderCommand
import prover9
from prover9 import Prover9Parent, Prover9CommandParent, \
                    call_mace4, call_interpformat

"""
A model builder that makes use of the external 'Mace4' package.
"""

class MaceCommand(Prover9CommandParent, BaseModelBuilderCommand):
    """
    A L{MaceCommand} specific to the L{Mace} model builder.  It contains
    the a print_assumptions() method that is used to print the list
    of assumptions in multiple formats.
    """
    def __init__(self, goal=None, assumptions=None, timeout=60):
        """
        @param goal: Input expression to prove
        @type goal: L{logic.Expression}
        @param assumptions: Input expressions to use as assumptions in
            the proof.
        @type assumptions: C{list} of L{logic.Expression}
        @param timeout: number of seconds before timeout; set to 0 for
            no timeout.
        @type timeout: C{int}
        """
        BaseModelBuilderCommand.__init__(self, Mace(timeout), goal, assumptions)
        
    def convert2val(self):
        """
        Transform the output file into an NLTK-style Valuation. 
        
        @return: A model if one is generated; None otherwise.
        @rtype: L{nltk.sem.Valuation} 
        """
        valuation = None
        if self.build_model():
            valuation_standard_format = self._transform_output('standard')
            
            d = {}
            for line in valuation_standard_format.splitlines(False):
                l = line.strip()
                # find the number of entities in the model
                if l.startswith('interpretation'):
                    num_entities = int(l[l.index('(')+1:l.index(',')].strip())
                # replace the integer identifier with a corresponding alphabetic character
                elif l.startswith('function') and l.find('_') == -1:
                    name = l[l.index('(')+1:l.index(',')].strip()
                    if is_indvar(name):
                        name = name.upper()
                    d[name] = MaceCommand._make_model_var(int(l[l.index('[')+1:l.index(']')].strip()))
                
                elif l.startswith('relation'):
                    name = l[l.index('(')+1:l.index('(', l.index('(')+1)].strip()
                    values = [int(v.strip()) for v in l[l.index('[')+1:l.index(']')].split(',')]
                    d[name] = MaceCommand._make_relation_set(num_entities, values)

            valuation = Valuation(d.items())
        return valuation
        
    @staticmethod
    def _make_relation_set(num_entities, values):
        """
        Convert a Mace4-style relation table into a dictionary.<commit_msg>cleaned up convert2val<commit_after># Natural Language Toolkit: Interface to the Mace4 Model Builder 
#
# Author: <NAME> <<EMAIL>>
#         <NAME> <<EMAIL>>

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

import os
import tempfile
from string import join
from nltk.sem.logic import *
from nltk.sem import Valuation
from api import ModelBuilder, BaseModelBuilderCommand
import prover9
from prover9 import Prover9Parent, Prover9CommandParent, \
                    call_mace4, call_interpformat

"""
A model builder that makes use of the external 'Mace4' package.
"""

class MaceCommand(Prover9CommandParent, BaseModelBuilderCommand):
    """
    A L{MaceCommand} specific to the L{Mace} model builder.  It contains
    the a print_assumptions() method that is used to print the list
    of assumptions in multiple formats.
    """
    def __init__(self, goal=None, assumptions=None, timeout=60):
        """
        @param goal: Input expression to prove
        @type goal: L{logic.Expression}
        @param assumptions: Input expressions to use as assumptions in
            the proof.
        @type assumptions: C{list} of L{logic.Expression}
        @param timeout: number of seconds before timeout; set to 0 for
            no timeout.
        @type timeout: C{int}
        """
        BaseModelBuilderCommand.__init__(self, Mace(timeout), goal, assumptions)
        
    def convert2val(self):
        """
        Transform the output file into an NLTK-style Valuation. 
        
        @return: A model if one is generated; None otherwise.
        @rtype: L{nltk.sem.Valuation} 
        """
        if self.build_model():
            valuation_standard_format = self._transform_output('standard')
            
            val = []
            for line in valuation_standard_format.splitlines(False):
                l = line.strip()
                # find the number of entities in the model
                if l.startswith('interpretation'):
                    num_entities = int(l[l.index('(')+1:l.index(',')].strip())
                # replace the integer identifier with a corresponding alphabetic character
                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'):
                    name = l[l.index('(')+1:l.index('(', l.index('(')+1)].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)))

            return Valuation(val)
        else:
            return None
        
    @staticmethod
    def _make_relation_set(num_entities, values):
        """
        Convert a Mace4-style relation table into a dictionary.
{'fraction_non_alphanumeric': 0.11327868852459017, 'fraction_numerical': 0.006721311475409836, 'mean_word_length': 2.2110526315789474, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 17, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3062792', 'n_tokens_mistral': 1735, 'n_tokens_neox': 1686, 'n_words': 480}