<s> """<STR_LIT:U+0020>""" <EOL> from z3_utils import z3_implies <EOL> from logic import Or <EOL> def alpha ( concept_domain , state , cache = None ) : <EOL> """<STR_LIT>""" <EOL> if z3_implies ( state , Or ( ) ) : <EOL> return [ ( tag , True ) for tag , formula in concept_domain . get_facts ( ) ] <EOL> if cache is None : <EOL> cache = dict ( ) <EOL> facts = concept_domain . get_facts ( ) <EOL> result = [ ] <EOL> for tag , formula in facts : <EOL> if tag in cache : <EOL> value = cache [ tag ] <EOL> else : <EOL> value = z3_implies ( state , formula ) <EOL> result . append ( ( tag , value ) ) <EOL> return result <EOL> if __name__ == '<STR_LIT:__main__>' : <EOL> from collections import OrderedDict <EOL> from logic import ( Var , Const , Apply , Eq , Not , And , Or , Implies , <EOL> ForAll , Exists ) <EOL> from logic import UninterpretedSort , FunctionSort , first_order_sort , Boolean <EOL> from logic_util import free_variables , substitute , substitute_apply <EOL> from concept import Concept , ConceptCombiner , ConceptDomain <EOL> def test ( st ) : <EOL> print st , "<STR_LIT:=>" , eval ( st ) <EOL> S = UninterpretedSort ( '<STR_LIT:S>' ) <EOL> UnaryRelation = FunctionSort ( S , Boolean ) <EOL> BinaryRelation = FunctionSort ( S , S , Boolean ) <EOL> X , Y , Z = ( Var ( n , S ) for n in [ '<STR_LIT:X>' , '<STR_LIT:Y>' , '<STR_LIT>' ] ) <EOL> U = Var ( '<STR_LIT>' , UnaryRelation ) <EOL> U1 = Var ( '<STR_LIT>' , UnaryRelation ) <EOL> U2 = Var ( '<STR_LIT>' , UnaryRelation ) <EOL> B = Var ( '<STR_LIT:B>' , BinaryRelation ) <EOL> B1 = Var ( '<STR_LIT>' , BinaryRelation ) <EOL> B2 = Var ( '<STR_LIT>' , BinaryRelation ) <EOL> nstar = Const ( '<STR_LIT>' , BinaryRelation ) <EOL> x = Const ( '<STR_LIT:x>' , S ) <EOL> y = Const ( '<STR_LIT:y>' , S ) <EOL> c11 = Concept ( [ X ] , And ( Eq ( x , X ) , Eq ( y , X ) ) ) <EOL> c10 = Concept ( [ X ] , And ( Eq ( x , X ) , Not ( Eq ( y , X ) ) ) ) <EOL> c01 = Concept ( [ X ] , And ( Not ( Eq ( x , X ) ) , Eq ( y , X ) ) ) <EOL> c00 = Concept ( [ X ] , And ( Not ( Eq ( x , X ) ) , Not ( Eq ( y , X ) ) ) ) <EOL> cnstar = Concept ( [ X , Y ] , nstar ( X , Y ) ) <EOL> cnplus = Concept ( [ X , Y ] , And ( nstar ( X , Y ) , Not ( Eq ( X , Y ) ) ) ) <EOL> notexists = ConceptCombiner ( [ U ] , Not ( Exists ( [ X ] , U ( X ) ) ) ) <EOL> exists = ConceptCombiner ( [ U ] , Exists ( [ X ] , U ( X ) ) ) <EOL> singleton = ConceptCombiner ( [ U ] , ForAll ( [ X , Y ] , Implies ( And ( U ( X ) , U ( Y ) ) , Eq ( X , Y ) ) ) ) <EOL> all_to_all = ConceptCombiner ( <EOL> [ U1 , U2 , B ] , <EOL> ForAll ( [ X , Y ] , Implies ( And ( U1 ( X ) , U2 ( Y ) ) , B ( X , Y ) ) ) <EOL> ) <EOL> cd = ConceptDomain ( <EOL> OrderedDict ( [ <EOL> ( '<STR_LIT>' , c11 ) , <EOL> ( '<STR_LIT>' , c00 ) , <EOL> ( '<STR_LIT:x>' , c10 ) , <EOL> ( '<STR_LIT:y>' , c01 ) , <EOL> ( '<STR_LIT>' , cnstar ) , <EOL> ( '<STR_LIT>' , cnplus ) , <EOL> ] ) , <EOL> OrderedDict ( [ <EOL> ( '<STR_LIT>' , notexists ) , <EOL> ( '<STR_LIT>' , exists ) , <EOL> ( '<STR_LIT>' , singleton ) , <EOL> ( '<STR_LIT>' , all_to_all ) , <EOL> ] ) , <EOL> OrderedDict ( [ <EOL> ( '<STR_LIT>' , ( <EOL> [ '<STR_LIT>' , '<STR_LIT>' , '<STR_LIT>' ] , <EOL> [ '<STR_LIT>' , '<STR_LIT>' , '<STR_LIT:x>' , '<STR_LIT:y>' ] , <EOL> ) ) , <EOL> ( '<STR_LIT>' , ( <EOL> [ '<STR_LIT>' ] , <EOL> [ '<STR_LIT>' , '<STR_LIT>' , '<STR_LIT:x>' , '<STR_LIT:y>' ] , <EOL> [ '<STR_LIT>' , '<STR_LIT>' , '<STR_LIT:x>' , '<STR_LIT:y>' ] , <EOL> [ '<STR_LIT>' , '<STR_LIT>' ] , <EOL> ) ) <EOL> ] ) , <EOL> ) <EOL> facts = cd . get_facts ( ) <EOL> print "<STR_LIT>" <EOL> for tag , formula in facts : <EOL> print '<STR_LIT:U+0020>' , tag , formula , '<STR_LIT:U+002C>' <EOL> print "<STR_LIT>" <EOL> state = And ( <EOL> ForAll ( [ X , Y , Z ] , And ( <EOL> nstar ( X , X ) , <EOL> Implies ( And ( nstar ( X , Y ) , nstar ( Y , X ) ) , Eq ( X , Y ) ) , <EOL> Implies ( And ( nstar ( X , Y ) , nstar ( Y , Z ) ) , nstar ( X , Z ) ) , <EOL> Implies ( And ( nstar ( X , Y ) , nstar ( X , Z ) ) , Or ( nstar ( Y , Z ) , nstar ( Z , Y ) ) ) , <EOL> ) ) , <EOL> nstar ( x , y ) , <EOL> Not ( Eq ( x , y ) ) , <EOL> ForAll ( [ Z ] , Implies ( And ( nstar ( x , Z ) , Not ( Eq ( x , Z ) ) ) , nstar ( y , Z ) ) ) , <EOL> ) <EOL> abstract_value = alpha ( cd , state ) <EOL> print "<STR_LIT>" <EOL> for tag , value in abstract_value : <EOL> print '<STR_LIT:U+0020>' , tag , value , '<STR_LIT:U+002C>' <EOL> print "<STR_LIT>" </s>
