Alt-Ergo Documentation

Contents

  • Install
  • Usage
  • SMT-LIB language
  • Alt-Ergo's native language
    • Summary
    • Declaration of symbols
    • Types
    • Declaration of axioms
    • Setting goals
    • Theories
    • Control Flow
    • Syntax of declarations and expressions
  • Model generation
  • Optimization
  • API documentation
  • Plugins
  • Developer's documentation
  • About
Alt-Ergo Documentation
  • 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.