aboutsummaryrefslogtreecommitdiffstats
path: root/libs/ezsat/ezsat.cc
Commit message (Expand)AuthorAgeFilesLines
* Fixed various VS warningsClifford Wolf2014-10-181-2/+2
* More win32 (mxe and vs) build fixesClifford Wolf2014-10-171-11/+18
* Not using std::to_string in ezsat (problems with mingw)Clifford Wolf2014-10-111-5/+11
* Renamed TRUE/FALSE to CONST_TRUE/CONST_FALSE because of name collision on Win32Clifford Wolf2014-10-101-60/+60
* Added native support for shift operations to ezSATClifford Wolf2014-07-301-0/+90
* Added ezSAT::keep_cnf() and ezSAT::non_incremental()Clifford Wolf2014-07-211-5/+41
* Merged a few fixes for non-posix systems from github.com/Siesh1oo/yosysClifford Wolf2014-03-111-1/+2
* ezSAT: Added frozen_literal() APIClifford Wolf2014-03-031-0/+14
* ezSAT: Fixed handling of eliminated Literals, added auto-freeze for expressionsClifford Wolf2014-03-031-7/+22
* Added ezSAT::eliminated API to help the SAT solver remember eliminated variablesClifford Wolf2014-03-011-3/+7
* ezSAT bugfix: don't call virtual methods in base class constructorClifford Wolf2014-03-011-2/+2
* Removed ezSAT::assumed() APIClifford Wolf2014-03-011-2/+0
* Removed ezSAT built-in brute-froce solverClifford Wolf2014-03-011-102/+6
* Added support for Minisat::SimpSolver + ezSAT frezze() APIClifford Wolf2014-02-231-6/+27
* Improved non-verbose ezSAT::printDIMACS() formatClifford Wolf2014-02-181-1/+6
* Added ezsat vec_const() apiClifford Wolf2013-11-251-12/+20
* Added ezsat api for creation of anonymous vectorsClifford Wolf2013-08-151-0/+8
* Added SAT support for $div and $mod cellsClifford Wolf2013-08-111-0/+6
* Added timout functionality to SAT solverClifford Wolf2013-06-201-0/+3
* Fixed gcc build (c++11 stuff in ezSAT)Clifford Wolf2013-06-121-0/+3
* Fixes and improvements in ezSAT libraryClifford Wolf2013-06-081-3/+39
* Improved sat generator and sat_solve passClifford Wolf2013-06-071-0/+4
* Added ezSAT libraryClifford Wolf2013-06-071-0/+1221
pre { line-height: 125%; margin: 0; } td.linenos pre { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; } span.linenos { color: #000000; background-color: #f0f0f0; padding: 0 5px 0 5px; } td.linenos pre.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; } span.linenos.special { color: #000000; background-color: #ffffc0; padding: 0 5px 0 5px; } .highlight .hll { background-color: #ffffcc } .highlight { background: #ffffff; } .highlight .c { color: #888888 } /* Comment */ .highlight .err { color: #a61717; background-color: #e3d2d2 } /* Error */ .highlight .k { color: #008800; font-weight: bold } /* Keyword */ .highlight .ch { color: #888888 } /* Comment.Hashbang */ .highlight .cm { color: #888888 } /* Comment.Multiline */ .highlight .cp { color: #cc0000; font-weight: bold } /* Comment.Preproc */ .highlight .cpf { color: #888888 } /* Comment.PreprocFile */ .highlight .c1 { color: #888888 } /* Comment.Single */ .highlight .cs { color: #cc0000; font-weight: bold; background-color: #fff0f0 } /* Comment.Special */ .highlight .gd { color: #000000; background-color: #ffdddd } /* Generic.Deleted */ .highlight .ge { font-style: italic } /* Generic.Emph */ .highlight .gr { color: #aa0000 } /* Generic.Error */ .highlight .gh { color: #333333 } /* Generic.Heading */ .highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */ .highlight .go { color: #888888 } /* Generic.Output */ .highlight .gp { color: #555555 } /* Generic.Prompt */ .highlight .gs { font-weight: bold } /* Generic.Strong */ .highlight .gu { color: #666666 } /* Generic.Subheading */ .highlight .gt { color: #aa0000 } /* Generic.Traceback */ .highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */ .highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */ .highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */ .highlight .kp { color: #008800 } /* Keyword.Pseudo */ .highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */ .highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */ .highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */ .highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */ .highlight .na { color: #336699 } /* Name.Attribute */ .highlight .nb { color: #003388 } /* Name.Builtin */ .highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */ .highlight .no { color: #003366; font-weight: bold } /* Name.Constant */ .highlight .nd { color: #555555 } /* Name.Decorator */ .highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */ .highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */ .highlight .nl { color: #336699; font-style: italic } /* Name.Label */ .highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */ .highlight .py { color: #336699; font-weight: bold } /* Name.Property */ .highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */ .highlight .nv { color: #336699 } /* Name.Variable */ .highlight .ow { color: #008800 } /* Operator.Word */ .highlight .w { color: #bbbbbb } /* Text.Whitespace */ .highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */ .highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */ .highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */ .highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */ .highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */ .highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */ .highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */ .highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */ .highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */ .highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */ .highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */ .highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */ .highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */ .highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */ .highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */ .highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */ .highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */ .highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */ .highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */ .highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */ .highlight .vc { color: #336699 } /* Name.Variable.Class */ .highlight .vg { color: #dd7700 } /* Name.Variable.Global */ .highlight .vi { color: #3333bb } /* Name.Variable.Instance */ .highlight .vm { color: #336699 } /* Name.Variable.Magic */ .highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */
import os
import logging
import json
from urllib.parse import unquote, quote

log = logging.getLogger("ghdl-ls")

is_windows = os.name == "nt"


class ProtocolError(Exception):
    pass


class LSPConn:
    def __init__(self, reader, writer):
        self.reader = reader
        self.writer = writer

    def readline(self):
        data = self.reader.readline()
        return data.decode("utf-8")

    def read(self, size):
        data = self.reader.read(size)
        return data.decode("utf-8")

    def write(self, out):
        self.writer.write(out.encode())
        self.writer.flush()


def path_from_uri(uri):
    # Convert file uri to path (strip html like head part)
    # This is needed to get the root path and to load a document when the
    # textual source is not present.
    if not uri.startswith("file://"):
        # No scheme
        return uri
    _, path = uri.split("file://", 1)
    if is_windows and path.startswith("/"):
        # On windows, absolute files start like "/C:/aa/bbb".
        # Remove the first "/".
        path = path[1:]
    return os.path.normpath(unquote(path))


def path_to_uri(path):
    # Convert path to file uri (add html like head part)
    # :param path: is an absolute path.
    if is_windows:
        # On windows, do not quote the colon after the driver letter, as
        # it is not quoted in uri from the client.
        path = path.replace("\\", "/")
        return "file:///{0}{1}".format(path[:2], quote(path[2:]))
    return "file://{0}".format(quote(path))


class LanguageProtocolServer(object):
    def __init__(self, handler, conn):
        self.conn = conn
        self.handler = handler
        if handler is not None:
            handler.set_lsp(self)
        self.running = True
        self._next_id = 0

    def read_request(self):
        headers = {}
        while True:
            # Read a line
            line = self.conn.readline()
            # Return on EOF.
            if not line:
                return None
            if line[-2:] != "\r\n":
                raise ProtocolError("invalid end of line in header")
            line = line[:-2]
            if not line:
                # End of headers.
                log.debug("Headers: %r", headers)
                length = headers.get("Content-Length", None)
                if length is not None:
                    body = self.conn.read(int(length))
                    return body
                else:
                    raise ProtocolError("missing Content-Length in header")
            else:
                key, value = line.split(": ", 1)
                headers[key] = value

    def run(self):
        while self.running:
            body = self.read_request()
            if body is None:
                # EOF
                break

            # Text to JSON
            msg = json.loads(body)
            log.debug("Read msg: %s", msg)

            reply = self.handle(msg)
            if reply is not None:
                self.write_output(reply)

    def handle(self, msg):
        if msg.get("jsonrpc", None) != "2.0":
            raise ProtocolError("invalid jsonrpc version")
        tid = msg.get("id", None)
        method = msg.get("method", None)
        if method is None:
            # This is a reply.
            log.error("Unexpected reply for %s", tid)
            return
        params = msg.get("params", None)
        fmethod = self.handler.dispatcher.get(method, None)
        if fmethod:
            if params is None:
                params = {}
            try:
                response = fmethod(**params)
            except Exception:
                log.exception("Caught exception while handling %s with params %s:", method, params)
                self.show_message(
                    MessageType.Error,
                    ("Caught exception while handling {}, see VHDL language server output for details.").format(method),
                )
                response = None
            if tid is None:
                # If this was just a notification, discard it
                return None
            log.debug("Response: %s", response)
            rbody = {
                "jsonrpc": "2.0",
                "id": tid,
                "result": response,
            }
        else:
            # Unknown method.
            log.error("Unknown method %s", method)
            # If this was just a notification, discard it
            if tid is None:
                return None
            # Otherwise create an error.
            rbody = {
                "jsonrpc": "2.0",
                "id": tid,
                "error": {
                    "code": JSONErrorCodes.MethodNotFound,
                    "message": "unknown method {}".format(method),
                },
            }
        return rbody

    def write_output(self, body):
        output = json.dumps(body, separators=(",", ":"))
        self.conn.write("Content-Length: {}\r\n".format(len(output)))
        self.conn.write("\r\n")
        self.conn.write(output)

    def notify(self, method, params):
        """Send a notification."""
        body = {
            "jsonrpc": "2.0",
            "method": method,
            "params": params,
        }
        self.write_output(body)

    def send_request(self, method, params):
        """Send a request."""
        self._next_id += 1
        body = {
            "jsonrpc": "2.0",
            "id": self._next_id,
            "method": method,
            "params": params,
        }
        self.write_output(body)

    def shutdown(self):
        """Prepare to shutdown the server."""
        self.running = False

    def show_message(self, typ, message):
        self.notify("window/showMessage", {"type": typ, "message": message})

    def configuration(self, items):
        return self.send_request("workspace/configuration", {"items": items})


# ----------------------------------------------------------------------
#  Standard defines and object types
#


class JSONErrorCodes(object):
    # Defined by JSON RPC
    ParseError = -32700
    InvalidRequest = -32600
    MethodNotFound = -32601
    InvalidParams = -32602
    InternalError = -32603
    serverErrorStart = -32099
    serverErrorEnd = -32000
    ServerNotInitialized = -32002
    UnknownErrorCode = -32001

    # Defined by the protocol.
    RequestCancelled = -32800
    ContentModified = -32801


class CompletionKind(object):
    Text = 1
    Method = 2
    Function = 3
    Constructor = 4
    Field = 5
    Variable = 6
    Class = 7
    Interface = 8
    Module = 9
    Property = 10
    Unit = 11
    Value = 12
    Enum = 13
    Keyword = 14
    Snippet = 15
    Color = 16
    File = 17
    Reference = 18


class DiagnosticSeverity(object):
    Error = 1
    Warning = 2
    Information = 3
    Hint = 4


class TextDocumentSyncKind(object):
    NONE = (0,)
    FULL = 1
    INCREMENTAL = 2


class MessageType(object):
    Error = 1
    Warning = 2
    Info = 3
    Log = 4


class SymbolKind(object):
    File = 1
    Module = 2
    Namespace = 3
    Package = 4
    Class = 5
    Method = 6
    Property = 7
    Field = 8
    Constructor = 9
    Enum = 10
    Interface = 11
    Function = 12
    Variable = 13
    Constant = 14
    String = 15
    Number = 16
    Boolean = 17
    Array = 18