boolean-expr: resurrect from the unmaintained
							parent
							
								
									0133a674a4
								
							
						
					
					
						commit
						9a813fa7f5
					
				| 
						 | 
					@ -0,0 +1 @@
 | 
				
			||||||
 | 
					Slava Pestov
 | 
				
			||||||
| 
						 | 
					@ -0,0 +1,95 @@
 | 
				
			||||||
 | 
					! Copyright (C) 2008 Slava Pestov.
 | 
				
			||||||
 | 
					! See http://factorcode.org/license.txt for BSD license.
 | 
				
			||||||
 | 
					USING: accessors arrays classes kernel sequences sets
 | 
				
			||||||
 | 
					io prettyprint multi-methods ;
 | 
				
			||||||
 | 
					IN: boolean-expr
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					! Demonstrates the use of Unicode symbols in source files, and
 | 
				
			||||||
 | 
					! multi-method dispatch.
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					TUPLE: ⋀ x y ;
 | 
				
			||||||
 | 
					TUPLE: ⋁ x y ;
 | 
				
			||||||
 | 
					TUPLE: ¬ x ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					SINGLETONS: ⊤ ⊥ ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					SINGLETONS: P Q R S T U V W X Y Z ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					UNION: □ ⋀ ⋁ ¬ ⊤ ⊥ P Q R S T U V W X Y Z ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					GENERIC: ⋀ ( x y -- expr )
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: ⋀ { ⊤ □ } nip ;
 | 
				
			||||||
 | 
					METHOD: ⋀ { □ ⊤ } drop ;
 | 
				
			||||||
 | 
					METHOD: ⋀ { ⊥ □ } drop ;
 | 
				
			||||||
 | 
					METHOD: ⋀ { □ ⊥ } nip ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: ⋀ { ⋁ □ } [ [ x>> ] dip ⋀ ] [ [ y>> ] dip ⋀ ] 2bi ⋁ ;
 | 
				
			||||||
 | 
					METHOD: ⋀ { □ ⋁ } [ x>> ⋀ ] [ y>> ⋀ ] 2bi ⋁ ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: ⋀ { □ □ } \ ⋀ boa ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					GENERIC: ⋁ ( x y -- expr )
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: ⋁ { ⊤ □ } drop ;
 | 
				
			||||||
 | 
					METHOD: ⋁ { □ ⊤ } nip ;
 | 
				
			||||||
 | 
					METHOD: ⋁ { ⊥ □ } nip ;
 | 
				
			||||||
 | 
					METHOD: ⋁ { □ ⊥ } drop ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: ⋁ { □ □ } \ ⋁ boa ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					GENERIC: ¬ ( x -- expr )
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: ¬ { ⊤ } drop ⊥ ;
 | 
				
			||||||
 | 
					METHOD: ¬ { ⊥ } drop ⊤ ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: ¬ { ⋀ } [ x>> ¬ ] [ y>> ¬ ] bi ⋁ ;
 | 
				
			||||||
 | 
					METHOD: ¬ { ⋁ } [ x>> ¬ ] [ y>> ¬ ] bi ⋀ ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: ¬ { □ } \ ¬ boa ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					: → ( x y -- expr ) ¬ ⋀ ;
 | 
				
			||||||
 | 
					: ⊕ ( x y -- expr ) [ ⋁ ] [ ⋀ ¬ ] 2bi ⋀ ;
 | 
				
			||||||
 | 
					: ≣ ( x y -- expr ) [ ⋀ ] [ [ ¬ ] bi@ ⋀ ] 2bi ⋁ ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					GENERIC: (cnf) ( expr -- cnf )
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: (cnf) { ⋀ } [ x>> (cnf) ] [ y>> (cnf) ] bi append ;
 | 
				
			||||||
 | 
					METHOD: (cnf) { □ } 1array ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					GENERIC: cnf ( expr -- cnf )
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: cnf { ⋁ } [ x>> cnf ] [ y>> cnf ] bi append ;
 | 
				
			||||||
 | 
					METHOD: cnf { □ } (cnf) 1array ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					GENERIC: satisfiable? ( expr -- ? )
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: satisfiable? { ⊤ } drop t ;
 | 
				
			||||||
 | 
					METHOD: satisfiable? { ⊥ } drop f ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					: partition ( seq quot -- left right )
 | 
				
			||||||
 | 
					    [ [ not ] compose filter ] [ filter ] 2bi ; inline
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					: (satisfiable?) ( seq -- ? )
 | 
				
			||||||
 | 
					    [ \ ¬ instance? ] partition [ x>> ] map intersect empty? ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: satisfiable? { □ }
 | 
				
			||||||
 | 
					    cnf [ (satisfiable?) ] any? ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					GENERIC: (expr.) ( expr -- )
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: (expr.) { □ } pprint ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					: op. ( expr -- )
 | 
				
			||||||
 | 
					    "(" write
 | 
				
			||||||
 | 
					    [ x>> (expr.) ]
 | 
				
			||||||
 | 
					    [ bl class pprint bl ]
 | 
				
			||||||
 | 
					    [ y>> (expr.) ]
 | 
				
			||||||
 | 
					    tri
 | 
				
			||||||
 | 
					    ")" write ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					METHOD: (expr.) { ⋀ } op. ;
 | 
				
			||||||
 | 
					METHOD: (expr.) { ⋁ } op. ;
 | 
				
			||||||
 | 
					METHOD: (expr.) { ¬ } [ class pprint ] [ x>> (expr.) ] bi ;
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					: expr. ( expr -- ) (expr.) nl ;
 | 
				
			||||||
| 
						 | 
					@ -0,0 +1 @@
 | 
				
			||||||
 | 
					Simple boolean expression evaluator and simplifier
 | 
				
			||||||
		Loading…
	
		Reference in New Issue