Skip to content

Commit

Permalink
refactor codes using ai
Browse files Browse the repository at this point in the history
  • Loading branch information
@hadipourh
hadipourh committed Nov 4, 2024
1 parent fb4d610 commit aa9b86e
Show file tree
Hide file tree
Showing 8 changed files with 462 additions and 817 deletions.
228 changes: 66 additions & 162 deletions autoguess.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,123 +36,61 @@
import os
from config import TEMP_DIR

def startsearch(tool_parameters):
def start_search(tool_parameters):
"""
Starts the search tool for the given parameters
"""

# Handle program flow
if tool_parameters["solver"] == 'milp':
search.search_using_milp(tool_parameters)
elif tool_parameters["solver"] == 'sat':
search.search_using_sat(tool_parameters)
elif tool_parameters["solver"] == 'smt':
search.search_using_smt(tool_parameters)
elif tool_parameters["solver"] == 'cp':
search.search_using_cp(tool_parameters)
elif tool_parameters["solver"] == 'groebner':
search.search_using_groebnerbasis(tool_parameters)
elif tool_parameters["solver"] == 'mark':
search.search_using_mark(tool_parameters)
elif tool_parameters["solver"] == 'elim':
search.search_using_elim(tool_parameters)
solver_map = {
'milp': search.search_using_milp,
'sat': search.search_using_sat,
'smt': search.search_using_smt,
'cp': search.search_using_cp,
'groebner': search.search_using_groebnerbasis,
'mark': search.search_using_mark,
'elim': search.search_using_elim
}

solver = tool_parameters.get("solver")
if solver in solver_map:
solver_map[solver](tool_parameters)
else:
print('Choose the solver from the following options please:%s' %
'cp, milp, sat, smt, groebner, mark')
return
print('Choose the solver from the following options please: cp, milp, sat, smt, groebner, mark')

def checkenvironment():
def check_environment():
"""
Basic checks if the environment is set up correctly
"""
os.makedirs(TEMP_DIR, exist_ok=True)

if not os.path.exists(TEMP_DIR):
os.makedirs(TEMP_DIR)
return

def loadparameters(args):
def load_parameters(args):
"""
Get parameters from the argument list and inputfile.
Get parameters from the argument list and input file.
"""

# Load default values
params = {"inputfile": "./ciphers/AES/relationfile_aes1kp_1r_mg6_ms14.txt",
"outputfile": "output",
"maxguess": 50,
"maxsteps": 5,
"solver": 'groebner',
"milpdirection": 'min',
"timelimit": -1,
"cpsolver": 'or-tools',
"satsolver": 'cadical153',
"smtsolver": 'z3',
"cpoptimization": 1,
"tikz": 0,
"preprocess" : 0,
"D" : 2,
"term_ordering": 'degrevlex',
"overlapping_number": 2,
"cnf_to_anf_conversion": 'simple',
"dglayout": "dot",
"log": 0}

# Override parameters if they are set on commandline
if args.inputfile:
params["inputfile"] = args.inputfile[0]

if args.outputfile:
params["outputfile"] = args.outputfile[0]

if args.maxguess:
params["maxguess"] = args.maxguess[0]

if args.maxsteps:
params["maxsteps"] = args.maxsteps[0]

if args.solver:
params["solver"] = args.solver[0]

if args.milpdirection:
params["milpdirection"] = args.milpdirection[0]

if args.cpsolver:
params["cpsolver"] = args.cpsolver[0]

if args.smtsolver:
params["smtsolver"] = args.smtsolver[0]

if args.satsolver:
params["satsolver"] = args.satsolver[0]

if args.timelimit:
params["timelimit"] = args.timelimit[0]

if args.cpoptimization:
params["cpoptimization"] = args.cpoptimization[0]

if args.tikz:
params["tikz"] = args.tikz[0]

if args.preprocess:
params["preprocess"] = args.preprocess[0]

if args.D:
params["D"] = args.D[0]

if args.term_ordering:
params["term_ordering"] = args.term_ordering[0]

