Alt-Ergo Documentation

Contents

  • Install
  • Usage
  • Input file formats
    • Alt-Ergo's native language
      • Summary
      • Declaration of symbols
      • Types
      • Declaration of axioms
      • Setting goals
      • Theories
      • Control Flow
      • Syntax of declarations and expressions
    • SMT-LIB 2
  • API documentation
  • Plugins
  • Developer's documentation
  • About
Alt-Ergo Documentation
  • Input file formats
  • Alt-Ergo’s native language

Alt-Ergo’s native language

This page documents Alt-Ergo’s native input language and its syntax.

In order to state a problem, the user may enrich the signature of the theory by adding new symbols and types, using keywords such as logic and type. Axioms can be declared through the axiom construct, and goals are set with goal. Additional constructs allow to define theories or to use if-then-else, let-bindings or pattern-matching. A full description of the syntax is available in the last chapter.

  • Summary
    • Keywords
  • Declaration of symbols
    • logic: uninterpreted symbols
    • ac modifier: associative and commutative symbols
    • function: user-defined functions
    • predicate: propositional valued functions
  • Types
    • Built-in types
    • Built-in operators
    • User-defined
  • Declaration of axioms
    • axiom
    • Triggers
    • rewriting
  • Setting goals
    • goal
    • Intermediate goals: cut and check
    • check_sat
  • Theories
    • Native theories
    • Floating-point Arithmetic
    • User-defined extensions of theories
  • Control Flow
    • let [...] in
    • match [...] with
    • if [...] then [...] else
  • Syntax of declarations and expressions
Previous Next

© Copyright 2020 - 2023, Alt-Ergo developers.

Built with Sphinx using a theme provided by Read the Docs.