polish the new symbolic logic code.

[williamstein]

This is a single commit bundle, so if somebody could extract the patch and post it here it would be a good idea.

Cheers,

Michael

Component: basic arithmetic

Keywords: editor_wstein

Issue created by migration from https://trac.sagemath.org/ticket/545

[williamstein]

comment:1

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.

[williamstein]

comment:2

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

[williamstein]

comment:4

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.

[williamstein]

comment:5

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

[pdenapo]

comment:6

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)

[pdenapo]

comment:7

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)

[williamstein]

comment:8

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

[williamstein]

comment:9

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

[williamstein]

Attachment: logic.hg.gz

this is from chris gorecki

[aghitza]

comment:14

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.

[robertwb]

comment:15

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.

[craigcitro]

Changed keywords from none to editor_wstein

[williamstein]

Attachment: sekine.pdf.gz

This is the referee report

[williamstein]

comment:17

REFEREE REPORT:
See the attached file sekine.pdf.

[williamstein]

comment:19

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

[sagetrac-GeorgSWeber]

comment:40

Urgh.

Currently this ticket already has three different patches to be applied from three different guys.

I've made my case, please another one step in and review this, thanks!

(The long doctests now do pass --- but there is the coverage problem, which is essentially a hen-and-egg problem: the code does not go into Sage because of the coverage, but who would work on code not being in Sage to make the coverage higher?)

[robertwb]

comment:41

In my experience, the motivation to increase coverage is the highest when trying to get something in.

How essential is boolopt.py to the rest of the package? Could it be pushed to a separate ticket (enhancement).

boolformula.py could probably be brought up to 100% without too much effort.

[sagetrac-GeorgSWeber]

comment:42

Ahh, excellent idea, this was just the input needed here. Robert, thank you very much!

So now what's to do (if nobody else does it, I'll do it):

• move the file "boolopt.py" to its own (enhancement) ticket "with patch, needs work" (easy)

• adjust the other five files of this patch so that they are stand-alone (rather easy, essentially only the "simplify" function in boolformula.py is concerned)

• add the two missing doctests to boolformula.py (very easy)

Please note that the file "logic.py" which has missing doctests according to the coverage report above is not among the new files, but already a part of Sage!
(So it couldn't possibly block this ticket to finally go in. But of course, it needs to be cleaned up itself.)

[sagetrac-mabshoff]

comment:43

Georg,

thanks for working on this since this is an incredible messy ticket. The main point here is that added functionality must be doctested while it is nice to increase the coverage on existing code that is being worked on. So I agree with the approach here. In addition you should open an enhancement ticket to get coverage of logic.py to 100%, too.

Cheers,

Michael

[sagetrac-mvngu]

Attachment: trac_545_boolformula-doctests.patch.gz

Bring doctest coverage of boolformula.py up to 100%

[sagetrac-mvngu]

comment:44

Replying to @sagetrac-GeorgSWeber:

• add the two missing doctests to boolformula.py (very easy)

This is done by trac_545_boolformula-doctests.patch.

[sagetrac-mvngu]

comment:45

So what happens here is one should apply the following in the specified order as suggested by Georg:

1. first apply logic4.patch
2. then trac_545_latex.patch
3. and finally trac_545_long-doctests-fixed.patch

Now trac_545_latex.patch applied fine, but hunk #2 suceeded with fuzz, as reported by Georg. Apart from this fuzz, all the above three patches applied OK in the specified order against 3.4-alpha0. Doctests including -long passed. Having done so, one can then apply trac_545_boolformula-doctests.patch (based on 3.4-alpha0) which adds two missing doctests to boolformula.py.

[sagetrac-mvngu]

based on sage-3.4.2.alpha0

[sagetrac-mvngu]

Attachment: trac_545-logic5.patch.gz

based on sage-3.4.2.alpha0

[sagetrac-mvngu]

Attachment: trac_545-latex2.patch.gz

Attachment: trac_545-adjust-simplify.patch.gz

based on sage-3.4.2.alpha0

[sagetrac-mvngu]

comment:46

Apply patches in the following order:

1. trac_545-logic5.patch -- Basically the same as logic4.patch, but without including those diff lines for boolopt.py. The module boolopt.py is now moved to ticket move logic module boolopt.py to another enhancement ticket #5910 as an enhancement.
2. trac_545-latex2.patch -- Essentially the same as trac_545_latex.patch, but you won't see any fuzz when applying it.
3. trac_545_long-doctests-fixed.patch
4. trac_545_boolformula-doctests.patch -- This should bring doctest coverage of boolformula.py up to 100%.
5. trac_545-adjust-simplify.patch -- This adjusts the method simplify() in boolformula.py and all doctests that uses simplify(). So this patch only touches boolformula.py and propcalc.py.
   If I read this ticket correctly, I think only trac_545_boolformula-doctests.patch and trac_545-adjust-simplify.patch need to be reviewed.

[sagetrac-whuss]

comment:47

In the class BooleanFormula there is a spelling mistake in a function name,
"equivlant" instead of equivalent. The same mistake is repeated a few times
in the documentation.

[sagetrac-whuss]

fix spelling mistakes

[sagetrac-GeorgSWeber]

Attachment: equivlant.patch.gz

Attachment: trac_545-equivlant_rebased.patch.gz

apply after the other five patches instead of "equivlant.patch"

[sagetrac-GeorgSWeber]

comment:48

Minh, thanks for your good work!
After applying the five patches Minh mentioned in the correct order to Sage-3.4.2.alpha0, the equivlant.patch didn't apply. So I rebased and made it such that Wilfried's name appears in it as originator.

Positive review to the sequence of five patches Minh mentioned. And positive review to the changes of Wilfried (I really did nothing but rebase them). The main author here is Chris Gorecki, of course.

After this ticket is finally closed (Requiescat In Pacem), the next steps would be to dismiss "logic.py" (I think it becomes mostly obsolete by this patch here), add the "rest" as a logic chapter to the Sphinx documentation (probably this needs some work, but hopefully some scripts will be available to help), and finally work on/solve #5910.

Cheers, gsw

[sagetrac-mabshoff]

comment:49

Merged

• trac_545-logic5.patch
• trac_545-latex2.patch
• trac_545_long-doctests-fixed.patch
• trac_545_boolformula-doctests.patch
• trac_545-adjust-simplify.patch
• trac_545-equivlant_rebased.patch

in Sage 3.4.2.rc0. Note that there are some odd whitespace issues in those files, so if someone could take care of that at #5910 it would be splendid :)

Cheers,

Michael