1# 2# This file is part of pySMT. 3# 4# Copyright 2015 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 provides classes used to analyze and determine 19properties of formulae. 20 21 * SizeOracle provides metrics about the formula 22 * QuantifierOracle says whether a formula is quantifier free 23 * TheoryOracle says which logic is used in the formula. 24 * FreeVarsOracle provides variables that are free in the formula 25 * AtomsOracle provides the set of boolean atoms in the formula 26 * TypesOracle provides the list of types in the formula 27""" 28 29import pysmt 30import pysmt.walkers as walkers 31import pysmt.operators as op 32 33from pysmt import typing 34 35from pysmt.logics import Logic, Theory, get_closer_pysmt_logic 36 37 38class SizeOracle(walkers.DagWalker): 39 """Evaluates the size of a formula""" 40 41 # Counting type can be: 42 # - TREE_NODES : counts the number of nodes in the formula seen as a tree 43 # - DAG_NODES : counts the number of nodes in the formula seen as a DAG 44 # - LEAVES : counts the number of leaves in the formula seen as a tree 45 # - DEPTH : counts the maximum number of levels in the formula 46 # - SYMBOLS : counts the number of different symbols occurring in the formula 47 # - BOOL_DAG : counts the dag size by considering theory atoms as leaf 48 (MEASURE_TREE_NODES, 49 MEASURE_DAG_NODES, 50 MEASURE_LEAVES, 51 MEASURE_DEPTH, 52 MEASURE_SYMBOLS, 53 MEASURE_BOOL_DAG) = range(6) 54 55 def __init__(self, env=None): 56 walkers.DagWalker.__init__(self, env=env) 57 58 self.measure_to_fun = \ 59 {SizeOracle.MEASURE_TREE_NODES: self.walk_count_tree, 60 SizeOracle.MEASURE_DAG_NODES: self.walk_count_dag, 61 SizeOracle.MEASURE_LEAVES: self.walk_count_leaves, 62 SizeOracle.MEASURE_DEPTH: self.walk_count_depth, 63 SizeOracle.MEASURE_SYMBOLS: self.walk_count_symbols, 64 SizeOracle.MEASURE_BOOL_DAG: self.walk_count_bool_dag, 65 } 66 67 68 def set_walking_measure(self, measure): 69 if measure not in self.measure_to_fun: 70 raise NotImplementedError 71 self.set_function(self.measure_to_fun[measure], *op.ALL_TYPES) 72 73 def _get_key(self, formula, measure, **kwargs): 74 """Memoize using a tuple (measure, formula).""" 75 return (measure, formula) 76 77 def get_size(self, formula, measure=None): 78 """Return the size of the formula according to the specified measure. 79 80 The default measure is MEASURE_TREE_NODES. 81 """ 82 if measure is None: 83 # By default, count tree nodes 84 measure = SizeOracle.MEASURE_TREE_NODES 85 86 self.set_walking_measure(measure) 87 res = self.walk(formula, measure=measure) 88 89 if measure == SizeOracle.MEASURE_DAG_NODES or \ 90 measure == SizeOracle.MEASURE_SYMBOLS or \ 91 measure == SizeOracle.MEASURE_BOOL_DAG : 92 return len(res) 93 return res 94 95 def walk_count_tree(self, formula, args, **kwargs): 96 #pylint: disable=unused-argument 97 return 1 + sum(args) 98 99 def walk_count_dag(self, formula, args, measure, **kwargs): 100 #pylint: disable=unused-argument 101 return frozenset([formula]) | frozenset([x for s in args for x in s]) 102 103 def walk_count_leaves(self, formula, args, measure, **kwargs): 104 #pylint: disable=unused-argument 105 is_leaf = (len(args) == 0) 106 return (1 if is_leaf else 0) + sum(args) 107 108 def walk_count_depth(self, formula, args, measure, **kwargs): 109 #pylint: disable=unused-argument 110 is_leaf = (len(args) == 0) 111 return 1 + (0 if is_leaf else max(args)) 112 113 def walk_count_symbols(self, formula, args, measure, **kwargs): 114 #pylint: disable=unused-argument 115 is_sym = formula.is_symbol() 116 a_res = frozenset([x for s in args for x in s]) 117 if is_sym: 118 return frozenset([formula]) | a_res 119 return a_res 120 121 def walk_count_bool_dag(self, formula, args, measure, **kwargs): 122 #pylint: disable=unused-argument 123 if formula.is_theory_relation(): 124 return frozenset([formula]) 125 return frozenset([formula]) | frozenset([x for s in args for x in s]) 126 127 128class QuantifierOracle(walkers.DagWalker): 129 def is_qf(self, formula): 130 """ Returns whether formula is Quantifier Free. """ 131 return self.walk(formula) 132 133 # Propagate truth value, but force False if a Quantifier is found. 134 @walkers.handles(set(op.ALL_TYPES) - op.QUANTIFIERS) 135 def walk_all(self, formula, args, **kwargs): 136 return walkers.DagWalker.walk_all(self, formula, args, **kwargs) 137 138 @walkers.handles(op.QUANTIFIERS) 139 def walk_false(self, formula, args, **kwargs): 140 return walkers.DagWalker.walk_false(self, formula, args, **kwargs) 141 142# EOC QuantifierOracle 143 144 145class TheoryOracle(walkers.DagWalker): 146 147 def get_theory(self, formula): 148 """Returns the thoery for the formula.""" 149 return self.walk(formula) 150 151 def _theory_from_type(self, ty): 152 theory = Theory() 153 if ty.is_real_type(): 154 theory.real_arithmetic = True 155 theory.real_difference = True 156 elif ty.is_int_type(): 157 theory.integer_arithmetic = True 158 theory.integer_difference = True 159 elif ty.is_bool_type(): 160 pass 161 elif ty.is_bv_type(): 162 theory.bit_vectors = True 163 elif ty.is_array_type(): 164 theory.arrays = True 165 theory = theory.combine(self._theory_from_type(ty.index_type)) 166 theory = theory.combine(self._theory_from_type(ty.elem_type)) 167 elif ty.is_string_type(): 168 theory.strings = True 169 elif ty.is_custom_type(): 170 theory.custom_type = True 171 else: 172 # ty is either a function type 173 theory.uninterpreted = True 174 return theory 175 176 @walkers.handles(op.RELATIONS) 177 @walkers.handles(op.BOOL_OPERATORS) 178 @walkers.handles(op.BV_OPERATORS) 179 @walkers.handles(op.STR_OPERATORS -\ 180 set([op.STR_LENGTH, op.STR_INDEXOF, op.STR_TO_INT])) 181 @walkers.handles(op.ITE, op.ARRAY_SELECT, op.ARRAY_STORE, op.MINUS) 182 def walk_combine(self, formula, args, **kwargs): 183 """Combines the current theory value of the children""" 184 #pylint: disable=unused-argument 185 if len(args) == 1: 186 return args[0].copy() 187 theory_out = args[0] 188 for t in args[1:]: 189 theory_out = theory_out.combine(t) 190 return theory_out 191 192 @walkers.handles(op.REAL_CONSTANT, op.BOOL_CONSTANT) 193 @walkers.handles(op.INT_CONSTANT, op.BV_CONSTANT) 194 @walkers.handles(op.STR_CONSTANT) 195 def walk_constant(self, formula, args, **kwargs): 196 """Returns a new theory object with the type of the constant.""" 197 #pylint: disable=unused-argument 198 theory_out = Theory() 199 if formula.is_real_constant(): 200 theory_out.real_arithmetic = True 201 theory_out.real_difference = True 202 elif formula.is_int_constant(): 203 theory_out.integer_arithmetic = True 204 theory_out.integer_difference = True 205 elif formula.is_bv_constant(): 206 theory_out.bit_vectors = True 207 elif formula.is_string_constant(): 208 theory_out.strings = True 209 else: 210 assert formula.is_bool_constant() 211 return theory_out 212 213 def walk_symbol(self, formula, args, **kwargs): 214 """Returns a new theory object with the type of the symbol.""" 215 #pylint: disable=unused-argument 216 f_type = formula.symbol_type() 217 theory_out = self._theory_from_type(f_type) 218 return theory_out 219 220 def walk_function(self, formula, args, **kwargs): 221 """Extends the Theory with UF.""" 222 #pylint: disable=unused-argument 223 if len(args) == 1: 224 theory_out = args[0].copy() 225 elif len(args) > 1: 226 theory_out = args[0] 227 for t in args[1:]: 228 theory_out = theory_out.combine(t) 229 else: 230 theory_out = Theory() 231 # Extend Theory with function return type 232 rtype = formula.function_name().symbol_type().return_type 233 theory_out = theory_out.combine(self._theory_from_type(rtype)) 234 theory_out.uninterpreted = True 235 return theory_out 236 237 def walk_toreal(self, formula, args, **kwargs): 238 #pylint: disable=unused-argument 239 """Extends the Theory with LIRA.""" 240 theory_out = args[0].set_lira() # This makes a copy of args[0] 241 return theory_out 242 rtype = formula.symbol_name() 243 244 @walkers.handles([op.STR_LENGTH, op.STR_INDEXOF, op.STR_TO_INT]) 245 def walk_str_int(self, formula, args, **kwargs): 246 theory_out = self.walk_combine(formula, args, **kwargs) 247 theory_out.integer_arithmetic = True 248 theory_out.integer_difference = True 249 return theory_out 250 251 def walk_bv_tonatural(self, formula, args, **kwargs): 252 #pylint: disable=unused-argument 253 """Extends the Theory with Integer.""" 254 theory_out = args[0].copy() 255 theory_out.integer_arithmetic = True 256 theory_out.integer_difference = True 257 return theory_out 258 259 def walk_times(self, formula, args, **kwargs): 260 """Extends the Theory with Non-Linear, if needed.""" 261 theory_out = args[0] 262 for t in args[1:]: 263 theory_out = theory_out.combine(t) 264 # Check for non-linear counting the arguments having at least 265 # one free variable 266 if sum(1 for x in formula.args() if x.get_free_variables()) > 1: 267 theory_out = theory_out.set_linear(False) 268 # This is not in DL anymore 269 theory_out = theory_out.set_difference_logic(False) 270 return theory_out 271 272 def walk_pow(self, formula, args, **kwargs): 273 return args[0].set_linear(False) 274 275 def walk_plus(self, formula, args, **kwargs): 276 theory_out = args[0] 277 for t in args[1:]: 278 theory_out = theory_out.combine(t) 279 theory_out = theory_out.set_difference_logic(value=False) 280 assert not theory_out.real_difference 281 assert not theory_out.integer_difference 282 return theory_out 283 284 def walk_strings(self, formula, args, **kwargs): 285 """Extends the Theory with Strings.""" 286 #pylint: disable=unused-argument 287 if formula.is_string_constant(): 288 theory_out = Theory(strings=True) 289 else: 290 theory_out = args[0].set_strings() # This makes a copy of args[0] 291 return theory_out 292 293 def walk_array_value(self, formula, args, **kwargs): 294 # First, we combine all the theories of all the indexes and values 295 theory_out = self.walk_combine(formula, args) 296 297 # We combine the index-type theory 298 i_type = formula.array_value_index_type() 299 idx_theory = self._theory_from_type(i_type) 300 theory_out = theory_out.combine(idx_theory) 301 302 # Finally, we add the array theory 303 theory_out.arrays = True 304 theory_out.arrays_const = True 305 return theory_out 306 307 def walk_div(self, formula, args, **kwargs): 308 """Extends the Theory with Non-Linear, if needed.""" 309 assert len(args) == 2 310 theory_out = args[0] 311 for t in args[1:]: 312 theory_out = theory_out.combine(t) 313 # Check for non-linear 314 left, right = formula.args() 315 if len(left.get_free_variables()) != 0 and \ 316 len(right.get_free_variables()) != 0: 317 theory_out = theory_out.set_linear(False) 318 elif formula.arg(1).is_zero(): 319 # DivBy0 is non-linear 320 theory_out = theory_out.set_linear(False) 321 else: 322 theory_out = theory_out.combine(args[1]) 323 return theory_out 324 325 # This is not in DL anymore 326 theory_out = theory_out.set_difference_logic(False) 327 return theory_out 328 329# EOC TheoryOracle 330 331 332# Operators for which Args is an FNode 333DEPENDENCIES_SIMPLE_ARGS = (set(op.ALL_TYPES) - \ 334 (set([op.SYMBOL, op.FUNCTION]) | op.QUANTIFIERS | op.CONSTANTS)) 335 336 337class FreeVarsOracle(walkers.DagWalker): 338 # We have only few categories for this walker. 339 # 340 # - Simple Args simply need to combine the cone/dependencies 341 # of the children. 342 # - Quantifiers need to exclude bounded variables 343 # - Constants have no impact 344 345 def get_free_variables(self, formula): 346 """Returns the set of Symbols appearing free in the formula.""" 347 return self.walk(formula) 348 349 @walkers.handles(DEPENDENCIES_SIMPLE_ARGS) 350 def walk_simple_args(self, formula, args, **kwargs): 351 #pylint: disable=unused-argument 352 res = set() 353 for arg in args: 354 res.update(arg) 355 return frozenset(res) 356 357 @walkers.handles(op.QUANTIFIERS) 358 def walk_quantifier(self, formula, args, **kwargs): 359 #pylint: disable=unused-argument 360 return args[0].difference(formula.quantifier_vars()) 361 362 def walk_symbol(self, formula, args, **kwargs): 363 #pylint: disable=unused-argument 364 return frozenset([formula]) 365 366 @walkers.handles(op.CONSTANTS) 367 def walk_constant(self, formula, args, **kwargs): 368 #pylint: disable=unused-argument 369 return frozenset() 370 371 def walk_function(self, formula, args, **kwargs): 372 res = set([formula.function_name()]) 373 for arg in args: 374 res.update(arg) 375 return frozenset(res) 376 377# EOC FreeVarsOracle 378 379 380class AtomsOracle(walkers.DagWalker): 381 """This class returns the set of Boolean atoms involved in a formula 382 A boolean atom is either a boolean variable or a theory atom 383 """ 384 # We have the following categories for this walker. 385 # 386 # - Boolean operators, e.g. and, or, not... 387 # - Theory operators, e.g. +, -, bvshift 388 # - Theory relations, e.g. ==, <= 389 # - ITE terms 390 # - Symbols 391 # - Constants 392 # 393 394 def get_atoms(self, formula): 395 """Returns the set of atoms appearing in the formula.""" 396 return self.walk(formula) 397 398 @walkers.handles(op.BOOL_CONNECTIVES) 399 @walkers.handles(op.QUANTIFIERS) 400 def walk_bool_op(self, formula, args, **kwargs): 401 #pylint: disable=unused-argument 402 return frozenset(x for a in args for x in a) 403 404 @walkers.handles(op.RELATIONS) 405 def walk_theory_relation(self, formula, **kwargs): 406 #pylint: disable=unused-argument 407 return frozenset([formula]) 408 409 @walkers.handles(op.THEORY_OPERATORS) 410 def walk_theory_op(self, formula, **kwargs): 411 #pylint: disable=unused-argument 412 return None 413 414 @walkers.handles(op.CONSTANTS) 415 def walk_constant(self, formula, **kwargs): 416 #pylint: disable=unused-argument 417 if formula.is_bool_constant(): 418 return frozenset() 419 return None 420 421 def walk_symbol(self, formula, **kwargs): 422 if formula.is_symbol(typing.BOOL): 423 return frozenset([formula]) 424 return None 425 426 def walk_function(self, formula, **kwargs): 427 if formula.function_name().symbol_type().return_type.is_bool_type(): 428 return frozenset([formula]) 429 return None 430 431 def walk_ite(self, formula, args, **kwargs): 432 #pylint: disable=unused-argument 433 if any(a is None for a in args): 434 # Theory ITE 435 return None 436 else: 437 return frozenset(x for a in args for x in a) 438 439# EOC AtomsOracle 440 441 442class TypesOracle(walkers.DagWalker): 443 444 def get_types(self, formula, custom_only=False): 445 """Returns the types appearing in the formula. 446 447 custom_only: filter the result by excluding base SMT-LIB types. 448 """ 449 types = self.walk(formula) 450 # types is a frozen set 451 # exp_types is a list 452 exp_types = self.expand_types(types) 453 assert len(types) <= len(exp_types) 454 # Base types filtering 455 if custom_only: 456 exp_types = [x for x in exp_types 457 if not x.is_bool_type() and 458 not x.is_int_type() and 459 not x.is_real_type() and 460 not x.is_bv_type() and 461 not x.is_array_type() and 462 not x.is_string_type() 463 ] 464 return exp_types 465 466 def expand_types(self, types): 467 """Recursively look into composite types. 468 469 Note: This returns a list. The list is ordered (by 470 construction) by having simpler types first) 471 """ 472 all_types = set() 473 expanded = [] 474 stack = list(types) 475 while stack: 476 t = stack.pop() 477 if t not in all_types: 478 expanded.append(t) 479 all_types.add(t) 480 if t.arity > 0: 481 for subtype in t.args: 482 if subtype not in all_types: 483 expanded.append(subtype) 484 all_types.add(subtype) 485 stack.append(subtype) 486 expanded.reverse() 487 return expanded 488 489 @walkers.handles(set(op.ALL_TYPES) - \ 490 set([op.SYMBOL, op.FUNCTION]) -\ 491 op.QUANTIFIERS - op.CONSTANTS) 492 def walk_combine(self, formula, args, **kwargs): 493 #pylint: disable=unused-argument 494 res = set() 495 for arg in args: 496 res.update(arg) 497 return frozenset(res) 498 499 @walkers.handles(op.SYMBOL) 500 def walk_symbol(self, formula, **kwargs): 501 return frozenset([formula.symbol_type()]) 502 503 @walkers.handles(op.FUNCTION) 504 def walk_function(self, formula, **kwargs): 505 ftype = formula.function_name().symbol_type() 506 return frozenset([ftype.return_type] + list(ftype.param_types)) 507 508 @walkers.handles(op.QUANTIFIERS) 509 def walk_quantifier(self, formula, args, **kwargs): 510 return frozenset([x.symbol_type() 511 for x in formula.quantifier_vars()]) | args[0] 512 513 @walkers.handles(op.CONSTANTS) 514 def walk_constant(self, formula, args, **kwargs): 515 return frozenset([formula.constant_type()]) 516 517# EOC TypesOracle 518 519 520def get_logic(formula, env=None): 521 if env is None: 522 env = pysmt.environment.get_env() 523 # Get Quantifier Information 524 qf = env.qfo.is_qf(formula) 525 theory = env.theoryo.get_theory(formula) 526 logic = Logic(name="Detected Logic", description="", 527 quantifier_free=qf, theory=theory) 528 # Return a logic supported by PySMT that is close to the one computed 529 return get_closer_pysmt_logic(logic) 530