fixed unevaluated functions introduced in earlier refactoring
minor refactoring
simplified SymbolicConstraint#isMatching since the validity of each single substitution is enforce elsewhere