diff --git a/marco.py b/marco.py index 72a80f7..91e37cf 100755 --- a/marco.py +++ b/marco.py @@ -128,7 +128,12 @@ def setup_solvers(args): # create appropriate constraint solver if args.cnf or infile.name.endswith('.cnf') or infile.name.endswith('.cnf.gz') or infile.name.endswith('.gcnf') or infile.name.endswith('.gcnf.gz'): if args.force_minisat: - csolver = CNFsolvers.MinisatSubsetSolver(infile) + try: + csolver = CNFsolvers.MinisatSubsetSolver(infile) + except OSError as e: + sys.stderr.write("ERROR: Unable to load pyminisolvers library.\nRun 'make -C pyminisolvers' to compile the library.\n\n") + sys.stderr.write(str(e) + "\n") + sys.exit(1) else: try: csolver = CNFsolvers.MUSerSubsetSolver(infile) @@ -136,6 +141,10 @@ def setup_solvers(args): sys.stderr.write("ERROR: Unable to use MUSer2 for MUS extraction.\nUse --force-minisat to use Minisat instead (NOTE: it will be much slower.)\n\n") sys.stderr.write(str(e) + "\n") sys.exit(1) + except OSError as e: + sys.stderr.write("ERROR: Unable to load pyminisolvers library.\nRun 'make -C pyminisolvers' to compile the library.\n\n") + sys.stderr.write(str(e) + "\n") + sys.exit(1) infile.close() elif args.smt or infile.name.endswith('.smt2'): try: @@ -159,10 +168,15 @@ def setup_solvers(args): else: varbias = (args.bias == 'MUSes') # High bias (True) for MUSes, low (False) for MCSes - if args.MAX or args.smus: - msolver = mapsolvers.MinicardMapSolver(n=csolver.n, bias=varbias) - else: - msolver = mapsolvers.MinisatMapSolver(n=csolver.n, bias=varbias, dump=args.dump_map) + try: + if args.MAX or args.smus: + msolver = mapsolvers.MinicardMapSolver(n=csolver.n, bias=varbias) + else: + msolver = mapsolvers.MinisatMapSolver(n=csolver.n, bias=varbias, dump=args.dump_map) + except OSError as e: + sys.stderr.write("ERROR: Unable to load pyminisolvers library.\nRun 'make -C pyminisolvers' to compile the library.\n\n") + sys.stderr.write(str(e) + "\n") + sys.exit(1) return (csolver, msolver)