<commit_before>#!/usr/bin/env python

# pylint: disable=F0401

import time
import logging

l = logging.getLogger("claripy.solvers.core_solver")
l_timing = logging.getLogger("claripy.solvers.core_solver_timing")

# we need to:
#  receive constraints
#  make a hash of the constraints
#  check for existing solution in the solution cache
#  solve

from .solver import Solver

import itertools
symbolic_count = itertools.count()

class CoreSolver(Solver):
	def __init__(self, claripy, solver_backend=None, results_backend=None, timeout=None, solver=None, result=None):
		Solver.__init__(self, claripy, timeout=timeout, solver_backend=solver_backend, results_backend=results_backend, result=result)

		self._to_add = [ ]
		self.constraints = [ ]
		self._solver = solver
		self.variables = set()

	def downsize(self):
		self._solver = None

	def _get_solver(self):
		if self._solver is None:
			self._solver = self._create_solver()
			self._solver_backend.add_exprs(self._solver, self.constraints)
		elif len(self._to_add) > 0:
			self._solver_backend.add_exprs(self._solver, self._to_add)
			self._to_add = [ ]

		return self._solver

	#
	# Util stuff
	#

	def _create_solver(self):
		solver = self._solver_backend.solver()
		solver.set('timeout', self._timeout)
		return solver

	#
	# Constraints
	#

	def add(self, *constraints):
		l.debug("%s.add(*%s)", self, constraints)

		if len(constraints) == 0:
			return None

		if type(constraints[0]) in (list, tuple):
			raise ValueError("don't pass lists to Solver.add()!")

		to_add = [ ]
		for e in constraints:
			#e_simp = self._solver_backend.simplify_expr(e)
			e_simp = e
			if not e_simp.symbolic and self._results_backend.convert_expr(e_simp):
				continue
			elif not e_simp.symbolic and not self._results_backend.convert_expr(e_simp):
				self._result = Result(False, { })
				f = self._claripy.BoolVal(False)
				self.constraints.append(f)
				self._to_add.append(f)
				return

			self._result = None
			self._simplified = False
			self.constraints.append(e_simp)
			to_add.append(e_simp)
			self.variables.update(e_simp.variables)

		if self._solver is not None:
			self._to_add += to_add
			#self._solver_backend.add_exprs(self._solver, to_add)

	#
	# Solving
	#

	def _solve(self, extra_constraints=None):
		l.debug("%s.solve()", self)

		# check it!
		l_timing.debug("Checking SATness of %d constraints", len(self.constraints))
		a = time.time()
		r = self._solver_backend.results(self._get_solver(), extra_constraints=self._solver_backend.convert_exprs(extra_constraints) if extra_constraints is not None else None, results_backend=self._results_backend)
		b = time.time()
		l_timing.debug("... %s in %s seconds", r.sat, b - a)
		return r


	def _eval(self, e, n, extra_constraints=None):
		l.debug("%s._eval()", self)

		if n == 1 and extra_constraints is None:
			l.debug("... n == 1: calling the results_backend")
			try:<commit_msg>don't solve empty constraint sets<commit_after>#!/usr/bin/env python

# pylint: disable=F0401

import time
import logging

l = logging.getLogger("claripy.solvers.core_solver")
l_timing = logging.getLogger("claripy.solvers.core_solver_timing")

# we need to:
#  receive constraints
#  make a hash of the constraints
#  check for existing solution in the solution cache
#  solve

from .solver import Solver

import itertools
symbolic_count = itertools.count()

class CoreSolver(Solver):
	def __init__(self, claripy, solver_backend=None, results_backend=None, timeout=None, solver=None, result=None):
		Solver.__init__(self, claripy, timeout=timeout, solver_backend=solver_backend, results_backend=results_backend, result=result)

		self._to_add = [ ]
		self.constraints = [ ]
		self._solver = solver
		self.variables = set()

	def downsize(self):
		self._solver = None

	def _get_solver(self):
		if self._solver is None:
			self._solver = self._create_solver()
			self._solver_backend.add_exprs(self._solver, self.constraints)
		elif len(self._to_add) > 0:
			self._solver_backend.add_exprs(self._solver, self._to_add)
			self._to_add = [ ]

		return self._solver

	#
	# Util stuff
	#

	def _create_solver(self):
		solver = self._solver_backend.solver()
		solver.set('timeout', self._timeout)
		return solver

	#
	# Constraints
	#

	def add(self, *constraints):
		l.debug("%s.add(*%s)", self, constraints)

		if len(constraints) == 0:
			return None

		if type(constraints[0]) in (list, tuple):
			raise ValueError("don't pass lists to Solver.add()!")

		to_add = [ ]
		for e in constraints:
			#e_simp = self._solver_backend.simplify_expr(e)
			e_simp = e
			if not e_simp.symbolic and self._results_backend.convert_expr(e_simp):
				continue
			elif not e_simp.symbolic and not self._results_backend.convert_expr(e_simp):
				self._result = Result(False, { })
				f = self._claripy.BoolVal(False)
				self.constraints.append(f)
				self._to_add.append(f)
				return

			self._result = None
			self._simplified = False
			self.constraints.append(e_simp)
			to_add.append(e_simp)
			self.variables.update(e_simp.variables)

		if self._solver is not None:
			self._to_add += to_add
			#self._solver_backend.add_exprs(self._solver, to_add)

	#
	# Solving
	#

	def _solve(self, extra_constraints=None):
		if len(self.constraints) == 0 and extra_constraints is None:
			return Result(True, { })

		l.debug("%s.solve()", self)

		# check it!
		l_timing.debug("Checking SATness of %d constraints", len(self.constraints))
		a = time.time()
		r = self._solver_backend.results(self._get_solver(), extra_constraints=self._solver_backend.convert_exprs(extra_constraints) if extra_constraints is not None else None, results_backend=self._results_backend)
		b = time.time()
		l_timing.debug("... %s in %s seconds", r.sat, b - a)
		return r


	def _eval(self, e, n, extra_constraints=None):
		l.debug("%s._eval()", self)

		if n == 1 and extra_constraints is None:
			l.debug("... n == 1: calling the results_backend")
			try:
{'fraction_non_alphanumeric': 0.12153012863913337, 'fraction_numerical': 0.003215978334461747, 'mean_word_length': 4.294802867383512, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6514732', 'n_tokens_mistral': 2365, 'n_tokens_neox': 2132, 'n_words': 454}