if args.overlapping_number:
params["overlapping_number"] = args.overlapping_number[0]

if args.cnf_to_anf_conversion:
params["cnf_to_anf_conversion"] = args.cnf_to_anf_conversion[0]

if args.dglayout:
params["dglayout"] = args.dglayout[0]

if args.log:
params["log"] = args.log[0]
params = {
"inputfile": "./ciphers/Example1/relationfile.txt",
"outputfile": "output",
"maxguess": 10,
"maxsteps": 5,
"solver": 'groebner',
"milpdirection": 'min',
"timelimit": -1,
"cpsolver": 'or-tools',
"satsolver": 'cadical153',
"smtsolver": 'z3',
"cpoptimization": 1,
"tikz": 0,
"preprocess": 0,
"D": 2,
"term_ordering": 'degrevlex',
"overlapping_number": 2,
"cnf_to_anf_conversion": 'simple',
"dglayout": "dot",
"log": 1
}

for key in params.keys():
if getattr(args, key, None):
params[key] = getattr(args, key)[0]

return params

Expand All @@ -167,64 +105,30 @@ def main():
" the algebraic method based on Groebner basis",
formatter_class=RawTextHelpFormatter)
parser.add_argument('-i', '--inputfile', nargs=1, help="Use an input file in plain text format")
parser.add_argument('-o', '--outputfile', nargs=1, help="Use an output file to"
" write the output into it")
parser.add_argument('-mg', '--maxguess', nargs=1, type=int,
help="An upper bound for the number of guessed variables")
parser.add_argument('-ms', '--maxsteps', nargs=1, type=int,
help="An integer number specifying the depth of search")
parser.add_argument('-s', '--solver', nargs=1,
choices=['cp', 'milp', 'sat', 'smt', 'groebner'], help="cp = solve the problem using CP solvers\n"
"milp = solve the problem using the MILP solvers\n"
"sat = solve the problem using the SAT solvers\n"
"smt = solve the problem using the SMT solvers\n"
"groebner = solve the problem using the Groebner basis algorithm\n"
)
parser.add_argument('-milpd', '--milpdirection', nargs=1,
choices=['min', 'max'], help="min = convert the problem to a minimization problem looking for the minimal set of guessed variables.\n"
"max = convert the problem to a maximization problem in which the known variables in final state are maximized,\n"
"when the size of the initially known variables is equal or less than \"maxguess\"\n")
parser.add_argument('-cps', '--cpsolver', nargs=1, type=str,
choices=['gecode', 'chuffed', 'coin-bc', 'gurobi', 'picat', 'scip', 'choco', 'or-tools'], help="\n")
parser.add_argument('-sats', '--satsolver', nargs=1, type=str,
choices=['cadical153', 'glucose3', 'glucose4', 'lingeling', 'maplechrono', 'maplecm', 'maplesat', 'minicard', 'minisat22', 'minisat-gh'], help="\n")
parser.add_argument('-smts', '--smtsolver', nargs=1, type=str,
choices=['msat', 'cvc4', 'z3', 'yices', 'btor', 'bdd'], help="\n")
parser.add_argument('-cpopt', '--cpoptimization', nargs=1, type=int, choices=[0, 1],
help="1: Looking for a minimal guess basis \n0: Decides whether a guess basis of size up to \"maxguess\" exists\n")
parser.add_argument('-tl', '--timelimit', nargs=1, type=int,
help="Set a timelimit for the search in seconds\n")
parser.add_argument('-tk', '--tikz', nargs=1, type=int,
help="Set to 1 to generate the tikz code of the determination flow graph\n")
parser.add_argument('-prep', '--preprocess', nargs=1, type=int,
help="Set to 1 to enable the preprocessing phase\n")
parser.add_argument('-D', '--D', nargs=1, type=int,
help="It specifies the degree of Macaulay matrix generated in preprocessing phase\n")
parser.add_argument('-tord', '--term_ordering', nargs=1, type=str,
help="A degree compatible term ordering such as \"degrevlex\" or \"deglex\"\n")
parser.add_argument('-oln', '--overlapping_number', nargs=1, type=int,
help="A positive integer specifying the overlapping number in block-wise CNF to ANF conversion\n")

