question on search

[jkhourybbn]

Do the bindings support expressing conditions in search? (the "such that" part of the search command)

Example from the Manual

search in SIMPLE-CLOCK : clock(0) =>* clock(T)
           such that T < 0 or T >= 24 .

How do we specify the such that part in the above?

[jkhourybbn]

found the answer in the docs

# init and define start term 'clock(0)' and goal term 'clock(T)'... 

condion_pattern_lhs = module.parseTerm('T < 0 or T >= 24')
condition_pattern_rhs = module.parseTerm('true')
condition = [maude.EqualityCondition(condion_pattern_lhs, condition_pattern_rhs)]
	
start_term.search(<type>, goal_pattern, condition=condition)