From 509cbd9abca810e400f0f188734bfbc7e0b7a6f0 Mon Sep 17 00:00:00 2001 From: Shaurya Gomber Date: Sat, 12 Nov 2022 12:46:45 -0600 Subject: [PATCH] Some updates to make code work with new changes in libraries - Enabled COMET to work with OptiMathSat 1.7.3, which uses the MathSat 5 syntax. MathSat 5 syntax requires that the -optimization=true flag be passed in order to utilize optimization extensions. - Changed use of pd.append, which is deprecated, to pd.concat. - Removed the silent catching of exceptions, since it prevented me from detecting any errors in OptiMathSat. - Stopped deleting the temporary files that are created, since they automatically delete themselves. (Changes picked from https://github.com/AishwaryaSivaraman/COMET/pull/3) --- src/Solver_OptiMathSat.py | 272 ++++++++++++++++++++++------------ src/Verification_framework.py | 9 +- 2 files changed, 182 insertions(+), 99 deletions(-) diff --git a/src/Solver_OptiMathSat.py b/src/Solver_OptiMathSat.py index 496fb56..9649429 100644 --- a/src/Solver_OptiMathSat.py +++ b/src/Solver_OptiMathSat.py @@ -13,6 +13,7 @@ epsilon = 0.001 +optimatsatsolver_path = "optimathsat -optimization=true" def verifier(monotonic_indices,path,layers,monotonicity_direction,min_dict,max_dict,variable_types,model="",logging="",isUpper = True, prefix_path=""): s = Optimize() @@ -73,22 +74,33 @@ def verifier(monotonic_indices,path,layers,monotonicity_direction,min_dict,max_d f.write(sexpr) f.write("(exit)") start_time = datetime.now() - try: - optimatsatsolver_path = "optimathsat" - cmd = optimatsatsolver_path+" "+prefix_path+tf.name - p = subprocess.Popen([cmd, ""], shell=True, - stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) - p.wait() - returned_value = p.stdout.read().decode('UTF-8') - elapsed_time = datetime.now() - start_time - if "unsat" in returned_value: - return "UNSAT", None, elapsed_time.total_seconds() - else: - if "sat" in returned_value: - return "SAT", returned_value, elapsed_time.total_seconds() - except Exception as e: - print("Exception ", e) - return "Exception while verifying",None, None + cmd = optimatsatsolver_path+" "+prefix_path+tf.name + p = subprocess.Popen([cmd, ""], shell=True, + stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) + p.wait() + returned_value = p.stdout.read().decode('UTF-8') + elapsed_time = datetime.now() - start_time + if "unsat" in returned_value: + return "UNSAT", None, elapsed_time.total_seconds() + else: + if "sat" in returned_value: + return "SAT", returned_value, elapsed_time.total_seconds() + # try: + # optimatsatsolver_path = "optimathsat" + # cmd = optimatsatsolver_path+" "+prefix_path+tf.name + # p = subprocess.Popen([cmd, ""], shell=True, + # stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) + # p.wait() + # returned_value = p.stdout.read().decode('UTF-8') + # elapsed_time = datetime.now() - start_time + # if "unsat" in returned_value: + # return "UNSAT", None, elapsed_time.total_seconds() + # else: + # if "sat" in returned_value: + # return "SAT", returned_value, elapsed_time.total_seconds() + # except Exception as e: + # print("Exception ", e) + # return "Exception while verifying",None, None def counter_pair_generator(datapoint, monotonic_index, index,label,path,layers,monotonicity_direction,min,max,variable_types,model="",logging="",isUpper = True, prefix_path=""): s = Optimize() @@ -177,32 +189,54 @@ def counter_pair_generator(datapoint, monotonic_index, index,label,path,layers,m # f.write("(get-value ("+variableNameForIndex+"))\n(get-value (f_y))\n(exit)") f.write("(get-value (x"+str(monotonic_index)+"))\n(get-value ("+variableNameForIndex+"))\n(get-value (diff))\n(exit)") start_time = time.time() - try: - optimatsatsolver_path = "optimathsat" - cmd = optimatsatsolver_path+" "+prefix_path+tf.name - elapsed_time = time.time() - start_time - p = subprocess.Popen([cmd, ""], shell=True, - stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) - p.wait() - elapsed_time = time.time() - start_time - # subprocess.call(cmd,shell = True) - returned_value = p.stdout.read().decode('UTF-8') - if "unsat" in returned_value: - logging.debug("Unsat: No model") - return None, elapsed_time,index - returned_values = returned_value.splitlines() - solved_vals = [] - for v in returned_values: - if "sat" in v: - continue - name, val = parseSexp(v) - if 'x' in dumps(name) or 'y' in dumps(name): - solved_vals.append(val) - return solved_vals,elapsed_time,index - except Exception as e: - print("Exception ", e) - elapsed_time = time.time() - start_time - return None,elapsed_time,index + + cmd = optimatsatsolver_path+" "+prefix_path+tf.name + elapsed_time = time.time() - start_time + p = subprocess.Popen([cmd, ""], shell=True, + stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) + p.wait() + elapsed_time = time.time() - start_time + # subprocess.call(cmd,shell = True) + returned_value = p.stdout.read().decode('UTF-8') + if "unsat" in returned_value: + logging.debug("Unsat: No model") + return None, elapsed_time,index + returned_values = returned_value.splitlines() + solved_vals = [] + for v in returned_values: + if "sat" in v: + continue + name, val = parseSexp(v) + if 'x' in dumps(name) or 'y' in dumps(name): + solved_vals.append(val) + return solved_vals,elapsed_time,index + + # try: + # optimatsatsolver_path = "optimathsat" + # cmd = optimatsatsolver_path+" "+prefix_path+tf.name + # elapsed_time = time.time() - start_time + # p = subprocess.Popen([cmd, ""], shell=True, + # stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) + # p.wait() + # elapsed_time = time.time() - start_time + # # subprocess.call(cmd,shell = True) + # returned_value = p.stdout.read().decode('UTF-8') + # if "unsat" in returned_value: + # logging.debug("Unsat: No model") + # return None, elapsed_time,index + # returned_values = returned_value.splitlines() + # solved_vals = [] + # for v in returned_values: + # if "sat" in v: + # continue + # name, val = parseSexp(v) + # if 'x' in dumps(name) or 'y' in dumps(name): + # solved_vals.append(val) + # return solved_vals,elapsed_time,index + # except Exception as e: + # print("Exception ", e) + # elapsed_time = time.time() - start_time + # return None,elapsed_time,index def nn_encoding(variableMap, weightDict, type_nn,layers,biasDict,s): @@ -220,7 +254,7 @@ def nn_encoding(variableMap, weightDict, type_nn,layers,biasDict,s): return encoding -def counter_example_generator_upper_env(datapoint, monotonic_indices, label, path, layers, monotonicity_direction, min_dict, max_dict, variable_types, logging="", prefix_path="", isClassification = False): +def counter_example_generator_upper_env(datapoint, monotonic_indices, label, path, layers, monotonicity_direction, min_dict, max_dict, variable_types, logging, prefix_path="", isClassification = False): s = Optimize() variableMap ={} variableMapF2 ={} @@ -304,7 +338,7 @@ def counter_example_generator_upper_env(datapoint, monotonic_indices, label, pat f.write("(get-value ("+variableNameForIndex+"))\n") f.write("(get-value (f_y))\n(exit)") - return solve(logging,variable_types,monotonic_indices,input_features,datapoint, tf,prefix_path) + return solve(logging,variable_types,monotonic_indices,input_features,datapoint, tf.name,prefix_path) def counter_example_generator_lower_env(datapoint, monotonic_indices, label, path, layers, monotonicity_direction, min_dict, max_dict, variable_types, logging="", prefix_path="", isClassification = False): s = Optimize() @@ -390,7 +424,7 @@ def counter_example_generator_lower_env(datapoint, monotonic_indices, label, pat f.write("(get-value ("+variableNameForIndex+"))\n") f.write("(get-value (f_y))\n(exit)") - return solve(logging, variable_types, monotonic_indices, input_features, datapoint, tf, prefix_path) + return solve(logging, variable_types, monotonic_indices, input_features, datapoint, tf.name, prefix_path) def parseSexp(sexp): parsed_sexp = loads(sexp) @@ -405,61 +439,107 @@ def parseSexp(sexp): return (parsed_sexp[0][0],val) -def solve(logging, variable_types,monotonic_indices,input_features,datapoint, smtFileName = "",prefix_path=""): +def solve(logging, variable_types,monotonic_indices,input_features,datapoint, smtFileName,prefix_path=""): start_time = time.time() - try: - optimatsatsolver_path = "optimathsat" - cmd = optimatsatsolver_path+" "+ prefix_path +smtFileName.name - - elapsed_time = time.time() - start_time - p = subprocess.Popen([cmd, ""], shell=True, - stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) - p.wait() - elapsed_time = time.time() - start_time - counter_examples = [] - returned_value = p.stdout.read().decode('UTF-8') - if "unsat" in returned_value: - logging.debug("Unsat: No model") - return None, elapsed_time, None - - noOfLines = len(returned_value.splitlines()) - f_y_parsedsexp = loads(returned_value.splitlines()[noOfLines-1]) - f_y = 0.0 - if '-' in returned_value.splitlines()[noOfLines-1]: - f_y = -1 * float((1.0*f_y_parsedsexp[0][1][1][1])/f_y_parsedsexp[0][1][1][2]) + cmd = optimatsatsolver_path+" "+ prefix_path +smtFileName + + elapsed_time = time.time() - start_time + p = subprocess.Popen([cmd, ""], shell=True, + stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) + p.wait() + elapsed_time = time.time() - start_time + counter_examples = [] + returned_value = p.stdout.read().decode('UTF-8') + if "unsat" in returned_value: + logging.debug("Unsat: No model") + return None, elapsed_time, None + + noOfLines = len(returned_value.splitlines()) + f_y_parsedsexp = loads(returned_value.splitlines()[noOfLines-1]) + + f_y = 0.0 + if '-' in returned_value.splitlines()[noOfLines-1]: + f_y = -1 * float((1.0*f_y_parsedsexp[0][1][1][1])/f_y_parsedsexp[0][1][1][2]) + else: + f_y = float((1.0*f_y_parsedsexp[0][1][1])/f_y_parsedsexp[0][1][2]) + + cg_parsedsexp = {} + count = 1 + for monotonic_index in monotonic_indices: + cg_parsed = loads(returned_value.splitlines()[count]) + cg = 0 + if variable_types[monotonic_index] == "Int": + cg = int(cg_parsed[0][1]) else: - f_y = float((1.0*f_y_parsedsexp[0][1][1])/f_y_parsedsexp[0][1][2]) - - cg_parsedsexp = {} - count = 1 - for monotonic_index in monotonic_indices: - cg_parsed = loads(returned_value.splitlines()[count]) - cg = 0 - if variable_types[monotonic_index] == "Int": - cg = int(cg_parsed[0][1]) - else: - if '/' in returned_value.splitlines()[count]: - if '-' in returned_value.splitlines()[count]: - cg = -1 * float(cg_parsed[0][1][1][1]/cg_parsed[0][1][1][2]) - else: - cg = float(cg_parsed[0][1][1]/cg_parsed[0][1][2]) + if '/' in returned_value.splitlines()[count]: + if '-' in returned_value.splitlines()[count]: + cg = -1 * float(cg_parsed[0][1][1][1]/cg_parsed[0][1][1][2]) else: - cg = float(cg_parsed[0][1]) - count = count + 1 - cg_parsedsexp[monotonic_index] = cg - - logging.debug('violation = %2f'%(f_y)) - for i in range(0,input_features): - if i in monotonic_indices: - datapoint[i] = cg_parsedsexp[i] - os.remove(prefix_path +smtFileName.name) - return datapoint,elapsed_time,f_y - except Exception as e: - print("Exception "+ str(e)) - elapsed_time = time.time() - start_time - os.remove(prefix_path +smtFileName.name) - return None,elapsed_time,None + cg = float(cg_parsed[0][1][1]/cg_parsed[0][1][2]) + else: + cg = float(cg_parsed[0][1]) + count = count + 1 + cg_parsedsexp[monotonic_index] = cg + + logging.debug('violation = %2f'%(f_y)) + for i in range(0,input_features): + if i in monotonic_indices: + datapoint[i] = cg_parsedsexp[i] + return datapoint,elapsed_time,f_y + # try: + # optimatsatsolver_path = "optimathsat" + # cmd = optimatsatsolver_path+" "+ prefix_path +smtFileName.name + + # elapsed_time = time.time() - start_time + # p = subprocess.Popen([cmd, ""], shell=True, + # stdin=subprocess.PIPE, stdout=subprocess.PIPE, close_fds=True) + # p.wait() + # elapsed_time = time.time() - start_time + # counter_examples = [] + # returned_value = p.stdout.read().decode('UTF-8') + # if "unsat" in returned_value: + # logging.debug("Unsat: No model") + # return None, elapsed_time, None + + # noOfLines = len(returned_value.splitlines()) + # f_y_parsedsexp = loads(returned_value.splitlines()[noOfLines-1]) + + # f_y = 0.0 + # if '-' in returned_value.splitlines()[noOfLines-1]: + # f_y = -1 * float((1.0*f_y_parsedsexp[0][1][1][1])/f_y_parsedsexp[0][1][1][2]) + # else: + # f_y = float((1.0*f_y_parsedsexp[0][1][1])/f_y_parsedsexp[0][1][2]) + + # cg_parsedsexp = {} + # count = 1 + # for monotonic_index in monotonic_indices: + # cg_parsed = loads(returned_value.splitlines()[count]) + # cg = 0 + # if variable_types[monotonic_index] == "Int": + # cg = int(cg_parsed[0][1]) + # else: + # if '/' in returned_value.splitlines()[count]: + # if '-' in returned_value.splitlines()[count]: + # cg = -1 * float(cg_parsed[0][1][1][1]/cg_parsed[0][1][1][2]) + # else: + # cg = float(cg_parsed[0][1][1]/cg_parsed[0][1][2]) + # else: + # cg = float(cg_parsed[0][1]) + # count = count + 1 + # cg_parsedsexp[monotonic_index] = cg + + # logging.debug('violation = %2f'%(f_y)) + # for i in range(0,input_features): + # if i in monotonic_indices: + # datapoint[i] = cg_parsedsexp[i] + # os.remove(prefix_path +smtFileName.name) + # return datapoint,elapsed_time,f_y + # except Exception as e: + # print("Exception "+ str(e)) + # elapsed_time = time.time() - start_time + # os.remove(prefix_path +smtFileName.name) + # return None,elapsed_time,None def generateFinalLayerConstraint(z3LayerConstraints,weights,bias): count =0 diff --git a/src/Verification_framework.py b/src/Verification_framework.py index a5a3525..f13cef4 100644 --- a/src/Verification_framework.py +++ b/src/Verification_framework.py @@ -217,10 +217,13 @@ def verification(data_path, log_file, n_folds, monotonic_indices): counter_batch = pd.DataFrame(counter_batch, columns= column_names) batch_labels = pd.DataFrame(batch_labels) - train_batch = original_train.append(counter_batch, ignore_index = True,sort=False) - train_batch_label = original_label.append(batch_labels, ignore_index = True) + # train_batch = original_train.append(counter_batch, ignore_index = True,sort=False) + # train_batch_label = original_label.append(batch_labels, ignore_index = True) + train_batch = pd.concat([original_train, counter_batch], ignore_index = True) + train_batch_label = pd.concat([original_label, batch_labels], ignore_index = True) - logging.debug('Mean Squared Error after batch %d/%d counterexample: '%((temp_batch_count,len(batches)))) + # logging.debug('Mean Squared Error after batch %d/%d counterexample: '%((temp_batch_count,len(batches)))) + logging.debug(f'Mean Squared Error after batch {temp_batch_count}/{len(batches)} counterexample: ') NN_model = update_model(train_batch, train_batch_label, NN_model,getConfigurations(),update_batch)