Il s'agit de la commande cvc3 qui peut être exécutée dans le fournisseur d'hébergement gratuit OnWorks en utilisant l'un de nos multiples postes de travail en ligne gratuits tels que Ubuntu Online, Fedora Online, l'émulateur en ligne Windows ou l'émulateur en ligne MAC OS
PROGRAMME:
Nom
cvc3 - prouveur de théorème SMT automatique
SYNOPSIS
cvc3 [option] ... [nom de fichier]
DESCRIPTION
CVC3 est un vérificateur de validité automatisé pour une logique du premier ordre à plusieurs tris (typés) avec
théories intégrées, y compris une prise en charge des quantificateurs, des fonctions partielles et
sous-types de prédicats. Les théories intégrées actuelles sont les théories de
· égalité sur les symboles de fonction et de prédicat libres (aka non interprétés),
· arithmétique linéaire réelle et entière (avec un certain support pour l'arithmétique non linéaire),
· vecteurs de bits,
· des tableaux,
· des tuples,
· enregistrements,
· types de données inductifs définis par l'utilisateur.
CVC3 fonctionne sur des fichiers dans le CVC Présentation Entrée Langue ou l' SMTLIB contribution
Langue. Si aucun fichier d'entrée n'est fourni sur la ligne de commande, CVC3 lit l'entrée standard.
OPTIONS
Seules quelques-unes des options les plus fréquemment utilisées sont présentées ci-dessous. Pour plus de détails, voir
L'aide intégrée de CVC3 (cvc3 -Aide) ou le site CVC3.
-aider]
Répertoriez toutes les options de contrôle de CVC3. Les options booléennes sont marquées (B). Ces palmes
sont activés en préfixant avec + et désactivé en préfixant avec -. A l'aide
sortie, le actuel le réglage est donné. Par exemple, les listes de sortie
(b) -mode interactif interactif
Indique que le mode interactif est désactivé. pour activer le mode interactif, le
option +interactif est donc utilisé. D'autres options sont marquées (S) pour chaîne
arguments, ou (I) pour les arguments entiers.
-version
Imprimez la version de CVC3 et quittez.
-long (présentation|smtlib|interne) Sélectionnez la langue de saisie utilisée. La valeur par défaut est
présentation.
+int[eractif]
Activer le mode interactif. Les commandes sont lues à partir de l'entrée standard et traitées
immédiatement.
+statistiques Imprimer les statistiques d'exécution.
-temps libre t
Terminer automatiquement CVC3 après t secondes.
Utilisez cvc3 en ligne en utilisant les services onworks.net
