[with patch, needs review, under review by gsw] polish the new symbolic logic code.

To do:

1. log.statement(...) could return a "LogicalStatement?" object, which has a nice print method -- repr(self) --, and a _latex_ method.

      class LogicalStatement:
         def __init__(self, ...)
             ...
   

Then this might work:

    sage: s = log.statement("a&b|!(c|a)")
    sage: s
    a&b|!(c|a)
    sage: s & s
    a&b|!(c|a)&a&b|!(c|a)
    sage: s.truthtable()
    ...
    sage: show(s.truthtable())    # calls _latex
    nice typeset version

2. Here:

     sage: s = log.statement("a&&b")
     Malformed Statement
   

   instead of printing, do

          raise ValueError, "malformed statement"
   

3. Don't use "eval" for a name, since that's a builtin Python.

4. Shift this over to line up with the r:

def eval(toks):
    r"""
        This function is for internal use by the class SymbollicLogic.
        It returns 'True' if the exression contained in toks would

5. Every function should have example doctests. And to test do this:

$ cd SAGE_ROOT/devel/sage/sage/logic
$ sage -t logic.py    

6. varaibles --> variables

7. Delete the vars stuff from the inputs in the docs here and clarify how they are used elsewhere:

        INPUT:
            self -- the calling object
            s -- a string containing the logic expression to be manipulated
            global vars -- a dictionary with the variable names and
                          their current boolean value
            global vars_order -- a list of the variable names in
                                the order they were found

Also, at the top of the file document that vars and vars_order are used

to simplify passing information around between various eval* functions. Or better just make all the eval functions be methods of the LogicalStatement? class, if that makes sense.

8. Possibly clarify what valid variable names are -- in the error message.

9. Write something in the docstring at the very top just summarizes the very basic of proposition calculus / symbolic logic / boolean algebra, with examples.

I've uploaded a new tarball that addresses all the todo's above. This should be integrated into the SAGE codebase and tried out by some people very soon.

Note that probably sage/logic/all.py and sage/all.py will need to be modified so that the doctests will actually work.

By the way, this shouldn't definitely stay at milestone 2.9, since it shouldn't be too difficult.

Some comments/ideas on this:

1) I'm not sure if SymbolicLogic? is the proper name for this class. A more accurate name would be PropositionalCalculus? (since there are other important theories in symbolic logic like PredicateCalculus?, i.e. first order logic) that we could support in the future.

2) An important feature to have would be computing the conjuntive normal form, and the output of this form in the DIMACS format used by SAT solvers, see

http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps

(see also ticket #418 on wrapping minisat)

Another comment: why using OPAREN and CPAREN as tokens? using just '(' and ')' would be much more clear, and faster to process (since they are a single character)

Comment from the author about the new version

Hi William,

Sorry about the long delay with getting this code to you, I got a little sidetracked with school and all.  But, here it is.  At this point I believe I've fixed all the issues listed in ticket 545 as well as incorporating all of Pablo De Napoli's ideas and implementing cnf conversions and a DIMACS satformat output method.  I'm not sure if you want to post the code on the trac ticket, or in the repository, or elsewhere.  If you could let me know where it goes I can start soliciting advice on the devel group though.

I have some ideas/questions for where the code should go next, but getting this release accepted first is probably at the top of the list.

-Chris Gorecki

From Pablo De Napoli:

Chris: many thanks for sending the new version of your code.
I think that it is a great work. Actually I see that you have
implemented many of
my previous suggestions like: using the the builting True/False
from python instead of strings, using a tree to parse propositional
formulas, avoid using the OPAN/CPAN tokens, etc.) and thank you for adding me
as an author (eventhough
I've not actually writen a single line of the code)

 I'll review it in more detail and tell you if I see something that can
be still improved.

Pablo

this is from chris gorecki

I *think* I managed to turn the bundle into a patch against sage-3.0.alpha4. I also tried to fiddle with the patch's header so that Chris Gorecki appears as its author.

While browsing the code I noticed lots of stuff that seemed overly verbose (and inefficient), e.g.

        124     def eval_ifthen_op(lval, rval): 
 	125	    r""" 
 	126	    This function returns the logical 'ifthen' operator applied to lval and rval. 
 	127	 
 	128	    INPUT: 
 	129	        lval -- boolean value to the left of the ifthen operator. 
 	130	        rval -- boolean value appearing to the right of the ifthen operator. 
 	131	                                     
 	132	    OUTPUT: 
 	133	        Returns the logical 'ifthen' operator applied to lval and rval.   
 	134	 
 	135	    EXAMPLES: 
 	136	        sage: import booleval 
 	137	        sage: booleval.eval_ifthen_op(True, False) 
 	138	        False 
 	139	        sage: booleval.eval_ifthen_op(False, False) 
 	140	        True 
 	141	    """ 
 	142	    if(lval == False and rval == False): 
 	143	        return True 
 	144	    elif(lval == False and rval == True): 
 	145	        return True 
 	146	    elif(lval == True and rval == False): 
 	147	        return False 
 	148	    elif(lval == True and rval == True): 
 	149	        return True 

which could be summarized as

return not lval or rval

Also, the operators are passed around (and compared) as strings everywhere (sometimes '&', sometimes 'and'). I think it would be better to use operator.not_, operator.and_, etc. and use is to compare, and then one can also write stuff like

return op(lval, rval)

rather than having big if-then-else statements.

Having a global __vars seems fragile as well.

Sorry it's taken so long to get this in, the boolean formula simplification stuff looks good, I just think some of it could be greatly improved.

This is the referee report

REFEREE REPORT:

See the attached file sekine.pdf.

Chris is too busy for the next two weeks to work on this, I think.

latest release

This release should address all the issues in sekine.pdf.

For the patch logic.patch, below are some possible fixes for improving its documentation. I was reviewing the plain text version of the diff, not the online version. This accounts for the number that precedes each line in the diffs below. In other words, such a number refers to the line number in the downloaded, plain text diff file, which should simplify the task of reviewing my suggestions.

1.

36 -    Evaluates the tree using the boolean values contained in dictinary
36 +    Evaluates the tree using the boolean values contained in dictionary

2.

40 -        tree -- a list of three elements corrospsponding to a branch of a
40 +        tree -- a list of three elements corresponding to a branch of a

3.

67 -        tree -- a list of three elements corrospsponding to a branch of a
67 +        tree -- a list of three elements corresponding to a branch of a

4.

201 -    underscores and aplphanumerics.  Parentheses may be used to
201 +    underscores and alphanumerics.  Parentheses may be used to

5.

320 -            tree -- a list continaing the parse tree of the expression.
320 +            tree -- a list containing the parse tree of the expression.

6.

322 -                  with each variable occuring only once.
322 +                  with each variable occurring only once.

7.

486 -        Returns two statements atatched by the -> operator.
486 +        Returns two statements attached by the -> operator.

8.

494 -            ithen'ed together.
494 +            ifthen'ed together.

9.

563 -            start -- an interger representing the row of the truth
563 +            start -- an integer representing the row of the truth

10.

564 -                     table from which to start intilized to 0 which
564 +                     table from which to start initialized to 0, which

11.

568 -                   to be created.  It is intilized to the last row of the
568 +                   to be created.  It is initialized to the last row of the

12.

601 -            When sent with no start or end paramaters this is an
601 +            When sent with no start or end parameters, this is an

13.

680 -        It does this by applying a set of rules that are gaurenteed to convert the
680 +        It does this by applying a set of rules that are guaranteed to convert the

14.

700 -            is typically prefered, but results can vary.
700 +            is typically preferred, but results can vary.

15.

718 -            A string representing the satformat represetatin of this object.
718 +            A string representing the satformat representation of this object.

16.

881 -            Returns a new statement that is the first statement attatched to
881 +            Returns a new statement that is the first statement attached to

17.

950 -        if-thens, and xor opperations to operations only involving and/or operations.
950 +        if-then, and xor operations to operations only involving and/or operations.

18.

954 -            tree -- a list of three elements corrospsponding to a branch of a
954 +            tree -- a list of three elements corresponding to a branch of a

19.

1068 -        This function converts the string expression asscociated with an instance
1068 +        This function converts the string expression associated with an instance

20.

1902 -        # FUTHER REDUCE COVER WITH EPI
1902 +        # FURTHER REDUCE COVER WITH EPI

21.

1948 -    An unforunate side affect of the Quine-McCluskey system is that x !=
1948 +    An unfortunate side effect of the Quine-McCluskey system is that x !=

22.

1977 -Module that creates and modifys parse trees of well formed
1977 +Module that creates and modifies parse trees of well formed

23.

2003 -    This function produces a parse tree from a boolen formula s.
2003 +    This function produces a parse tree from a boolean formula s.

24.

2042 -        Returns a list of tokens corrosponding to s.
2042 +        Returns a list of tokens corresponding to s.

25.

2137 -             are occuring.
2137 +             are occurring.

26.

2267 -It is not an error to use nonsenical numeric inputs.
2267 +It is not an error to use nonsensical numeric inputs.

27.

2326 -                  with each variable occuring only once.
2326 +                  with each variable occurring only once.

28.

2370 -        Strange paramaters can lead to the table header with no body.
2370 +        Strange parameters can lead to the table header with no body.

29.

2415 -        Strange paramaters can lead to the table header with no body.
2415 +        Strange parameters can lead to a table header with no body.

30.

2478 -    Formulas consist of the operators &, |, ~, ^, ->, <->, corrosponding
2478 +    Formulas consist of the operators &, |, ~, ^, ->, <->, corresponding

31.

2481 -    underscores and aplphanumerics.  Parentheses may be used to
2481 +    underscores and alphanumerics.  Parentheses may be used to

32.

362 -        Returns a latex representation of this statement.
362 +        Returns a LaTeX representation of this statement.

33.

368 -            Returns the latex representation of this statement.
368 +            Returns the LaTeX representation of this statement.

34.

384 +            other --the left hand side statement.
384 +            other -- the left hand side statement.

35.

404 +            other --the left hand side statement.
404 +            other -- the left hand side statement.

36.

425 -            other --the left hand side statement.
425 +            other -- the left hand side statement.

37.

446 -            other --the left hand side statement.
446 +            other -- the left hand side statement.

38.

467 -            other --the left hand side statement.
467 +            other -- the left hand side statement.

39.

490 -            other --the left hand side statement.
490 +            other -- the left hand side statement.

40.

511 -            other --the left hand side statement.
511 +            other -- the left hand side statement.

41.

533 -            other --the left hand side statement.
533 +            other -- the left hand side statement.

42.

537 -            right hand side and false otherwise.
537 +            right hand side, and false otherwise.

43.

558 -        start inclusive and end exclusive so a truthtable(0, 2) will include
558 +        start inclusive and end exclusive so truthtable(0, 2) will include

44.

572 -            Returns the truthtable (a 2-d array with the creating statement
572 +            Returns the truthtable (a 2-D array with the creating statement

45. Please carefully read through the following snippet from the original diff file:

590 +        We can now create truthtable of rows 1 to 5
591 +            sage: s.truthtable(1, 5)
592 +            a      b      c      value
593 +            False  False  True   False
594 +            False  True   False  True
595 +            False  True   True   False
596 +            True   False  False  False

Why "rows 1 to 5" when you're using the command s.truthtable(1, 5)? My understanding is that s.truthtable(1, 5) includes row 1 all the way up to but excluding row 5. In effect, that command actually creates 4 rows, excluding the standard header row. Perhaps you might want to consider this diff:

590 -        We can now create truthtable of rows 1 to 5
590 +        We can now create a truth table of rows 1 to 4, inclusive.

or this one:

590 -        We can now create truthtable of rows 1 to 5
590 +        We can now create a truth table of rows 1 to 5, exclusive.

46.

637 -        It does this by examining the truthtable of the formula.
637 +        It does this by examining the truth table of the formula.

47.

653 -            This method creates the cnf parse tree by examining the logic
653 +            This method creates the CNF parse tree by examining the logic

48.

699 -            Unless a formula is already in (or close to) being in cnf convert_cnf()
699 +            Unless a formula is already in (or close to) being in CNF, convert_cnf()

49. No tabs, please. This issue is especially important since we're using Python and most folks who program in Python use only spaces --- NOT tabs --- for their indentation. For official reasons why tabs are not used, please refer to PEP 666. The Sage Developer's Guide provides various general guidelines to be adhered to when writing code (and documentation) to be included within Sage itself. In particular, you might want to consult this section. If you feel that my comment is unfair to you, please don't flame me. Instead, provide me with reasons why it's unfair (to you). If your reasons turn out to be valid and they show that I'm being unfair, I'd stand corrected and offer you my apology.

711 -	    See www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps for a
711 +        See www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps for a

50.

730 -            cnf form by a call to convert_cnf() or convert_cnf_recur()
730 +            CNF form by a call to convert_cnf() or convert_cnf_recur(),

51.

806 -            cnf form by a call to convert_cnf() or convert_cnf_recur()
806 +            CNF form by a call to convert_cnf() or convert_cnf_recur(),

52.

838 -        '~', operators.
838 +        '~' operators.

53.

1117 -            The next operator in the string
1117 +            The next operator in the string.

54.

1276 -        Will create a composite functor which will add 1, multiply by
1276 +        will create a composite functor which will add 1, multiply by

55.

1343 -    is defined so that that tc(ast) returns the count of ts.  The
1343 +    is defined so that tc(ast) returns the count of ts.  The

56.

1575 -    The exclusive-or operator, will turn into:
1575 +    The exclusive-or operator will turn into:

57.

1945 -    DNF formulae generated from prepositional logic ASTs as described
1945 +    DNF formulae generated from propositional logic ASTs as described

58.

2216 -A logic table is essentially a 2-d array that is created by the statement class
2216 +A logic table is essentially a 2-D array that is created by the statement class

59.

2221 -For instance, with the variables A, B, and C the truthtable looks like:
2221 +For instance, with the variables A, B, and C the truth table looks like:

60.

2233 -This is equivalent to counting in binary, where a table would appear thusly;
2233 +This is equivalent to counting in binary, where a table would appear thus:

61.

2279 -If one argument is provided truthtable defaults to the end.
2279 +If one argument is provided, truthtable defaults to the end.

62.

2291 -If the second argument is negative truthtable defaults to the end.
2291 +If the second argument is negative, truthtable defaults to the end.

63.

2324 -            t -- a 2-d array containing the table values
2324 +            t -- a 2-D array containing the table values.

64.

2396 -            self -- the calling object: not used
2396 +            self -- the calling object: not used.

65.

2454 -            self -- the calling object: not used
2454 +            self -- the calling object: not used.

66.

2592 -    Formula returns an instance if BooleanFormula if possible, and throws
2592 +    Formula returns an instance of BooleanFormula if possible, and throws

Minh,

you should really post patches on top of given patches to make it easier to apply your changes.

Cheers,

Michael

Replying to mabshoff:

you should really post patches on top of given patches to make it easier to apply your changes.

You mean like applying the original patch first, then upload a patch of the patched file? Is that what you mean?

Replying to mvngu:

You mean like applying the original patch first, then upload a patch of the patched file? Is that what you mean?

Yes, exactly.

Cheers,

Michael

Chris,

do *not* attach tgz files to trac since it causes massive problems. Instead post plain hg patches.

Cheers,

Michael

Replying to mabshoff:

Replying to mvngu:

You mean like applying the original patch first, then upload a patch of the patched file? Is that what you mean?

Yes, exactly.

I'm having trouble applying the patch logic.hg. For example, I've received this abort message:

sage: hg_sage.patch("/home/mvngu/usr/bin/sage-3.1.4/devel/sage-mvngu-review/patch-review/logic.hg")
cd "/home/mvngu/usr/bin/sage-3.1.4/devel/sage" && hg status
cd "/home/mvngu/usr/bin/sage-3.1.4/devel/sage" && hg status
cd "/home/mvngu/usr/bin/sage-3.1.4/devel/sage" && hg import   "/home/mvngu/usr/bin/sage-3.1.4/devel/sage-mvngu-review/patch-review/logic.hg"
applying /home/mvngu/usr/bin/sage-3.1.4/devel/sage-mvngu-review/patch-review/logic.hg
abort: no diffs found

OK, so perhaps it's because logic.hg is bzip2 compressed:

$ file logic.hg 
logic.hg: Mercurial changeset bundle (bzip2 compressed)

But why can't I do bunzip2:

$ bunzip2 logic.hg 
bunzip2: Can't guess original name for logic.hg -- using logic.hg.out
bunzip2: logic.hg is not a bzip2 file.

Any other way(s) of getting the diff file(s) bundled in logic.hg?

Having trouble with the patch, don't use logic.patch.

Fixed documentation.

All of mvngu's changes have been incorporated into logic2.patch.

Improve latex output for boolean formulas, fix a few spelling mistakes

Bizarrely this patch put *all* the new code in a bunch of files in SAGE_ROOT/devel/sage/!? This code should go in SAGE_ROOT/devel/sage/sage/logic and be properly imported. I'm really confused about what happened here.

was@sage:~/build/sage-3.2.rc1/devel/sage$ ls
booleval.py     build     c_lib    install         MANIFEST.in      PKG-INFO     README.txt    sage-push          spkg-delauto
boolformula.py  build.py  clib.py  logicparser.py  module_list.py   propcalc.py  sage          setup.py           spkg-dist
boolopt.py      bundle    export   logictable.py   module_list.pyc  pull         sagebuild.py  spkg-debian-maybe  spkg-install

Note the boolformula.py, etc., above.

Once there are new patches someone please clean up the old deadwood.

Cheers,

Michael

Changed directory.

I believe this patch should output to SAGE_ROOT/devel/sage/sage/logic. I'm not sure if it is being imported properly.

It doesn't have the trac_545_latex.patch applied against it either. Should this be done?

Target time for the review: January 11th