seL4-l4v-10.1.1/graph-refine/solver.py

14 This tool requires the use of an SMT solver.
20 The .solverlist format is one solver per line, e.g.
22 # SONOLAR is the strongest offline solver in our experiments.
27 # Z3 is a useful online solver. Use of Z3 in offline mode is not recommended,
32 N.B. only ONE online solver is needed, so Z3 is redundant in the above.
37 The name is used to identify the solver. The second token specifies
38 the solver mode. Solvers in "fast" or "online" mode must support all
40 the solver will be executed once per query, and push/pop will not be used.
42 The remainder of each line is a shell command that executes the solver in
44 limit, after which the offline solver will be run.
46 The first online solver will be used. The offline solvers will be used in
78 		print 'solver.py: solver list could not be parsed'
100 			print "solver.py: '.solverlist' missing"
134 			print "solver.py: strategy element %r" % bits
141 def parse_config_change (config, solver):
150 			solver.mem_mode = rhs
165 			print "solver.py: strategy option %r" % nm
167 			print "not an offline solver (required for parallel use)"
235 		return '(cannot import psutil, cannot time solver)'
674 	"""retreives responses from a solver until parens match"""
764 				solv.close ('active solver limit')
767 			solver = use_this_solver
769 			solver = self.fast_solver
771 		self.online_solver = subprocess.Popen (solver.args,
773 			stderr = devnull, preexec_fn = preexec (solver.timeout))
776 		for msg in self.preamble (solver):
833 				trace ('restarting solver')
1064 			# couldn't get a useful response from either solver.
1067 			trace ('last solver result %r' % response)
1083 	def write_solv_script (self, f, input_msgs, solver = slow_solver,
1085 		if solver.mem_mode == '8':
1089 		for msg in self.preamble (solver):
1106 		solver = self.slow_solver
1108 			solver = use_this_solver
1109 		if not solver:
1110 			return 'no-slow-solver'
1116 			solver = solver)
1119 		proc = subprocess.Popen (solver.args,
1138 			solver = use_this_solver
1140 			solver = self.slow_solver
1143 			timeout = solver.timeout, use_this_solver = solver)
1150 			trace ('WARNING no unsat core from %s' % solver.name)
1159 		trace ('Got %r from %s.' % (response, solver.name))
1179 		trace ('  --> new parallel solver %s' % str (k))
1182 			raise IndexError ('duplicate parallel solver ID', k)
1183 		solver = self.slow_solver
1185 			solver = use_this_solver
1187 			timeout = solver.timeout, use_this_solver = solver)
1188 		self.parallel_solvers[k] = (hyps, proc, output, solver, model)
1201 		(hyps, proc, output, solver, model) = self.parallel_solvers[k]
1204 		trace ('  <-- parallel solver %s closed: %s' % (k, response))
1207 			trace ('SMT conversation problem in parallel solver')
1208 		trace ('Got %r from %s in parallel.' % (response, solver.name))
1223 			# just drop this solver at this point
1292 			[self.add_parallel_solver ((solver.name, strat, k),
1293 					[goal], use_this_solver = solver,
1295 				for (solver, strat) in self.strategy
1310 				ks = [(solver.name, strat, k)
1311 					for (solver, strat) in self.strategy]
1353 				self.solver = None
1512 		# the most recently returned model. that expires the solver
1863 	def narrow_unsat_core (self, solver, asserts):
1864 		process = subprocess.Popen (solver[1],
1866 			preexec_fn = preexec (solver[2]))
1867 		self.write_solv_script (process.stdin, [], solver = solver,
1881 		trace ('got response %r from %s' % (res, solver[0]))
1896 			for solver in unsat_solver_loop:
1897 				asserts = self.narrow_unsat_core (solver,
2184 	"""quick test that the solver supports the needed features."""
2201 	print 'Loaded solver list from %s' % solverlist