Changeset View
Changeset View
Standalone View
Standalone View
usr.sbin/config/hp2sat.cpp
- This file was added.
| /*- | |||||
| * Copyright (c) 2021 Hans Petter Selasky. All rights reserved. | |||||
| * | |||||
| * Redistribution and use in source and binary forms, with or without | |||||
| * modification, are permitted provided that the following conditions | |||||
| * are met: | |||||
| * 1. Redistributions of source code must retain the above copyright | |||||
| * notice, this list of conditions and the following disclaimer. | |||||
| * 2. Redistributions in binary form must reproduce the above copyright | |||||
| * notice, this list of conditions and the following disclaimer in the | |||||
| * documentation and/or other materials provided with the distribution. | |||||
| * | |||||
| * THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' AND | |||||
| * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE | |||||
| * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE | |||||
| * ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE | |||||
| * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL | |||||
| * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS | |||||
| * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) | |||||
| * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT | |||||
| * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY | |||||
| * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF | |||||
| * SUCH DAMAGE. | |||||
| */ | |||||
| #include "hp2sat.h" | |||||
| #include <ctype.h> | |||||
| char * | |||||
| hp2sat_option_dup(const char *str) | |||||
| { | |||||
| size_t len; | |||||
| char *option; | |||||
| if (str[0] == '!') { | |||||
| len = strlen(str) + 1; | |||||
| option = new char [len]; | |||||
| } else { | |||||
| len = strlen(str) + 2; | |||||
| option = new char [len]; | |||||
| option[0] = '!'; | |||||
| len--; | |||||
| option++; /* hide the '!' character */ | |||||
| } | |||||
| memcpy(option, str, len); | |||||
| /* lower case all options */ | |||||
| while (len--) { | |||||
| if (isupper(option[len])) | |||||
| option[len] = tolower(option[len]); | |||||
| } | |||||
| return (option); | |||||
| } | |||||
| void | |||||
| hp2sat_free(ANDMAP_HEAD_t *phead) | |||||
| { | |||||
| ANDMAP *pa; | |||||
| while ((pa = TAILQ_FIRST(phead))) | |||||
| delete pa->remove(phead); | |||||
| } | |||||
| static int | |||||
| hp2sat_compare(const void *a, const void *b) | |||||
| { | |||||
| return ((ANDMAP * const *)a)[0][0].compare(((ANDMAP * const *)b)[0][0]); | |||||
| } | |||||
| bool | |||||
| hp2sat_sort_ored(ANDMAP_HEAD_t *phead) | |||||
| { | |||||
| ANDMAP *pa; | |||||
| ANDMAP **pp; | |||||
| size_t count = 0; | |||||
| bool did_sort = false; | |||||
| for (pa = TAILQ_FIRST(phead); pa; pa = pa->next()) | |||||
| count++; | |||||
| if (count == 0) | |||||
| return (false); | |||||
| pp = new ANDMAP * [count]; | |||||
| count = 0; | |||||
| for (pa = TAILQ_FIRST(phead); pa; pa = pa->next()) { | |||||
| if (pa->isOne()) { | |||||
| pa->remove(phead); | |||||
| hp2sat_free(phead); | |||||
| pa->insert_tail(phead); | |||||
| goto done; | |||||
| } | |||||
| pp[count++] = pa; | |||||
| } | |||||
| for (size_t x = 1; x != count; x++) { | |||||
| if (pp[x - 1]->compare(*pp[x]) > 0) { | |||||
| did_sort = true; | |||||
| break; | |||||
| } | |||||
| } | |||||
| if (did_sort) | |||||
| mergesort(pp, count, sizeof(pp[0]), &hp2sat_compare); | |||||
| TAILQ_INIT(phead); | |||||
| for (size_t x = 1; x != count; x++) { | |||||
| if (pp[x - 1]->isZero() || | |||||
| pp[x - 1]->compare(*pp[x]) == 0) { | |||||
| delete pp[x - 1]; | |||||
| } else { | |||||
| pp[x - 1]->insert_tail(phead); | |||||
| } | |||||
| } | |||||
| if (pp[count - 1]->isZero()) | |||||
| delete pp[count - 1]; | |||||
| else | |||||
| pp[count - 1]->insert_tail(phead); | |||||
| done: | |||||
| delete [] pp; | |||||
| return (did_sort); | |||||
| } | |||||
| void | |||||
| hp2sat_multiply(const ANDMAP_HEAD_t *ph0, const ANDMAP_HEAD_t *ph1, ANDMAP_HEAD_t *ph2) | |||||
| { | |||||
| size_t count[2] = {}; | |||||
| ANDMAP_HEAD_t temp; | |||||
| ANDMAP *pa; | |||||
| ANDMAP *pb; | |||||
| ANDMAP *pc; | |||||
| TAILQ_INIT(&temp); | |||||
| for (pa = TAILQ_FIRST(ph0); pa != 0; pa = pa->next()) | |||||
| count[0]++; | |||||
| for (pa = TAILQ_FIRST(ph1); pa != 0; pa = pa->next()) | |||||
| count[1]++; | |||||
| if (count[0] < count[1]) { | |||||
| for (pa = TAILQ_FIRST(ph0); pa != 0; pa = pa->next()) { | |||||
| for (pb = TAILQ_FIRST(ph1); pb != 0; pb = pb->next()) { | |||||
| pc = new ANDMAP(*pa & *pb); | |||||
| if (pc->isZero()) | |||||
| delete pc; | |||||
| else | |||||
| pc->insert_tail(&temp); | |||||
| } | |||||
| hp2sat_sort_ored(&temp); | |||||
| } | |||||
| } else { | |||||
| for (pa = TAILQ_FIRST(ph1); pa != 0; pa = pa->next()) { | |||||
| for (pb = TAILQ_FIRST(ph0); pb != 0; pb = pb->next()) { | |||||
| pc = new ANDMAP(*pa & *pb); | |||||
| if (pc->isZero()) | |||||
| delete pc; | |||||
| else | |||||
| pc->insert_tail(&temp); | |||||
| } | |||||
| hp2sat_sort_ored(&temp); | |||||
| } | |||||
| } | |||||
| TAILQ_CONCAT(ph2, &temp, entry); | |||||
| hp2sat_sort_ored(ph2); | |||||
| } | |||||
| bool | |||||
| hp2sat_solve(ANDMAP_HEAD_t *phead, OPTION *pvar, size_t nvar, OPTION *pconflict) | |||||
| { | |||||
| ANDMAP_HEAD_t *pderiv; | |||||
| ANDMAP_HEAD_t ahead[2]; | |||||
| ANDMAP *pa; | |||||
| ANDMAP *pn; | |||||
| hp2sat_sort_ored(phead); | |||||
| for (uint8_t x = 0; x != 2; x++) | |||||
| TAILQ_INIT(ahead + x); | |||||
| pderiv = new ANDMAP_HEAD_t [nvar]; | |||||
| for (size_t x = 0; x != nvar; x++) | |||||
| TAILQ_INIT(pderiv + x); | |||||
| for (size_t v = nvar; v--; ) { | |||||
| for (pa = TAILQ_FIRST(phead); pa != 0; pa = pn) { | |||||
| bool isInverted; | |||||
| pn = pa->next(); | |||||
| if (pa->options[0].contains(pvar[v])) { | |||||
| isInverted = pa->options[0].isInverted(); | |||||
| } else if (pa->options[1].contains(pvar[v])) { | |||||
| isInverted = pa->options[1].isInverted(); | |||||
| } else { | |||||
| continue; | |||||
| } | |||||
| /* remove the OPTION() matching pvar[v] from the ANDMAP() */ | |||||
| pa->expand(pvar[v], !isInverted); | |||||
| /* | |||||
| * Make sure the loop below uses the right | |||||
| * inversion to restore the expression: | |||||
| */ | |||||
| isInverted ^= pvar[v].isInverted(); | |||||
| if (pa->isZero()) | |||||
| delete pa->remove(phead); | |||||
| else | |||||
| pa->remove(phead)->insert_tail(ahead + isInverted); | |||||
| } | |||||
| /* | |||||
| * Compute the conflicts for no solution and put that | |||||
| * back into the list: | |||||
| */ | |||||
| hp2sat_multiply(ahead + 0, ahead + 1, phead); | |||||
| /* | |||||
| * Create the final list of conflicts for a solution: | |||||
| */ | |||||
| for (uint8_t x = 0; x != 2; x++) { | |||||
| for (pa = TAILQ_FIRST(ahead + x); pa; pa = pn) { | |||||
| pn = pa->next(); | |||||
| *pa &= pvar[v]; | |||||
| pa->remove(ahead + x)->insert_head(pderiv + v); | |||||
| } | |||||
| pvar[v].toggleInverted(); | |||||
| } | |||||
| } | |||||
| for (size_t v = 0; v != nvar; v++) { | |||||
| bool once = false; | |||||
| for (pa = TAILQ_FIRST(pderiv + v); pa; pa = pn) { | |||||
| pn = pa->next(); | |||||
| if (pa->expand_all(pvar, nvar)) { | |||||
| /* found a conflict */ | |||||
| if (once == false) { | |||||
| /* try the other value */ | |||||
| pvar[v].toggleInverted(); | |||||
| } | |||||
| /* check if still in conflict */ | |||||
| if (pconflict != 0 && (once || pa->expand_all(pvar, nvar))) | |||||
| *pconflict = pvar[v]; | |||||
| once = true; | |||||
| } | |||||
| delete pa->remove(pderiv + v); | |||||
| } | |||||
| } | |||||
| return (TAILQ_FIRST(phead) != 0); | |||||
| } | |||||