Source code for claripy.backends.backend_smtlib_solvers.abc_popen

import subprocess
import logging

import re
from . import SMTLibSolverBackend, PopenSolverProxy
from ...errors import MissingSolverError

log = logging.getLogger(__name__)

[docs]def get_version(): try: version_string = subprocess.check_output(["abc", "--help"]).decode("utf-8") # version_match = re.match('This is CVC4 version (.*)\n', version_string) # if not version_match: # return False, None, "Found malformed version string: {}".format(version_string) return True, None, None # True,, None except subprocess.CalledProcessError as ex: return False, None, f"Not found, error: {ex}" except OSError as ex: return False, None, f"Not found, error: {ex}"
[docs]class ABCProxy(PopenSolverProxy):
[docs] def __init__(self): self.installed = False p = None super().__init__(p)
[docs] def create_process(self): if not IS_INSTALLED: raise MissingSolverError("ABC not found! Please install ABC before using this backend") p = subprocess.Popen(["abc"], stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.PIPE) self.installed = True return p
[docs]class SolverBackendABC(SMTLibSolverBackend):
[docs] def solver(self, timeout=None, max_memory=None): """ This function should return an instance of whatever object handles solving for this backend. For example, in Z3, this would be z3.Solver(). """ return ABCProxy()
from ... import backend_manager as backend_manager backend_manager.backends._register_backend(SolverBackendABC(), "smtlib_abc", False, False)