{"id":13,"date":"2017-02-17T10:55:32","date_gmt":"2017-02-17T09:55:32","guid":{"rendered":"https:\/\/tapas.labri.fr\/wp\/?page_id=13"},"modified":"2017-02-23T14:11:20","modified_gmt":"2017-02-23T13:11:20","slug":"generic-presburger-programming-interface","status":"publish","type":"page","link":"https:\/\/tapas.labri.fr\/wp\/?page_id=13","title":{"rendered":"GENEric Presburger programming Interface"},"content":{"rendered":"<p>The <strong>GENEPI<\/strong> library gathers a set of routines that can be used in place of Presburger solver. GENEPI is not a real solver but rather an abstraction layer of a solver. The decision procedures are not implemented into the GENEPI library; the necessary functions are imported from dynamically loaded <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13#plugins\">plugins<\/a>. Each plugin must furnish a set of functions specified by the <a href=\"\/apis\/current\/html\/genepi-plugin_8h.html\">plugin API<\/a>.<\/p>\n<p>GENEPI is useful at both sides of the programming interface:<\/p>\n<ul>\n<li>On one side, applications that require the resolution of Presburger formulas can take advantage of the abstraction that allows to use dynamically loaded solvers and thus, to postpone the choice of the actually used solver at run-time.<\/li>\n<li>On the other side, solver developers can use any GENEPI-based application to benchmark their solver and compare it to other solvers.<\/li>\n<\/ul>\n<h2 id=\"Documentation\">Documentation<\/h2>\n<p>The API documentation is available <a href=\"\/apis\/current\/html\/genepi.html\">here<\/a>.<\/p>\n<h2 id=\"Plugins\">Plugins<\/h2>\n<p>Several implementations of the <a href=\"\/apis\/current\/html\/genepi-plugin_8h.html\">GENEPI Plugin API<\/a> have been developed. Each one is a simple encapsulation of an existing solver library.<\/p>\n<ul>\n<li><strong>Plugins over natural numbers<\/strong>\n<ul>\n<li>The automaton data-structure (DFA library) of <a class=\"ext-link\" href=\"http:\/\/www.brics.dk\/mona\/index.html\"><span class=\"icon\">\u200b<\/span>MONA<\/a> is used to encode binary automata.<\/li>\n<li>The <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=14\">Shared Automata<\/a> data-structure is used to implement the plugin <a class=\"wiki\" href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=14\">PresTAF<\/a>.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<ul>\n<li><strong>Plugins over integers<\/strong>\n<ul>\n<li>The <a class=\"ext-link\" href=\"http:\/\/www.montefiore.ulg.ac.be\/%7Eboigelot\/research\/lash\/\"><span class=\"icon\">\u200b<\/span>LASH<\/a> (Li\u00e8ge Automata-based Symbolic Handler) is used to implement a solver over integers; the <a class=\"ext-link\" href=\"http:\/\/www.montefiore.ulg.ac.be\/%7Eboigelot\/research\/lash\/lash\/ndd\/doc.html\"><span class=\"icon\">\u200b<\/span>NDD<\/a> (Number Decision Diagrams) are used to implement it.<\/li>\n<li>One of the plugins not based on binary automata uses the <a class=\"ext-link\" href=\"http:\/\/www.cs.umd.edu\/projects\/omega\/\"><span class=\"icon\">\u200b<\/span>Omega<\/a> library (formula transformations).<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<ul>\n<li><strong>Plugins over real numbers<\/strong>\n<ul>\n<li>The <a class=\"ext-link\" href=\"http:\/\/www.cs.unipr.it\/ppl\/\"><span class=\"icon\">\u200b<\/span>PPL<\/a> (Parma Polyhedra Library) plugin is another plugin not based on the automaton representation.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n<ul>\n<li><strong>Plugins mixing real and integer variables<\/strong>\n<ul>\n<li>The <a class=\"ext-link\" href=\"http:\/\/lira.gforge.avacs.org\/\"><span class=\"icon\">\u200b<\/span>LIRA<\/a> (Linear Integer\/Real Arithmetic Solver) plugin is based on weak deterministic B\u00fcchi automata.<\/li>\n<li>The <a class=\"ext-link\" href=\"http:\/\/www.montefiore.ulg.ac.be\/%7Eboigelot\/research\/lash\/\"><span class=\"icon\">\u200b<\/span>LASH<\/a> (Li\u00e8ge Automata-based Symbolic Handler) is also used to implement a solver over reals and integers; the <a class=\"ext-link\" href=\"http:\/\/www.montefiore.ulg.ac.be\/%7Eboigelot\/research\/lash\/lash\/rva\/doc.html\"><span class=\"icon\">\u200b<\/span>RVA<\/a> (Real Vector Automata) library is used to implement it.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>The GENEPI library gathers a set of routines that can be used in place of Presburger solver. GENEPI is not a real solver but rather an abstraction layer of a solver. The decision procedures are not implemented into the GENEPI &hellip; <a href=\"https:\/\/tapas.labri.fr\/wp\/?page_id=13\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-13","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/13","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=13"}],"version-history":[{"count":8,"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/13\/revisions"}],"predecessor-version":[{"id":121,"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=\/wp\/v2\/pages\/13\/revisions\/121"}],"wp:attachment":[{"href":"https:\/\/tapas.labri.fr\/wp\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=13"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}