Ticket #5910: trac_5910-doctest-simplify.patch

File trac_5910-doctest-simplify.patch, 8.6 KB (added by mvngu, 4 years ago)

Restore the method simplify() and its doctests

  • sage/logic/boolformula.py 

    # HG changeset patch
# User Minh Van Nguyen <nguyenminh2@gmail.com>
# Date 1240834030 25200
# Node ID 4fad8f552f62fbbc6e5dabf5f018f3533dc0f0ab
# Parent  3480240d9df8532648e26d06e0d261de0a950d4a
trac 5910: add Chris Gorecki's doctests for simplify(), which was removed in trac 545

diff -r 3480240d9df8 -r 4fad8f552f62 sage/logic/boolformula.py
    a b  
    6565        sage: f 
    6666        (a|~b|c)&(a|~b|~c)&(~a|b|~c) 
    6767 
     68    We can also simplify an expression. 
     69 
     70        sage: f = propcalc.formula("a&((b|c)^a->c)<->b") 
     71        sage: f.truthtable() 
     72        a      b      c      value 
     73        False  False  False  True 
     74        False  False  True   True 
     75        False  True   False  False 
     76        False  True   True   False 
     77        True   False  False  True 
     78        True   False  True   False 
     79        True   True   False  True 
     80        True   True   True   True 
     81        sage: f.simplify() 
     82        (~a&~b)|(a&~b&~c)|(a&b) 
     83        sage: f.truthtable() 
     84        a      b      c      value 
     85        False  False  False  True 
     86        False  False  True   True 
     87        False  True   False  False 
     88        False  True   True   False 
     89        True   False  False  True 
     90        True   False  True   False 
     91        True   True   False  True 
     92        True   True   True   True 
     93 
    6894    Or determine if an epression is satisfiable, a contradiction, or a tautology. 
    6995        sage: f = propcalc.formula("a|b") 
    7096        sage: f.is_satisfiable() 
    … …  
    121147import booleval 
    122148import logictable 
    123149import logicparser 
    124 #import boolopt 
     150import boolopt 
    125151from types import * 
    126152 
    127153latex_operators = [('&', '\\wedge '), 
    … …  
    792818        s = 'p cnf ' + str(len(self.__vars_order)) + ' ' + str(clauses) + '\n' + s 
    793819        return s[:-1]     
    794820 
    795 #    def simplify(self): 
    796 #        r""" 
    797 #        This function uses the propcalc package to simplify an expression to 
    798 #        its minimal form. 
    799 # 
    800 #        INPUT: 
    801 #             self -- the calling object. 
    802 # 
    803 #        OUTPUT: 
    804 #            A simplified expression. 
    805 # 
    806 #        EXAMPLES:       
    807 #            sage: import sage.logic.propcalc as propcalc 
    808 #            sage: f = propcalc.formula("a&((b|c)^a->c)<->b") 
    809 #            sage: f.truthtable() 
    810 #            a      b      c      value 
    811 #            False  False  False  True 
    812 #            False  False  True   True 
    813 #            False  True   False  False 
    814 #            False  True   True   False 
    815 #            True   False  False  True 
    816 #            True   False  True   False 
    817 #            True   True   False  True 
    818 #            True   True   True   True 
    819 #            sage: f.simplify() 
    820 #            (~a&~b)|(a&~b&~c)|(a&b) 
    821 #            sage: f.truthtable() 
    822 #            a      b      c      value 
    823 #            False  False  False  True 
    824 #            False  False  True   True 
    825 #            False  True   False  False 
    826 #            False  True   True   False 
    827 #            True   False  False  True 
    828 #            True   False  True   False 
    829 #            True   True   False  True 
    830 #            True   True   True   True 
    831 #             
    832 #        NOTES: 
    833 #            If the instance of boolean formula has not been converted to  
    834 #            cnf form by a call to convert_cnf() or convert_cnf_recur()  
    835 #            satformat() will call convert_cnf().  Please see the notes for 
    836 #            convert_cnf() and convert_cnf_recur() for performance issues. 
    837 #        """ 
    838 #        exp = '' 
    839 #        self.__tree = logicparser.apply_func(self.__tree, self.reduce_op) 
    840 #        plf = logicparser.apply_func(self.__tree, self.convert_opt) 
    841 #        wff = boolopt.PLFtoWFF()(plf) # convert to positive-normal form 
    842 #        wtd = boolopt.WFFtoDNF() 
    843 #        dnf = wtd(wff) 
    844 #        dnf = wtd.clean(dnf) 
    845 #        if(dnf == [] or dnf == [[]]): 
    846 #            exp = self.__vars_order[0] + '&~' + self.__vars_order[0] + ' ' 
    847 #        opt = boolopt.optimize(dnf) 
    848 #        if(exp == '' and (opt == [] or opt == [[]])): 
    849 #            exp = self.__vars_order[0] + '|~' + self.__vars_order[0] + ' ' 
    850 #        if(exp == ''): 
    851 #            for con in opt: 
    852 #                s = '(' 
    853 #                for prop in con: 
    854 #                    if(prop[0] == 'notprop'): 
    855 #                       s += '~' 
    856 #                    s += prop[1] + '&' 
    857 #                exp += s[:-1] + ')|' 
    858 #        self.__expression = exp[:-1] 
    859 #        self.__tree, self.__vars_order = logicparser.parse(self.__expression)  
    860 #        return BooleanFormula(self.__expression, self.__tree, self.__vars_order) 
     821    def simplify(self): 
     822        r""" 
     823        This function uses the propcalc package to simplify an expression to 
     824        its minimal form. 
     825 
     826        INPUT: 
     827             self -- the calling object. 
     828 
     829        OUTPUT: 
     830            A simplified expression. 
     831 
     832        EXAMPLES:        
     833            sage: import sage.logic.propcalc as propcalc 
     834            sage: f = propcalc.formula("a&((b|c)^a->c)<->b") 
     835            sage: f.truthtable() 
     836            a      b      c      value 
     837            False  False  False  True 
     838            False  False  True   True 
     839            False  True   False  False 
     840            False  True   True   False 
     841            True   False  False  True 
     842            True   False  True   False 
     843            True   True   False  True 
     844            True   True   True   True 
     845            sage: f.simplify() 
     846            (~a&~b)|(a&~b&~c)|(a&b) 
     847            sage: f.truthtable() 
     848            a      b      c      value 
     849            False  False  False  True 
     850            False  False  True   True 
     851            False  True   False  False 
     852            False  True   True   False 
     853            True   False  False  True 
     854            True   False  True   False 
     855            True   True   False  True 
     856            True   True   True   True 
     857             
     858        NOTES: 
     859            If the instance of boolean formula has not been converted to  
     860            cnf form by a call to convert_cnf() or convert_cnf_recur()  
     861            satformat() will call convert_cnf().  Please see the notes for 
     862            convert_cnf() and convert_cnf_recur() for performance issues. 
     863        """ 
     864        exp = '' 
     865        self.__tree = logicparser.apply_func(self.__tree, self.reduce_op) 
     866        plf = logicparser.apply_func(self.__tree, self.convert_opt) 
     867        wff = boolopt.PLFtoWFF()(plf) # convert to positive-normal form 
     868        wtd = boolopt.WFFtoDNF() 
     869        dnf = wtd(wff) 
     870        dnf = wtd.clean(dnf) 
     871        if(dnf == [] or dnf == [[]]): 
     872            exp = self.__vars_order[0] + '&~' + self.__vars_order[0] + ' ' 
     873        opt = boolopt.optimize(dnf) 
     874        if(exp == '' and (opt == [] or opt == [[]])): 
     875            exp = self.__vars_order[0] + '|~' + self.__vars_order[0] + ' ' 
     876        if(exp == ''): 
     877            for con in opt: 
     878                s = '(' 
     879                for prop in con: 
     880                    if(prop[0] == 'notprop'): 
     881                       s += '~' 
     882                    s += prop[1] + '&' 
     883                exp += s[:-1] + ')|' 
     884        self.__expression = exp[:-1] 
     885        self.__tree, self.__vars_order = logicparser.parse(self.__expression)  
     886        return BooleanFormula(self.__expression, self.__tree, self.__vars_order) 
    861887 
    862888    def convert_opt(self, tree): 
    863889        r""" 

  • sage/logic/propcalc.py 

    diff -r 3480240d9df8 -r 4fad8f552f62 sage/logic/propcalc.py
    a b  
    5959        sage: f 
    6060        (a|~b|c)&(a|~b|~c)&(~a|b|~c) 
    6161 
     62    We can also simplify an expression. 
     63 
     64        sage: f = propcalc.formula("a&((b|c)^a->c)<->b") 
     65        sage: f.truthtable() 
     66        a      b      c      value 
     67        False  False  False  True 
     68        False  False  True   True 
     69        False  True   False  False 
     70        False  True   True   False 
     71        True   False  False  True 
     72        True   False  True   False 
     73        True   True   False  True 
     74        True   True   True   True 
     75        sage: f.simplify() 
     76        (~a&~b)|(a&~b&~c)|(a&b) 
     77        sage: f.truthtable() 
     78        a      b      c      value 
     79        False  False  False  True 
     80        False  False  True   True 
     81        False  True   False  False 
     82        False  True   True   False 
     83        True   False  False  True 
     84        True   False  True   False 
     85        True   True   False  True 
     86        True   True   True   True 
     87 
    6288    Or determine if an expression is satisfiable, a contradiction, or a tautology. 
    6389        sage: f = propcalc.formula("a|b") 
    6490        sage: f.is_satisfiable()