1#
2# This file is part of pySMT.
3#
4#   Copyright 2014 Andrea Micheli and Marco Gario
5#
6#   Licensed under the Apache License, Version 2.0 (the "License");
7#   you may not use this file except in compliance with the License.
8#   You may obtain a copy of the License at
9#
10#       http://www.apache.org/licenses/LICENSE-2.0
11#
12#   Unless required by applicable law or agreed to in writing, software
13#   distributed under the License is distributed on an "AS IS" BASIS,
14#   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15#   See the License for the specific language governing permissions and
16#   limitations under the License.
17#
18"""Defines constants for the commands of the SMT-LIB"""
19
20ASSERT='assert'
21CHECK_SAT='check-sat'
22CHECK_SAT_ASSUMING='check-sat-assuming'
23DECLARE_CONST='declare-const'
24DECLARE_FUN='declare-fun'
25DECLARE_SORT='declare-sort'
26DEFINE_FUN='define-fun'
27DEFINE_FUN_REC='define-fun-rec'
28DEFINE_FUNS_REC='define-funs-rec'
29DEFINE_SORT='define-sort'
30ECHO='echo'
31EXIT='exit'
32GET_ASSERTIONS='get-assertions'
33GET_ASSIGNMENT='get-assignment'
34GET_INFO='get-info'
35GET_MODEL='get-model'
36GET_OPTION='get-option'
37GET_PROOF='get-proof'
38GET_UNSAT_ASSUMPTIONS='get-unsat-assumptions'
39GET_UNSAT_CORE='get-unsat-core'
40GET_VALUE='get-value'
41POP='pop'
42PUSH='push'
43RESET='reset'
44RESET_ASSERTIONS='reset-assertions'
45SET_INFO='set-info'
46SET_LOGIC='set-logic'
47SET_OPTION='set-option'
48
49#
50
51SMT_LIB_2_0 = [
52    SET_LOGIC,
53    SET_OPTION,
54    SET_INFO,
55    DECLARE_SORT,
56    DEFINE_SORT,
57    DECLARE_FUN,
58    DEFINE_FUN,
59    PUSH,
60    POP,
61    ASSERT,
62    CHECK_SAT,
63    GET_ASSERTIONS,
64    GET_VALUE,
65    GET_MODEL,
66    GET_PROOF,
67    GET_UNSAT_CORE,
68    GET_INFO,
69    GET_OPTION,
70    EXIT,
71]
72
73SMT_LIB_2_5 = SMT_LIB_2_0 + [
74    CHECK_SAT_ASSUMING,
75    DECLARE_CONST,
76    DEFINE_FUN_REC,
77    DEFINE_FUNS_REC,
78    ECHO,
79    GET_ASSIGNMENT,
80    GET_UNSAT_ASSUMPTIONS,
81    RESET,
82    RESET_ASSERTIONS,
83]
84
85ALL_COMMANDS = SMT_LIB_2_5
86