Index

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

M

main(String...) - Static method in class APIExample

main(String[]) - Static method in class org.smtlib.Driver

The main entry point to the application

main(String[]) - Static method in class org.smtlib.SMT

The main method of the SMT application

match(IExpr, List<IExpr.IMatchCase>) - Method in interface org.smtlib.IExpr.IFactory

Creates a match expression.

match(IExpr, List<IExpr.IMatchCase>) - Method in class org.smtlib.impl.Factory

Match(IExpr, List<IExpr.IMatchCase>) - Constructor for class org.smtlib.impl.SMTExpr.Match

Creates a match expression from the given scrutinee and list of cases.

MATCH - Static variable in class org.smtlib.sexpr.Utils

Concrete syntax for the match token

matchCase(IExpr.IPattern, IExpr) - Method in interface org.smtlib.IExpr.IFactory

Creates a single match case.

matchCase(IExpr.IPattern, IExpr) - Method in class org.smtlib.impl.Factory

MatchCase(IExpr.IPattern, IExpr) - Constructor for class org.smtlib.impl.SMTExpr.MatchCase

Creates a match case from the given pattern and body expression.

matcher - Variable in class org.smtlib.sexpr.Lexer

The Matcher used to do lexical scanning

memout() - Method in class org.smtlib.impl.Response.Factory

memout() - Method in interface org.smtlib.IResponse.IFactory

MEMOUT - Static variable in class org.smtlib.impl.Response

MEMOUT - Static variable in class org.smtlib.Utils

A REASON_UNKNOWN return value

merge() - Method in class org.smtlib.SymbolTable

Combines the top two symbol scopes, removing the current top scope; presumes that there is no shadowing of symbols; the top sort scope is discarded.

message - Variable in class org.smtlib.impl.SMTExpr.Error

MINUS - Static variable in class org.smtlib.Utils

MOD - Static variable in class org.smtlib.Utils

modelResponse(IResponse) - Method in class org.smtlib.AbstractSolver

The get-model response r, without the leading symbol model if it has one: z3 4.3 to 4.7 and yices2 2.6.5 (with --smt2-model-format) answer (model (define-fun ...) ...), where SMT-LIB has the plain list ((define-fun ...) ...).

MULT - Static variable in class org.smtlib.Utils

A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form