mace4 - En ligne dans le cloud

PROGRAMME:

Nom

mace4 - recherche des contre-modèles finis d'instructions du premier ordre

SYNOPSIS

mace4 [Options] fichier-entrée > fichier de sortie

DESCRIPTION

Cette page de manuel documente brièvement les mace4 commander.

Le programme mace4 recherche de structures finies satisfaisant au premier ordre et équationnelles
déclarations, le même genre de déclaration que prouve9(1) accepte. Si la déclaration est la
déni de certaines conjectures, toutes les structures trouvées par mace4 sont des contre-exemples aux
conjecture. mace4 peut être un complément précieux à prouve9(1), à la recherche de contre-exemples
avant (ou en même temps que) l'utilisation prouve9(1) pour rechercher une preuve. Il peut aussi être
utilisé pour aider à déboguer les clauses d'entrée et les formules pour prouve9 (1).

OPTIONS

Un résumé des options est inclus ci-dessous. Les options remplacent les paramètres équivalents donnés dans
le fichier d'entrée. Pour définir ou effacer un indicateur, vous devez donner 1 ou 0 comme valeur.

-Aide Cela raconte mace4 pour imprimer un résumé de ces options de ligne de commande.

-n n Cela donne la taille de domaine de départ pour la recherche. La valeur par défaut est 2. Si vous
donner aussi un -N option, mace4 itérera les tailles de domaine jusqu'à -N valeur,
en utilisant un incrément donné par le -I valeur. Autrement, mace4 recherchera uniquement le
-n valeur.

-N n Cela donne la taille du domaine de fin pour la recherche. La valeur par défaut est 10.

-i n Cela donne l'incrément de taille de domaine pour la recherche. La valeur par défaut est 1.

-q n Cet indicateur remplace le paramètre itérer. Il dit d'essayer les tailles qui sont de premier ordre
nombres, de -n à travers -N.

-m n Arrêtez de chercher lorsque le nLa structure a été trouvée. La valeur par défaut est 1.

-t n Arrêter de chercher après n secondes.

-s n Autoriser au maximum n secondes pour chaque taille de domaine. Le paramètre peut être utilisé (ensemble
avec -t) pour donner un délai global.

-b n Arrêter la recherche quand (environ) n mégaoctets de mémoire ont été utilisés.

-V n Une règle est nécessaire pour distinguer les variables des constantes dans les clauses et
formules à variables libres. Si ce drapeau est clair, les variables commencent par (inférieur
cas) « u » à « z ». Si cet indicateur est défini, les variables dans les clauses commencent par (supérieur
cas) "A" à "Z" ou "_".

-P n Si ce drapeau est activé, toutes les structures trouvées sont imprimées sous une forme « standard »,
ce qui signifie qu'ils conviennent comme entrée à d'autres programmes LADR tels que isofiltre(1)
et format d'interprétation (1).

-p n Si ce drapeau est défini, et si -P est clair, toutes les structures trouvées sont imprimées
sous forme de tableau.

-R n Si ce drapeau est défini, une structure en anneau est appliquée à la recherche. Les opérations
{+,-,*} sont supposés être l'anneau d'entiers (mod domain_size). Cette méthode met
une contrainte forte sur la recherche, permettant d'avoir des structures beaucoup plus grandes
enquêté.

-v n Si cet indicateur est défini, le fichier de sortie reçoit des informations sur la recherche,
y compris le modèle partiel initial (la partie du modèle qui peut être déterminée
avant le début du retour en arrière) et la synchronisation et d'autres statistiques pour chaque taille de domaine.
(Il ne donne pas de trace du backtracking, donc il ne consomme pas beaucoup de fichier
espacer.)

-T n Si l'indicateur de trace est défini, des informations détaillées sur la recherche, y compris une trace
de toutes les affectations et retours en arrière, est imprimé sur la sortie standard. Ce drapeau
provoque beaucoup de sorties, il ne doit donc être utilisé que sur de petites recherches.

Il existe également un certain nombre d'options avancées, qui sont utilisées pour l'expérimentation avec
méthodes de recherche. Ils peuvent être ignorés par presque tous les utilisateurs. Pour les descriptions de ces
options, voir l'original mace4 manuel.

Utilisez mace4 en ligne en utilisant les services onworks.net