From 0db94db0f43bcc64ebc7d1410bf60c72d68d5978 Mon Sep 17 00:00:00 2001 From: Quan Zhou Date: Tue, 4 Mar 2025 09:55:32 -0500 Subject: [PATCH] updating for python3 compatibility --- solver.py | 174 +++++++++++++++++++++++++++++++------------------ test_solver.py | 97 +++++++++++++++------------ z3supp.py | 71 +++++++++++++------- 3 files changed, 211 insertions(+), 131 deletions(-) diff --git a/solver.py b/solver.py index 971678e..347026d 100755 --- a/solver.py +++ b/solver.py @@ -1,6 +1,6 @@ #!/usr/bin/env python3 # python >= 3.7 - + from lattice import * from partt import * from rm_solver import RMSolver @@ -14,6 +14,7 @@ import logging import unittest + class PartitionDerivationSolver: def __init__(self, partt=SequentialPartition(), lat=TwoPointLattice(), timeout=3): assert isinstance(lat, Lattice) @@ -40,7 +41,7 @@ def time_check(self): return True return False - def sound_derive(self, pconset:List[PCon], p): + def sound_derive(self, pconset: List[PCon], p): conset = [] for pcon in pconset: if self.time_check(): @@ -50,7 +51,7 @@ def sound_derive(self, pconset:List[PCon], p): # print("Sound Derive for {0}: {1}".format(p, pretty_conset_print(conset))) return conset - def complete_derive(self, pconset:List[PCon], p): + def complete_derive(self, pconset: List[PCon], p): conset = [] for pcon in pconset: if self.time_check(): @@ -60,7 +61,7 @@ def complete_derive(self, pconset:List[PCon], p): # print("Complete Derive for {0}: {1}".format(p, pretty_conset_print(conset))) return conset - def solve_one_shot(self, pconset:List[PCon]): + def solve_one_shot(self, pconset: List[PCon]): done = {} self.partt.init_partt(pconset) self.partt.one_shot_partt() @@ -73,7 +74,9 @@ def solve_one_shot(self, pconset:List[PCon]): return False if globals.DEBUG: print(".") - if self.rm.solve(self.sound_derive(pconset, predicate)): # sound == complete, either is good + if self.rm.solve( + self.sound_derive(pconset, predicate) + ): # sound == complete, either is good done[predicate] = self.rm.solution else: self.unsolved = [predicate] @@ -81,7 +84,7 @@ def solve_one_shot(self, pconset:List[PCon]): self.solution = done return True - def solve_early_accept(self, pconset:List[PCon])->bool: + def solve_early_accept(self, pconset: List[PCon]) -> bool: done = {} self.partt.init_partt(pconset) while not self.partt.stop_partt: @@ -110,7 +113,7 @@ def solve_early_accept(self, pconset:List[PCon])->bool: self.unsolved = self.partt.parttset return False - def solve_early_reject(self, pconset:List[PCon])->bool: + def solve_early_reject(self, pconset: List[PCon]) -> bool: done = {} self.partt.init_partt(pconset) while not self.partt.stop_partt: @@ -135,7 +138,7 @@ def solve_early_reject(self, pconset:List[PCon])->bool: self.solution = done return True - def solve_hybrid(self, pconset:List[PCon])->bool: + def solve_hybrid(self, pconset: List[PCon]) -> bool: done = {} self.partt.init_partt(pconset) while not self.partt.stop_partt: @@ -167,17 +170,24 @@ def solve_hybrid(self, pconset:List[PCon])->bool: # If reach here: the partition algorithm does not reach an equivalent state at the last iteration raise PartitionNotEquivalentAtEndError - def solve_constraint(self, pconset:List[PCon], approach=globals.EARLY_ACCETP_APPROACH)->bool: + def solve_constraint( + self, pconset: List[PCon], approach=globals.EARLY_ACCETP_APPROACH + ) -> bool: self.partt.z3.init_pconset(pconset) - print(self.partt.__class__.__name__ + " Partition, " + globals.Approach[approach] + " Approach:") + print( + self.partt.__class__.__name__ + + " Partition, " + + globals.Approach[approach] + + " Approach:" + ) solve = False for app in globals.Approach.keys(): if approach == app: t_start = time.time() - self.set_stop_time(t_start + 60*self.timeout) - solve = getattr(self, "solve_"+globals.Approach[app].lower())(pconset) + self.set_stop_time(t_start + 60 * self.timeout) + solve = getattr(self, "solve_" + globals.Approach[app].lower())(pconset) self.time = time.time() - t_start break @@ -194,7 +204,13 @@ def solve_constraint(self, pconset:List[PCon], approach=globals.EARLY_ACCETP_APP def pretty_solution(self): msg = "{\n" for predicate in self.solution: - msg += "\t" + predicate + " => " + RMSolver.pretty_solution(self.solution[predicate]) + "\n" + msg += ( + "\t" + + predicate + + " => " + + RMSolver.pretty_solution(self.solution[predicate]) + + "\n" + ) msg += "}" return msg @@ -204,68 +220,96 @@ def test_solver_combination(self): solver = PartitionDerivationSolver(CombinationPartition()) parser = CoreConstraintParser() for i in globals.Approach.keys(): - self.assertTrue(solver.solve_constraint(parser.parse('''True => L <: ax And az <: ax; dddd>0 => H <: ay; Not(dddd>0) => L <: ay; - dddd>0 => H<: ay; dddd<0=> ay<:ax; True=>ax<:L'''), i)) + self.assertTrue( + solver.solve_constraint( + parser.parse( + """True => L <: ax And az <: ax; dddd>0 => H <: ay; Not(dddd>0) => L <: ay; + dddd>0 => H<: ay; dddd<0=> ay<:ax; True=>ax<:L""" + ), + i, + ) + ) for i in globals.Approach.keys(): - self.assertFalse(solver.solve_constraint(parser.parse('''a>0=>H<:a And H<:c; a<0 => a<:L And L <: b; b>0=>H <:b; And(bbbb<0, (dddd<0)) => b<:L; - c>0=>H<:c And L<:a; c<0=>c<:L'''), i)) + self.assertFalse( + solver.solve_constraint( + parser.parse( + """a>0=>H<:a And H<:c; a<0 => a<:L And L <: b; b>0=>H <:b; And(bbbb<0, (dddd<0)) => b<:L; + c>0=>H<:c And L<:a; c<0=>c<:L""" + ), + i, + ) + ) + def test_solver_sequential(self): solver = PartitionDerivationSolver(SequentialPartition()) parser = CoreConstraintParser() for i in globals.Approach.keys(): - self.assertTrue(solver.solve_constraint(parser.parse('''True => L <: ax And az <: ax; d>0 => H <: ay; Not(d>0) => L <: ay; - d>0 => H<: ay; d<0=> ay<:ax; True=>ax<:L'''), i)) + self.assertTrue( + solver.solve_constraint( + parser.parse( + """True => L <: ax And az <: ax; d>0 => H <: ay; Not(d>0) => L <: ay; + d>0 => H<: ay; d<0=> ay<:ax; True=>ax<:L""" + ), + i, + ) + ) for i in globals.Approach.keys(): - self.assertFalse(solver.solve_constraint(parser.parse('''a>0=>H<:a And H<:c; a<0 => a<:L And L <: b; b>0=>H <:b; And(b<0, (d<0)) => b<:L; - c>0=>H<:c And L<:a; c<0=>c<:L'''), i)) + self.assertFalse( + solver.solve_constraint( + parser.parse( + """a>0=>H<:a And H<:c; a<0 => a<:L And L <: b; b>0=>H <:b; And(b<0, (d<0)) => b<:L; + c>0=>H<:c And L<:a; c<0=>c<:L""" + ), + i, + ) + ) -if __name__ == '__main__': -# if len(sys.argv) <= 1: -# print ("Usage: test_solver.py [test_file] -op [op]") -# print ("\t [test_file]: test file .con; use \'all\' to run all the file under tests/") -# print ("\t -partt [0-1]: -partt [0-1]: specifying partition algorithm: 0=sequential,") -# print ("\t\t\t1=combinational; if not specified, it tests all the partt ") -# print ("\t\t\talgorithms") -# print ("\t -appr [0-3]: specifying approaches: 0=hybrid, 1=early-accept, 2=one-shot,") -# print ("\t\t\t3=early-reject; if not specified, it tests [0,1,2] approaches.") -# print ("\t -time i : specifying time-out minutes; default i=3 min.") -# print ("\t -debug [0-1] : print debug message; default 1 with debug message on") +if __name__ == "__main__": + # if len(sys.argv) <= 1: + # print ("Usage: test_solver.py [test_file] -op [op]") + # print ("\t [test_file]: test file .con; use \'all\' to run all the file under tests/") + # print ("\t -partt [0-1]: -partt [0-1]: specifying partition algorithm: 0=sequential,") + # print ("\t\t\t1=combinational; if not specified, it tests all the partt ") + # print ("\t\t\talgorithms") + # print ("\t -appr [0-3]: specifying approaches: 0=hybrid, 1=early-accept, 2=one-shot,") + # print ("\t\t\t3=early-reject; if not specified, it tests [0,1,2] approaches.") + # print ("\t -time i : specifying time-out minutes; default i=3 min.") + # print ("\t -debug [0-1] : print debug message; default 1 with debug message on") -# else: -# file_name = output_file_name("Test1") -# # print file_name -# # try: -# partt = globals.ParttAlg.keys() -# appr = globals.Approach.keys() -# #appr.pop(globals.EARLY_REJECT_APPROACH) - -# for i in range(2, len(sys.argv)): -# if sys.argv[i] == "-partt": -# partt = [int(sys.argv[i+1])] -# print (partt) -# elif sys.argv[i] == "-appr": -# appr = [int(sys.argv[i+1])] -# elif sys.argv[i] == "-time": -# globals.STOP_MIN = float(sys.argv[i+1]) -# elif sys.argv[i] == "-debug": -# globals.DEBUG = int(sys.argv[i+1]) + # else: + # file_name = output_file_name("Test1") + # # print file_name + # # try: + # partt = globals.ParttAlg.keys() + # appr = globals.Approach.keys() + # #appr.pop(globals.EARLY_REJECT_APPROACH) -# file_test = sys.argv[1] -# if sys.argv[1] == "all": -# file_test = [TEST_DIR + file for file in os.listdir(TEST_DIR)] -# for test_file_name in file_test: -# test_file(test_file_name, partt, appr) -# else: -# test_file(file_test, partt, appr) + # for i in range(2, len(sys.argv)): + # if sys.argv[i] == "-partt": + # partt = [int(sys.argv[i+1])] + # print (partt) + # elif sys.argv[i] == "-appr": + # appr = [int(sys.argv[i+1])] + # elif sys.argv[i] == "-time": + # globals.STOP_MIN = float(sys.argv[i+1]) + # elif sys.argv[i] == "-debug": + # globals.DEBUG = int(sys.argv[i+1]) -# # save result: -# if files: -# store_result_file(file_name, files, number, partt_alg, perform) + # file_test = sys.argv[1] + # if sys.argv[1] == "all": + # file_test = [TEST_DIR + file for file in os.listdir(TEST_DIR)] + # for test_file_name in file_test: + # test_file(test_file_name, partt, appr) + # else: + # test_file(file_test, partt, appr) - # if sys.argv[1] == 'all': - # plot_line_chart(file_name + plt_ext, partt, appr, number, partt_alg, perform) - unittest.main(argv=['first-arg-is-ignored'], exit=False, verbosity=2) - #unittest.main() - #unittest.main(verbosity=2) + # # save result: + # if files: + # store_result_file(file_name, files, number, partt_alg, perform) + # if sys.argv[1] == 'all': + # plot_line_chart(file_name + plt_ext, partt, appr, number, partt_alg, perform) + unittest.main(argv=["first-arg-is-ignored"], exit=False, verbosity=2) + # unittest.main() + # unittest.main(verbosity=2) diff --git a/test_solver.py b/test_solver.py index 7ed64ac..89861be 100644 --- a/test_solver.py +++ b/test_solver.py @@ -1,8 +1,8 @@ # This file is part of Derivation Solver. Derivation Solver provides # implementation of derivation solvers for dependent type inference. -# +# # Copyright (C) 2018 Peixuan Li -# +# # Derivation Solver is free software: you can redistribute it and/or modify # it under the terms of the GNU General Public License as published by # the Free Software Foundation, either version 3 of the License, or @@ -15,9 +15,10 @@ # # You should have received a copy of the GNU General Public License # along with Foobar. If not, see . -# +# from solver import * -#from plot import * + +# from plot import * from result import * from parser import * import globals @@ -28,19 +29,19 @@ class CommentToken(Token): - lex_reg = r';.*\n' + lex_reg = r";.*\n" class JoinToken(Token): - lex_reg = r'[jJ]oin' + lex_reg = r"[jJ]oin" class ParenLeftToken(Token): - lex_reg = r'\(' + lex_reg = r"\(" class ParenRightToken(Token): - lex_reg = r'\)' + lex_reg = r"\)" class LeftJoinParser(CoreConstraintParser): @@ -57,24 +58,32 @@ def __extract_predicates(self, input_str): return ["True"] for char in input_str: - if char == '(': + if char == "(": if deep == 0: start = index deep += 1 - elif char == ')': + elif char == ")": if deep == 1: - result.append(input_str[start+1:index]) + result.append(input_str[start + 1 : index]) if deep > 0: deep -= 1 index += 1 return result def init_lexer(self): - self.lexer.add_tokens(NoneToken(), ParenLeftToken(), ParenRightToken(), JoinToken(), - AndToken(), SubToken(), SemiToken(), VariableToken()) + self.lexer.add_tokens( + NoneToken(), + ParenLeftToken(), + ParenRightToken(), + JoinToken(), + AndToken(), + SubToken(), + SemiToken(), + VariableToken(), + ) def pre_process(self, input_str): - return re.sub(CommentToken().lex_reg, ';', input_str) + return re.sub(CommentToken().lex_reg, ";", input_str) def post_process(self, pconset): result = [] @@ -95,6 +104,7 @@ def post_process(self, pconset): def generate_predicate(self, input_str): input_str = input_str.strip() preds = self.__extract_predicates(input_str) + print(preds) return self.z3.and_predicates(*preds) def generate_conset(self, input_str): @@ -124,7 +134,7 @@ def __init__(self, partt=SequentialPartition()): PartitionDerivationSolver.__init__(self, partt) def pretty_solution(self): - msg = " {\n" + msg = "{\n" for predicate in self.solution: msg += "\t" + predicate + " => {" empty = 0 @@ -140,19 +150,18 @@ def pretty_solution(self): def test_file(file_name, partts, appr): - if file_name[len(con_ext)*-1:] == con_ext: - print ("Working on file: " + file_name) - test_file = open(file_name, 'r') + if file_name[len(con_ext) * -1 :] == con_ext: + print("Working on file: " + file_name) + test_file = open(file_name, "r") input_str = test_file.read() test_file.close() pconset = LeftJoinParser().parse(input_str) num = len(pconset) if globals.DEBUG: - print(len(pretty_pcon_set_print(pconset))) - print ("Constraint Set: \n" + pretty_pcon_set_print(pconset)) - print ("#predicates: " + str(num)) - #print "#predicates: " + str(pconset) + print("Constraint Set: \n" + pretty_pcon_set_print(pconset)) + print("#predicates: ", str(num), "\n") + # print "#predicates: " + str(pconset) cur_perform = {} for i in globals.Approach.keys(): @@ -165,7 +174,7 @@ def test_file(file_name, partts, appr): # elif partt == globals.OP_COMB_PARTT: # solver = TestSolver(OpCombinationPartition()) - files.append(file_name[len(TEST_DIR):len(con_ext)*-1]) + files.append(file_name[len(TEST_DIR) : len(con_ext) * -1]) number.append(num) partt_alg.append(partt) for i in globals.Approach: @@ -189,17 +198,23 @@ def test_file(file_name, partts, appr): for i in globals.Approach.keys(): perform[i] = [] -if __name__ == '__main__': +if __name__ == "__main__": if len(sys.argv) <= 1: - print ("Usage: test_solver.py [test_file] -op [op]") - print ("\t [test_file]: test file .con; use \'all\' to run all the file under tests/") - print ("\t -partt [0-1]: -partt [0-1]: specifying partition algorithm: 0=sequential,") - print ("\t\t\t1=combinational; if not specified, it tests all the partt ") - print ("\t\t\talgorithms") - print ("\t -appr [0-3]: specifying approaches: 0=hybrid, 1=early-accept, 2=one-shot,") - print ("\t\t\t3=early-reject; if not specified, it tests [0,1,2] approaches.") - print ("\t -time i : specifying time-out minutes; default i=3 min.") - print ("\t -debug [0-1] : print debug message; default 1 with debug message on") + print("Usage: test_solver.py [test_file] -op [op]") + print( + "\t [test_file]: test file .con; use 'all' to run all the file under tests/" + ) + print( + "\t -partt [0-1]: -partt [0-1]: specifying partition algorithm: 0=sequential," + ) + print("\t\t\t1=combinational; if not specified, it tests all the partt ") + print("\t\t\talgorithms") + print( + "\t -appr [0-3]: specifying approaches: 0=hybrid, 1=early-accept, 2=one-shot," + ) + print("\t\t\t3=early-reject; if not specified, it tests [0,1,2] approaches.") + print("\t -time i : specifying time-out minutes; default i=3 min.") + print("\t -debug [0-1] : print debug message; default 1 with debug message on") else: file_name = output_file_name("Test_file") @@ -207,21 +222,21 @@ def test_file(file_name, partts, appr): # try: partt = globals.ParttAlg.keys() appr = globals.Approach.keys() - #appr.pop(globals.EARLY_REJECT_APPROACH) - #appr.pop(globals.EARLY_REJECT_APPROACH) + # appr.pop(globals.EARLY_REJECT_APPROACH) + # appr.pop(globals.EARLY_REJECT_APPROACH) for i in range(2, len(sys.argv)): if sys.argv[i] == "-partt": - partt = [int(sys.argv[i+1])] - print (partt) + partt = [int(sys.argv[i + 1])] + print(partt) elif sys.argv[i] == "-appr": - appr = [int(sys.argv[i+1])] + appr = [int(sys.argv[i + 1])] elif sys.argv[i] == "-time": - globals.STOP_MIN = float(sys.argv[i+1]) + globals.STOP_MIN = float(sys.argv[i + 1]) elif sys.argv[i] == "-debug": - globals.DEBUG = int(sys.argv[i+1]) + globals.DEBUG = int(sys.argv[i + 1]) file_test = sys.argv[1] - if sys.argv[1] == 'all': + if sys.argv[1] == "all": file_test = [TEST_DIR + file for file in os.listdir(TEST_DIR)] for test_file_name in file_test: test_file(test_file_name, partt, appr) diff --git a/z3supp.py b/z3supp.py index 8564dba..806e2f2 100644 --- a/z3supp.py +++ b/z3supp.py @@ -9,6 +9,7 @@ import logging import unittest + class Z3Supp: time_init = 0 time_intersection = 0 @@ -16,7 +17,7 @@ class Z3Supp: time_valid = 0 def __init__(self): - self.reserved = {'And', 'Or', 'Not', 'True', 'False'} + self.reserved = {"And", "Or", "Not", "True", "False"} self.varset = set() self.declare = "" self.inductset = {} @@ -31,15 +32,15 @@ def init_pconset(self, pconset): # exec self.declare logging.debug("Initialization for And_Dict Finished.") - def __declare_vars(self, p): # find the variables and declare them as int in Z3 + def __declare_vars(self, p): # find the variables and declare them as int in Z3 varlist = re.findall(VariableToken.lex_reg, p) for var in varlist: if var not in self.reserved and var not in self.varset: self.varset.add(var) - declare = "{0} = Int(\'{0}\')".format(var) - self.declare += declare+"\n" + declare = "{0} = Int('{0}')".format(var) + self.declare += declare + "\n" - def intersect(self, p1, p2): # Check if p1 and p2 intersects + def intersect(self, p1, p2): # Check if p1 and p2 intersects t_start = time.time() # Skip the trivial cases so that no Z3 processing if p1 == "False" or p2 == "False": @@ -49,24 +50,24 @@ def intersect(self, p1, p2): # Check if p1 and p2 intersects self.__declare_vars(p1) self.__declare_vars(p2) - exec(self.declare) + exec(self.declare, globals()) s = Solver() stmt1 = "s.add({0})".format(p1) stmt2 = "s.add({0})".format(p2) eval(stmt1) eval(stmt2) - self.time_intersection += time.time()-t_start + self.time_intersection += time.time() - t_start return s.check() == sat - def induct(self, p1, p2): # check if p1 => p2, returns a bool + def induct(self, p1, p2): # check if p1 => p2, returns a bool t_start = time.time() if p2 == "True" or p1 == "False": return True self.__declare_vars(p1) self.__declare_vars(p2) - exec(self.declare) + exec(self.declare, globals()) s = Solver() stmt1 = "s.add({0})".format(p1) stmt2 = "s.add(Not({0}))".format(p2) @@ -75,16 +76,16 @@ def induct(self, p1, p2): # check if p1 => p2, returns a bool self.time_induct += time.time() - t_start return s.check() == unsat - def not_p_string(self, p): # return not p + def not_p_string(self, p): # return not p if p == "True": return "False" if p == "False": return "True" - if len(p) > 5 and p[0:4] == "Not(" and p[-1] == ')': + if len(p) > 5 and p[0:4] == "Not(" and p[-1] == ")": return p[4:-1] return "Not({0})".format(p) - def and_predicates(self, *predicates): # return p1 AND p2 AND ... + def and_predicates(self, *predicates): # return p1 AND p2 AND ... valid = [] for p in predicates: if p == "False" or not self.valid_p(p): @@ -105,25 +106,32 @@ def and_predicates(self, *predicates): # return p1 AND p2 AND ... result += ")" return result - def valid_p(self, p): # Check whether a predicate is still satisifiable + def valid_p(self, p): # Check whether a predicate is still satisifiable t_start = time.time() self.__declare_vars(p) - exec(self.declare) + exec(self.declare, globals()) s = Solver() stmt1 = "s.add({0})".format(p) eval(stmt1) - self.time_valid += time.time()-t_start + self.time_valid += time.time() - t_start return s.check() == sat + class TestZ3Supp(unittest.TestCase): def test_z3Installation(self): s = Solver() - s.add(parse_smt2_string('(declare-const x Int) (assert (< x 10)) (assert (> x 0))')) - self.assertEqual(str(s.check()), 'sat') + s.add( + parse_smt2_string( + "(declare-const x Int) (assert (< x 10)) (assert (> x 0))" + ) + ) + self.assertEqual(str(s.check()), "sat") + def test_z3Supp_induct(self): z3 = Z3Supp() self.assertTrue(z3.induct("x>5", "x>0")) self.assertFalse(z3.induct("x>5", "x>10")) + def test_z3Supp_intersect(self): z3 = Z3Supp() self.assertTrue(z3.intersect("x>5", "x>0")) @@ -131,26 +139,39 @@ def test_z3Supp_intersect(self): self.assertTrue(z3.intersect("x>=5", "x<=5")) self.assertFalse(z3.intersect("x>5", "x<5")) self.assertTrue(z3.intersect("And(x+y>5, x==5)", "a+y<4+6")) + def test_z3Supp_valid_p(self): z3 = Z3Supp() self.assertTrue(z3.valid_p("And(x>5, x>0)")) self.assertFalse(z3.valid_p("And(x>5, Not(x>0))")) + def test_z3Supp_not_p_string(self): z3 = Z3Supp() self.assertFalse(z3.induct("x>5", z3.not_p_string("x>0"))) self.assertTrue(z3.induct(z3.not_p_string("x>5"), z3.not_p_string("x>10"))) + def test_z3Supp_and_predicates(self): z3 = Z3Supp() - self.assertTrue(z3.valid_p(z3.and_predicates('x>5', 'y>0'))) - self.assertFalse(z3.valid_p(z3.and_predicates('x>5', 'Not(x>0)'))) - self.assertTrue(z3.valid_p(z3.and_predicates('x>5', 'x>0', 'y>=0', 'y<=0'))) - self.assertFalse(z3.valid_p(z3.and_predicates('x>5', 'x>0', 'y>=0', 'y<0'))) + self.assertTrue(z3.valid_p(z3.and_predicates("x>5", "y>0"))) + self.assertFalse(z3.valid_p(z3.and_predicates("x>5", "Not(x>0)"))) + self.assertTrue(z3.valid_p(z3.and_predicates("x>5", "x>0", "y>=0", "y<=0"))) + self.assertFalse(z3.valid_p(z3.and_predicates("x>5", "x>0", "y>=0", "y<0"))) + def test_variable_name_extraction(self): z3 = Z3Supp() self.assertTrue(z3.valid_p("And(x__1>5, x__1>0)")) self.assertFalse(z3.valid_p("And(x__1>5, x__1<0)")) - self.assertFalse(z3.valid_p("And(x_very____long_name_1__variable_name>5, x_very____long_name_1__variable_name<0)")) - self.assertTrue(z3.valid_p("And(x_very____long_name_1__variable_name>5, x_very____long_name_2__variable_name<0)")) - -if __name__ == '__main__': + self.assertFalse( + z3.valid_p( + "And(x_very____long_name_1__variable_name>5, x_very____long_name_1__variable_name<0)" + ) + ) + self.assertTrue( + z3.valid_p( + "And(x_very____long_name_1__variable_name>5, x_very____long_name_2__variable_name<0)" + ) + ) + + +if __name__ == "__main__": unittest.main(verbosity=2)