<s> import itertools <EOL> from ivy_logic import * <EOL> from ivy_logic_utils import substitute_clause , canonize_clause , used_variables_clauses <EOL> class NamedSpace ( AST ) : <EOL> def __init__ ( self , lit ) : <EOL> self . lit = lit <EOL> self . args = [ lit ] <EOL> def __repr__ ( self ) : <EOL> return repr ( self . lit ) <EOL> def enumerate ( self , memo , test ) : <EOL> atom = self . lit . atom <EOL> if self . lit . polarity == <NUM_LIT:1> and is_atom ( atom ) and atom . relname in memo : <EOL> params , value = memo [ atom . relname ] <EOL> assert len ( params ) == len ( atom . args ) <EOL> subst = dict ( zip ( params , atom . args ) ) <EOL> res = [ substitute_clause ( cl , subst ) for cl in value ] <EOL> return res <EOL> return [ [ self . lit ] ] if test ( [ self . lit ] ) else [ ] <EOL> def eval ( self , memo , relalg ) : <EOL> atom = self . lit . atom <EOL> if self . lit . polarity == <NUM_LIT:1> and atom . relname in memo : <EOL> params , value = memo [ atom . relname ] <EOL> if len ( params ) != len ( atom . args ) : <EOL> print "<STR_LIT>" . format ( self , params , value ) <EOL> assert len ( params ) == len ( atom . args ) <EOL> subst = dict ( zip ( params , atom . args ) ) <EOL> return [ ( substitute_clause ( cl , subst ) , relalg . subst ( r , subst ) ) for ( cl , r ) in value ] <EOL> v = relalg . prim ( self . lit ) <EOL> return [ ( [ self . lit ] , v ) ] if not relalg . empty ( v ) else [ ] <EOL> class SumSpace ( AST ) : <EOL> def __init__ ( self , spaces ) : <EOL> self . spaces = spaces <EOL> self . args = spaces <EOL> def clone ( self , args ) : <EOL> return SumSpace ( args ) <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT:(>' + '<STR_LIT>' . join ( [ repr ( s ) for s in self . spaces ] ) + '<STR_LIT:)>' <EOL> def enumerate ( self , memo , test ) : <EOL> return [ cl for s in self . spaces for cl in s . enumerate ( memo , test ) ] <EOL> def eval ( self , memo , relalg ) : <EOL> return [ cl for s in self . spaces for cl in s . eval ( memo , relalg ) ] <EOL> class ProductSpace ( AST ) : <EOL> def __init__ ( self , spaces ) : <EOL> self . spaces = spaces <EOL> self . args = spaces <EOL> def __repr__ ( self ) : <EOL> return '<STR_LIT:(>' + '<STR_LIT>' . join ( [ repr ( s ) for s in self . spaces ] ) + '<STR_LIT:)>' <EOL> def clone ( self , args ) : <EOL> return ProductSpace ( args ) <EOL> def enumerate ( self , memo , test ) : <EOL> if not self . spaces : <EOL> return [ [ ] ] <EOL> fs = self . spaces [ <NUM_LIT:0> ] . enumerate ( memo , test ) <EOL> for s in self . spaces [ <NUM_LIT:1> : ] : <EOL> fs2 = s . enumerate ( memo , test ) <EOL> prod = [ x + y for x , y in itertools . product ( fs , fs2 ) ] <EOL> fs = [ cl for cl in prod if test ( cl ) ] <EOL> return fs <EOL> def eval ( self , memo , relalg ) : <EOL> if not self . spaces : <EOL> return [ ( [ ] , relalg . top ( ) ) ] <EOL> fs = self . spaces [ <NUM_LIT:0> ] . eval ( memo , relalg ) <EOL> for s in self . spaces [ <NUM_LIT:1> : ] : <EOL> fs2 = s . eval ( memo , relalg ) <EOL> prod = [ ( x + y , relalg . prod ( xv , yv ) ) for ( x , xv ) , ( y , yv ) in itertools . product ( fs , fs2 ) ] <EOL> fs = [ ( cl , v ) for cl , v in prod if not relalg . empty ( v ) ] <EOL> if relalg . parent : <EOL> for cube , v in fs : <EOL> relalg . parent . inhabited_cube ( cube , witness = v ) <EOL> return fs <EOL> import ply . lex as lex <EOL> tokens = ( <EOL> '<STR_LIT>' , <EOL> '<STR_LIT>' , <EOL> '<STR_LIT>' , <EOL> '<STR_LIT>' , <EOL> '<STR_LIT>' , <EOL> '<STR_LIT>' , <EOL> '<STR_LIT>' , <EOL> '<STR_LIT>' , <EOL> '<STR_LIT>' <EOL> ) <EOL> t_TILDA = r'<STR_LIT>' <EOL> t_COMMA = r'<STR_LIT>' <EOL> t_PLUS = r'<STR_LIT>' <EOL> t_TIMES = r'<STR_LIT>' <EOL> t_LPAREN = r'<STR_LIT>' <EOL> t_RPAREN = r'<STR_LIT>' <EOL> t_LBR = r'<STR_LIT>' <EOL> t_RBR = r'<STR_LIT>' <EOL> t_ignore = '<STR_LIT>' <EOL> def t_SYMBOL ( t ) : <EOL> r'<STR_LIT>' <EOL> return t <EOL> def t_error ( t ) : <EOL> print "<STR_LIT>" % t . value [ <NUM_LIT:0> ] <EOL> t . lexer . skip ( <NUM_LIT:1> ) <EOL> lexer = lex . lex ( ) <EOL> import ply . yacc as yacc <EOL> def p_expr_lit ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = NamedSpace ( p [ <NUM_LIT:1> ] ) <EOL> def p_expr_prod ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = ProductSpace ( p [ <NUM_LIT:2> ] ) <EOL> def p_expr_sum ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = SumSpace ( p [ <NUM_LIT:2> ] ) <EOL> def p_term_symbol ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = Variable ( p [ <NUM_LIT:1> ] ) if str . isupper ( p [ <NUM_LIT:1> ] [ <NUM_LIT:0> ] ) else Constant ( p [ <NUM_LIT:1> ] ) <EOL> def p_terms ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = [ ] <EOL> def p_terms_term ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = [ p [ <NUM_LIT:1> ] ] <EOL> def p_terms_terms_term ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = p [ <NUM_LIT:1> ] <EOL> p [ <NUM_LIT:0> ] . append ( p [ <NUM_LIT:3> ] ) <EOL> def p_atom_terms ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = Atom ( p [ <NUM_LIT:1> ] , p [ <NUM_LIT:3> ] ) <EOL> def p_lit_atom ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = Literal ( <NUM_LIT:1> , p [ <NUM_LIT:1> ] ) <EOL> def p_lit_tilda_atom ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = Literal ( <NUM_LIT:0> , p [ <NUM_LIT:2> ] ) <EOL> def p_prod_expr_expr ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = [ p [ <NUM_LIT:1> ] , p [ <NUM_LIT:3> ] ] <EOL> def p_prod_prod_expr ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = p [ <NUM_LIT:1> ] <EOL> p [ <NUM_LIT:0> ] . append ( p [ <NUM_LIT:3> ] ) <EOL> def p_sum_expr_expr ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = [ p [ <NUM_LIT:1> ] , p [ <NUM_LIT:3> ] ] <EOL> def p_sum_sum_expr ( p ) : <EOL> '<STR_LIT>' <EOL> p [ <NUM_LIT:0> ] = p [ <NUM_LIT:1> ] <EOL> p [ <NUM_LIT:0> ] . append ( p [ <NUM_LIT:3> ] ) <EOL> def p_error ( p ) : <EOL> print "<STR_LIT>" <EOL> parser = yacc . yacc ( tabmodule = '<STR_LIT>' , errorlog = yacc . NullLogger ( ) ) <EOL> def to_concept_space ( s ) : <EOL> return parser . parse ( s ) <EOL> if __name__ == '<STR_LIT:__main__>' : <EOL> while True : <EOL> try : <EOL> s = raw_input ( '<STR_LIT>' ) <EOL> except EOFError : <EOL> break <EOL> if not s : continue <EOL> result = parser . parse ( s ) <EOL> print result <EOL> print "<STR_LIT>" % result . enumerate ( dict ( ) , lambda x : True ) <EOL> def clauses_to_concept ( name , clauses ) : <EOL> vars = used_variables_clauses ( clauses ) <EOL> ps = [ ProductSpace ( [ NamedSpace ( ~ lit ) for lit in clause ] ) for clause in clauses . triv_clauses ( ) ] <EOL> ss = ps [ <NUM_LIT:0> ] if len ( ps ) == <NUM_LIT:1> else SumSpace ( ps ) <EOL> return ( Atom ( Symbol ( name , RelationSort ( [ v . sort for v in vars ] ) ) , [ v for v in vars ] ) , ss ) </s>
