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"""This module defines all the operators used internally by pySMT. 19 20Note that other expressions can be built in the FormulaManager, but 21they will be rewritten (during construction) in order to only use 22these operators. 23""" 24from itertools import chain 25from six.moves import xrange 26 27 28ALL_TYPES = list(xrange(0,66)) 29 30( 31FORALL, EXISTS, AND, OR, NOT, IMPLIES, IFF, # Boolean Logic (0-6) 32SYMBOL, FUNCTION, # Symbols and functions calls (7-8) 33REAL_CONSTANT, BOOL_CONSTANT, INT_CONSTANT, STR_CONSTANT, # Constants (9-12) 34PLUS, MINUS, TIMES, # LIA/LRA operators (13-15) 35LE, LT, EQUALS, # LIA/LRA relations (16-18) 36ITE, # Term-ite (19) 37TOREAL, # LIRA toreal() function (20) 38# 39# MG: FLOOR? INT_MOD_CONGR? 40# 41# BV 42BV_CONSTANT, # Bit-Vector constant (21) 43BV_NOT, BV_AND, BV_OR, BV_XOR, # Logical Operators on Bit (22-25) 44BV_CONCAT, # BV Concatenation (26) 45BV_EXTRACT, # BV sub-vector extraction (27) 46BV_ULT, BV_ULE, # Unsigned Comparison (28-29) 47BV_NEG, BV_ADD, BV_SUB, # Basic arithmetic (30-32) 48BV_MUL, BV_UDIV, BV_UREM, # Division/Multiplication (33-35) 49BV_LSHL, BV_LSHR, # Shifts (36-37) 50BV_ROL, BV_ROR, # Rotation (38-39) 51BV_ZEXT, BV_SEXT, # Extension (40-41) 52BV_SLT, BV_SLE, # Signed Comparison (42-43) 53BV_COMP, # Returns 1_1 if the arguments are 54 # equal otherwise it returns 0_1 (44) 55BV_SDIV, BV_SREM, # Signed Division and Reminder(45-46) 56BV_ASHR, # Arithmetic shift right (47) 57# 58# STRINGS 59# 60STR_LENGTH, # Length (48) 61STR_CONCAT, # Concat (49) 62STR_CONTAINS, # Contains (50) 63STR_INDEXOF, # IndexOf (51) 64STR_REPLACE, # Replace (52) 65STR_SUBSTR, # Sub String (53) 66STR_PREFIXOF, # Prefix (54) 67STR_SUFFIXOF, # Suffix (55) 68STR_TO_INT, # atoi (56) 69INT_TO_STR, # itoa (57) 70STR_CHARAT, # Char at an index (58) 71# 72# ARRAYS 73# 74ARRAY_SELECT, # Array Select (59) 75ARRAY_STORE, # Array Store (60) 76ARRAY_VALUE, # Array Value (61) 77 78DIV, # Arithmetic Division (62) 79POW, # Arithmetic Power (63) 80ALGEBRAIC_CONSTANT, # Algebraic Number (64) 81BV_TONATURAL, # BV to Natural Conversion (65) 82) = ALL_TYPES 83 84QUANTIFIERS = frozenset([FORALL, EXISTS]) 85 86BOOL_CONNECTIVES = frozenset([AND, OR, NOT, IMPLIES, IFF]) 87 88BOOL_OPERATORS = frozenset(QUANTIFIERS | BOOL_CONNECTIVES) 89 90CONSTANTS = frozenset([BOOL_CONSTANT, REAL_CONSTANT, INT_CONSTANT, 91 BV_CONSTANT, STR_CONSTANT, ALGEBRAIC_CONSTANT]) 92 93# Relations are predicates on theory atoms. 94# Relations have boolean type. They are a subset of the operators for a theory 95BV_RELATIONS = frozenset([BV_ULE, BV_ULT, BV_SLT, BV_SLE]) 96 97IRA_RELATIONS = frozenset([LE, LT]) 98 99STR_RELATIONS = frozenset([STR_CONTAINS, STR_PREFIXOF, STR_SUFFIXOF]) 100 101RELATIONS = frozenset((EQUALS,)) | BV_RELATIONS | IRA_RELATIONS | STR_RELATIONS 102 103# Operators are functions that return a Theory object 104BV_OPERATORS = frozenset([BV_NOT, BV_AND, BV_OR, BV_XOR, 105 BV_CONCAT, BV_EXTRACT, BV_NEG, BV_ADD, 106 BV_SUB, BV_MUL, BV_UDIV, BV_UREM, BV_LSHL, BV_LSHR, 107 BV_ROL, BV_ROR, BV_ZEXT, BV_SEXT, 108 BV_COMP, BV_SDIV, BV_SREM, BV_ASHR]) 109 110STR_OPERATORS = frozenset([STR_LENGTH, STR_CONCAT, STR_INDEXOF, STR_REPLACE, 111 STR_SUBSTR, STR_CHARAT, STR_TO_INT, INT_TO_STR,]) 112 113IRA_OPERATORS = frozenset([PLUS, MINUS, TIMES, TOREAL, DIV, POW, BV_TONATURAL]) 114 115ARRAY_OPERATORS = frozenset([ARRAY_SELECT, ARRAY_STORE, ARRAY_VALUE]) 116 117THEORY_OPERATORS = IRA_OPERATORS | BV_OPERATORS | ARRAY_OPERATORS | STR_OPERATORS 118 119CUSTOM_NODE_TYPES = [] 120 121assert (BOOL_OPERATORS | THEORY_OPERATORS | RELATIONS | \ 122 CONSTANTS | frozenset((SYMBOL, FUNCTION, ITE))) == frozenset(ALL_TYPES) 123 124assert len(BOOL_OPERATORS & THEORY_OPERATORS) == 0 125assert len(BOOL_OPERATORS & RELATIONS) == 0 126assert len(BOOL_OPERATORS & CONSTANTS) == 0 127assert len(THEORY_OPERATORS & RELATIONS) == 0 128assert len(THEORY_OPERATORS & CONSTANTS) == 0 129assert len(RELATIONS & CONSTANTS) == 0 130 131 132def new_node_type(node_id=None, node_str=None): 133 """Adds a new node type to the list of custom node types and returns the ID.""" 134 if node_id is None: 135 if len(CUSTOM_NODE_TYPES) == 0: 136 node_id = ALL_TYPES[-1] + 1 137 else: 138 node_id = CUSTOM_NODE_TYPES[-1] + 1 139 140 assert node_id not in ALL_TYPES 141 assert node_id not in CUSTOM_NODE_TYPES 142 CUSTOM_NODE_TYPES.append(node_id) 143 if node_str is None: 144 node_str = "Node_%d" % node_id 145 __OP_STR__[node_id] = node_str 146 return node_id 147 148 149def op_to_str(node_id): 150 """Returns a string representation of the given node.""" 151 return __OP_STR__[node_id] 152 153 154def all_types(): 155 """Returns an iterator over all base and custom types.""" 156 return chain(iter(ALL_TYPES), iter(CUSTOM_NODE_TYPES)) 157 158 159__OP_STR__ = { 160 FORALL : "FORALL", 161 EXISTS : "EXISTS", 162 AND : "AND", 163 OR : "OR", 164 NOT : "NOT", 165 IMPLIES : "IMPLIES", 166 IFF : "IFF", 167 SYMBOL : "SYMBOL", 168 FUNCTION : "FUNCTION", 169 REAL_CONSTANT : "REAL_CONSTANT", 170 BOOL_CONSTANT : "BOOL_CONSTANT", 171 INT_CONSTANT : "INT_CONSTANT", 172 STR_CONSTANT : "STR_CONSTANT", 173 PLUS : "PLUS", 174 MINUS : "MINUS", 175 TIMES : "TIMES", 176 LE : "LE", 177 LT : "LT", 178 EQUALS : "EQUALS", 179 ITE : "ITE", 180 TOREAL : "TOREAL", 181 BV_CONSTANT : "BV_CONSTANT", 182 BV_NOT : "BV_NOT", 183 BV_AND : "BV_AND", 184 BV_OR : "BV_OR", 185 BV_XOR : "BV_XOR", 186 BV_CONCAT : "BV_CONCAT", 187 BV_EXTRACT : "BV_EXTRACT", 188 BV_ULT : "BV_ULT", 189 BV_ULE : "BV_ULE", 190 BV_NEG : "BV_NEG", 191 BV_ADD : "BV_ADD", 192 BV_SUB : "BV_SUB", 193 BV_MUL : "BV_MUL", 194 BV_UDIV : "BV_UDIV", 195 BV_UREM : "BV_UREM", 196 BV_LSHL : "BV_LSHL", 197 BV_LSHR : "BV_LSHR", 198 BV_ROL : "BV_ROL", 199 BV_ROR : "BV_ROR", 200 BV_ZEXT : "BV_ZEXT", 201 BV_SEXT : "BV_SEXT", 202 BV_SLT : "BV_SLT", 203 BV_SLE : "BV_SLE", 204 BV_COMP : "BV_COMP", 205 BV_SDIV : "BV_SDIV", 206 BV_SREM : "BV_SREM", 207 BV_ASHR : "BV_ASHR", 208 STR_LENGTH: "STR_LENGTH", 209 STR_CONCAT: "STR_CONCAT", 210 STR_CONTAINS: "STR_CONTAINS", 211 STR_INDEXOF: "STR_INDEXOF", 212 STR_REPLACE:"STR_REPLACE", 213 STR_SUBSTR: "STR_SUBSTR", 214 STR_PREFIXOF: "STR_PREFIXOF", 215 STR_SUFFIXOF: "STR_SUFFIXOF", 216 STR_TO_INT: "STR_TO_INT", 217 INT_TO_STR: "INT_TO_STR", 218 STR_CHARAT: "STR_CHARAT", 219 BV_TONATURAL : "BV_TONATURAL", 220 ARRAY_SELECT : "ARRAY_SELECT", 221 ARRAY_STORE : "ARRAY_STORE", 222 ARRAY_VALUE : "ARRAY_VALUE", 223 DIV: "DIV", 224 POW: "POW", 225 ALGEBRAIC_CONSTANT: "ALGEBRAIC_CONSTANT", 226} 227