Closed arademaker closed 9 years ago
Podemos usar o OrgMode de Emacs para produzir tabelas a partir de dados:
#+BEGIN_SRC lisp :results value
(let ((a (make-array '(9 9))))
(setf (aref a 0 0) 4)
a)
(list '(1 2) '(2 3) '(3 4))
#+END_SRC
#+RESULTS:
| 1 | 2 |
| 2 | 3 |
| 3 | 4 |
Vejam função sudoku no commit ee973af. Ainda não testei. Observar que a entrada é um branch de fórmulas atômicas (onde fórmulas são instâncias de `formula``).
Também podemos implementar uma função para ler uma matriz (array) com o tabuleiro inicial, transformar em fórmula, juntar com as demais fórmulas que definem as regras do jogo e submeter ao provador.
Falta testar a função que fiz para ler saída e implementar e testar a função agora sugerida para ler entrada. Por isso este issue ainda está aberto.
Função criada. Commit 565a58b. Trata a lista de entrada e retorna uma lista com triplas, compostas da linha, coluna e valor dos elementos não nulos.
vide resposta do pull request. Não entendi a func e acho que além do nome errado ela está no lugar errado. Ela não é uma func para o tableaux, mas apenas para o ex. sudoku. ela retorna listas de 3 números? Para que serve? O que queremos aqui é uma func que receba uma matriz e crie formulas para o prove e uma outra func que com a saída de prove mostre um tabuleiro.
andamos um pouco com 2a767a6 mas ainda precisamos melhorar o nome das funções e limpar lixo deixado para trás.
Creio que este issue possa ser fechado.
correto.
Precisamos de funções para pré e pós processar Sudoku. A saída poderia mesmo imprimir o tabuleiro final. A entrada precisa ser de fácil codificação pelo usuário. Teríamos assim uma interface que usa a função
prove
.