From 0db46ea7165114d9ab25d9ba0e939a5cb7b67ff0 Mon Sep 17 00:00:00 2001 From: Christoph Schwering Date: Tue, 14 Mar 2017 23:40:48 +1100 Subject: [PATCH] Fixed: Solver::Assign() should check subsumption in original setup. When adding all isomorphic literals, the order of these literals should be irrelevant. --- examples/index.html | 1 + examples/minesweeper/minesweeper-js.html | 1 + examples/sudoku/sudoku-js.html | 1 + examples/tui/tui-js.html | 79 ++++++++++++++---------- src/lela/solver.h | 2 +- 5 files changed, 50 insertions(+), 34 deletions(-) diff --git a/examples/index.html b/examples/index.html index ac36e5f..8341e57 100644 --- a/examples/index.html +++ b/examples/index.html @@ -35,6 +35,7 @@
  • Sudoku demo
    • +

    About the Reasoner

    diff --git a/examples/minesweeper/minesweeper-js.html b/examples/minesweeper/minesweeper-js.html index e13a960..4351185 100644 --- a/examples/minesweeper/minesweeper-js.html +++ b/examples/minesweeper/minesweeper-js.html @@ -4,6 +4,7 @@ + Limited reasoner demo diff --git a/examples/sudoku/sudoku-js.html b/examples/sudoku/sudoku-js.html index 67adfd9..4134b06 100644 --- a/examples/sudoku/sudoku-js.html +++ b/examples/sudoku/sudoku-js.html @@ -4,6 +4,7 @@ + Limited reasoner demo diff --git a/examples/tui/tui-js.html b/examples/tui/tui-js.html index 11ef381..4fb2dd4 100644 --- a/examples/tui/tui-js.html +++ b/examples/tui/tui-js.html @@ -4,6 +4,7 @@ + Limited reasoner demo @@ -69,6 +70,40 @@ { value: 'test-veggie-with-guarantee', text: 'Test: Veggie 2' }, // { value: 'test-battleship-1x4', text: 'Test: Battleship 1x4' }, // test-battleship-1x4 test is specificially for "my" computer as it assumes a specific "random" ship placement, which is different under Javascript due to different random numbers --> ]; + var help = [ + { value: 'ls', text: 'list predefined examples' }, + { value: 'load ', text: 'load the specified example' }, + { value: '[hide|show]-debug', text: 'show/hide debug output' }, + { value: '', text: '' }, + { value: 'Sort ', text: 'define new sort with specified id' }, + { value: 'Var -> ', text: 'define new variable' }, + { value: 'Name -> ', text: 'define new standard name' }, + { value: 'Fun / -> ', text: 'define new function' }, + { value: '', text: '' }, + { value: 'Let := ', text: 'define formula abbreviation' }, + { value: '', text: '' }, + { value: 'KB: ', text: 'add clausal formula to knowledge base' }, + { value: '', text: '' }, + { value: '', text: 'evaluate query formula in knowledge base ...' }, + { value: 'Query: ', text: '' }, + { value: 'Assert: ', text: '... and fail if formula is false' }, + { value: 'Refute: ', text: '... and fail if formula is true' }, + //t.echo('Formula are of the form:'); + //t.echo(' t == t t /= t literals'); + //t.echo(' ~formula negation'); + //t.echo(' formula v formula disjunction'); + //t.echo(' formula ^ formula conjunction'); + //t.echo(' Ex x formula existential quantification'); + //t.echo(' Fa x formula universal quantification'); + //t.echo(' formula -> formula implication'); + //t.echo(' formula <-> formula implication'); + //t.echo(' K formula knowledge modality, k >= 0'); + //t.echo(' M formula consistency modality, k >= 0'); + //t.echo(' B formula ==> formula conditional belief modality, k, l >= 0'); + //t.echo(' G formula consistency guarantee'); + //t.echo(' ( formula ) brackets'); + //t.echo(' formula-id id of abbreviation'); + ]; @@ -99,6 +134,7 @@ Load an example: + @@ -190,37 +226,18 @@ function loadExample(file) { function lela_exec(command) { var t = $('#terminal').terminal(); if (command == 'help') { + var maxlen = 0; + for (var i = 0; i < help.length; ++i) { + if (maxlen < help[i].value.length) { + maxlen = help[i].value.length; + } + } t.echo('Commands:'); - t.echo(' ls list predefined examples'); - t.echo(' load load the specified example'); - t.echo(' [hide|show]-debug show/hide debug output'); - t.echo(''); - t.echo(' Sort define new sort with specified id'); - t.echo(' Var -> define new variable'); - t.echo(' Name -> define new standard name'); - t.echo(' Fun / -> define new function'); - t.echo(' Let := define formula abbreviation'); - t.echo(' KB: add clausal formula to knowledge base'); - t.echo(' evaluate query formula in knowledge base ...'); - t.echo(' Query: '); - t.echo(' Assert: ... and fail if formula is false'); - t.echo(' Refute: ... and fail if formula is true'); + for (var i = 0; i < help.length; ++i) { + var pad = new Array(maxlen - help[i].value.length + 1).join(' '); + t.echo(' '+ help[i].value + pad +' ' + help[i].text); + } t.echo('See below for the grammar of formulas.'); - //t.echo('Formula are of the form:'); - //t.echo(' t == t t /= t literals'); - //t.echo(' ~formula negation'); - //t.echo(' formula v formula disjunction'); - //t.echo(' formula ^ formula conjunction'); - //t.echo(' Ex x formula existential quantification'); - //t.echo(' Fa x formula universal quantification'); - //t.echo(' formula -> formula implication'); - //t.echo(' formula <-> formula implication'); - //t.echo(' K formula knowledge modality, k >= 0'); - //t.echo(' M formula consistency modality, k >= 0'); - //t.echo(' B formula ==> formula conditional belief modality, k, l >= 0'); - //t.echo(' G formula consistency guarantee'); - //t.echo(' ( formula ) brackets'); - //t.echo(' formula-id id of abbreviation'); } else if (command == 'ls') { var maxlen = 0; for (var i = 0; i < examples.length; ++i) { @@ -249,10 +266,6 @@ $(document).ready(function() { Module.ccall('lela_init', 'void', [], []); - for (var i = 0; i < examples.length; ++i) { - $('#examples').append($('