parser.add_argument('-cnf2anf', '--cnf_to_anf_conversion', nargs=1, type=str, choices=['simple', 'blockwise'],
help="It specifies the CNF to ANF conversion method\n")

parser.add_argument('-dgl', '--dglayout', nargs=1, type=str, choices=["dot", "circo", "twopi", "fdp", \
"neato", "nop", "nop1", "nop2", "osage", "patchwork", "sfdp"],
help="It specifies the layout of determination flow graph\n")

parser.add_argument('-log', '--log', nargs=1, type=int, choices=[0, 1],
help="By setting this parameter to 1, the intermediate generated files such as CP/MILP/SAT models as well as\n"
"some intermediate results are stored inside the temp folder\n")

# Parse command line arguments and construct parameter list.
args = parser.parse_args()
params = loadparameters(args)
parser.add_argument('-o', '--outputfile', nargs=1, help="Use an output file to write the output into it")
parser.add_argument('-mg', '--maxguess', nargs=1, type=int, help="An upper bound for the number of guessed variables")
parser.add_argument('-ms', '--maxsteps', nargs=1, type=int, help="An integer number specifying the depth of search")
parser.add_argument('-s', '--solver', nargs=1, choices=['cp', 'milp', 'sat', 'smt', 'groebner'], help="Choose the solver")
parser.add_argument('-milpd', '--milpdirection', nargs=1, choices=['min', 'max'], help="Choose the MILP direction")
parser.add_argument('-cps', '--cpsolver', nargs=1, type=str, choices=['gecode', 'chuffed', 'coin-bc', 'gurobi', 'picat', 'scip', 'choco', 'or-tools'], help="Choose the CP solver")
parser.add_argument('-sats', '--satsolver', nargs=1, type=str, choices=['cadical153', 'glucose3', 'glucose4', 'lingeling', 'maplechrono', 'maplecm', 'maplesat', 'minicard', 'minisat22', 'minisat-gh'], help="Choose the SAT solver")
parser.add_argument('-smts', '--smtsolver', nargs=1, type=str, choices=['msat', 'cvc4', 'z3', 'yices', 'btor', 'bdd'], help="Choose the SMT solver")
parser.add_argument('-cpopt', '--cpoptimization', nargs=1, type=int, choices=[0, 1], help="CP optimization")
parser.add_argument('-tl', '--timelimit', nargs=1, type=int, help="Set a time limit for the search in seconds")
parser.add_argument('-tk', '--tikz', nargs=1, type=int, help="Generate the tikz code of the determination flow graph")
parser.add_argument('-prep', '--preprocess', nargs=1, type=int, help="Enable the preprocessing phase")
parser.add_argument('-D', '--D', nargs=1, type=int, help="Specify the degree of Macaulay matrix generated in preprocessing phase")
parser.add_argument('-tord', '--term_ordering', nargs=1, type=str, help="Specify the term ordering")
parser.add_argument('-oln', '--overlapping_number', nargs=1, type=int, help="Specify the overlapping number in block-wise CNF to ANF conversion")
parser.add_argument('-cnf2anf', '--cnf_to_anf_conversion', nargs=1, type=str, choices=['simple', 'blockwise'], help="Specify the CNF to ANF conversion method")
parser.add_argument('-dgl', '--dglayout', nargs=1, type=str, choices=["dot", "circo", "twopi", "fdp", "neato", "nop", "nop1", "nop2", "osage", "patchwork", "sfdp"], help="Specify the layout of determination flow graph")
parser.add_argument('-log', '--log', nargs=1, type=int, choices=[0, 1], help="Enable logging of intermediate files")

# Check if environment is setup correctly.
checkenvironment()
args = parser.parse_args()
params = load_parameters(args)

# Start the solver
startsearch(params)
check_environment()
start_search(params)

if __name__ == '__main__':
main()
Loading

0 comments on commit aa9b86e

Please sign in to comment.