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 different; | |||||
pn = pa->next(); | |||||
if (pa->contains(pvar[v]) == false) | |||||
continue; | |||||
if (pa->options[0].contains(pvar[v])) { | |||||
different = (pa->options[0] != pvar[v]); | |||||
if (!different) | |||||
pa->options[0].toggleInverted(); | |||||
} else { | |||||
different = (pa->options[1] != pvar[v]); | |||||
if (!different) | |||||
pa->options[1].toggleInverted(); | |||||
} | |||||
pa->expand(pvar[v]); | |||||
if (pa->isZero()) | |||||
delete pa->remove(phead); | |||||
else | |||||
pa->remove(phead)->insert_tail(ahead + different); | |||||
} | |||||
hp2sat_multiply(ahead + 0, ahead + 1, phead); | |||||
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)) { | |||||
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); | |||||
} |