/* Copyright (C) 2009 Hugh McGuire http://www.cis.gvsu.edu/~mcguire/ * Grand Valley State University, MI 49401-9403 */ /* This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. For a copy of the GNU General Public License, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth floor, Boston, MA 02110-1301, USA. Another option as of January 1, 2009 is to browse the following URL: http://www.gnu.org/copyleft/gpl.html */ import java.awt.Toolkit; import javax.swing.JOptionPane; import javax.swing.JLabel; import java.awt.GridLayout; import javax.swing.JTable; import javax.swing.JButton; import javax.swing.JPanel; import javax.swing.JDialog; import javax.swing.JFrame; import java.awt.event.KeyEvent; import java.awt.Container; import javax.swing.JTextArea; import javax.swing.JScrollPane; import java.awt.BorderLayout; import javax.swing.InputMap; import java.awt.Event; import javax.swing.KeyStroke; import javax.swing.text.DefaultEditorKit; import java.awt.Font; import java.util.ArrayList; import java.util.LinkedList; import java.util.ListIterator; import java.awt.event.ActionEvent; import java.awt.event.ActionListener; import java.awt.event.WindowAdapter; import java.awt.event.WindowEvent; import javax.swing.AbstractAction; /** * Handles the Rewriting deduction. * @author Hugh McGuire */ class Canonical_Eqs extends JDialog { static final String PHI_1 = Character.toString(Symbol.PHI_LOWERCASE_UNICODE) + Symbol.SUBSCRIPT_1_UNICODE; static final String PHI_2 = Character.toString(Symbol.PHI_LOWERCASE_UNICODE) + Symbol.SUBSCRIPT_2_UNICODE; static final String PHI_3 = Character.toString(Symbol.PHI_LOWERCASE_UNICODE) + Symbol.SUBSCRIPT_3_UNICODE; static final String PHI_BRACKETED = "[" + Symbol.PHI_LOWERCASE_UNICODE + ']'; /* static final String CLOSING_PAREN_W_PHI_BRACKETED = ')' + PHI_BRACKETED; static final String NU_CLOSEPAREN_PHIBRACKETED = NU_LOWERCASE_UNICODE + CLOSING_PAREN_W_PHI_BRACKETED; */ static final String TAU_1 = Character.toString(Symbol.TAU_LOWERCASE_UNICODE) + Symbol.SUBSCRIPT_1_UNICODE; static final String TAU_2 = Character.toString(Symbol.TAU_LOWERCASE_UNICODE) + Symbol.SUBSCRIPT_2_UNICODE; static final String TAU_1_ = TAU_1 + ' '; static final String TAU_2_ = ' ' + TAU_2; static final String TAU_3 = Character.toString(Symbol.TAU_LOWERCASE_UNICODE) + Symbol.SUBSCRIPT_3_UNICODE; // Incidentally, there's a little waste since some |Expression|s get // constructed though not necessarily used. //private Deduction.Rewrite rewrite_action; private JTable table; private PB_TableModel table_model; private Container content_pane; private Deduction_Prep prep; private boolean consideration; private String not_, and_, or_, xor_, implies_, equiv_, forall, exists, times; private final String PLUS_ = " + "; private void note_symbols_used(Expression expr) { if ( expr == null ) return; // recursing first ==> more likely end up with top-level values note_symbols_used(expr.get_argument2()); note_symbols_used(expr.get_argument1()); switch ( expr.get_operator().get_specifier() ) { case NOT: not_ = expr.get_operator().get_text(); if ( not_.equalsIgnoreCase("NOT") ) not_ += ' '; break; case AND: and_ = ' ' + expr.get_operator().get_text() + ' '; break; case OR: or_ = ' ' + expr.get_operator().get_text() + ' '; break; case XOR: xor_ = ' ' + expr.get_operator().get_text() + ' '; break; case IMPLIES: implies_ = ' ' + expr.get_operator().get_text() + ' '; break; case EQUIV: equiv_ = ' ' + expr.get_operator().get_text() + ' '; break; case FORALL: forall = expr.get_operator().get_text(); break; case EXISTS: exists = expr.get_operator().get_text(); break; case TIMES: times = expr.get_operator().get_text(); break; } } void activate_item(final String form_subexpr, final String form_replacement, final Expression replacement ) { consideration = true; JButton button = new JButton( new AbstractAction( "rewrite the form \"" + form_subexpr + "\" to \"" + form_replacement + '"' ) { public void actionPerformed(ActionEvent ae) { prep.subexpr.this_structure_replace(replacement); String narrative_base = " the form \"" + form_subexpr + "\"\n\tto \"" + form_replacement + '"'; table_model .add( prep.selected_rows, prep.selected_column_id, table_model.EQUIV_BY_ + "rewriting the form \"" + form_subexpr + "\"\n\tto \"" + form_replacement + '"', "With formula " + prep.ref_num_name + ", we can\nrewrite the form \"" + form_subexpr + "\"\nto \"" + form_replacement + "\", yielding:", prep.expr ); setVisible(false); // ?deallocate? } } ); button.setFont( new Font( "Monospaced", Font.PLAIN, table.getFont().getSize() ) ); content_pane.add(button); } Canonical_Eqs(JTable table_given) { //Create and set up the window. // here |super((table = table_given)....| doesn't work super((JFrame) table_given.getTopLevelAncestor(), "Apply a canonical equivalence", true ); //dialog.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); //rewrite_action = action_given; table = table_given; table_model = (PB_TableModel) table.getModel(); //JPanel content_pane = new JPanel(new BorderLayout()); content_pane = getContentPane(); content_pane.setLayout(new GridLayout(0, 1)); JLabel label = new JLabel( " Select one of the following rewritings, or \"Cancel\":" ); label.setFont( label.getFont().deriveFont( table.getFont().getSize2D() ) ); content_pane.add(label); prep = new Deduction_Prep(table); prep.subexpr = prep.subexpr.ungroup(); Symbol.Specifier logical_negation_sym_spec = prep.expressionsmgmt.get_lognegsymspec(); final Expression arg1 = prep.subexpr.get_argument1(); final Expression arg2 = prep.subexpr.get_argument2(); Expression arg1_ungroup, arg1_negand, arg2_ungroup, arg2_negand; if ( arg1 != null ) { arg1_ungroup = arg1.ungroup(); arg1_negand = arg1_ungroup.op_spec_equals(logical_negation_sym_spec) ? arg1_ungroup.get_argument1() : null; } else { arg1_ungroup = null; arg1_negand = null; } if ( arg2 != null ) { arg2_ungroup = arg2.ungroup(); arg2_negand = arg2_ungroup.op_spec_equals(logical_negation_sym_spec) ? arg2_ungroup.get_argument1() : null; } else { arg2_ungroup = null; arg2_negand = null; } not_ = prep.expressionsmgmt.get_spec_String(Symbol.Specifier.NOT); if ( not_.toUpperCase().equals("NOT") ) not_ += ' '; and_ = ' ' + prep.expressionsmgmt.get_spec_String(Symbol.Specifier.AND) + ' '; or_ = ' ' + prep.expressionsmgmt.get_spec_String(Symbol.Specifier.OR) + ' '; xor_ = ' ' + prep.expressionsmgmt.get_spec_String(Symbol.Specifier.XOR) + ' '; implies_ = ' ' + prep.expressionsmgmt.get_spec_String(Symbol.Specifier.IMPLIES) + ' '; equiv_ = ' ' + prep.expressionsmgmt.get_spec_String(Symbol.Specifier.EQUIV) + ' '; forall = prep.expressionsmgmt.get_spec_String(Symbol.Specifier.FORALL); exists = prep.expressionsmgmt.get_spec_String(Symbol.Specifier.EXISTS); times = prep.expressionsmgmt.get_spec_String(Symbol.Specifier.TIMES); // obtaining them from the specific overall formula under consideration // is better: note_symbols_used(prep.expr); // obtaining them from the selected subexpression to be manipulated // is best: note_symbols_used(prep.subexpr); String if_ = prep.expressionsmgmt.get_spec_String(Symbol.Specifier.IMPLIES) .equalsIgnoreCase("then") ? "if " : ""; // I tried to order the following chunks of code // so more useful items would end up more 'at hand': if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.op_spec_equals(Symbol.Specifier.AND) && arg2_ungroup.op_spec_equals(Symbol.Specifier.AND) && arg1_ungroup.get_argument1() .equivalent_form(arg2_ungroup.get_argument1()) ) activate_item( '(' + PHI_1 + and_ + PHI_2 + ')' + or_ + '(' + PHI_1 + and_ + PHI_3 + ')', PHI_1 + and_ + '(' + PHI_2 + or_ + PHI_3 + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_ungroup.get_argument1(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1_ungroup.get_argument2(), arg2_ungroup.get_argument2() ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.op_spec_equals(Symbol.Specifier.AND) && arg2_ungroup.op_spec_equals(Symbol.Specifier.AND) && arg1_ungroup.get_argument2() .equivalent_form(arg2_ungroup.get_argument2()) ) activate_item( '(' + PHI_1 + and_ + PHI_3 + ')' + or_ + '(' + PHI_2 + and_ + PHI_3 + ')', '(' + PHI_1 + or_ + PHI_2 + ')' + and_ + PHI_3, new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1_ungroup.get_argument1(), arg2_ungroup.get_argument1() ).ensure_group(), arg1_ungroup.get_argument2() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg1_ungroup.op_spec_equals(Symbol.Specifier.OR) && arg2_ungroup.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.get_argument1() .equivalent_form(arg2_ungroup.get_argument1()) ) activate_item( '(' + PHI_1 + or_ + PHI_2 + ')' + and_ + '(' + PHI_1 + or_ + PHI_3 + ')', PHI_1 + or_ + '(' + PHI_2 + and_ + PHI_3 + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1_ungroup.get_argument1(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_ungroup.get_argument2(), arg2_ungroup.get_argument2() ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg1_ungroup.op_spec_equals(Symbol.Specifier.OR) && arg2_ungroup.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.get_argument2() .equivalent_form(arg2_ungroup.get_argument2()) ) activate_item( '(' + PHI_1 + or_ + PHI_3 + ')' + and_ + '(' + PHI_2 + or_ + PHI_3 + ')', '(' + PHI_1 + and_ + PHI_2 + ')' + or_ + PHI_3, new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_ungroup.get_argument1(), arg2_ungroup.get_argument1() ).ensure_group(), arg1_ungroup.get_argument2() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg1_ungroup.op_spec_equals(Symbol.Specifier.IMPLIES) && arg2_ungroup.op_spec_equals(Symbol.Specifier.IMPLIES) && arg1_ungroup.get_argument1() .equivalent_form(arg2_ungroup.get_argument2()) && arg1_ungroup.get_argument2() .equivalent_form(arg2_ungroup.get_argument1()) ) activate_item( '(' + if_ + PHI_1 + implies_ + PHI_2 + ')' + and_ + '(' + if_ + PHI_2 + implies_ + PHI_1 + ')', PHI_1 + equiv_ + PHI_2, new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg1_ungroup.get_argument1().un_if(), arg1_ungroup.get_argument2().un_if() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.op_spec_equals(Symbol.Specifier.AND) && arg2_ungroup.op_spec_equals(Symbol.Specifier.AND) ) { Expression arg2_arg1 = arg2_ungroup.get_argument1(); Expression arg2_arg1_ungroup = arg2_arg1.ungroup(); Expression arg2_arg2 = arg2_ungroup.get_argument2(); Expression arg2_arg2_ungroup = arg2_arg2.ungroup(); if ( arg2_arg1_ungroup.op_spec_equals(logical_negation_sym_spec) && arg2_arg2_ungroup.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.get_argument1() .equivalent_form(arg2_arg1_ungroup.get_argument1()) && arg1_ungroup.get_argument2() .equivalent_form(arg2_arg2_ungroup.get_argument1()) ) activate_item( prep.expressionsmgmt .get_useprimefornot() ? '(' + PHI_1 + and_ + PHI_2 + ')' + or_ + '(' + PHI_1 + Symbol.PRIME_UNICODE + and_ + PHI_2 + Symbol.PRIME_UNICODE + ')' : '(' + PHI_1 + and_ + PHI_2 + ')' + or_ + '(' + not_ + PHI_1 + and_ + not_ + PHI_2 + ')', PHI_1 + equiv_ + PHI_2, new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg1_ungroup.get_argument1(), arg1_ungroup.get_argument2() ) ); } if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.op_spec_equals(Symbol.Specifier.AND) && arg2_ungroup.op_spec_equals(Symbol.Specifier.AND) ) { Expression arg1_arg1 = arg1_ungroup.get_argument1(); Expression arg1_arg1_ungroup = arg1_arg1.ungroup(); Expression arg1_arg2 = arg1_ungroup.get_argument2(); Expression arg1_arg2_ungroup = arg1_arg2.ungroup(); if ( arg1_arg1_ungroup.op_spec_equals(logical_negation_sym_spec) && arg1_arg2_ungroup.op_spec_equals( logical_negation_sym_spec ) && arg2_ungroup.get_argument1() .equivalent_form(arg1_arg1_ungroup.get_argument1()) && arg2_ungroup.get_argument2() .equivalent_form(arg1_arg2_ungroup.get_argument1()) ) activate_item( prep.expressionsmgmt .get_useprimefornot() ? '(' + PHI_1 + Symbol.PRIME_UNICODE + and_ + PHI_2 + Symbol.PRIME_UNICODE + ')' + or_ + '(' + PHI_1 + and_ + PHI_2 + ')' : '(' + not_ + PHI_1 + and_ + not_ + PHI_2 + ')' + or_ + '(' + PHI_1 + and_ + PHI_2 + ')', PHI_1 + equiv_ + PHI_2, new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg2_ungroup.get_argument1(), arg2_ungroup.get_argument2() ) ); } if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.op_spec_equals(Symbol.Specifier.AND) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? '(' + PHI_1 + and_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + PHI_1 + and_ + PHI_2 + ')', '(' + (prep.expressionsmgmt.get_useprimefornot() ? PHI_1 + Symbol.PRIME_UNICODE + or_ + PHI_2 + Symbol.PRIME_UNICODE : not_ + PHI_1 + or_ + not_ + PHI_2 ) + ')', new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.OR ), new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), arg1_ungroup.get_argument1().ensure_group() ), new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), arg1_ungroup.get_argument2().ensure_group() ) ) .ensure_group() ); if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.op_spec_equals(Symbol.Specifier.OR) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? '(' + PHI_1 + or_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + PHI_1 + or_ + PHI_2 + ')', '(' + (prep.expressionsmgmt.get_useprimefornot() ? PHI_1 + Symbol.PRIME_UNICODE + and_ + PHI_2 + Symbol.PRIME_UNICODE : not_ + PHI_1 + and_ + not_ + PHI_2 ) + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), arg1_ungroup.get_argument1().ensure_group() ), new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), arg1_ungroup.get_argument2().ensure_group() ) ) .ensure_group() ); if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.op_spec_equals(Symbol.Specifier.IMPLIES) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? '(' + if_ + PHI_1 + implies_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + if_ + PHI_1 + implies_ + PHI_2 + ')', '(' + (prep.expressionsmgmt.get_useprimefornot() ? PHI_1 + and_ + PHI_2 + Symbol.PRIME_UNICODE : PHI_1 + and_ + not_ + PHI_2 ) + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_ungroup.get_argument1().un_if(), new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), arg1_ungroup.get_argument2().ensure_group() ) ) .ensure_group() ); if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.op_spec_equals(Symbol.Specifier.EQUIV) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? '(' + PHI_1 + equiv_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + PHI_1 + equiv_ + PHI_2 + ')', '(' + (prep.expressionsmgmt.get_useprimefornot() ? PHI_1 + equiv_ + PHI_2 + Symbol.PRIME_UNICODE : PHI_1 + equiv_ + not_ + PHI_2 ) + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg1_ungroup.get_argument1(), new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), arg1_ungroup.get_argument2().ensure_group() ) ) .ensure_group() ); if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.op_spec_equals(Symbol.Specifier.EQUIV) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? '(' + PHI_1 + equiv_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + PHI_1 + equiv_ + PHI_2 + ')', '(' + (prep.expressionsmgmt.get_useprimefornot() ? PHI_1 + Symbol.PRIME_UNICODE + equiv_ + PHI_2 : not_ + PHI_1 + equiv_ + PHI_2 ) + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), arg1_ungroup.get_argument1().ensure_group() ), arg1_ungroup.get_argument2() ) .ensure_group() ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg2_ungroup.op_spec_equals(Symbol.Specifier.OR) ) activate_item( PHI_1 + and_ + '(' + PHI_2 + or_ + PHI_3 + ')', '(' + PHI_1 + and_ + PHI_2 + ')' + or_ + '(' + PHI_1 + and_ + PHI_3 + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1, arg2_ungroup.get_argument1() ).ensure_group(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), (Expression) arg1.clone(), // Avoid aliasing // which did indeed once cause a problem. arg2_ungroup.get_argument2() ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg1_ungroup.op_spec_equals(Symbol.Specifier.OR) ) activate_item( '(' + PHI_1 + or_ + PHI_2 + ')' + and_ + PHI_3, '(' + PHI_1 + and_ + PHI_3 + ')' + or_ + '(' + PHI_2 + and_ + PHI_3 + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_ungroup.get_argument1(), arg2 ).ensure_group(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_ungroup.get_argument2(), (Expression) arg2.clone() // Avoid aliasing // which did indeed once cause a problem. ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg2_ungroup.op_spec_equals(Symbol.Specifier.AND) ) activate_item( PHI_1 + or_ + '(' + PHI_2 + and_ + PHI_3 + ')', '(' + PHI_1 + or_ + PHI_2 + ')' + and_ + '(' + PHI_1 + or_ + PHI_3 + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1, arg2_ungroup.get_argument1() ).ensure_group(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), (Expression) arg1.clone(), // Avoid aliasing // which did indeed once cause a problem. arg2_ungroup.get_argument2() ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.op_spec_equals(Symbol.Specifier.AND) ) activate_item( '(' + PHI_1 + and_ + PHI_2 + ')' + or_ + PHI_3, '(' + PHI_1 + or_ + PHI_3 + ')' + and_ + '(' + PHI_2 + or_ + PHI_3 + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1_ungroup.get_argument1(), arg2 ).ensure_group(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1_ungroup.get_argument2(), (Expression) arg2.clone() // Avoid aliasing // which did indeed once cause a problem. ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.op_spec_equals(logical_negation_sym_spec) && arg2_ungroup.op_spec_equals(logical_negation_sym_spec) ) activate_item( prep.expressionsmgmt .get_useprimefornot() ? PHI_1 + Symbol.PRIME_UNICODE + or_ + PHI_2 + Symbol.PRIME_UNICODE : not_ + PHI_1 + or_ + not_ + PHI_2, prep.expressionsmgmt .get_useprimefornot() ? '(' + PHI_1 + and_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + PHI_1 + and_ + PHI_2 + ')', new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_negand, arg2_negand ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg1_ungroup.op_spec_equals(logical_negation_sym_spec) && arg2_ungroup.op_spec_equals(logical_negation_sym_spec) ) activate_item( prep.expressionsmgmt .get_useprimefornot() ? PHI_1 + Symbol.PRIME_UNICODE + and_ + PHI_2 + Symbol.PRIME_UNICODE : not_ + PHI_1 + and_ + not_ + PHI_2, prep.expressionsmgmt .get_useprimefornot() ? '(' + PHI_1 + or_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + PHI_1 + or_ + PHI_2 + ')', new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1_negand, arg2_negand ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg2_ungroup.op_spec_equals(logical_negation_sym_spec) ) activate_item( prep.expressionsmgmt .get_useprimefornot() ? PHI_1 + and_ + PHI_2 + Symbol.PRIME_UNICODE : PHI_1 + and_ + not_ + PHI_2, prep.expressionsmgmt .get_useprimefornot() ? '(' + if_ + PHI_1 + implies_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + if_ + PHI_1 + implies_ + PHI_2 + ')', new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.IMPLIES ), !if_.equals("") ? new Expression( new Symbol( Symbol.Specifier.OPENING_DELIMITER, if_.trim() ), arg1, new Expression( new Symbol( Symbol.Specifier.CLOSING_DELIMITER, "" ) ) ) : arg1, arg2_negand ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) && arg2_ungroup.op_spec_equals(logical_negation_sym_spec) ) activate_item( prep.expressionsmgmt .get_useprimefornot() ? PHI_1 + equiv_ + PHI_2 + Symbol.PRIME_UNICODE : PHI_1 + equiv_ + not_ + PHI_2, prep.expressionsmgmt .get_useprimefornot() ? '(' + PHI_1 + equiv_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + PHI_1 + equiv_ + PHI_2 + ')', new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg1, arg2_negand ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) && arg1_ungroup.op_spec_equals(logical_negation_sym_spec) ) activate_item( prep.expressionsmgmt .get_useprimefornot() ? PHI_1 + Symbol.PRIME_UNICODE + equiv_ + PHI_2 : not_ + PHI_1 + equiv_ + PHI_2, prep.expressionsmgmt .get_useprimefornot() ? '(' + PHI_1 + equiv_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : not_ + '(' + PHI_1 + equiv_ + PHI_2 + ')', new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg1_negand, arg2 ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.op_spec_equals(logical_negation_sym_spec) ) activate_item( prep.expressionsmgmt .get_useprimefornot() ? PHI_1 + or_ + PHI_2 + Symbol.PRIME_UNICODE : not_ + PHI_1 + or_ + PHI_2, if_ + PHI_1 + implies_ + PHI_2, new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.IMPLIES), !if_.equals("") ? new Expression( new Symbol( Symbol.Specifier.OPENING_DELIMITER, if_.trim() ), arg1_negand, new Expression( new Symbol( Symbol.Specifier.CLOSING_DELIMITER, "" ) ) ) : arg1_negand, arg2 ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.IMPLIES) ) activate_item( if_ + PHI_1 + implies_ + PHI_2 , prep.expressionsmgmt .get_useprimefornot() ? PHI_1 + Symbol.PRIME_UNICODE + or_ + PHI_2 : not_ + PHI_1 + or_ + PHI_2 , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), arg1.un_if().ensure_group() ), arg2 ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.IMPLIES) ) activate_item( if_ + PHI_1 + implies_ + PHI_2 , prep.expressionsmgmt .get_useprimefornot() ? if_ + PHI_2 + Symbol.PRIME_UNICODE + implies_ + PHI_1 + Symbol.PRIME_UNICODE : if_ + not_ + PHI_2 + implies_ + not_ + PHI_1 , new Expression( prep.expressionsmgmt .new_Symbol(Symbol.Specifier.IMPLIES), !if_.equals("") ? new Expression( new Symbol( Symbol.Specifier.OPENING_DELIMITER, if_.trim() ), new Expression( prep.expressionsmgmt .new_Symbol(logical_negation_sym_spec), arg2.ensure_group() ), new Expression( new Symbol( Symbol.Specifier.CLOSING_DELIMITER, "" ) ) ) : new Expression( prep.expressionsmgmt .new_Symbol(logical_negation_sym_spec), arg2.ensure_group() ), new Expression( prep.expressionsmgmt .new_Symbol(logical_negation_sym_spec), arg1.un_if().ensure_group() ) ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) ) activate_item( PHI_1 + equiv_ + PHI_2 , '(' + if_ + PHI_1 + implies_ + PHI_2 + ')' + and_ + '(' + if_ + PHI_2 + implies_ + PHI_1 + ')' , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep.expressionsmgmt .new_Symbol(Symbol.Specifier.IMPLIES), !if_.equals("") ? new Expression( new Symbol( Symbol.Specifier.OPENING_DELIMITER, if_.trim() ), arg1, new Expression( new Symbol( Symbol.Specifier.CLOSING_DELIMITER, "" ) ) ) : arg1, arg2 ).ensure_group(), new Expression( prep.expressionsmgmt .new_Symbol(Symbol.Specifier.IMPLIES), !if_.equals("") ? new Expression( new Symbol( Symbol.Specifier.OPENING_DELIMITER, if_.trim() ), (Expression) arg2.clone(), new Expression( new Symbol( Symbol.Specifier.CLOSING_DELIMITER, "" ) ) ) : (Expression) arg2.clone(), // Avoid aliasing // which did indeed once cause a problem. (Expression) arg1.clone() ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) ) activate_item( PHI_1 + equiv_ + PHI_2 , prep.expressionsmgmt .get_useprimefornot() ? '(' + PHI_1 + and_ + PHI_2 + ')' + or_ + '(' + PHI_1 + Symbol.PRIME_UNICODE + and_ + PHI_2 + Symbol.PRIME_UNICODE + ')' : '(' + PHI_1 + and_ + PHI_2 + ')' + or_ + '(' + not_ + PHI_1 + and_ + not_ + PHI_2 + ')' , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1.ensure_group(), arg2.ensure_group() ), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), ((Expression) arg1.clone() ) .ensure_group() // Avoid aliasing // which did indeed once cause a problem. ), new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec) , ((Expression) arg2.clone() ) .ensure_group() ) ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.XOR) && (prep.parent == null // not associative || !prep.parent.op_spec_equals(Symbol.Specifier.XOR) ) ) { // NEED TO DO MORE if ( !arg1_ungroup.op_spec_equals(Symbol.Specifier.XOR) && !arg2_ungroup.op_spec_equals(Symbol.Specifier.XOR) ) activate_item( PHI_1 + xor_ + PHI_2, prep.expressionsmgmt.get_useprimefornot() ? '(' + PHI_1 + or_ + PHI_2 + ')' + and_ + '(' + PHI_1 + and_ + PHI_2 + ')' + Symbol.PRIME_UNICODE : '(' + PHI_1 + or_ + PHI_2 + ')' + and_ + not_ + '(' + PHI_1 + and_ + PHI_2 + ')', new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1.ensure_group(), arg2.ensure_group() ).ensure_group(), new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.AND ), ((Expression) arg1.clone()).ensure_group(), // Avoid aliasing // which did indeed once cause a problem. ((Expression) arg2.clone()).ensure_group() ).ensure_group() ).ensure_group() ) ); } if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg1_ungroup.op_spec_equals(Symbol.Specifier.AND) ) activate_item( '(' + PHI_1 + and_ + PHI_2 + ')' + and_ + PHI_3 , PHI_1 + and_ + '(' + PHI_2 + and_ + PHI_3 + ')' , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_ungroup.get_argument1(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1_ungroup.get_argument2(), arg2 ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) && arg2_ungroup.op_spec_equals(Symbol.Specifier.AND) ) activate_item( PHI_1 + and_ + '(' + PHI_2 + and_ + PHI_3 + ')' , '(' + PHI_1 + and_ + PHI_2 + ')' + and_ + PHI_3 , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg1, arg2_ungroup.get_argument1() ).ensure_group(), arg2_ungroup.get_argument2() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg1_ungroup.op_spec_equals(Symbol.Specifier.OR) ) activate_item( '(' + PHI_1 + or_ + PHI_2 + ')' + or_ + PHI_3 , PHI_1 + or_ + '(' + PHI_2 + or_ + PHI_3 + ')' , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1_ungroup.get_argument1(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1_ungroup.get_argument2(), arg2 ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) && arg2_ungroup.op_spec_equals(Symbol.Specifier.OR) ) activate_item( PHI_1 + or_ + '(' + PHI_2 + or_ + PHI_3 + ')' , '(' + PHI_1 + or_ + PHI_2 + ')' + or_ + PHI_3 , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg1, arg2_ungroup.get_argument1() ).ensure_group(), arg2_ungroup.get_argument2() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) && arg2_ungroup.op_spec_equals(Symbol.Specifier.EQUIV) ) activate_item( PHI_1 + equiv_ + '(' + PHI_2 + equiv_ + PHI_3 + ')' , '(' + PHI_1 + equiv_ + PHI_2 + ')' + equiv_ + PHI_3 , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg1, arg2_ungroup.get_argument1() ).ensure_group(), arg2_ungroup.get_argument2() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) && arg1_ungroup.op_spec_equals(Symbol.Specifier.EQUIV) ) activate_item( '(' + PHI_1 + equiv_ + PHI_2 + ')' + equiv_ + PHI_3 , PHI_1 + equiv_ + '(' + PHI_2 + equiv_ + PHI_3 + ')' , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg1_ungroup.get_argument1(), new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg1_ungroup.get_argument2(), arg2 ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.AND) ) activate_item( PHI_1 + and_ + PHI_2 , PHI_2 + and_ + PHI_1 , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.AND), arg2, arg1 ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.OR) ) activate_item( PHI_1 + or_ + PHI_2 , PHI_2 + or_ + PHI_1 , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.OR), arg2, arg1 ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EQUIV) ) activate_item( PHI_1 + equiv_ + PHI_2 , PHI_2 + equiv_ + PHI_1 , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.EQUIV), arg2, arg1 ) ); if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.op_spec_equals(Symbol.Specifier.QUANT_SEP) && arg1_ungroup.get_argument1().ungroup() .op_spec_equals(Symbol.Specifier.EXISTS) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? '(' + arg1_ungroup.get_argument1().ungroup() .get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + PHI_BRACKETED + ")' " : not_ + arg1_ungroup.get_argument1().ungroup() .get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + PHI_BRACKETED , prep.expressionsmgmt.get_useprimefornot() ? forall + Symbol.NU_LOWERCASE_UNICODE + "[(" + Symbol.PHI_LOWERCASE_UNICODE + ")']" : forall + Symbol.NU_LOWERCASE_UNICODE + '[' + not_ + Symbol.PHI_LOWERCASE_UNICODE + ']' , new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.QUANT_SEP ), new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.FORALL ), arg1_ungroup.get_argument1().ungroup() .get_argument1() ), //.ensure_group(), new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), arg1_ungroup.get_argument2()//.ensure_group() ) //.ensure_group() ) ); if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.op_spec_equals(Symbol.Specifier.QUANT_SEP) && arg1_ungroup.get_argument1().ungroup() .op_spec_equals(Symbol.Specifier.FORALL) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? '(' + arg1_ungroup.get_argument1().ungroup() .get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + PHI_BRACKETED + ")' " : not_ + arg1_ungroup.get_argument1().ungroup() .get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + PHI_BRACKETED , prep.expressionsmgmt.get_useprimefornot() ? exists + Symbol.NU_LOWERCASE_UNICODE + "[(" + Symbol.PHI_LOWERCASE_UNICODE + ")']" : exists + Symbol.NU_LOWERCASE_UNICODE + '[' + not_ + Symbol.PHI_LOWERCASE_UNICODE + ']' , new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.QUANT_SEP), new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.EXISTS ), arg1_ungroup.get_argument1().ungroup().get_argument1() ), //.ensure_group(), new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), arg1_ungroup.get_argument2()//.ensure_group() ) //.ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.QUANT_SEP) && prep.subexpr.get_argument1().ungroup() .op_spec_equals(Symbol.Specifier.EXISTS) && arg2_ungroup.op_spec_equals(logical_negation_sym_spec) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? prep.subexpr.get_argument1().ungroup() .get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + "[(" + Symbol.PHI_LOWERCASE_UNICODE + ")']" : prep.subexpr.get_argument1().ungroup() .get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + '[' + not_ + Symbol.PHI_LOWERCASE_UNICODE + ']' , prep.expressionsmgmt.get_useprimefornot() ? '(' + forall + Symbol.NU_LOWERCASE_UNICODE + PHI_BRACKETED + ")' " : not_ + forall + Symbol.NU_LOWERCASE_UNICODE + PHI_BRACKETED , new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.QUANT_SEP ), new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.FORALL ), arg1_ungroup.get_argument1() ), //.ensure_group(), arg2_ungroup.get_argument1() //.ensure_group() ) ) //.ensure_group() ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.QUANT_SEP) && prep.subexpr.get_argument1().ungroup() .op_spec_equals(Symbol.Specifier.FORALL) && arg2_ungroup.op_spec_equals(logical_negation_sym_spec) ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? prep.subexpr.get_argument1().ungroup() .get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + "[(" + Symbol.PHI_LOWERCASE_UNICODE + ")']" : prep.subexpr.get_argument1().ungroup() .get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + '[' + not_ + Symbol.PHI_LOWERCASE_UNICODE + ']' , prep.expressionsmgmt.get_useprimefornot() ? '(' + exists + Symbol.NU_LOWERCASE_UNICODE + PHI_BRACKETED + ")' " : not_ + exists + Symbol.NU_LOWERCASE_UNICODE + PHI_BRACKETED , new Expression( prep.expressionsmgmt.new_Symbol( logical_negation_sym_spec ), new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.QUANT_SEP ), new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.EXISTS ), arg1_ungroup.get_argument1() ), //.ensure_group(), arg2_ungroup.get_argument1() //.ensure_group() ) ) //.ensure_group() ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.QUANT_SEP) && arg1_ungroup.get_argument1().ungroup().get_operator() .is_relation() ) activate_item( "(" + arg1_ungroup.get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + 'R' + Symbol.SIGMA_LOWERCASE_UNICODE // "set" or "start" + ")[" + Symbol.PHI_LOWERCASE_UNICODE + "]", "(" + arg1_ungroup.get_operator().get_text() + Symbol.NU_LOWERCASE_UNICODE + ")[(" + Symbol.NU_LOWERCASE_UNICODE + " R " + Symbol.SIGMA_LOWERCASE_UNICODE // "set" or "start" + ')' + ( arg1_ungroup.op_spec_equals( Symbol.Specifier.FORALL ) ? implies_ : and_ ) + Symbol.PHI_LOWERCASE_UNICODE + "]", new Expression( prep.expressionsmgmt.new_Symbol( Symbol.Specifier.QUANT_SEP ), new Expression( arg1_ungroup.get_operator(), arg1_ungroup.get_argument1().ungroup().get_argument1() ), //.ensure_group(), new Expression( prep.expressionsmgmt.new_Symbol( arg1_ungroup.op_spec_equals( Symbol.Specifier.FORALL ) ? Symbol.Specifier.IMPLIES : Symbol.Specifier.AND ), arg1_ungroup.get_argument1().ensure_group(), prep.subexpr.get_argument2() ) .ensure_group() ) //.ensure_group() ); if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.get_operator().specifier_negate() != null ) activate_item( prep.expressionsmgmt.get_useprimefornot() ? '(' + TAU_1_ + arg1_ungroup.get_operator().get_text() + TAU_2_ + ")' " : not_ + '(' + TAU_1_ + arg1_ungroup.get_operator().get_text() + TAU_2_ + ')' , '(' + TAU_1_ + prep.expressionsmgmt.get_spec_String( arg1_ungroup.get_operator().specifier_negate() ) + TAU_2_ + ')' , new Expression( prep.expressionsmgmt.new_Symbol( arg1_ungroup.get_operator().specifier_negate() ), arg1_ungroup.get_argument1(), arg1_ungroup.get_argument2() ) .ensure_group() ); if ( prep.subexpr.get_operator().specifier_unnegate() != null ) activate_item( TAU_1_ + prep.subexpr.get_operator().get_text() + TAU_2_ , prep.expressionsmgmt.get_useprimefornot() ? '(' + TAU_1_ + prep.expressionsmgmt.get_spec_String( prep.subexpr.get_operator().specifier_unnegate() ) + TAU_2_ + ")' " : not_ + '(' + TAU_1_ + prep.expressionsmgmt.get_spec_String( prep.subexpr.get_operator().specifier_unnegate() ) + TAU_2_ + ')' , new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), new Expression( prep.expressionsmgmt.new_Symbol( prep.subexpr.get_operator().specifier_unnegate() ), arg1, arg2 ) .ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.IS) // without any grouping && arg2.get_operator().get_text().equalsIgnoreCase("NOT") // without any grouping && arg2.get_argument1() .op_spec_equals(Symbol.Specifier.IDENTIFIER) ) // using the glyph pi for "predicate" activate_item( Symbol.TAU_LOWERCASE_UNICODE + " " + prep.subexpr.get_operator().get_text() + ' ' + arg2.get_operator().get_text() + ' ' + Symbol.PI_LOWERCASE_UNICODE, prep.expressionsmgmt.get_useprimefornot() ? "(" + Symbol.TAU_LOWERCASE_UNICODE + ' ' + prep.subexpr.get_operator().get_text() + ' ' + Symbol.PI_LOWERCASE_UNICODE + ")' " : arg2.get_operator().get_text() + ' ' + '(' + Symbol.TAU_LOWERCASE_UNICODE + ' ' + prep.subexpr.get_operator().get_text() + ' ' + Symbol.PI_LOWERCASE_UNICODE + ')' , new Expression( prep.expressionsmgmt.new_Symbol(logical_negation_sym_spec), new Expression( prep.subexpr.get_operator(), arg1, arg2.get_argument1() ) .ensure_group() ) ); if ( prep.subexpr.op_spec_equals(logical_negation_sym_spec) && arg1_ungroup.op_spec_equals(Symbol.Specifier.IS) // without any grouping around the ID/predicate && arg1_ungroup.get_argument2() .op_spec_equals(Symbol.Specifier.IDENTIFIER) ) // using the glyph pi for "predicate" activate_item( // not_.equals("'") prep.expressionsmgmt.get_useprimefornot() ? "(" + Symbol.TAU_LOWERCASE_UNICODE + ' ' + arg1_ungroup.get_operator().get_text() + ' ' + Symbol.PI_LOWERCASE_UNICODE + ")' " : not_ + '(' + Symbol.TAU_LOWERCASE_UNICODE + ' ' + arg1_ungroup.get_operator().get_text() + ' ' + Symbol.PI_LOWERCASE_UNICODE + ')' , Symbol.TAU_LOWERCASE_UNICODE + " " + arg1_ungroup.get_operator().get_text() + " not " + Symbol.PI_LOWERCASE_UNICODE, new Expression( arg1_ungroup.get_operator(), arg1_ungroup.get_argument1(), new Expression( new Symbol(Symbol.Specifier.NOT, "not"), arg1_ungroup.get_argument2() ) ) .ensure_group() ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.TIMES) ) { boolean arg1_pm = arg1_ungroup.op_spec_equals(Symbol.Specifier.PLUS) || arg1_ungroup.op_spec_equals(Symbol.Specifier.MINUS), arg2_pm = arg2_ungroup.op_spec_equals(Symbol.Specifier.PLUS) || arg2_ungroup.op_spec_equals(Symbol.Specifier.MINUS); if ( arg1_pm || arg2_pm ) { consideration = true; JButton button = new JButton( new AbstractAction("distributivity") { public void actionPerformed(ActionEvent ae) { prep.subexpr.this_structure_replace( prep.expressionsmgmt .try_distribute(prep.subexpr, 0) ); table_model .add( prep.selected_rows, prep.selected_column_id, (table_model .get_transformationgoal_relationship ( prep.selected_row ) == Symbol.Specifier.EQUIV || prep.expr.get_operator() .spec_yields_boolean() ? table_model.EQUIV_BY_ : table_model.EQUALS_BY_ ) + ae.getActionCommand(), "Applying " + ae.getActionCommand() + " to formula " + prep.ref_num_name + " yields:", prep.expr ); setVisible(false); // ?deallocate? } } ); button.setFont( new Font("Monospaced", Font.PLAIN, table.getFont().getSize()) ); content_pane.add(button); if ( arg1_pm && arg2_pm ) { button = new JButton( new AbstractAction("left distributivity") { public void actionPerformed(ActionEvent ae) { prep.subexpr.this_structure_replace( prep.expressionsmgmt .try_distribute(prep.subexpr, -1) ); table_model .add( prep.selected_rows, prep.selected_column_id, (table_model .get_transformationgoal_relationship( prep.selected_row ) == Symbol.Specifier.EQUIV || prep.expr.get_operator() .spec_yields_boolean() ? table_model.EQUIV_BY_ : table_model.EQUALS_BY_ ) + ae.getActionCommand(), "Applying " + ae.getActionCommand() + " to formula " + prep.ref_num_name + " yields:", prep.expr ); setVisible(false); // ?deallocate? } } ); button.setFont( new Font("Monospaced", Font.PLAIN, table.getFont().getSize()) ); content_pane.add(button); button = new JButton( new AbstractAction("right distributivity") { public void actionPerformed(ActionEvent ae) { prep.subexpr.this_structure_replace( prep.expressionsmgmt .try_distribute(prep.subexpr, 1) ); table_model .add( prep.selected_rows, prep.selected_column_id, (table_model .get_transformationgoal_relationship( prep.selected_row ) == Symbol.Specifier.EQUIV || prep.expr.get_operator() .spec_yields_boolean() ? table_model.EQUIV_BY_ : table_model.EQUALS_BY_ ) + ae.getActionCommand(), "Applying " + ae.getActionCommand() + " to formula " + prep.ref_num_name + " yields:", prep.expr ); setVisible(false); // ?deallocate? } } ); button.setFont( new Font("Monospaced", Font.PLAIN, table.getFont().getSize()) ); content_pane.add(button); } } } if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EXP) && arg2.op_spec_equals(Symbol.Specifier.INT) && (arg1_ungroup.op_spec_equals(Symbol.Specifier.PLUS) || arg1_ungroup.op_spec_equals(Symbol.Specifier.MINUS) ) ) { consideration = true; JButton button = new JButton( new AbstractAction("binomial expansion") { public void actionPerformed(ActionEvent ae) { prep.subexpr.this_structure_replace( prep.expressionsmgmt .try_binomial_expand(prep.subexpr) ); table_model .add( prep.selected_rows, prep.selected_column_id, (table_model .get_transformationgoal_relationship ( prep.selected_row ) == Symbol.Specifier.EQUIV || prep.expr.get_operator() .spec_yields_boolean() ? table_model.EQUIV_BY_ : table_model.EQUALS_BY_ ) + ae.getActionCommand(), "Applying " + ae.getActionCommand() + " to formula " + prep.ref_num_name + " yields:", prep.expr ); setVisible(false); // ?deallocate? } } ); button.setFont( new Font("Monospaced", Font.PLAIN, table.getFont().getSize()) ); content_pane.add(button); } if ( prep.subexpr.op_spec_equals(Symbol.Specifier.EXP) && arg2.op_spec_equals(Symbol.Specifier.INT) && arg2.get_val() >= 2 ) { consideration = true; JButton button = new JButton( new AbstractAction( "definition of \"" + Symbol.TAU_LOWERCASE_UNICODE + prep.subexpr.get_operator().get_text() + arg2.get_operator().get_text() + '"' ) { public void actionPerformed(ActionEvent ae) { Expression result = arg1; for ( int x = arg2.get_val() - 1; x > 0; x-- ) result = new Expression( new Symbol( Symbol.Specifier.TIMES, arg1.op_spec_equals( Symbol.Specifier .OPENING_DELIMITER ) ? "" : Character.toString( Symbol.MIDDLE_DOT_UNICODE ) ), arg1, result ); prep.subexpr.this_structure_replace( result.ensure_group() ); table_model .add( prep.selected_rows, prep.selected_column_id, (table_model .get_transformationgoal_relationship ( prep.selected_row ) == Symbol.Specifier.EQUIV || prep.expr.get_operator() .spec_yields_boolean() ? table_model.EQUIV_BY_ : table_model.EQUALS_BY_ ) + ae.getActionCommand(), "Applying " + ae.getActionCommand() + " to formula " + prep.ref_num_name + " yields:", prep.expr ); setVisible(false); // ?deallocate? } } ); button.setFont( new Font("Monospaced", Font.PLAIN, table.getFont().getSize()) ); content_pane.add(button); } // added for e.g. |(s*t)(s*t)| for Rosen page077_Example2: // |if m is square and n is square, then mn is square| if ( prep.subexpr.op_spec_equals(Symbol.Specifier.TIMES) && arg1_ungroup.equivalent_form(arg2_ungroup) ) activate_item( Symbol.TAU_LOWERCASE_UNICODE + prep.subexpr.get_operator().get_text() + Symbol.TAU_LOWERCASE_UNICODE, Character.toString(Symbol.TAU_LOWERCASE_UNICODE) + Symbol.SUPERSCRIPT_2_UNICODE, new Expression( new Symbol(Symbol.Specifier.EXP, ""), arg1, new Expression( new Symbol( Symbol.Specifier.INT, Symbol.SUPERSCRIPT_2_UNICODE ) ) ) ); // added for e.g. |(s*t)(s*t)(s*t)| --- see above re square if ( prep.subexpr.op_spec_equals(Symbol.Specifier.TIMES) && arg1_ungroup.op_spec_equals(Symbol.Specifier.TIMES) && arg1_ungroup.get_argument1().equivalent_form(arg2_ungroup) && arg1_ungroup.get_argument2().equivalent_form(arg2_ungroup) ) activate_item( Symbol.TAU_LOWERCASE_UNICODE + arg1_ungroup.get_operator().get_text() + Symbol.TAU_LOWERCASE_UNICODE + prep.subexpr.get_operator().get_text() + Symbol.TAU_LOWERCASE_UNICODE, Character.toString(Symbol.TAU_LOWERCASE_UNICODE) + Symbol.SUPERSCRIPT_3_UNICODE, new Expression( new Symbol(Symbol.Specifier.EXP, ""), arg2, new Expression( new Symbol( Symbol.Specifier.INT, Symbol.SUPERSCRIPT_3_UNICODE ) ) ) ); // added for e.g. |(s*t)(s*t)(s*t)| --- see above re square if ( prep.subexpr.op_spec_equals(Symbol.Specifier.TIMES) && arg2_ungroup.op_spec_equals(Symbol.Specifier.TIMES) && arg2_ungroup.get_argument1().equivalent_form(arg1_ungroup) && arg2_ungroup.get_argument2().equivalent_form(arg1_ungroup) ) activate_item( Symbol.TAU_LOWERCASE_UNICODE + prep.subexpr.get_operator().get_text() + Symbol.TAU_LOWERCASE_UNICODE + arg2_ungroup.get_operator().get_text() + Symbol.TAU_LOWERCASE_UNICODE, Character.toString(Symbol.TAU_LOWERCASE_UNICODE) + Symbol.SUPERSCRIPT_3_UNICODE, new Expression( new Symbol(Symbol.Specifier.EXP, ""), arg1, new Expression( new Symbol( Symbol.Specifier.INT, Symbol.SUPERSCRIPT_3_UNICODE ) ) ) ); // Extraction of common factor(s). // Intended to work even if material isn't simplified. // Breaks integer exponents as in k`2 + k ----> k(k + 1) // but doesn't break compound exponents as in x`[y+z] + x`[2y] // because it's not clear what to do in all cases // such as x`[y-z] + x`[2y] --?--> (x`y)(x`[-z] + x`y) // (maybe x`[y-z] + x`[2y] --?--> (x`[y-z])(1 + x`[y+z]) ?). // minimum of two polynomials in general, e.g. if ( prep.subexpr.op_spec_equals(Symbol.Specifier.PLUS) || prep.subexpr.op_spec_equals(Symbol.Specifier.MINUS) ) { ArrayList terms = prep.expressionsmgmt.get_terms(prep.subexpr); LinkedList common_factors_besides_int; int common_int_factor; do { common_factors_besides_int = terms.remove(terms.size() - 1).multiary_op_args( Symbol.Specifier.TIMES ); common_int_factor = 1; for ( ListIterator cfbi_lit = common_factors_besides_int.listIterator(); cfbi_lit.hasNext(); ) { Expression f = cfbi_lit.next(); if ( f.ungrp_op_spec_equals(Symbol.Specifier.INT) ) { common_int_factor *= f.ungroup().get_val(); cfbi_lit.remove(); } } } while ( common_int_factor == 0 && !terms.isEmpty() ); for ( Expression term : terms ) { LinkedList term_factors = term.ungroup().multiary_op_args(Symbol.Specifier.TIMES); int term_int_factor = 1; // will collect all the for ( ListIterator tf_lit = term_factors.listIterator(); tf_lit.hasNext(); ) { Expression term_factor = tf_lit.next(); if ( term_factor.ungrp_op_spec_equals(Symbol.Specifier.INT) ) { term_int_factor *= term_factor.ungroup().get_val(); tf_lit.remove(); } } if ( term_int_factor == 0 ) continue; common_int_factor = prep.expressionsmgmt.common_factor( term_int_factor, common_int_factor ); LinkedList common_factors_besides_int_so_far = common_factors_besides_int; common_factors_besides_int = new LinkedList(); for ( Expression cf_sofar : common_factors_besides_int_so_far ) { Expression base_cf_sofar, exponent_cf_sofar; if ( cf_sofar.ungrp_op_spec_equals(Symbol.Specifier.EXP) ) { base_cf_sofar = cf_sofar.ungroup().get_argument1(); exponent_cf_sofar = cf_sofar.ungroup().get_argument2().ungroup(); } else { base_cf_sofar = cf_sofar; exponent_cf_sofar = new Expression(1); } int int_exponent_cf_sofar = exponent_cf_sofar.op_spec_equals(Symbol.Specifier.INT) ? exponent_cf_sofar.get_val() : Integer.MAX_VALUE; int int_term_exponent_for_base = 0; for ( ListIterator tf_lit = term_factors.listIterator(); int_term_exponent_for_base < int_exponent_cf_sofar && tf_lit.hasNext(); ) { Expression term_factor = tf_lit.next(); Expression base_tf, exponent_tf; if ( term_factor .ungrp_op_spec_equals(Symbol.Specifier.EXP) ) { base_tf = term_factor.ungroup().get_argument1(); exponent_tf = term_factor.ungroup().get_argument2().ungroup(); } else { base_tf = term_factor; exponent_tf = new Expression(1); } if ( base_tf.equivalent_form(base_cf_sofar) ) { if ( exponent_tf .op_spec_equals(Symbol.Specifier.INT) ) int_term_exponent_for_base += exponent_tf.get_val(); else if ( exponent_tf .equivalent_form(exponent_cf_sofar) ) { int_exponent_cf_sofar = 0; // kludge break; } else // doing nothing for other, compound exponents continue; tf_lit.remove(); } } // excess int unused_int_term_exponent_for_base; if ( int_term_exponent_for_base >= int_exponent_cf_sofar ) { common_factors_besides_int.add(cf_sofar); unused_int_term_exponent_for_base = int_term_exponent_for_base - int_exponent_cf_sofar; } else if ( int_term_exponent_for_base > 0 && int_exponent_cf_sofar < Integer.MAX_VALUE ) { common_factors_besides_int.add( new Expression( new Symbol(Symbol.Specifier.EXP, ""), base_cf_sofar, new Expression( new Symbol( Symbol.Specifier.INT, Symbol.superscript( int_term_exponent_for_base ) ) ) ) ); unused_int_term_exponent_for_base = 0; } else unused_int_term_exponent_for_base = int_term_exponent_for_base; if ( unused_int_term_exponent_for_base > 0 ) term_factors.add( new Expression( new Symbol(Symbol.Specifier.EXP, ""), base_cf_sofar, new Expression( new Symbol( Symbol.Specifier.INT, Symbol.superscript( unused_int_term_exponent_for_base ) ) ) ) ); } if ( common_int_factor == 1 && common_factors_besides_int.isEmpty() ) break; } if ( common_int_factor != 1 || !common_factors_besides_int.isEmpty() ) { consideration = true; terms = prep.expressionsmgmt.get_terms(prep.subexpr); Expression new_terms_together = null; for ( Expression term : terms ) { LinkedList term_factors = term.ungroup() .multiary_op_args(Symbol.Specifier.TIMES); int remaining_common_int_factor = common_int_factor; for ( ListIterator tf_lit = term_factors.listIterator(); tf_lit.hasNext() && remaining_common_int_factor != 1; ) { Expression term_factor = tf_lit.next(); if ( term_factor .ungrp_op_spec_equals(Symbol.Specifier.INT) ) { int int_term_factor = term_factor.ungroup().get_val(); int cff = prep.expressionsmgmt.common_factor( int_term_factor, remaining_common_int_factor ); if ( cff != 1 ) { tf_lit.set( new Expression(int_term_factor / cff) ); remaining_common_int_factor /= cff; } } } for ( Expression cf : common_factors_besides_int ) { Expression base_cf, exponent_cf; if ( cf.ungrp_op_spec_equals(Symbol.Specifier.EXP) ) { base_cf = cf.ungroup().get_argument1(); exponent_cf = cf.ungroup().get_argument2().ungroup(); } else { base_cf = cf; exponent_cf = new Expression(1); } int remaining_int_exponent_cf = exponent_cf.op_spec_equals(Symbol.Specifier.INT) ? exponent_cf.get_val() : Integer.MAX_VALUE; for ( ListIterator tf_lit = term_factors.listIterator(); tf_lit.hasNext(); ) { Expression term_factor = tf_lit.next(); if ( term_factor.equivalent_form(cf) ) { tf_lit.remove(); break; } if ( !exponent_cf.op_spec_equals( Symbol.Specifier.INT ) ) continue; Expression base_tf, exponent_tf; if ( term_factor .ungrp_op_spec_equals(Symbol.Specifier.EXP) ) { base_tf = term_factor.ungroup().get_argument1(); exponent_tf = term_factor.ungroup().get_argument2().ungroup(); } else { base_tf = term_factor; exponent_tf = new Expression(1); } if ( !(base_tf.equivalent_form(base_cf) && exponent_tf.op_spec_equals( Symbol.Specifier.INT ) ) ) continue; int using_int_term_exponent_for_base = Math.min( exponent_tf.get_val(), remaining_int_exponent_cf ); tf_lit.set( new Expression( new Symbol(Symbol.Specifier.EXP, ""), base_tf, new Expression( new Symbol( Symbol.Specifier.INT, Symbol.superscript( exponent_tf.get_val() - using_int_term_exponent_for_base ) ) ) ) ); remaining_int_exponent_cf -= using_int_term_exponent_for_base; } } Expression new_term = term_factors.isEmpty() ? new Expression(1) : term_factors.removeLast(); for ( ListIterator tf_lit = term_factors.listIterator(term_factors.size()); tf_lit.hasPrevious(); ) new_term = new Expression( term.get_operator(), tf_lit.previous(), new_term ); if ( new_terms_together == null ) { new_terms_together = new_term; continue; } Symbol op; int coeff; if ( new_term.op_spec_equals(Symbol.Specifier.INT) && (coeff = new_term.get_val()) < 0 ) { new_term = new Expression(Math.abs(coeff)); // -coeff op = prep.expressionsmgmt.new_Symbol( Symbol.Specifier.MINUS ); } /* else if ( new_term.op_spec_equals(Symbol.Specifier.NEGATIVE) ) { t = t.get_argument1(); op = new_Symbol(Symbol.Specifier.MINUS); } */ else if ( new_term.op_spec_equals(Symbol.Specifier.TIMES) && new_term.get_argument1() .ungrp_op_spec_equals(Symbol.Specifier.INT) && (coeff = new_term.get_argument1().ungroup().get_val() ) < 0 ) { new_term.get_argument1().this_structure_replace(-coeff); op = new Symbol(Symbol.Specifier.MINUS, "-"); } else op = new Symbol(Symbol.Specifier.PLUS, "+"); new_terms_together = new Expression(op, new_terms_together, new_term); } if ( common_int_factor != 1 ) // kludge common_factors_besides_int.add( 0, new Expression(common_int_factor) ); // right-associating: Expression common_factors_together = common_factors_besides_int.removeLast(); while ( !common_factors_besides_int.isEmpty() ) common_factors_together = new Expression( new Symbol(Symbol.Specifier.TIMES, times), common_factors_besides_int.removeLast(), common_factors_together ); final Expression replacement = new Expression( prep.expressionsmgmt.new_Symbol(Symbol.Specifier.TIMES), common_factors_together, new_terms_together.ensure_group() ); prep.expressionsmgmt.simplify(replacement); JButton button = new JButton( new AbstractAction("extraction of common factor(s)") { public void actionPerformed(ActionEvent ae) { prep.subexpr.this_structure_replace( replacement ); table_model .add( prep.selected_rows, prep.selected_column_id, (table_model .get_transformationgoal_relationship ( prep.selected_row ) == Symbol.Specifier.EQUIV || prep.expr.get_operator() .spec_yields_boolean() ? table_model.EQUIV_BY_ : table_model.EQUALS_BY_ ) + ae.getActionCommand(), "Applying " + ae.getActionCommand() + " to formula " + prep.ref_num_name + " yields:", prep.expr ); setVisible(false); // ?deallocate? } } ); button.setFont( new Font( "Monospaced", Font.PLAIN, table.getFont().getSize() ) ); content_pane.add(button); } } if ( prep.subexpr.op_spec_equals(Symbol.Specifier.TIMES) && arg1_ungroup.op_spec_equals(Symbol.Specifier.TIMES) ) activate_item( '(' + TAU_1 + times + TAU_2 + ')' + times + TAU_3 , TAU_1 + times + '(' + TAU_2 + times + TAU_3 + ')' , new Expression( new Symbol(Symbol.Specifier.TIMES, times), arg1_ungroup.get_argument1(), new Expression( new Symbol(Symbol.Specifier.TIMES, times), arg1_ungroup.get_argument2(), arg2 ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.TIMES) && arg2_ungroup.op_spec_equals(Symbol.Specifier.TIMES) ) activate_item( TAU_1 + times + '(' + TAU_2 + times + TAU_3 + ')' , '(' + TAU_1 + times + TAU_2 + ')' + times + TAU_3 , new Expression( new Symbol(Symbol.Specifier.TIMES, times), new Expression( new Symbol(Symbol.Specifier.TIMES, times), arg1, arg2_ungroup.get_argument1() ).ensure_group(), arg2_ungroup.get_argument2() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.PLUS) && arg1_ungroup.op_spec_equals(Symbol.Specifier.PLUS) ) activate_item( '(' + TAU_1 + " + " + TAU_2 + ')' + " + " + TAU_3 , TAU_1 + " + " + '(' + TAU_2 + " + " + TAU_3 + ')' , new Expression( new Symbol(Symbol.Specifier.PLUS, "+"), arg1_ungroup.get_argument1(), new Expression( new Symbol(Symbol.Specifier.PLUS, "+"), arg1_ungroup.get_argument2(), arg2 ).ensure_group() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.PLUS) && arg2_ungroup.op_spec_equals(Symbol.Specifier.PLUS) ) activate_item( TAU_1 + " + " + '(' + TAU_2 + " + " + TAU_3 + ')' , '(' + TAU_1 + " + " + TAU_2 + ')' + " + " + TAU_3 , new Expression( new Symbol(Symbol.Specifier.PLUS, "+"), new Expression( new Symbol(Symbol.Specifier.PLUS, "+"), arg1, arg2_ungroup.get_argument1() ).ensure_group(), arg2_ungroup.get_argument2() ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.TIMES) && !arg1_ungroup.equivalent_form(arg2_ungroup) ) activate_item( TAU_1 + times + TAU_2 , TAU_2 + times + TAU_1 , new Expression( new Symbol(Symbol.Specifier.TIMES, times), arg2, arg1 ) ); if ( prep.subexpr.op_spec_equals(Symbol.Specifier.PLUS) ) activate_item( TAU_1 + " + " + TAU_2 , TAU_2 + " + " + TAU_1 , new Expression( prep.subexpr.get_operator(), arg2, arg1 ) ); JButton cancel_button = new JButton( new AbstractAction("Cancel") { public void actionPerformed(ActionEvent ae) { setVisible(false); // ?deallocate? } } ); cancel_button.setFont( cancel_button.getFont().deriveFont( table.getFont().getSize2D() ) ); content_pane.add(cancel_button); if ( !consideration && Ded_Action.get_actingvsjustcheckingapplicability() ) { Toolkit.getDefaultToolkit().beep(); JOptionPane.showMessageDialog( table.getTopLevelAncestor(), "Actually, no known canonical equivalences are applicable" + " to the (sub)expression that you selected; sorry." ); return; } //Display the window. pack(); /* // components weren't appearing, // so temporarily make this not modal // so below |setVisible(true)| returns // and then |paintComponents(getGraphics())|. setModal(false); setVisible(true); paintComponents(getGraphics()); setModal(true); */ //setVisible(true); } boolean get_consideration() { return consideration; } }