Fix 24-bit rendering
This commit is contained in:
parent
dc2badc80e
commit
21218be799
@ -43,6 +43,11 @@ clean:
|
||||
@${CC} ${CFLAGS} -s -I ../util/toaru-toolchain/i686-pc-toaru/include/freetype2/ -o $@ $< lib/graphics.o lib/list.o ../util/toaru-toolchain/i686-pc-toaru/lib/libfreetype.a ${ERRORS}
|
||||
@${END} "CC" "$< [w/libs]"
|
||||
|
||||
../hdd/bin/solver: solver.c lib/list.o
|
||||
@${BEG} "CC" "$< [w/libs]"
|
||||
@${CC} ${CFLAGS} -s -o $@ $< lib/list.o ${ERRORS}
|
||||
@${END} "CC" "$< [w/libs]"
|
||||
|
||||
../hdd/bin/%: %.cpp
|
||||
@${BEG} "CPP" "$<"
|
||||
@${CPP} ${CPPFLAGS} -s -o $@ $< ${ERRORS}
|
||||
|
250
userspace/solver.c
Normal file
250
userspace/solver.c
Normal file
@ -0,0 +1,250 @@
|
||||
/* vim: tabstop=4 shiftwidth=4 noexpandtab
|
||||
*
|
||||
* Brute-Force SAT Solver
|
||||
*
|
||||
* Copyright (c) 2012 Kevin Lange. All rights reserved.
|
||||
*
|
||||
*
|
||||
* Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
* of this software and associated documentation files (the "Software"), to
|
||||
* deal with the Software without restriction, including without limitation the
|
||||
* rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
|
||||
* sell copies of the Software, and to permit persons to whom the Software is
|
||||
* furnished to do so, subject to the following conditions:
|
||||
* 1. Redistributions of source code must retain the above copyright notice,
|
||||
* this list of conditions and the following disclaimers.
|
||||
* 2. Redistributions in binary form must reproduce the above copyright
|
||||
* notice, this list of conditions and the following disclaimers in the
|
||||
* documentation and/or other materials provided with the distribution.
|
||||
* 3. Neither the names of Kevin Lange, nor the names of its contributors
|
||||
* may be used to endorse or promote products derived from this Software
|
||||
* without specific prior written permission.
|
||||
*
|
||||
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
* CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
|
||||
* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
|
||||
* WITH THE SOFTWARE.
|
||||
*
|
||||
*/
|
||||
|
||||
#define _XOPEN_SOURCE 500
|
||||
#include <stdint.h>
|
||||
#include <assert.h>
|
||||
#include <stdio.h>
|
||||
#include <string.h>
|
||||
#include "lib/list.h"
|
||||
|
||||
/* Width of a line to read for a clause. Clauses should not be too terrible long. */
|
||||
#define LINE_WIDTH 4096
|
||||
|
||||
/* This brute-force solution uses bitsets, one bit per variable */
|
||||
#define BITS_IN_SET 8
|
||||
uint8_t * bit_sets = NULL;
|
||||
uint64_t bit_sets_n = 0;
|
||||
uint64_t variables = 0;
|
||||
uint64_t clause_n = 0;
|
||||
uint64_t collected = 0;
|
||||
|
||||
#define DEBUG 0
|
||||
|
||||
/* Clauses are stored as dynamic linked-lists of variable states */
|
||||
list_t ** clauses;
|
||||
|
||||
/* Check a bit (variable) for the current state */
|
||||
inline uint8_t checkbit(uint64_t bit) {
|
||||
uint64_t set_id = bit / BITS_IN_SET;
|
||||
uint8_t offset = bit - set_id * BITS_IN_SET;
|
||||
uint8_t tmp = ((bit_sets[set_id] & (1 << offset)) > 0);
|
||||
|
||||
#if DEBUG
|
||||
fprintf(stderr,"bit %ld [%ld:%d] = %d [%x, %d]\n", bit, set_id, offset, tmp, bit_sets[set_id], 1 << offset);
|
||||
#endif
|
||||
|
||||
return tmp;
|
||||
}
|
||||
|
||||
/* Initialize the bitsets */
|
||||
inline void setup_bitsets() {
|
||||
bit_sets_n = variables / BITS_IN_SET + 1;
|
||||
bit_sets = (uint8_t *)malloc(sizeof(uint8_t) * bit_sets_n);
|
||||
memset(bit_sets, 0x00, sizeof(uint8_t) * bit_sets_n);
|
||||
}
|
||||
|
||||
/*
|
||||
* Increment the state.
|
||||
* The bit sets are like a very large integer, and we are
|
||||
* incrementing by one.
|
||||
*/
|
||||
inline void next_bitset(uint64_t i) {
|
||||
if (__builtin_expect(bit_sets[i] == 0xFF, 0)) {
|
||||
bit_sets[i] = 0;
|
||||
if (__builtin_expect(i + 1 == bit_sets_n, 0)) {
|
||||
/* If we have run out of state, there is no solution. */
|
||||
printf("UNSATISFIABLE\n");
|
||||
exit(0);
|
||||
}
|
||||
next_bitset(i + 1);
|
||||
} else {
|
||||
bit_sets[i]++;
|
||||
if (i + 1 == bit_sets_n) {
|
||||
if (__builtin_expect(bit_sets[i] == (1 << variables), 0)) {
|
||||
/* If we have run out of state, there is no solution. */
|
||||
printf("UNSATISFIABLE\n");
|
||||
exit(0);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/*
|
||||
* We can determine if a clause is true by
|
||||
* running through each of the values in it and checking
|
||||
* if any of them are true (as a clause is a set of ORs)
|
||||
*/
|
||||
inline uint8_t is_clause_true(uint64_t i) {
|
||||
list_t * clause = clauses[i];
|
||||
|
||||
foreach(node, clause) {
|
||||
int64_t var = (int64_t)node->value;
|
||||
if (var < 0) {
|
||||
if (!checkbit(-var - 1)) return 1;
|
||||
} else {
|
||||
if (checkbit(var - 1)) return 1;
|
||||
}
|
||||
}
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
inline uint8_t solved_with_bitset() {
|
||||
for (uint64_t i = 0; i < clause_n; ++i) {
|
||||
if (!is_clause_true(i)) {
|
||||
/* If any clause is not true, the entire statement
|
||||
* is false for this state */
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
/* If all of the clauses are true, we are done. */
|
||||
return 1;
|
||||
}
|
||||
|
||||
/* Read a line of input and process it */
|
||||
int read_line() {
|
||||
char c = fgetc(stdin);
|
||||
switch (c) {
|
||||
case 'c':
|
||||
/* Comment */
|
||||
while (fgetc(stdin) != '\n');
|
||||
break;
|
||||
case 'p':
|
||||
/* Problem definition */
|
||||
{
|
||||
fgetc(stdin);
|
||||
while (fgetc(stdin) != ' ');
|
||||
char num[30];
|
||||
int offset = 0;
|
||||
char input;
|
||||
while ((input = fgetc(stdin)) != ' ') {
|
||||
num[offset] = input;
|
||||
offset++;
|
||||
}
|
||||
num[offset] = '\0';
|
||||
variables = atoi(num);
|
||||
offset = 0;
|
||||
while ((input = fgetc(stdin)) != '\n') {
|
||||
num[offset] = input;
|
||||
offset++;
|
||||
}
|
||||
num[offset] = '\0';
|
||||
clause_n = atoi(num);
|
||||
clauses = malloc(sizeof(list_t *) * clause_n);
|
||||
setup_bitsets();
|
||||
#if DEBUG
|
||||
fprintf(stderr, "%ld variables, %ld clauses\n", variables, clause_n);
|
||||
#endif
|
||||
}
|
||||
break;
|
||||
default:
|
||||
/* Clause */
|
||||
{
|
||||
assert(variables > 0);
|
||||
assert(clauses > 0);
|
||||
|
||||
ungetc(c, stdin);
|
||||
|
||||
clauses[collected] = list_create();
|
||||
char * line = malloc(LINE_WIDTH);
|
||||
fgets(line, LINE_WIDTH - 1, stdin);
|
||||
if (line[strlen(line) - 1] == '\n') {
|
||||
line[strlen(line) - 1] = '\0';
|
||||
}
|
||||
|
||||
#if DEBUG
|
||||
fprintf(stderr, "Preparing to add clause %ld: %s\n", collected, line);
|
||||
#endif
|
||||
|
||||
char *p, *last;
|
||||
for ((p = strtok_r(line, " ", &last)); ;
|
||||
(p = strtok_r(NULL, " ", &last))) {
|
||||
int var = atoi(p);
|
||||
if (var == 0) break;
|
||||
uintptr_t x = var;
|
||||
list_insert(clauses[collected], (void *)x);
|
||||
}
|
||||
free(line);
|
||||
|
||||
#if DEBUG
|
||||
fprintf(stderr, "Added clause.\n");
|
||||
#endif
|
||||
|
||||
collected++;
|
||||
if (collected == clause_n) return 0;
|
||||
}
|
||||
break;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
int main(int argc, char * argv[]) {
|
||||
/* Read the CNF file from standard in and process it into clauses */
|
||||
while (read_line());
|
||||
|
||||
#if DEBUG
|
||||
/* Debug: Print out the clauses */
|
||||
for (uint32_t i = 0; i < clause_n; ++i) {
|
||||
list_t * clause = clauses[i];
|
||||
fprintf(stderr, "[clause #%d] ", (i + 1));
|
||||
foreach(node, clause) {
|
||||
fprintf(stderr, "%ld ", (uintptr_t)node->value);
|
||||
}
|
||||
fprintf(stderr, "\n");
|
||||
}
|
||||
|
||||
/* Print out variable information */
|
||||
fprintf(stderr, "%ld variables to check, which means %d combinations to bruteforce.\n", variables, 1 << variables);
|
||||
#endif
|
||||
|
||||
/* Brute force! */
|
||||
while (!solved_with_bitset()) {
|
||||
next_bitset(0);
|
||||
}
|
||||
|
||||
/* If we get to this point, we have a solution. */
|
||||
for (uint64_t i = 0; i < variables; ++i) {
|
||||
/* Print the state of each variable. */
|
||||
if (checkbit(i)) {
|
||||
printf("%ld", i + 1);
|
||||
} else {
|
||||
printf("-%ld", i + 1);
|
||||
}
|
||||
if (i != variables - 1) {
|
||||
printf(" ");
|
||||
} else {
|
||||
printf("\n");
|
||||
}
|
||||
}
|
||||
|
||||
}
|
@ -738,8 +738,10 @@ term_set_point(
|
||||
) {
|
||||
if (graphics_depth == 32) {
|
||||
GFX(x,y) = color;
|
||||
} else {
|
||||
printf("Unsupported mode!\n");
|
||||
} else if (graphics_depth == 24) {
|
||||
gfx_mem[((y) * graphics_width + x) * 3 + 2] = _RED(color);
|
||||
gfx_mem[((y) * graphics_width + x) * 3 + 1] = _GRE(color);
|
||||
gfx_mem[((y) * graphics_width + x) * 3 + 0] = _BLU(color);
|
||||
}
|
||||
}
|
||||
|
||||
@ -2495,7 +2497,7 @@ void drawChar(FT_Bitmap * bitmap, int x, int y, uint32_t fg, uint32_t bg) {
|
||||
for (j = y, q = 0; j < y_max; j++, q++) {
|
||||
for ( i = x, p = 0; i < x_max; i++, p++) {
|
||||
//GFX(i,j) = alpha_blend(GFX(i,j),rgb(0xff,0xff,0xff),rgb(bitmap->buffer[q * bitmap->width + p],0,0));
|
||||
GFX(i,j) = alpha_blend(bg, fg, rgb(bitmap->buffer[q * bitmap->width + p],0,0));
|
||||
term_set_point(i,j, alpha_blend(bg, fg, rgb(bitmap->buffer[q * bitmap->width + p],0,0)));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user