Permalink
Browse files

Small, syntactic refactoring to improve overall code style and landsc…

…ape.io evaluation
  • Loading branch information...
mikand committed Jun 10, 2015
1 parent 6bceb2c commit 47bc2f203611581ec59a9e416908c2397416b70e
View
@@ -2,4 +2,5 @@ strictness: medium
pylint: pylint:
disable: disable:
- cyclic-import - cyclic-import
- redefined-builtin
View
@@ -4,7 +4,6 @@
import urllib import urllib
import zipfile import zipfile
import os.path import os.path
import sys
class BenchmarkNotFoundError(Exception): class BenchmarkNotFoundError(Exception):
pass pass
View
@@ -118,15 +118,15 @@ def smtlib_solver(self, stream):
def main(self): def main(self):
if self.args.interactive: if self.args.interactive:
if self.args.file != None: if self.args.file is not None:
print("Unable to execute in interactive mode with an input file") print("Unable to execute in interactive mode with an input file")
exit(1) sys.exit(1)
if self.args.solver != "auto": if self.args.solver != "auto":
warn("The solver option will be ignored in interactive mode") warn("The solver option will be ignored in interactive mode")
self.interactive() self.interactive()
else: else:
input_stream = sys.stdin input_stream = sys.stdin
if self.args.file != None: if self.args.file is not None:
input_stream = open(self.args.file, "r") input_stream = open(self.args.file, "r")
self.smtlib_solver(input_stream) self.smtlib_solver(input_stream)
View
@@ -89,7 +89,7 @@ def configure_environment(config_filename, environment):
else: else:
warn("Unknown value for 'use_infix_notation': %s" % infix) warn("Unknown value for 'use_infix_notation': %s" % infix)
if pref_list != None: if pref_list is not None:
prefs = pref_list.split() prefs = pref_list.split()
for s in prefs: for s in prefs:
if s not in factory.all_solvers(): if s not in factory.all_solvers():
View
@@ -32,11 +32,10 @@
class Environment(object): class Environment(object):
FormulaManagerClass = pysmt.formula.FormulaManager
def __init__(self): def __init__(self):
self._stc = pysmt.type_checker.SimpleTypeChecker(self) self._stc = pysmt.type_checker.SimpleTypeChecker(self)
self._formula_manager = self.FormulaManagerClass(self) self._formula_manager = pysmt.formula.FormulaManager(self)
# NOTE: Both Simplifier and Substituter keep an internal copy # NOTE: Both Simplifier and Substituter keep an internal copy
# of the Formula Manager # of the Formula Manager
self._simplifier = pysmt.simplifier.Simplifier(self) self._simplifier = pysmt.simplifier.Simplifier(self)
View
@@ -634,16 +634,16 @@ def get_logic(quantifier_free=False,
""" """
for logic in LOGICS: for logic in LOGICS:
if (logic.quantifier_free == quantifier_free and if ( logic.quantifier_free == quantifier_free and
logic.theory.arrays == arrays and \ logic.theory.arrays == arrays and \
logic.theory.bit_vectors == bit_vectors and \ logic.theory.bit_vectors == bit_vectors and \
logic.theory.floating_point == floating_point and \ logic.theory.floating_point == floating_point and \
logic.theory.integer_arithmetic == integer_arithmetic and \ logic.theory.integer_arithmetic == integer_arithmetic and \
logic.theory.real_arithmetic == real_arithmetic and \ logic.theory.real_arithmetic == real_arithmetic and \
logic.theory.integer_difference == integer_difference and \ logic.theory.integer_difference == integer_difference and \
logic.theory.real_difference == real_difference and \ logic.theory.real_difference == real_difference and \
logic.theory.linear == linear and \ logic.theory.linear == linear and \
logic.theory.uninterpreted == uninterpreted): logic.theory.uninterpreted == uninterpreted):
return logic return logic
raise UndefinedLogicError raise UndefinedLogicError

This file was deleted.

Oops, something went wrong.
View
@@ -70,7 +70,7 @@ def set_walking_measure(self, measure):
assert self.is_complete(verbose=True) assert self.is_complete(verbose=True)
def _get_key(self, formula, measure): def _get_key(self, formula, measure, **kwargs):
# Memoize using a tuple (measure, formula) # Memoize using a tuple (measure, formula)
return (measure, formula) return (measure, formula)
@@ -89,21 +89,26 @@ def get_size(self, formula, measure=None):
return res return res
def walk_count_tree(self, formula, args, measure): def walk_count_tree(self, formula, args, **kwargs):
#pylint: disable=unused-argument
return 1 + sum(args) return 1 + sum(args)
def walk_count_dag(self, formula, args, measure): def walk_count_dag(self, formula, args, measure, **kwargs):
#pylint: disable=unused-argument
return frozenset([formula]) | frozenset([x for s in args for x in s]) return frozenset([formula]) | frozenset([x for s in args for x in s])
def walk_count_leaves(self, formula, args, measure): def walk_count_leaves(self, formula, args, measure, **kwargs):
#pylint: disable=unused-argument
is_leaf = (len(args) == 0) is_leaf = (len(args) == 0)
return (1 if is_leaf else 0) + sum(args) return (1 if is_leaf else 0) + sum(args)
def walk_count_depth(self, formula, args, measure): def walk_count_depth(self, formula, args, measure, **kwargs):
#pylint: disable=unused-argument
is_leaf = (len(args) == 0) is_leaf = (len(args) == 0)
return 1 + (0 if is_leaf else max(args)) return 1 + (0 if is_leaf else max(args))
def walk_count_symbols(self, formula, args, measure): def walk_count_symbols(self, formula, args, measure, **kwargs):
#pylint: disable=unused-argument
is_sym = formula.is_symbol() is_sym = formula.is_symbol()
a_res = frozenset([x for s in args for x in s]) a_res = frozenset([x for s in args for x in s])
if is_sym: if is_sym:
@@ -172,7 +177,8 @@ def __init__(self, env=None):
self.functions[op.BV_CONSTANT] = self.walk_constant self.functions[op.BV_CONSTANT] = self.walk_constant
def walk_combine(self, formula, args): def walk_combine(self, formula, args, **kwargs):
#pylint: disable=unused-argument
"""Combines the current theory value of the children""" """Combines the current theory value of the children"""
if len(args) == 1: if len(args) == 1:
return args[0].copy() return args[0].copy()
@@ -182,7 +188,8 @@ def walk_combine(self, formula, args):
theory_out = theory_out.combine(t) theory_out = theory_out.combine(t)
return theory_out return theory_out
def walk_constant(self, formula, args): def walk_constant(self, formula, args, **kwargs):
#pylint: disable=unused-argument
"""Returns a new theory object with the type of the constant.""" """Returns a new theory object with the type of the constant."""
if formula.is_real_constant(): if formula.is_real_constant():
theory_out = Theory(real_arithmetic=True, real_difference=True) theory_out = Theory(real_arithmetic=True, real_difference=True)
@@ -196,7 +203,8 @@ def walk_constant(self, formula, args):
return theory_out return theory_out
def walk_symbol(self, formula, args): def walk_symbol(self, formula, args, **kwargs):
#pylint: disable=unused-argument
"""Returns a new theory object with the type of the symbol.""" """Returns a new theory object with the type of the symbol."""
f_type = formula.symbol_type() f_type = formula.symbol_type()
if f_type.is_real_type(): if f_type.is_real_type():
@@ -213,7 +221,7 @@ def walk_symbol(self, formula, args):
return theory_out return theory_out
def walk_function(self, formula, args): def walk_function(self, formula, args, **kwargs):
"""Extends the Theory with UF.""" """Extends the Theory with UF."""
if len(args) == 1: if len(args) == 1:
theory_out = args[0].copy() theory_out = args[0].copy()
@@ -227,13 +235,14 @@ def walk_function(self, formula, args):
theory_out.uninterpreted = True theory_out.uninterpreted = True
return theory_out return theory_out
def walk_lira(self, formula, args): def walk_lira(self, formula, args, **kwargs):
#pylint: disable=unused-argument
"""Extends the Theory with LIRA.""" """Extends the Theory with LIRA."""
theory_out = args[0].copy() theory_out = args[0].copy()
theory_out = theory_out.set_lira() theory_out = theory_out.set_lira()
return theory_out return theory_out
def walk_times(self, formula, args): def walk_times(self, formula, args, **kwargs):
"""Extends the Theory with Non-Linear, if needed.""" """Extends the Theory with Non-Linear, if needed."""
if len(args) == 1: if len(args) == 1:
theory_out = args[0].copy() theory_out = args[0].copy()
@@ -245,7 +254,7 @@ def walk_times(self, formula, args):
theory_out = theory_out.set_difference_logic(False) theory_out = theory_out.set_difference_logic(False)
return theory_out return theory_out
def walk_plus(self, formula, args): def walk_plus(self, formula, args, **kwargs):
theory_out = args[0] theory_out = args[0]
for t in args[1:]: for t in args[1:]:
theory_out = theory_out.combine(t) theory_out = theory_out.combine(t)
@@ -254,9 +263,7 @@ def walk_plus(self, formula, args):
assert not theory_out.integer_difference assert not theory_out.integer_difference
return theory_out return theory_out
def walk_equals(self, formula, args): def walk_equals(self, formula, args, **kwargs):
# TODO: Does EQUAL need a special treatment?
# We consider EUF as UF, shall we split the two concepts?
return self.walk_combine(formula, args) return self.walk_combine(formula, args)
def get_theory(self, formula): def get_theory(self, formula):
@@ -306,22 +313,26 @@ def get_free_variables(self, formula):
"""Returns the set of Symbols appearing free in the formula.""" """Returns the set of Symbols appearing free in the formula."""
return self.walk(formula) return self.walk(formula)
def walk_simple_args(self, formula, args): def walk_simple_args(self, formula, args, **kwargs):
#pylint: disable=unused-argument
res = set() res = set()
for arg in args: for arg in args:
res.update(arg) res.update(arg)
return frozenset(res) return frozenset(res)
def walk_quantifier(self, formula, args): def walk_quantifier(self, formula, args, **kwargs):
#pylint: disable=unused-argument
return args[0].difference(formula.quantifier_vars()) return args[0].difference(formula.quantifier_vars())
def walk_symbol(self, formula, args): def walk_symbol(self, formula, args, **kwargs):
#pylint: disable=unused-argument
return frozenset([formula]) return frozenset([formula])
def walk_constant(self, formula, args): def walk_constant(self, formula, args, **kwargs):
#pylint: disable=unused-argument
return frozenset() return frozenset()
def walk_function(self, formula, args): def walk_function(self, formula, args, **kwargs):
res = set([formula.function_name()]) res = set([formula.function_name()])
for arg in args: for arg in args:
res.update(arg) res.update(arg)
@@ -372,26 +383,31 @@ def get_atoms(self, formula):
"""Returns the set of atoms appearing in the formula.""" """Returns the set of atoms appearing in the formula."""
return self.walk(formula) return self.walk(formula)
def walk_bool_op(self, formula, args): def walk_bool_op(self, formula, args, **kwargs):
#pylint: disable=unused-argument
return frozenset(x for a in args for x in a) return frozenset(x for a in args for x in a)
def walk_theory_relation(self, formula, args): def walk_theory_relation(self, formula, **kwargs):
#pylint: disable=unused-argument
return frozenset([formula]) return frozenset([formula])
def walk_theory_op(self, formula, args): def walk_theory_op(self, formula, **kwargs):
#pylint: disable=unused-argument
return None return None
def walk_symbol(self, formula, args): def walk_symbol(self, formula, **kwargs):
if formula.is_symbol(types.BOOL): if formula.is_symbol(types.BOOL):
return frozenset([formula]) return frozenset([formula])
return None return None
def walk_constant(self, formula, args): def walk_constant(self, formula, **kwargs):
#pylint: disable=unused-argument
if formula.is_bool_constant(): if formula.is_bool_constant():
return frozenset() return frozenset()
return None return None
def walk_ite(self, formula, args): def walk_ite(self, formula, args, **kwargs):
#pylint: disable=unused-argument
if any(a is None for a in args): if any(a is None for a in args):
# Theory ITE # Theory ITE
return None return None
Oops, something went wrong.

0 comments on commit 47bc2f2

Please sign in to comment.