Skip to content

Commit

Permalink
Some updates to make code work with new changes in libraries
Browse files Browse the repository at this point in the history 
- 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 AishwaryaSivaraman#3)
  • Loading branch information
@sgomber
sgomber committed Nov 12, 2022
1 parent 1357afa commit 509cbd9
Show file tree
Hide file tree
Showing 2 changed files with 182 additions and 99 deletions.
272 changes: 176 additions & 96 deletions src/Solver_OptiMathSat.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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):
Expand All @@ -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 ={}
Expand Down Expand Up @@ -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()
Expand Down Expand Up @@ -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)
Expand All @@ -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
Expand Down
9 changes: 6 additions & 3 deletions src/Verification_framework.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)


Expand Down

0 comments on commit 509cbd9

Please sign in to comment.